:: RATFUNC1 semantic presentation
begin
theorem df: :: RATFUNC1:1
for L being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr
for a being Element of L
for p, q being FinSequence of L st len p = len q & ( for i being Element of NAT st i in dom p holds
q /. i = a * (p /. i) ) holds
Sum q = a * (Sum p)
proof
let L be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for a being Element of L
for p, q being FinSequence of L st len p = len q & ( for i being Element of NAT st i in dom p holds
q /. i = a * (p /. i) ) holds
Sum q = a * (Sum p)
let a be Element of L; ::_thesis: for p, q being FinSequence of L st len p = len q & ( for i being Element of NAT st i in dom p holds
q /. i = a * (p /. i) ) holds
Sum q = a * (Sum p)
let p, q be FinSequence of L; ::_thesis: ( len p = len q & ( for i being Element of NAT st i in dom p holds
q /. i = a * (p /. i) ) implies Sum q = a * (Sum p) )
assume AS: ( len p = len q & ( for i being Element of NAT st i in dom p holds
q /. i = a * (p /. i) ) ) ; ::_thesis: Sum q = a * (Sum p)
consider fq being Function of NAT, the carrier of L such that
A6: Sum q = fq . (len q) and
A7: fq . 0 = 0. L and
A8: for j being Element of NAT
for v being Element of L st j < len q & v = q . (j + 1) holds
fq . (j + 1) = (fq . j) + v by RLVECT_1:def_12;
consider fp being Function of NAT, the carrier of L such that
A12: Sum p = fp . (len p) and
A13: fp . 0 = 0. L and
A14: for j being Element of NAT
for v being Element of L st j < len p & v = p . (j + 1) holds
fp . (j + 1) = (fp . j) + v by RLVECT_1:def_12;
defpred S1[ Element of NAT ] means fq . $1 = a * (fp . $1);
B1: S1[ 0 ] by A13, A7, VECTSP_1:6;
B2: for j being Element of NAT st 0 <= j & j < len p & S1[j] holds
S1[j + 1]
proof
let j be Element of NAT ; ::_thesis: ( 0 <= j & j < len p & S1[j] implies S1[j + 1] )
assume A18: ( 0 <= j & j < len p ) ; ::_thesis: ( not S1[j] or S1[j + 1] )
assume A19: S1[j] ; ::_thesis: S1[j + 1]
B3: 1 <= j + 1 by NAT_1:11;
B4: j + 1 <= len p by A18, NAT_1:13;
then j + 1 in Seg (len q) by B3, AS;
then A20: j + 1 in dom q by FINSEQ_1:def_3;
j + 1 in Seg (len p) by B3, B4;
then A20a: j + 1 in dom p by FINSEQ_1:def_3;
set vq = q /. (j + 1);
set vp = p /. (j + 1);
A21: q /. (j + 1) = q . (j + 1) by A20, PARTFUN1:def_6;
A21a: p /. (j + 1) = p . (j + 1) by A20a, PARTFUN1:def_6;
fq . (j + 1) = (a * (fp . j)) + (q /. (j + 1)) by A19, AS, A21, A18, A8
.= (a * (fp . j)) + (a * (p /. (j + 1))) by AS, A20a
.= a * ((fp . j) + (p /. (j + 1))) by VECTSP_1:def_2
.= a * (fp . (j + 1)) by A21a, A18, A14 ;
hence S1[j + 1] ; ::_thesis: verum
end;
for j being Element of NAT st 0 <= j & j <= len p holds
S1[j] from INT_1:sch_7(B1, B2);
hence Sum q = a * (Sum p) by AS, A12, A6; ::_thesis: verum
end;
theorem del1a: :: RATFUNC1:2
for L being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr
for f being FinSequence of L
for i, j being Element of NAT st i in dom f & j = i - 1 holds
Ins ((Del (f,i)),j,(f /. i)) = f
proof
let L be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for f being FinSequence of L
for i, j being Element of NAT st i in dom f & j = i - 1 holds
Ins ((Del (f,i)),j,(f /. i)) = f
let f be FinSequence of L; ::_thesis: for i, j being Element of NAT st i in dom f & j = i - 1 holds
Ins ((Del (f,i)),j,(f /. i)) = f
let i, j be Element of NAT ; ::_thesis: ( i in dom f & j = i - 1 implies Ins ((Del (f,i)),j,(f /. i)) = f )
set g = Ins ((Del (f,i)),j,(f /. i));
assume AS: ( i in dom f & j = i - 1 ) ; ::_thesis: Ins ((Del (f,i)),j,(f /. i)) = f
then consider n being Nat such that
H0: ( len f = n + 1 & len (Del (f,i)) = n ) by FINSEQ_3:104;
dom f = Seg (n + 1) by H0, FINSEQ_1:def_3;
then consider ii being Element of NAT such that
H1: ( i = ii & 1 <= ii & ii <= n + 1 ) by AS;
i - 1 < i - 0 by XREAL_1:15;
then j < n + 1 by AS, H1, XXREAL_0:2;
then H2: j <= n by NAT_1:13;
H3: len (Ins ((Del (f,i)),j,(f /. i))) = (len (Del (f,i))) + 1 by FINSEQ_5:69;
now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_(Ins_((Del_(f,i)),j,(f_/._i)))_holds_
(Ins_((Del_(f,i)),j,(f_/._i)))_._k_=_f_._k
let k be Nat; ::_thesis: ( 1 <= k & k <= len (Ins ((Del (f,i)),j,(f /. i))) implies (Ins ((Del (f,i)),j,(f /. i))) . k = f . k )
assume B: ( 1 <= k & k <= len (Ins ((Del (f,i)),j,(f /. i))) ) ; ::_thesis: (Ins ((Del (f,i)),j,(f /. i))) . k = f . k
then k in Seg (len (Ins ((Del (f,i)),j,(f /. i)))) by FINSEQ_1:1;
then D: k in dom (Ins ((Del (f,i)),j,(f /. i))) by FINSEQ_1:def_3;
now__::_thesis:_(Ins_((Del_(f,i)),j,(f_/._i)))_._k_=_f_._k
percases ( k < i or k = i or k > i ) by XXREAL_0:1;
supposeC: k < i ; ::_thesis: (Ins ((Del (f,i)),j,(f /. i))) . k = f . k
then k + 1 <= i by NAT_1:13;
then (k + 1) - 1 <= i - 1 by XREAL_1:9;
then ( 1 <= k & k <= len ((Del (f,i)) | j) ) by B, AS, H2, H0, FINSEQ_1:59;
then k in Seg (len ((Del (f,i)) | j)) by FINSEQ_1:1;
then D1: k in dom ((Del (f,i)) | j) by FINSEQ_1:def_3;
k < n + 1 by H1, C, XXREAL_0:2;
then k <= n by NAT_1:13;
then k in Seg (len (Del (f,i))) by H0, B, FINSEQ_1:1;
then D2: k in dom (Del (f,i)) by FINSEQ_1:def_3;
(Ins ((Del (f,i)),j,(f /. i))) /. k = (Del (f,i)) /. k by D1, FINSEQ_5:72
.= (Del (f,i)) . k by D2, PARTFUN1:def_6
.= f . k by C, FINSEQ_3:110 ;
hence (Ins ((Del (f,i)),j,(f /. i))) . k = f . k by D, PARTFUN1:def_6; ::_thesis: verum
end;
supposeC: k = i ; ::_thesis: (Ins ((Del (f,i)),j,(f /. i))) . k = f . k
then k = j + 1 by AS;
then E: (Ins ((Del (f,i)),j,(f /. i))) /. k = f /. i by H0, H2, FINSEQ_5:73;
thus (Ins ((Del (f,i)),j,(f /. i))) . k = (Ins ((Del (f,i)),j,(f /. i))) /. k by D, PARTFUN1:def_6
.= f . k by AS, C, E, PARTFUN1:def_6 ; ::_thesis: verum
end;
supposeC: k > i ; ::_thesis: f . k = (Ins ((Del (f,i)),j,(f /. i))) . k
then reconsider k1 = k - 1 as Element of NAT by H1, XXREAL_0:2, INT_1:5;
C2: k - 1 <= (n + 1) - 1 by B, H0, H3, XREAL_1:9;
1 < k1 + 1 by C, H1, XXREAL_0:2;
then 1 <= k1 by NAT_1:13;
then k1 in Seg n by C2;
then D1: k1 in dom (Del (f,i)) by H0, FINSEQ_1:def_3;
i < k1 + 1 by C;
then C1: j + 1 <= k - 1 by AS, NAT_1:13;
then (Ins ((Del (f,i)),j,(f /. i))) /. (k1 + 1) = (Del (f,i)) /. k1 by C2, H0, FINSEQ_5:74
.= (Del (f,i)) . k1 by D1, PARTFUN1:def_6
.= f . (k1 + 1) by C1, C2, H0, AS, FINSEQ_3:111 ;
hence f . k = (Ins ((Del (f,i)),j,(f /. i))) . k by D, PARTFUN1:def_6; ::_thesis: verum
end;
end;
end;
hence (Ins ((Del (f,i)),j,(f /. i))) . k = f . k ; ::_thesis: verum
end;
hence Ins ((Del (f,i)),j,(f /. i)) = f by H0, FINSEQ_5:69, FINSEQ_1:14; ::_thesis: verum
end;
theorem del1: :: RATFUNC1:3
for L being non empty right_complementable unital associative commutative right-distributive add-associative right_zeroed doubleLoopStr
for f being FinSequence of L
for i being Element of NAT st i in dom f holds
Product f = (f /. i) * (Product (Del (f,i)))
proof
let L be non empty right_complementable unital associative commutative right-distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for f being FinSequence of L
for i being Element of NAT st i in dom f holds
Product f = (f /. i) * (Product (Del (f,i)))
let f be FinSequence of L; ::_thesis: for i being Element of NAT st i in dom f holds
Product f = (f /. i) * (Product (Del (f,i)))
let i be Element of NAT ; ::_thesis: ( i in dom f implies Product f = (f /. i) * (Product (Del (f,i))) )
assume AS: i in dom f ; ::_thesis: Product f = (f /. i) * (Product (Del (f,i)))
then i in Seg (len f) by FINSEQ_1:def_3;
then consider ii being Element of NAT such that
H: ( ii = i & 1 <= ii & ii <= len f ) ;
reconsider j = i - 1 as Element of NAT by H, INT_1:5;
set g = Del (f,i);
thus Product f = Product (Ins ((Del (f,i)),j,(f /. i))) by AS, del1a
.= (Product (((Del (f,i)) | j) ^ <*(f /. i)*>)) * (Product ((Del (f,i)) /^ j)) by GROUP_4:5
.= ((Product ((Del (f,i)) | j)) * (f /. i)) * (Product ((Del (f,i)) /^ j)) by GROUP_4:6
.= (f /. i) * ((Product ((Del (f,i)) | j)) * (Product ((Del (f,i)) /^ j))) by GROUP_1:def_3
.= (f /. i) * (Product (((Del (f,i)) | j) ^ ((Del (f,i)) /^ j))) by GROUP_4:5
.= (f /. i) * (Product (Del (f,i))) by RFINSEQ:8 ; ::_thesis: verum
end;
registration
let L be non trivial right_complementable almost_left_invertible associative commutative left-distributive well-unital add-associative right_zeroed domRing-like doubleLoopStr ;
let x, y be non zero Element of L;
clusterx / y -> non zero ;
coherence
not x / y is zero
proof
( x <> 0. L & y <> 0. L ) ;
then (y ") * y = 1. L by VECTSP_1:def_10;
then y " <> 0. L by VECTSP_1:7;
hence x / y <> 0. L by VECTSP_2:def_1; :: according to STRUCT_0:def_12 ::_thesis: verum
end;
end;
registration
cluster non empty right_complementable right-distributive add-associative right_zeroed domRing-like -> non empty right_complementable almost_left_cancelable right-distributive add-associative right_zeroed for doubleLoopStr ;
coherence
for b1 being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr st b1 is domRing-like holds
b1 is almost_left_cancelable
proof
let L be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: ( L is domRing-like implies L is almost_left_cancelable )
assume B: L is domRing-like ; ::_thesis: L is almost_left_cancelable
let x be Element of L; :: according to ALGSTR_0:def_36 ::_thesis: ( x = 0. L or x is left_mult-cancelable )
assume A: x <> 0. L ; ::_thesis: x is left_mult-cancelable
let y, z be Element of L; :: according to ALGSTR_0:def_20 ::_thesis: ( not x * y = x * z or y = z )
assume x * y = x * z ; ::_thesis: y = z
then (x * y) - (x * z) = 0. L by RLVECT_1:15;
then x * (y - z) = 0. L by VECTSP_1:11;
then y - z = 0. L by A, B, VECTSP_2:def_1;
hence y = z by RLVECT_1:21; ::_thesis: verum
end;
cluster non empty right_complementable left-distributive add-associative right_zeroed domRing-like -> non empty right_complementable almost_right_cancelable left-distributive add-associative right_zeroed for doubleLoopStr ;
coherence
for b1 being non empty right_complementable left-distributive add-associative right_zeroed doubleLoopStr st b1 is domRing-like holds
b1 is almost_right_cancelable
proof
let L be non empty right_complementable left-distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: ( L is domRing-like implies L is almost_right_cancelable )
assume B: L is domRing-like ; ::_thesis: L is almost_right_cancelable
let x be Element of L; :: according to ALGSTR_0:def_37 ::_thesis: ( x = 0. L or x is right_mult-cancelable )
assume A: x <> 0. L ; ::_thesis: x is right_mult-cancelable
let y, z be Element of L; :: according to ALGSTR_0:def_21 ::_thesis: ( not y * x = z * x or y = z )
assume y * x = z * x ; ::_thesis: y = z
then (y * x) - (z * x) = 0. L by RLVECT_1:15;
then (y - z) * x = 0. L by VECTSP_1:13;
then y - z = 0. L by A, B, VECTSP_2:def_1;
hence y = z by RLVECT_1:21; ::_thesis: verum
end;
end;
registration
let x, y be Integer;
cluster max (x,y) -> integer ;
coherence
max (x,y) is integer by XXREAL_0:16;
cluster min (x,y) -> integer ;
coherence
min (x,y) is integer by XXREAL_0:15;
end;
theorem maxx: :: RATFUNC1:4
for x, y, z being Integer holds max ((x + y),(x + z)) = x + (max (y,z))
proof
let x, y, z be Integer; ::_thesis: max ((x + y),(x + z)) = x + (max (y,z))
percases ( y <= z or y > z ) ;
supposeA: y <= z ; ::_thesis: max ((x + y),(x + z)) = x + (max (y,z))
then x + y <= x + z by XREAL_1:6;
hence max ((x + y),(x + z)) = x + z by XXREAL_0:def_10
.= x + (max (y,z)) by A, XXREAL_0:def_10 ;
::_thesis: verum
end;
supposeA: y > z ; ::_thesis: max ((x + y),(x + z)) = x + (max (y,z))
then x + y > x + z by XREAL_1:8;
hence max ((x + y),(x + z)) = x + y by XXREAL_0:def_10
.= x + (max (y,z)) by A, XXREAL_0:def_10 ;
::_thesis: verum
end;
end;
end;
begin
definition
let L be non empty ZeroStr ;
let p be Polynomial of L;
attrp is zero means :defzer: :: RATFUNC1:def 1
p = 0_. L;
attrp is constant means :defconst: :: RATFUNC1:def 2
deg p <= 0 ;
end;
:: deftheorem defzer defines zero RATFUNC1:def_1_:_
for L being non empty ZeroStr
for p being Polynomial of L holds
( p is zero iff p = 0_. L );
:: deftheorem defconst defines constant RATFUNC1:def_2_:_
for L being non empty ZeroStr
for p being Polynomial of L holds
( p is constant iff deg p <= 0 );
registration
let L be non trivial ZeroStr ;
clusterV1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support non zero for Element of K19(K20(NAT, the carrier of L));
existence
not for b1 being Polynomial of L holds b1 is zero
proof
now__::_thesis:_ex_x_being_Element_of_the_carrier_of_L_st_x_<>_0._L
assume AS: for x being Element of the carrier of L holds not x <> 0. L ; ::_thesis: contradiction
now__::_thesis:_for_x,_y_being_Element_of_the_carrier_of_L_holds_y_=_x
let x, y be Element of the carrier of L; ::_thesis: y = x
thus y = 0. L by AS
.= x by AS ; ::_thesis: verum
end;
hence contradiction by STRUCT_0:def_10; ::_thesis: verum
end;
then consider x being Element of the carrier of L such that
C: x <> 0. L ;
set p = (0_. L) +* (0,x);
ex n being Nat st
for i being Nat st i >= n holds
((0_. L) +* (0,x)) . i = 0. L
proof
take 1 ; ::_thesis: for i being Nat st i >= 1 holds
((0_. L) +* (0,x)) . i = 0. L
now__::_thesis:_for_i_being_Nat_st_i_>=_1_holds_
((0_._L)_+*_(0,x))_._i_=_0._L
let i be Nat; ::_thesis: ( i >= 1 implies ((0_. L) +* (0,x)) . i = 0. L )
assume AS: i >= 1 ; ::_thesis: ((0_. L) +* (0,x)) . i = 0. L
B: i in NAT by ORDINAL1:def_12;
thus ((0_. L) +* (0,x)) . i = (0_. L) . i by AS, FUNCT_7:32
.= 0. L by B, FUNCOP_1:7 ; ::_thesis: verum
end;
hence for i being Nat st i >= 1 holds
((0_. L) +* (0,x)) . i = 0. L ; ::_thesis: verum
end;
then reconsider p = (0_. L) +* (0,x) as Polynomial of L by ALGSEQ_1:def_1;
take p ; ::_thesis: not p is zero
now__::_thesis:_for_i_being_Nat_st_i_<_1_holds_
p_._i_<>_0._L
let i be Nat; ::_thesis: ( i < 1 implies p . i <> 0. L )
assume i < 1 ; ::_thesis: p . i <> 0. L
then A: i = 0 by NAT_1:14;
i in NAT by ORDINAL1:def_12;
then 0 in dom (0_. L) by A, FUNCT_2:def_1;
hence p . i <> 0. L by C, A, FUNCT_7:31; ::_thesis: verum
end;
then len p <> 0 by ALGSEQ_1:9;
hence p <> 0_. L by POLYNOM4:3; :: according to RATFUNC1:def_1 ::_thesis: verum
end;
end;
registration
let L be non empty ZeroStr ;
cluster 0_. L -> zero constant ;
coherence
( 0_. L is zero & 0_. L is constant )
proof
deg (0_. L) = - 1 by HURWITZ:20;
hence ( 0_. L is zero & 0_. L is constant ) by defconst, defzer; ::_thesis: verum
end;
end;
registration
let L be non degenerated multLoopStr_0 ;
cluster 1_. L -> non zero ;
coherence
not 1_. L is zero
proof
A: (1_. L) . 0 = 1. L by POLYNOM3:30;
(0_. L) . 0 = 0. L by FUNCOP_1:7;
hence not 1_. L is zero by defzer, A; ::_thesis: verum
end;
end;
registration
let L be non empty multLoopStr_0 ;
cluster 1_. L -> constant ;
coherence
1_. L is constant
proof
set p = 1_. L;
now__::_thesis:_1_._L_is_constant
percases ( 0. L = 1. L or 0. L <> 1. L ) ;
supposeI: 0. L = 1. L ; ::_thesis: 1_. L is constant
A: dom (1_. L) = NAT by FUNCT_2:def_1
.= dom (0_. L) by FUNCT_2:def_1 ;
now__::_thesis:_for_x_being_set_st_x_in_dom_(1_._L)_holds_
(1_._L)_._x_=_(0_._L)_._x
let x be set ; ::_thesis: ( x in dom (1_. L) implies (1_. L) . x = (0_. L) . x )
assume x in dom (1_. L) ; ::_thesis: (1_. L) . x = (0_. L) . x
then reconsider xx = x as Element of NAT ;
B: (0_. L) . xx = 0. L by FUNCOP_1:7;
( xx = 0 or xx <> 0 ) ;
hence (1_. L) . x = (0_. L) . x by I, B, POLYNOM3:30; ::_thesis: verum
end;
hence 1_. L is constant by A, FUNCT_1:2; ::_thesis: verum
end;
supposeI: 0. L <> 1. L ; ::_thesis: 1_. L is constant
now__::_thesis:_for_i_being_Nat_st_i_>=_1_holds_
(1_._L)_._i_=_0._L
let i be Nat; ::_thesis: ( i >= 1 implies (1_. L) . i = 0. L )
assume AS: i >= 1 ; ::_thesis: (1_. L) . i = 0. L
B: i in NAT by ORDINAL1:def_12;
thus (1_. L) . i = (0_. L) . i by AS, FUNCT_7:32
.= 0. L by B, FUNCOP_1:7 ; ::_thesis: verum
end;
then D: 1 is_at_least_length_of 1_. L by ALGSEQ_1:def_2;
now__::_thesis:_for_m_being_Nat_st_m_is_at_least_length_of_1_._L_holds_
1_<=_m
let m be Nat; ::_thesis: ( m is_at_least_length_of 1_. L implies 1 <= m )
assume AS: m is_at_least_length_of 1_. L ; ::_thesis: 1 <= m
now__::_thesis:_not_m_<_1
assume m < 1 ; ::_thesis: contradiction
then m < 1 + 0 ;
then m <= 0 by NAT_1:13;
then E: (1_. L) . 0 = 0. L by AS, ALGSEQ_1:def_2;
dom (0_. L) = NAT by FUNCOP_1:13;
hence contradiction by I, E, FUNCT_7:31; ::_thesis: verum
end;
hence 1 <= m ; ::_thesis: verum
end;
then len (1_. L) = 1 by D, ALGSEQ_1:def_3;
then deg (1_. L) = 0 ;
hence 1_. L is constant by defconst; ::_thesis: verum
end;
end;
end;
hence 1_. L is constant ; ::_thesis: verum
end;
end;
registration
let L be non empty ZeroStr ;
cluster Function-like V18( NAT , the carrier of L) finite-Support zero -> constant for Element of K19(K20(NAT, the carrier of L));
coherence
for b1 being Polynomial of L st b1 is zero holds
b1 is constant
proof
let p be Polynomial of L; ::_thesis: ( p is zero implies p is constant )
assume p is zero ; ::_thesis: p is constant
then p = 0_. L by defzer;
hence p is constant ; ::_thesis: verum
end;
end;
registration
let L be non empty ZeroStr ;
cluster Function-like V18( NAT , the carrier of L) finite-Support non constant -> non zero for Element of K19(K20(NAT, the carrier of L));
coherence
for b1 being Polynomial of L st not b1 is constant holds
not b1 is zero ;
end;
registration
let L be non trivial ZeroStr ;
clusterV1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support non constant for Element of K19(K20(NAT, the carrier of L));
existence
not for b1 being Polynomial of L holds b1 is constant
proof
now__::_thesis:_ex_x_being_Element_of_the_carrier_of_L_st_x_<>_0._L
assume AS: for x being Element of the carrier of L holds not x <> 0. L ; ::_thesis: contradiction
now__::_thesis:_for_x,_y_being_Element_of_the_carrier_of_L_holds_y_=_x
let x, y be Element of the carrier of L; ::_thesis: y = x
thus y = 0. L by AS
.= x by AS ; ::_thesis: verum
end;
hence contradiction by STRUCT_0:def_10; ::_thesis: verum
end;
then consider x being Element of the carrier of L such that
C: x <> 0. L ;
set p = ((0_. L) +* (0,x)) +* (1,x);
ex n being Nat st
for i being Nat st i >= n holds
(((0_. L) +* (0,x)) +* (1,x)) . i = 0. L
proof
take 2 ; ::_thesis: for i being Nat st i >= 2 holds
(((0_. L) +* (0,x)) +* (1,x)) . i = 0. L
now__::_thesis:_for_i_being_Nat_st_i_>=_2_holds_
(((0_._L)_+*_(0,x))_+*_(1,x))_._i_=_0._L
let i be Nat; ::_thesis: ( i >= 2 implies (((0_. L) +* (0,x)) +* (1,x)) . i = 0. L )
assume AS: i >= 2 ; ::_thesis: (((0_. L) +* (0,x)) +* (1,x)) . i = 0. L
then C: 1 <> i ;
B: i in NAT by ORDINAL1:def_12;
thus (((0_. L) +* (0,x)) +* (1,x)) . i = ((0_. L) +* (0,x)) . i by C, FUNCT_7:32
.= (0_. L) . i by AS, FUNCT_7:32
.= 0. L by B, FUNCOP_1:7 ; ::_thesis: verum
end;
hence for i being Nat st i >= 2 holds
(((0_. L) +* (0,x)) +* (1,x)) . i = 0. L ; ::_thesis: verum
end;
then reconsider p = ((0_. L) +* (0,x)) +* (1,x) as Polynomial of L by ALGSEQ_1:def_1;
take p ; ::_thesis: not p is constant
now__::_thesis:_for_i_being_Nat_st_i_>=_2_holds_
p_._i_=_0._L
let i be Nat; ::_thesis: ( i >= 2 implies p . i = 0. L )
assume AS: i >= 2 ; ::_thesis: p . i = 0. L
then C: 1 <> i ;
B: i in NAT by ORDINAL1:def_12;
thus p . i = ((0_. L) +* (0,x)) . i by C, FUNCT_7:32
.= (0_. L) . i by AS, FUNCT_7:32
.= 0. L by B, FUNCOP_1:7 ; ::_thesis: verum
end;
then D: 2 is_at_least_length_of p by ALGSEQ_1:def_2;
now__::_thesis:_for_m_being_Nat_st_m_is_at_least_length_of_p_holds_
2_<=_m
let m be Nat; ::_thesis: ( m is_at_least_length_of p implies 2 <= m )
assume AS: m is_at_least_length_of p ; ::_thesis: 2 <= m
now__::_thesis:_not_m_<_2
assume m < 2 ; ::_thesis: contradiction
then m < 1 + 1 ;
then m <= 1 by NAT_1:13;
then E: p . 1 = 0. L by AS, ALGSEQ_1:def_2;
dom (0_. L) = NAT by FUNCOP_1:13;
then dom ((0_. L) +* (0,x)) = NAT by FUNCT_7:30;
hence contradiction by C, E, FUNCT_7:31; ::_thesis: verum
end;
hence 2 <= m ; ::_thesis: verum
end;
then len p = 2 by D, ALGSEQ_1:def_3;
then deg p = 1 ;
hence not p is constant by defconst; ::_thesis: verum
end;
end;
registration
let L be non empty non degenerated well-unital doubleLoopStr ;
let z be Element of L;
let k be Element of NAT ;
cluster rpoly (k,z) -> non zero ;
coherence
not rpoly (k,z) is zero
proof
deg (rpoly (k,z)) = k by HURWITZ:27;
then rpoly (k,z) <> 0_. L by HURWITZ:20;
hence not rpoly (k,z) is zero by defzer; ::_thesis: verum
end;
end;
registration
let L be non degenerated right_complementable distributive add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring L -> non degenerated ;
coherence
not Polynom-Ring L is degenerated
proof
set S = Polynom-Ring L;
( 0. (Polynom-Ring L) = 0_. L & 1. (Polynom-Ring L) = 1_. L ) by POLYNOM3:def_10;
hence not Polynom-Ring L is degenerated by STRUCT_0:def_8; ::_thesis: verum
end;
end;
registration
let L be non trivial right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr ;
cluster Polynom-Ring L -> domRing-like ;
coherence
Polynom-Ring L is domRing-like
proof
set Q = Polynom-Ring L;
let x, y be Element of (Polynom-Ring L); :: according to VECTSP_2:def_1 ::_thesis: ( not x * y = 0. (Polynom-Ring L) or x = 0. (Polynom-Ring L) or y = 0. (Polynom-Ring L) )
assume aa: x * y = 0. (Polynom-Ring L) ; ::_thesis: ( x = 0. (Polynom-Ring L) or y = 0. (Polynom-Ring L) )
assume AS: ( x <> 0. (Polynom-Ring L) & y <> 0. (Polynom-Ring L) ) ; ::_thesis: contradiction
reconsider p = x as Polynomial of L by POLYNOM3:def_10;
reconsider q = y as Polynomial of L by POLYNOM3:def_10;
p <> 0_. L by AS, POLYNOM3:def_10;
then reconsider p = p as non zero Polynomial of L by defzer;
q <> 0_. L by AS, POLYNOM3:def_10;
then reconsider q = q as non zero Polynomial of L by defzer;
p <> 0_. L ;
then deg p <> - 1 by HURWITZ:20;
then Ap: len p <> 0 ;
(len p) + 1 > 0 + 1 by Ap, XREAL_1:8;
then Dp: len p >= 1 by NAT_1:13;
then (len p) - 1 >= 1 - 1 by XREAL_1:9;
then Cp: (len p) -' 1 = (len p) - 1 by XREAL_0:def_2;
then reconsider lp = (len p) - 1 as Nat ;
q <> 0_. L ;
then deg q <> - 1 by HURWITZ:20;
then Aq: len q <> 0 ;
(len q) + 1 > 0 + 1 by Aq, XREAL_1:8;
then Dq: len q >= 1 by NAT_1:13;
then Eq: (len q) - 1 >= 1 - 1 by XREAL_1:9;
then (len q) -' 1 = (len q) - 1 by XREAL_0:def_2;
then reconsider lq = (len q) - 1 as Nat ;
set m = ((len p) + (len q)) - 2;
(len p) + (len q) >= 1 + 1 by Dp, Dq, XREAL_1:7;
then ((len p) + (len q)) - 2 >= 2 - 2 by XREAL_1:9;
then reconsider m = ((len p) + (len q)) - 2 as Element of NAT by INT_1:3;
consider r being FinSequence of the carrier of L such that
X: ( len r = m + 1 & (p *' q) . m = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((m + 1) -' k)) ) ) by POLYNOM3:def_9;
((((len p) + (len q)) - 2) + 1) - (len p) = lq ;
then X1a: (m + 1) -' (len p) = lq by XREAL_0:def_2;
X6: (len p) + 0 <= (len p) + ((len q) - 1) by Eq, XREAL_1:6;
then len p in Seg (len r) by Dp, X;
then X1: len p in dom r by FINSEQ_1:def_3;
then X2: r . (len p) = (p . lp) * (q . lq) by X1a, Cp, X;
X4: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_r_&_k_<>_len_p_holds_
r_._k_=_0._L
let k be Element of NAT ; ::_thesis: ( k in dom r & k <> len p implies r . k = 0. L )
assume Y: ( k in dom r & k <> len p ) ; ::_thesis: r . k = 0. L
now__::_thesis:_r_._k_=_0._L
percases ( k > len p or k <= len p ) ;
suppose k > len p ; ::_thesis: r . k = 0. L
then k >= (len p) + 1 by NAT_1:13;
then H: k - 1 >= ((len p) + 1) - 1 by XREAL_1:9;
k -' 1 >= len p by H, XREAL_0:def_2;
then p . (k -' 1) = 0. L by ALGSEQ_1:8;
then (p . (k -' 1)) * (q . ((m + 1) -' k)) = 0. L by VECTSP_1:7;
hence r . k = 0. L by Y, X; ::_thesis: verum
end;
supposeU: k <= len p ; ::_thesis: r . k = 0. L
k < len p by Y, U, XXREAL_0:1;
then (m + 1) - k > (m + 1) - (len p) by XREAL_1:10;
then (m + 1) - k >= ((len q) - 1) + 1 by INT_1:7;
then (m + 1) -' k >= len q by XREAL_0:def_2;
then q . ((m + 1) -' k) = 0. L by ALGSEQ_1:8;
then (p . (k -' 1)) * (q . ((m + 1) -' k)) = 0. L by VECTSP_1:6;
hence r . k = 0. L by Y, X; ::_thesis: verum
end;
end;
end;
hence r . k = 0. L ; ::_thesis: verum
end;
X3: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_r_&_i_<>_len_p_holds_
r_/._i_=_0._L
let i be Element of NAT ; ::_thesis: ( i in dom r & i <> len p implies r /. i = 0. L )
assume Y: ( i in dom r & i <> len p ) ; ::_thesis: r /. i = 0. L
then i in Seg (len r) by FINSEQ_1:def_3;
then ( 1 <= i & i <= len r ) by FINSEQ_1:1;
hence r /. i = r . i by FINSEQ_4:15
.= 0. L by Y, X4 ;
::_thesis: verum
end;
X5: (p *' q) . m = r /. (len p) by X, X1, X3, POLYNOM2:3
.= (p . lp) * (q . lq) by X2, X6, Dp, X, FINSEQ_4:15 ;
len p = lp + 1 ;
then XX: p . lp <> 0. L by ALGSEQ_1:10;
len q = lq + 1 ;
then q . lq <> 0. L by ALGSEQ_1:10;
then X6: (p *' q) . m <> 0. L by XX, X5, VECTSP_2:def_1;
(0_. L) . m = 0. L by FUNCOP_1:7;
then p *' q <> 0. (Polynom-Ring L) by X6, POLYNOM3:def_10;
hence contradiction by aa, POLYNOM3:def_10; ::_thesis: verum
end;
end;
theorem :: RATFUNC1:5
for L being non empty right_complementable associative right-distributive add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of L
for a being Element of L holds (a * p) *' q = a * (p *' q)
proof
let L be non empty right_complementable associative right-distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q being Polynomial of L
for a being Element of L holds (a * p) *' q = a * (p *' q)
let p, q be Polynomial of L; ::_thesis: for a being Element of L holds (a * p) *' q = a * (p *' q)
let a be Element of L; ::_thesis: (a * p) *' q = a * (p *' q)
set f = (a * p) *' q;
set g = a * (p *' q);
A: dom ((a * p) *' q) = NAT by FUNCT_2:def_1
.= dom (a * (p *' q)) by FUNCT_2:def_1 ;
now__::_thesis:_for_i_being_set_st_i_in_dom_((a_*_p)_*'_q)_holds_
((a_*_p)_*'_q)_._i_=_(a_*_(p_*'_q))_._i
let i be set ; ::_thesis: ( i in dom ((a * p) *' q) implies ((a * p) *' q) . i = (a * (p *' q)) . i )
assume i in dom ((a * p) *' q) ; ::_thesis: ((a * p) *' q) . i = (a * (p *' q)) . i
then reconsider n = i as Element of NAT ;
consider fr being FinSequence of the carrier of L such that
A1: ( len fr = n + 1 & ((a * p) *' q) . i = Sum fr & ( for k being Element of NAT st k in dom fr holds
fr . k = ((a * p) . (k -' 1)) * (q . ((n + 1) -' k)) ) ) by POLYNOM3:def_9;
consider fa being FinSequence of the carrier of L such that
A2: ( len fa = n + 1 & (p *' q) . i = Sum fa & ( for k being Element of NAT st k in dom fa holds
fa . k = (p . (k -' 1)) * (q . ((n + 1) -' k)) ) ) by POLYNOM3:def_9;
Seg (len fa) = dom fr by A1, A2, FINSEQ_1:def_3;
then A4: dom fa = dom fr by FINSEQ_1:def_3;
A3: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_fa_holds_
fr_/._k_=_a_*_(fa_/._k)
let k be Element of NAT ; ::_thesis: ( k in dom fa implies fr /. k = a * (fa /. k) )
assume A3a: k in dom fa ; ::_thesis: fr /. k = a * (fa /. k)
then fa . k = fa /. k by PARTFUN1:def_6;
then reconsider x = fa . k as Element of L ;
thus fr /. k = fr . k by A3a, A4, PARTFUN1:def_6
.= ((a * p) . (k -' 1)) * (q . ((n + 1) -' k)) by A4, A3a, A1
.= (a * (p . (k -' 1))) * (q . ((n + 1) -' k)) by POLYNOM5:def_3
.= a * ((p . (k -' 1)) * (q . ((n + 1) -' k))) by GROUP_1:def_3
.= a * x by A3a, A2
.= a * (fa /. k) by A3a, PARTFUN1:def_6 ; ::_thesis: verum
end;
(a * (p *' q)) . n = a * (Sum fa) by A2, POLYNOM5:def_3
.= ((a * p) *' q) . n by A3, A2, A1, df ;
hence ((a * p) *' q) . i = (a * (p *' q)) . i ; ::_thesis: verum
end;
hence (a * p) *' q = a * (p *' q) by A, FUNCT_1:2; ::_thesis: verum
end;
theorem :: RATFUNC1:6
for L being non empty right_complementable associative commutative right-distributive add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of L
for a being Element of L holds p *' (a * q) = a * (p *' q)
proof
let L be non empty right_complementable associative commutative right-distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q being Polynomial of L
for a being Element of L holds p *' (a * q) = a * (p *' q)
let p, q be Polynomial of L; ::_thesis: for a being Element of L holds p *' (a * q) = a * (p *' q)
let a be Element of L; ::_thesis: p *' (a * q) = a * (p *' q)
set f = p *' (a * q);
set g = a * (p *' q);
A: dom (p *' (a * q)) = NAT by FUNCT_2:def_1
.= dom (a * (p *' q)) by FUNCT_2:def_1 ;
now__::_thesis:_for_i_being_set_st_i_in_dom_(p_*'_(a_*_q))_holds_
(p_*'_(a_*_q))_._i_=_(a_*_(p_*'_q))_._i
let i be set ; ::_thesis: ( i in dom (p *' (a * q)) implies (p *' (a * q)) . i = (a * (p *' q)) . i )
assume i in dom (p *' (a * q)) ; ::_thesis: (p *' (a * q)) . i = (a * (p *' q)) . i
then reconsider n = i as Element of NAT ;
consider fr being FinSequence of the carrier of L such that
A1: ( len fr = n + 1 & (p *' (a * q)) . i = Sum fr & ( for k being Element of NAT st k in dom fr holds
fr . k = (p . (k -' 1)) * ((a * q) . ((n + 1) -' k)) ) ) by POLYNOM3:def_9;
consider fa being FinSequence of the carrier of L such that
A2: ( len fa = n + 1 & (p *' q) . i = Sum fa & ( for k being Element of NAT st k in dom fa holds
fa . k = (p . (k -' 1)) * (q . ((n + 1) -' k)) ) ) by POLYNOM3:def_9;
Seg (len fa) = dom fr by A1, A2, FINSEQ_1:def_3;
then A4: dom fa = dom fr by FINSEQ_1:def_3;
A3: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_fa_holds_
fr_/._k_=_a_*_(fa_/._k)
let k be Element of NAT ; ::_thesis: ( k in dom fa implies fr /. k = a * (fa /. k) )
assume A3a: k in dom fa ; ::_thesis: fr /. k = a * (fa /. k)
then fa . k = fa /. k by PARTFUN1:def_6;
then reconsider x = fa . k as Element of L ;
thus fr /. k = fr . k by A3a, A4, PARTFUN1:def_6
.= (p . (k -' 1)) * ((a * q) . ((n + 1) -' k)) by A4, A3a, A1
.= (p . (k -' 1)) * (a * (q . ((n + 1) -' k))) by POLYNOM5:def_3
.= a * ((p . (k -' 1)) * (q . ((n + 1) -' k))) by GROUP_1:def_3
.= a * x by A3a, A2
.= a * (fa /. k) by A3a, PARTFUN1:def_6 ; ::_thesis: verum
end;
(a * (p *' q)) . n = a * (Sum fa) by A2, POLYNOM5:def_3
.= (p *' (a * q)) . n by A3, df, A2, A1 ;
hence (p *' (a * q)) . i = (a * (p *' q)) . i ; ::_thesis: verum
end;
hence p *' (a * q) = a * (p *' q) by A, FUNCT_1:2; ::_thesis: verum
end;
registration
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ;
let p be non zero Polynomial of L;
let a be non zero Element of L;
clustera * p -> non zero ;
coherence
not a * p is zero
proof
a <> 0. L ;
then len (a * p) = len p by POLYNOM5:25;
then a * p <> 0_. L by POLYNOM4:3, POLYNOM4:5;
hence not a * p is zero by defzer; ::_thesis: verum
end;
end;
registration
let L be non trivial right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr ;
let p1, p2 be non zero Polynomial of L;
clusterp1 *' p2 -> non zero ;
coherence
not p1 *' p2 is zero
proof
reconsider x1 = p1 as Element of (Polynom-Ring L) by POLYNOM3:def_10;
reconsider x2 = p2 as Element of (Polynom-Ring L) by POLYNOM3:def_10;
p1 <> 0_. L ;
then A: x1 <> 0. (Polynom-Ring L) by POLYNOM3:def_10;
p2 <> 0_. L ;
then x2 <> 0. (Polynom-Ring L) by POLYNOM3:def_10;
then x1 * x2 <> 0. (Polynom-Ring L) by A, VECTSP_2:def_1;
then p1 *' p2 <> 0. (Polynom-Ring L) by POLYNOM3:def_10;
then p1 *' p2 <> 0_. L by POLYNOM3:def_10;
hence not p1 *' p2 is zero by defzer; ::_thesis: verum
end;
end;
theorem thequiv1: :: RATFUNC1:7
for L being non trivial right_complementable distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr
for p1, p2 being Polynomial of L
for p3 being non zero Polynomial of L st p1 *' p3 = p2 *' p3 holds
p1 = p2
proof
let L be non trivial right_complementable distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for p1, p2 being Polynomial of L
for p3 being non zero Polynomial of L st p1 *' p3 = p2 *' p3 holds
p1 = p2
let p1, p2 be Polynomial of L; ::_thesis: for p3 being non zero Polynomial of L st p1 *' p3 = p2 *' p3 holds
p1 = p2
let p3 be non zero Polynomial of L; ::_thesis: ( p1 *' p3 = p2 *' p3 implies p1 = p2 )
assume AS: p1 *' p3 = p2 *' p3 ; ::_thesis: p1 = p2
reconsider x1 = p1 as Element of (Polynom-Ring L) by POLYNOM3:def_10;
reconsider x2 = p2 as Element of (Polynom-Ring L) by POLYNOM3:def_10;
reconsider x3 = p3 as Element of (Polynom-Ring L) by POLYNOM3:def_10;
p3 <> 0_. L ;
then A: x3 <> 0. (Polynom-Ring L) by POLYNOM3:def_10;
B: x1 * x3 = p2 *' p3 by AS, POLYNOM3:def_10
.= x2 * x3 by POLYNOM3:def_10 ;
x3 is right_mult-cancelable by A, ALGSTR_0:def_37;
hence p1 = p2 by B, ALGSTR_0:def_21; ::_thesis: verum
end;
registration
let L be non trivial ZeroStr ;
let p be non zero Polynomial of L;
cluster degree p -> natural ;
coherence
degree p is natural
proof
p <> 0_. L ;
then deg p <> - 1 by HURWITZ:20;
then len p <> 0 ;
then (deg p) + 1 > 0 ;
then deg p in NAT by INT_1:7, INT_1:3;
hence degree p is natural ; ::_thesis: verum
end;
end;
theorem degrat2: :: RATFUNC1:8
for L being non empty right_complementable unital right-distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of L st deg p = 0 holds
for x being Element of L holds eval (p,x) <> 0. L
proof
let L be non empty right_complementable unital right-distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being Polynomial of L st deg p = 0 holds
for x being Element of L holds eval (p,x) <> 0. L
let p be Polynomial of L; ::_thesis: ( deg p = 0 implies for x being Element of L holds eval (p,x) <> 0. L )
assume AS: deg p = 0 ; ::_thesis: for x being Element of L holds eval (p,x) <> 0. L
let x be Element of L; ::_thesis: eval (p,x) <> 0. L
assume eval (p,x) = 0. L ; ::_thesis: contradiction
then x is_a_root_of p by POLYNOM5:def_6;
then p is with_roots by POLYNOM5:def_7;
hence contradiction by AS, HURWITZ:24; ::_thesis: verum
end;
theorem div1: :: RATFUNC1:9
for L being non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p being Polynomial of L
for x being Element of L holds
( eval (p,x) = 0. L iff rpoly (1,x) divides p )
proof
let L be non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being Polynomial of L
for x being Element of L holds
( eval (p,x) = 0. L iff rpoly (1,x) divides p )
let p be Polynomial of L; ::_thesis: for x being Element of L holds
( eval (p,x) = 0. L iff rpoly (1,x) divides p )
let x be Element of L; ::_thesis: ( eval (p,x) = 0. L iff rpoly (1,x) divides p )
A: now__::_thesis:_(_rpoly_(1,x)_divides_p_implies_eval_(p,x)_=_0._L_)
assume rpoly (1,x) divides p ; ::_thesis: eval (p,x) = 0. L
then p mod (rpoly (1,x)) = 0_. L by HURWITZ:def_7;
then (p - ((p div (rpoly (1,x))) *' (rpoly (1,x)))) + ((p div (rpoly (1,x))) *' (rpoly (1,x))) = (p div (rpoly (1,x))) *' (rpoly (1,x)) by POLYNOM3:28;
then B: (p div (rpoly (1,x))) *' (rpoly (1,x)) = p + ((- ((p div (rpoly (1,x))) *' (rpoly (1,x)))) + ((p div (rpoly (1,x))) *' (rpoly (1,x)))) by POLYNOM3:26
.= p + (((p div (rpoly (1,x))) *' (rpoly (1,x))) - ((p div (rpoly (1,x))) *' (rpoly (1,x))))
.= p + (0_. L) by POLYNOM3:29
.= p by POLYNOM3:28 ;
C: eval ((rpoly (1,x)),x) = x - x by HURWITZ:29
.= 0. L by RLVECT_1:15 ;
thus eval (p,x) = (eval ((p div (rpoly (1,x))),x)) * (0. L) by C, B, POLYNOM4:24
.= 0. L by VECTSP_1:6 ; ::_thesis: verum
end;
( eval (p,x) = 0. L implies rpoly (1,x) divides p ) by HURWITZ:35, POLYNOM5:def_6;
hence ( eval (p,x) = 0. L iff rpoly (1,x) divides p ) by A; ::_thesis: verum
end;
theorem div3: :: RATFUNC1:10
for L being non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr
for p, q being Polynomial of L
for x being Element of L holds
( not rpoly (1,x) divides p *' q or rpoly (1,x) divides p or rpoly (1,x) divides q )
proof
let L be non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for p, q being Polynomial of L
for x being Element of L holds
( not rpoly (1,x) divides p *' q or rpoly (1,x) divides p or rpoly (1,x) divides q )
let p, q be Polynomial of L; ::_thesis: for x being Element of L holds
( not rpoly (1,x) divides p *' q or rpoly (1,x) divides p or rpoly (1,x) divides q )
let x be Element of L; ::_thesis: ( not rpoly (1,x) divides p *' q or rpoly (1,x) divides p or rpoly (1,x) divides q )
assume rpoly (1,x) divides p *' q ; ::_thesis: ( rpoly (1,x) divides p or rpoly (1,x) divides q )
then eval ((p *' q),x) = 0. L by div1;
then A: (eval (p,x)) * (eval (q,x)) = 0. L by POLYNOM4:24;
percases ( eval (p,x) = 0. L or eval (q,x) = 0. L ) by A, VECTSP_2:def_1;
suppose eval (p,x) = 0. L ; ::_thesis: ( rpoly (1,x) divides p or rpoly (1,x) divides q )
hence ( rpoly (1,x) divides p or rpoly (1,x) divides q ) by div1; ::_thesis: verum
end;
suppose eval (q,x) = 0. L ; ::_thesis: ( rpoly (1,x) divides p or rpoly (1,x) divides q )
hence ( rpoly (1,x) divides p or rpoly (1,x) divides q ) by div1; ::_thesis: verum
end;
end;
end;
theorem div4: :: RATFUNC1:11
for L being non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f being FinSequence of (Polynom-Ring L) st ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) holds
for p being Polynomial of L st p = Product f holds
p <> 0_. L
proof
let L be non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for f being FinSequence of (Polynom-Ring L) st ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) holds
for p being Polynomial of L st p = Product f holds
p <> 0_. L
let f be FinSequence of (Polynom-Ring L); ::_thesis: ( ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) implies for p being Polynomial of L st p = Product f holds
p <> 0_. L )
assume AS1: for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ; ::_thesis: for p being Polynomial of L st p = Product f holds
p <> 0_. L
let p be Polynomial of L; ::_thesis: ( p = Product f implies p <> 0_. L )
assume AS2: p = Product f ; ::_thesis: p <> 0_. L
defpred S1[ Nat] means for f being FinSequence of (Polynom-Ring L) st len f = $1 & ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) holds
for p being Polynomial of L st p = Product f holds
p <> 0_. L;
now__::_thesis:_for_f_being_FinSequence_of_(Polynom-Ring_L)_st_len_f_=_0_&_(_for_i_being_Nat_st_i_in_dom_f_holds_
ex_z_being_Element_of_L_st_f_._i_=_rpoly_(1,z)_)_holds_
for_p_being_Polynomial_of_L_st_p_=_Product_f_holds_
p_<>_0_._L
let f be FinSequence of (Polynom-Ring L); ::_thesis: ( len f = 0 & ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) implies for p being Polynomial of L st p = Product f holds
p <> 0_. L )
assume A1: ( len f = 0 & ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) ) ; ::_thesis: for p being Polynomial of L st p = Product f holds
p <> 0_. L
let p be Polynomial of L; ::_thesis: ( p = Product f implies p <> 0_. L )
assume A2: p = Product f ; ::_thesis: p <> 0_. L
f = <*> the carrier of (Polynom-Ring L) by A1;
then p = 1_ (Polynom-Ring L) by A2, GROUP_4:8
.= 1. (Polynom-Ring L) ;
then p <> 0. (Polynom-Ring L) ;
hence p <> 0_. L by POLYNOM3:def_10; ::_thesis: verum
end;
then IA: S1[ 0 ] ;
IS: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume IV: S1[n] ; ::_thesis: S1[n + 1]
now__::_thesis:_for_f_being_FinSequence_of_(Polynom-Ring_L)_st_len_f_=_n_+_1_&_(_for_i_being_Nat_st_i_in_dom_f_holds_
ex_z_being_Element_of_L_st_f_._i_=_rpoly_(1,z)_)_holds_
for_p_being_Polynomial_of_L_st_p_=_Product_f_holds_
p_<>_0_._L
let f be FinSequence of (Polynom-Ring L); ::_thesis: ( len f = n + 1 & ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) implies for p being Polynomial of L st p = Product f holds
p <> 0_. L )
assume A1: ( len f = n + 1 & ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) ) ; ::_thesis: for p being Polynomial of L st p = Product f holds
p <> 0_. L
let p be Polynomial of L; ::_thesis: ( p = Product f implies p <> 0_. L )
assume A2: p = Product f ; ::_thesis: p <> 0_. L
f <> {} by A1;
then consider g being FinSequence, u being set such that
A6: f = g ^ <*u*> by FINSEQ_1:46;
reconsider g = g as FinSequence of (Polynom-Ring L) by A6, FINSEQ_1:36;
A2c: dom f = Seg (n + 1) by A1, FINSEQ_1:def_3;
1 <= n + 1 by NAT_1:11;
then A2a: n + 1 in dom f by A2c;
A2c: n + 1 = (len g) + (len <*u*>) by A1, A6, FINSEQ_1:22
.= (len g) + 1 by FINSEQ_1:40 ;
then f . (n + 1) = u by A6, FINSEQ_1:42;
then consider z being Element of L such that
U: u = rpoly (1,z) by A1, A2a;
reconsider u = u as Element of (Polynom-Ring L) by U, POLYNOM3:def_10;
reconsider q = Product g as Polynomial of L by POLYNOM3:def_10;
A4: Product f = (Product g) * u by A6, GROUP_4:6;
A3: u <> 0. (Polynom-Ring L) by U, POLYNOM3:def_10;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_g_holds_
ex_z_being_Element_of_L_st_g_._i_=_rpoly_(1,z)
let i be Nat; ::_thesis: ( i in dom g implies ex z being Element of L st g . i = rpoly (1,z) )
assume G: i in dom g ; ::_thesis: ex z being Element of L st g . i = rpoly (1,z)
then H: g . i = f . i by A6, FINSEQ_1:def_7;
dom g c= dom f by A6, FINSEQ_1:26;
hence ex z being Element of L st g . i = rpoly (1,z) by G, H, A1; ::_thesis: verum
end;
then q <> 0_. L by IV, A2c;
then q <> 0. (Polynom-Ring L) by POLYNOM3:def_10;
then p <> 0. (Polynom-Ring L) by A2, A3, A4, VECTSP_2:def_1;
hence p <> 0_. L by POLYNOM3:def_10; ::_thesis: verum
end;
hence S1[n + 1] ; ::_thesis: verum
end;
I: for n being Nat holds S1[n] from NAT_1:sch_2(IA, IS);
len f is Nat ;
hence p <> 0_. L by AS1, AS2, I; ::_thesis: verum
end;
theorem div2: :: RATFUNC1:12
for L being non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr
for f being FinSequence of (Polynom-Ring L) st ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) holds
for p being Polynomial of L st p = Product f holds
for x being Element of L holds
( eval (p,x) = 0. L iff ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) )
proof
let L be Field; ::_thesis: for f being FinSequence of (Polynom-Ring L) st ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) holds
for p being Polynomial of L st p = Product f holds
for x being Element of L holds
( eval (p,x) = 0. L iff ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) )
let f be FinSequence of (Polynom-Ring L); ::_thesis: ( ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) implies for p being Polynomial of L st p = Product f holds
for x being Element of L holds
( eval (p,x) = 0. L iff ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) ) )
assume AS1: for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ; ::_thesis: for p being Polynomial of L st p = Product f holds
for x being Element of L holds
( eval (p,x) = 0. L iff ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) )
let p be Polynomial of L; ::_thesis: ( p = Product f implies for x being Element of L holds
( eval (p,x) = 0. L iff ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) ) )
assume AS2: p = Product f ; ::_thesis: for x being Element of L holds
( eval (p,x) = 0. L iff ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) )
let x be Element of L; ::_thesis: ( eval (p,x) = 0. L iff ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) )
A: now__::_thesis:_(_ex_i_being_Nat_st_
(_i_in_dom_f_&_f_._i_=_rpoly_(1,x)_)_implies_eval_(p,x)_=_0._L_)
assume ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) ; ::_thesis: eval (p,x) = 0. L
then consider i being Nat such that
A1: ( i in dom f & f . i = rpoly (1,x) ) ;
reconsider g = Del (f,i) as FinSequence of (Polynom-Ring L) by FINSEQ_3:105;
reconsider q = Product g as Polynomial of L by POLYNOM3:def_10;
A2: f /. i = rpoly (1,x) by A1, PARTFUN1:def_6;
Product f = (f /. i) * (Product g) by A1, del1;
then p = (rpoly (1,x)) *' q by AS2, A2, POLYNOM3:def_10;
then A3: eval (p,x) = (eval ((rpoly (1,x)),x)) * (eval (q,x)) by POLYNOM4:24;
eval ((rpoly (1,x)),x) = x - x by HURWITZ:29
.= 0. L by RLVECT_1:15 ;
hence eval (p,x) = 0. L by A3, VECTSP_1:7; ::_thesis: verum
end;
now__::_thesis:_(_eval_(p,x)_=_0._L_implies_ex_i_being_Nat_st_
(_i_in_dom_f_&_f_._i_=_rpoly_(1,x)_)_)
assume A0: eval (p,x) = 0. L ; ::_thesis: ex i being Nat st
( i in dom f & f . i = rpoly (1,x) )
defpred S1[ Nat] means for f being FinSequence of (Polynom-Ring L) st len f = $1 & ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) holds
for p being Polynomial of L st p = Product f holds
for x being Element of L st eval (p,x) = 0. L holds
ex i being Nat st
( i in dom f & f . i = rpoly (1,x) );
now__::_thesis:_for_f_being_FinSequence_of_(Polynom-Ring_L)_st_len_f_=_0_&_(_for_i_being_Nat_st_i_in_dom_f_holds_
ex_z_being_Element_of_L_st_f_._i_=_rpoly_(1,z)_)_holds_
for_p_being_Polynomial_of_L_st_p_=_Product_f_holds_
for_x_being_Element_of_L_st_eval_(p,x)_=_0._L_holds_
ex_i_being_Nat_st_
(_i_in_dom_f_&_f_._i_=_rpoly_(1,x)_)
let f be FinSequence of (Polynom-Ring L); ::_thesis: ( len f = 0 & ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) implies for p being Polynomial of L st p = Product f holds
for x being Element of L st eval (p,x) = 0. L holds
ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) )
assume A1: ( len f = 0 & ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) ) ; ::_thesis: for p being Polynomial of L st p = Product f holds
for x being Element of L st eval (p,x) = 0. L holds
ex i being Nat st
( i in dom f & f . i = rpoly (1,x) )
let p be Polynomial of L; ::_thesis: ( p = Product f implies for x being Element of L st eval (p,x) = 0. L holds
ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) )
assume A2: p = Product f ; ::_thesis: for x being Element of L st eval (p,x) = 0. L holds
ex i being Nat st
( i in dom f & f . i = rpoly (1,x) )
let x be Element of L; ::_thesis: ( eval (p,x) = 0. L implies ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) )
assume A3: eval (p,x) = 0. L ; ::_thesis: ex i being Nat st
( i in dom f & f . i = rpoly (1,x) )
f = <*> the carrier of (Polynom-Ring L) by A1;
then p = 1_ (Polynom-Ring L) by A2, GROUP_4:8
.= 1_. L by POLYNOM3:def_10 ;
hence ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) by A3, POLYNOM4:18; ::_thesis: verum
end;
then IA: S1[ 0 ] ;
IS: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume IV: S1[n] ; ::_thesis: S1[n + 1]
now__::_thesis:_for_f_being_FinSequence_of_(Polynom-Ring_L)_st_len_f_=_n_+_1_&_(_for_i_being_Nat_st_i_in_dom_f_holds_
ex_z_being_Element_of_L_st_f_._i_=_rpoly_(1,z)_)_holds_
for_p_being_Polynomial_of_L_st_p_=_Product_f_holds_
for_x_being_Element_of_L_st_eval_(p,x)_=_0._L_holds_
ex_i_being_Nat_st_
(_i_in_dom_f_&_f_._i_=_rpoly_(1,x)_)
let f be FinSequence of (Polynom-Ring L); ::_thesis: ( len f = n + 1 & ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) implies for p being Polynomial of L st p = Product f holds
for x being Element of L st eval (p,x) = 0. L holds
ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) )
assume A1: ( len f = n + 1 & ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) ) ; ::_thesis: for p being Polynomial of L st p = Product f holds
for x being Element of L st eval (p,x) = 0. L holds
ex i being Nat st
( i in dom f & f . i = rpoly (1,x) )
let p be Polynomial of L; ::_thesis: ( p = Product f implies for x being Element of L st eval (p,x) = 0. L holds
ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) )
assume A2: p = Product f ; ::_thesis: for x being Element of L st eval (p,x) = 0. L holds
ex i being Nat st
( i in dom f & f . i = rpoly (1,x) )
let x be Element of L; ::_thesis: ( eval (p,x) = 0. L implies ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) )
assume A3: eval (p,x) = 0. L ; ::_thesis: ex i being Nat st
( i in dom f & f . i = rpoly (1,x) )
f <> {} by A1;
then consider g being FinSequence, u being set such that
A6: f = g ^ <*u*> by FINSEQ_1:46;
reconsider g = g as FinSequence of (Polynom-Ring L) by A6, FINSEQ_1:36;
A2c: dom f = Seg (n + 1) by A1, FINSEQ_1:def_3;
1 <= n + 1 by NAT_1:11;
then A2a: n + 1 in dom f by A2c;
A2c: n + 1 = (len g) + (len <*u*>) by A1, A6, FINSEQ_1:22
.= (len g) + 1 by FINSEQ_1:40 ;
A2b: f . (n + 1) = u by A2c, A6, FINSEQ_1:42;
then consider z being Element of L such that
U: u = rpoly (1,z) by A1, A2a;
reconsider u = u as Element of (Polynom-Ring L) by U, POLYNOM3:def_10;
reconsider q = Product g as Polynomial of L by POLYNOM3:def_10;
Product f = (Product g) * u by A6, GROUP_4:6
.= q *' (rpoly (1,z)) by U, POLYNOM3:def_10 ;
then A4: eval (p,x) = (eval (q,x)) * (eval ((rpoly (1,z)),x)) by A2, POLYNOM4:24;
A10: now__::_thesis:_for_i_being_Nat_st_i_in_dom_g_holds_
ex_z_being_Element_of_L_st_g_._i_=_rpoly_(1,z)
let i be Nat; ::_thesis: ( i in dom g implies ex z being Element of L st g . i = rpoly (1,z) )
assume C1: i in dom g ; ::_thesis: ex z being Element of L st g . i = rpoly (1,z)
C2: dom g c= dom f by A6, FINSEQ_1:26;
g . i = f . i by C1, A6, FINSEQ_1:def_7;
hence ex z being Element of L st g . i = rpoly (1,z) by C1, C2, A1; ::_thesis: verum
end;
now__::_thesis:_ex_i_being_Nat_st_
(_i_in_dom_f_&_f_._i_=_rpoly_(1,x)_)
percases ( eval (q,x) = 0. L or eval ((rpoly (1,z)),x) = 0. L ) by A4, A3, VECTSP_2:def_1;
suppose eval (q,x) = 0. L ; ::_thesis: ex i being Nat st
( i in dom f & f . i = rpoly (1,x) )
then consider i being Nat such that
B1: ( i in dom g & g . i = rpoly (1,x) ) by A2c, A10, IV;
B2: dom g c= dom f by A6, FINSEQ_1:26;
f . i = rpoly (1,x) by B1, A6, FINSEQ_1:def_7;
hence ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) by B2, B1; ::_thesis: verum
end;
suppose eval ((rpoly (1,z)),x) = 0. L ; ::_thesis: ex i being Nat st
( i in dom f & f . i = rpoly (1,x) )
then x - z = 0. L by HURWITZ:29;
then x = z by RLVECT_1:21;
hence ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) by A2a, A2b, U; ::_thesis: verum
end;
end;
end;
hence ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) ; ::_thesis: verum
end;
hence S1[n + 1] ; ::_thesis: verum
end;
I: for n being Nat holds S1[n] from NAT_1:sch_2(IA, IS);
len f is Nat ;
hence ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) by A0, AS1, AS2, I; ::_thesis: verum
end;
hence ( eval (p,x) = 0. L iff ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) ) by A; ::_thesis: verum
end;
begin
definition
let L be non empty unital doubleLoopStr ;
let p1, p2 be Polynomial of L;
let x be Element of L;
predx is_a_common_root_of p1,p2 means :root1: :: RATFUNC1:def 3
( x is_a_root_of p1 & x is_a_root_of p2 );
end;
:: deftheorem root1 defines is_a_common_root_of RATFUNC1:def_3_:_
for L being non empty unital doubleLoopStr
for p1, p2 being Polynomial of L
for x being Element of L holds
( x is_a_common_root_of p1,p2 iff ( x is_a_root_of p1 & x is_a_root_of p2 ) );
definition
let L be non empty unital doubleLoopStr ;
let p1, p2 be Polynomial of L;
predp1,p2 have_a_common_root means :root2: :: RATFUNC1:def 4
ex x being Element of L st x is_a_common_root_of p1,p2;
end;
:: deftheorem root2 defines have_a_common_root RATFUNC1:def_4_:_
for L being non empty unital doubleLoopStr
for p1, p2 being Polynomial of L holds
( p1,p2 have_a_common_root iff ex x being Element of L st x is_a_common_root_of p1,p2 );
notation
let L be non empty unital doubleLoopStr ;
let p1, p2 be Polynomial of L;
synonym p1,p2 have_common_roots for p1,p2 have_a_common_root ;
antonym p1,p2 have_no_common_roots for p1,p2 have_a_common_root ;
end;
theorem root3: :: RATFUNC1:13
for L being non empty right_complementable unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p being Polynomial of L
for x being Element of L st x is_a_root_of p holds
x is_a_root_of - p
proof
let L be non empty right_complementable unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being Polynomial of L
for x being Element of L st x is_a_root_of p holds
x is_a_root_of - p
let p be Polynomial of L; ::_thesis: for x being Element of L st x is_a_root_of p holds
x is_a_root_of - p
let x be Element of L; ::_thesis: ( x is_a_root_of p implies x is_a_root_of - p )
assume AS: x is_a_root_of p ; ::_thesis: x is_a_root_of - p
eval ((- p),x) = - (eval (p,x)) by POLYNOM4:20
.= - (0. L) by AS, POLYNOM5:def_6
.= 0. L by RLVECT_1:12 ;
hence x is_a_root_of - p by POLYNOM5:def_6; ::_thesis: verum
end;
theorem root4: :: RATFUNC1:14
for L being non empty right_complementable unital left-distributive Abelian add-associative right_zeroed doubleLoopStr
for p1, p2 being Polynomial of L
for x being Element of L st x is_a_common_root_of p1,p2 holds
x is_a_root_of p1 + p2
proof
let L be non empty right_complementable unital left-distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for p1, p2 being Polynomial of L
for x being Element of L st x is_a_common_root_of p1,p2 holds
x is_a_root_of p1 + p2
let p1, p2 be Polynomial of L; ::_thesis: for x being Element of L st x is_a_common_root_of p1,p2 holds
x is_a_root_of p1 + p2
let x be Element of L; ::_thesis: ( x is_a_common_root_of p1,p2 implies x is_a_root_of p1 + p2 )
assume x is_a_common_root_of p1,p2 ; ::_thesis: x is_a_root_of p1 + p2
then ( x is_a_root_of p1 & x is_a_root_of p2 ) by root1;
then AS: ( eval (p1,x) = 0. L & eval (p2,x) = 0. L ) by POLYNOM5:def_6;
eval ((p1 + p2),x) = (0. L) + (0. L) by AS, POLYNOM4:19
.= 0. L by RLVECT_1:def_4 ;
hence x is_a_root_of p1 + p2 by POLYNOM5:def_6; ::_thesis: verum
end;
theorem :: RATFUNC1:15
for L being non empty right_complementable unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p1, p2 being Polynomial of L
for x being Element of L st x is_a_common_root_of p1,p2 holds
x is_a_root_of - (p1 + p2) by root3, root4;
theorem :: RATFUNC1:16
for L being non empty right_complementable unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of L
for x being Element of L st x is_a_common_root_of p,q holds
x is_a_root_of p + q
proof
let L be non empty right_complementable unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q being Polynomial of L
for x being Element of L st x is_a_common_root_of p,q holds
x is_a_root_of p + q
let p, q be Polynomial of L; ::_thesis: for x being Element of L st x is_a_common_root_of p,q holds
x is_a_root_of p + q
let x be Element of L; ::_thesis: ( x is_a_common_root_of p,q implies x is_a_root_of p + q )
assume x is_a_common_root_of p,q ; ::_thesis: x is_a_root_of p + q
then H: ( x is_a_root_of p & x is_a_root_of q ) by root1;
then H1: eval (p,x) = 0. L by POLYNOM5:def_6;
H2: eval (q,x) = 0. L by H, POLYNOM5:def_6;
eval ((p + q),x) = (0. L) + (0. L) by H1, H2, POLYNOM4:19
.= 0. L by RLVECT_1:def_4 ;
hence x is_a_root_of p + q by POLYNOM5:def_6; ::_thesis: verum
end;
theorem :: RATFUNC1:17
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p1, p2 being Polynomial of L st p1 divides p2 & p1 is with_roots holds
p1,p2 have_common_roots
proof
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for p1, p2 being Polynomial of L st p1 divides p2 & p1 is with_roots holds
p1,p2 have_common_roots
let p1, p2 be Polynomial of L; ::_thesis: ( p1 divides p2 & p1 is with_roots implies p1,p2 have_common_roots )
assume AS: ( p1 divides p2 & p1 is with_roots ) ; ::_thesis: p1,p2 have_common_roots
percases ( p1 = 0_. L or p1 <> 0_. L ) ;
supposeA: p1 = 0_. L ; ::_thesis: p1,p2 have_common_roots
p2 mod p1 = 0_. L by AS, HURWITZ:def_7;
then 0_. L = p2 - (0_. L) by A, POLYNOM3:34
.= p2 + (0_. L) by HURWITZ:9 ;
then B: p2 = 0_. L by POLYNOM3:28;
eval ((0_. L),(0. L)) = 0. L by POLYNOM4:17;
then 0. L is_a_root_of 0_. L by POLYNOM5:def_6;
then 0. L is_a_common_root_of p1,p2 by A, B, root1;
hence p1,p2 have_common_roots by root2; ::_thesis: verum
end;
suppose p1 <> 0_. L ; ::_thesis: p1,p2 have_common_roots
then consider s being Polynomial of L such that
A: s *' p1 = p2 by AS, HURWITZ:34;
consider x being Element of L such that
B: x is_a_root_of p1 by AS, POLYNOM5:def_7;
C: eval (p1,x) = 0. L by B, POLYNOM5:def_6;
eval (p2,x) = (eval (s,x)) * (eval (p1,x)) by A, POLYNOM4:24
.= 0. L by C, VECTSP_1:6 ;
then x is_a_root_of p2 by POLYNOM5:def_6;
then x is_a_common_root_of p1,p2 by B, root1;
hence p1,p2 have_common_roots by root2; ::_thesis: verum
end;
end;
end;
definition
let L be non empty unital doubleLoopStr ;
let p, q be Polynomial of L;
func Common_Roots (p,q) -> Subset of L equals :: RATFUNC1:def 5
{ x where x is Element of L : x is_a_common_root_of p,q } ;
coherence
{ x where x is Element of L : x is_a_common_root_of p,q } is Subset of L
proof
set M = { x where x is Element of L : x is_a_common_root_of p,q } ;
now__::_thesis:_for_u_being_set_st_u_in__{__x_where_x_is_Element_of_L_:_x_is_a_common_root_of_p,q__}__holds_
u_in_the_carrier_of_L
let u be set ; ::_thesis: ( u in { x where x is Element of L : x is_a_common_root_of p,q } implies u in the carrier of L )
assume u in { x where x is Element of L : x is_a_common_root_of p,q } ; ::_thesis: u in the carrier of L
then ex x being Element of L st
( u = x & x is_a_common_root_of p,q ) ;
hence u in the carrier of L ; ::_thesis: verum
end;
hence { x where x is Element of L : x is_a_common_root_of p,q } is Subset of L by TARSKI:def_3; ::_thesis: verum
end;
end;
:: deftheorem defines Common_Roots RATFUNC1:def_5_:_
for L being non empty unital doubleLoopStr
for p, q being Polynomial of L holds Common_Roots (p,q) = { x where x is Element of L : x is_a_common_root_of p,q } ;
begin
definition
let L be non empty ZeroStr ;
let p be Polynomial of L;
func Leading-Coefficient p -> Element of L equals :: RATFUNC1:def 6
p . ((len p) -' 1);
coherence
p . ((len p) -' 1) is Element of L ;
end;
:: deftheorem defines Leading-Coefficient RATFUNC1:def_6_:_
for L being non empty ZeroStr
for p being Polynomial of L holds Leading-Coefficient p = p . ((len p) -' 1);
notation
let L be non empty ZeroStr ;
let p be Polynomial of L;
synonym LC p for Leading-Coefficient p;
end;
registration
let L be non trivial doubleLoopStr ;
let p be non zero Polynomial of L;
cluster Leading-Coefficient p -> non zero ;
coherence
not LC p is zero
proof
p <> 0_. L ;
then len p <> 0 by POLYNOM4:5;
then 0 + 1 < (len p) + 1 by XREAL_1:8;
then len p >= 1 by NAT_1:13;
then ((len p) -' 1) + 1 = len p by XREAL_1:235;
then p . ((len p) -' 1) <> 0. L by ALGSEQ_1:10;
hence not LC p is zero by STRUCT_0:def_12; ::_thesis: verum
end;
end;
theorem lcp1: :: RATFUNC1:18
for L being non empty right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of L
for a being Element of L holds LC (a * p) = a * (LC p)
proof
let L be non empty right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being Polynomial of L
for a being Element of L holds LC (a * p) = a * (LC p)
let p be Polynomial of L; ::_thesis: for a being Element of L holds LC (a * p) = a * (LC p)
let a be Element of L; ::_thesis: LC (a * p) = a * (LC p)
percases ( a = 0. L or a <> 0. L ) ;
supposeA: a = 0. L ; ::_thesis: LC (a * p) = a * (LC p)
then B: a * (LC p) = 0. L by VECTSP_1:6;
a * p = 0_. L by A, POLYNOM5:26;
hence LC (a * p) = a * (LC p) by B, FUNCOP_1:7; ::_thesis: verum
end;
supposeA: a <> 0. L ; ::_thesis: LC (a * p) = a * (LC p)
thus LC (a * p) = a * (p . ((len (a * p)) -' 1)) by POLYNOM5:def_3
.= a * (LC p) by A, POLYNOM5:25 ; ::_thesis: verum
end;
end;
end;
definition
let L be non empty doubleLoopStr ;
let p be Polynomial of L;
attrp is normalized means :defnormp: :: RATFUNC1:def 7
LC p = 1. L;
end;
:: deftheorem defnormp defines normalized RATFUNC1:def_7_:_
for L being non empty doubleLoopStr
for p being Polynomial of L holds
( p is normalized iff LC p = 1. L );
registration
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ;
let p be non zero Polynomial of L;
cluster((1. L) / (LC p)) * p -> normalized ;
coherence
((1. L) / (LC p)) * p is normalized
proof
A: LC p <> 0. L ;
LC (((1. L) / (LC p)) * p) = ((1. L) / (LC p)) * (LC p) by lcp1
.= (1. L) * (((LC p) ") * (LC p)) by GROUP_1:def_3
.= (1. L) * (1. L) by A, VECTSP_1:def_10
.= 1. L by VECTSP_1:def_4 ;
hence ((1. L) / (LC p)) * p is normalized by defnormp; ::_thesis: verum
end;
end;
registration
let L be Field;
let p be non zero Polynomial of L;
cluster NormPolynomial p -> normalized ;
coherence
NormPolynomial p is normalized
proof
set q = NormPolynomial p;
A: p <> 0_. L ;
then (NormPolynomial p) . ((len p) -' 1) = 1. L by POLYNOM5:56, POLYNOM4:5;
then LC (NormPolynomial p) = 1. L by A, POLYNOM5:57, POLYNOM4:5;
hence NormPolynomial p is normalized by defnormp; ::_thesis: verum
end;
end;
begin
definition
let L be non trivial multLoopStr_0 ;
mode rational_function of L -> set means :defratf: :: RATFUNC1:def 8
ex p1 being Polynomial of L ex p2 being non zero Polynomial of L st it = [p1,p2];
existence
ex b1 being set ex p1 being Polynomial of L ex p2 being non zero Polynomial of L st b1 = [p1,p2]
proof
take [ the Polynomial of L, the non zero Polynomial of L] ; ::_thesis: ex p1 being Polynomial of L ex p2 being non zero Polynomial of L st [ the Polynomial of L, the non zero Polynomial of L] = [p1,p2]
thus ex p1 being Polynomial of L ex p2 being non zero Polynomial of L st [ the Polynomial of L, the non zero Polynomial of L] = [p1,p2] ; ::_thesis: verum
end;
end;
:: deftheorem defratf defines rational_function RATFUNC1:def_8_:_
for L being non trivial multLoopStr_0
for b2 being set holds
( b2 is rational_function of L iff ex p1 being Polynomial of L ex p2 being non zero Polynomial of L st b2 = [p1,p2] );
definition
let L be non trivial multLoopStr_0 ;
let p1 be Polynomial of L;
let p2 be non zero Polynomial of L;
:: original: [
redefine func[p1,p2] -> rational_function of L;
coherence
[p1,p2] is rational_function of L by defratf;
end;
definition
let L be non trivial multLoopStr_0 ;
let z be rational_function of L;
:: original: `1
redefine funcz `1 -> Polynomial of L;
coherence
z `1 is Polynomial of L
proof
consider p1 being Polynomial of L such that
H: ex p2 being non zero Polynomial of L st z = [p1,p2] by defratf;
consider p2 being non zero Polynomial of L such that
H1: z = [p1,p2] by H;
thus z `1 is Polynomial of L by H1, XTUPLE_0:def_2; ::_thesis: verum
end;
:: original: `2
redefine funcz `2 -> non zero Polynomial of L;
coherence
z `2 is non zero Polynomial of L
proof
consider p1 being Polynomial of L such that
H: ex p2 being non zero Polynomial of L st z = [p1,p2] by defratf;
consider p2 being non zero Polynomial of L such that
H1: z = [p1,p2] by H;
thus z `2 is non zero Polynomial of L by H1, XTUPLE_0:def_3; ::_thesis: verum
end;
end;
definition
let L be non trivial multLoopStr_0 ;
let z be rational_function of L;
attrz is zero means :defzerrat: :: RATFUNC1:def 9
z `1 = 0_. L;
end;
:: deftheorem defzerrat defines zero RATFUNC1:def_9_:_
for L being non trivial multLoopStr_0
for z being rational_function of L holds
( z is zero iff z `1 = 0_. L );
registration
let L be non trivial multLoopStr_0 ;
cluster non zero for rational_function of L;
existence
not for b1 being rational_function of L holds b1 is zero
proof
set p1 = the non zero Polynomial of L;
set p2 = the non zero Polynomial of L;
take [ the non zero Polynomial of L, the non zero Polynomial of L] ; ::_thesis: not [ the non zero Polynomial of L, the non zero Polynomial of L] is zero
H: the non zero Polynomial of L = [ the non zero Polynomial of L, the non zero Polynomial of L] `1 ;
the non zero Polynomial of L <> 0_. L ;
hence not [ the non zero Polynomial of L, the non zero Polynomial of L] is zero by H, defzerrat; ::_thesis: verum
end;
end;
theorem ttt: :: RATFUNC1:19
for L being non trivial multLoopStr_0
for z being rational_function of L holds z = [(z `1),(z `2)]
proof
let L be non trivial multLoopStr_0 ; ::_thesis: for z being rational_function of L holds z = [(z `1),(z `2)]
let z be rational_function of L; ::_thesis: z = [(z `1),(z `2)]
consider p1 being Polynomial of L such that
H1: ex p2 being non zero Polynomial of L st z = [p1,p2] by defratf;
consider p2 being non zero Polynomial of L such that
H2: z = [p1,p2] by H1;
( z `1 = p1 & z `2 = p2 ) by H2, XTUPLE_0:def_2, XTUPLE_0:def_3;
hence z = [(z `1),(z `2)] by H2; ::_thesis: verum
end;
definition
let L be non trivial right_complementable unital distributive add-associative right_zeroed doubleLoopStr ;
let z be rational_function of L;
attrz is irreducible means :defirred: :: RATFUNC1:def 10
z `1 ,z `2 have_no_common_roots ;
end;
:: deftheorem defirred defines irreducible RATFUNC1:def_10_:_
for L being non trivial right_complementable unital distributive add-associative right_zeroed doubleLoopStr
for z being rational_function of L holds
( z is irreducible iff z `1 ,z `2 have_no_common_roots );
notation
let L be non trivial right_complementable unital distributive add-associative right_zeroed doubleLoopStr ;
let z be rational_function of L;
antonym reducible z for irreducible ;
end;
definition
let L be non trivial right_complementable unital distributive add-associative right_zeroed doubleLoopStr ;
let z be rational_function of L;
attrz is normalized means :defnorm: :: RATFUNC1:def 11
( z is irreducible & z `2 is normalized );
end;
:: deftheorem defnorm defines normalized RATFUNC1:def_11_:_
for L being non trivial right_complementable unital distributive add-associative right_zeroed doubleLoopStr
for z being rational_function of L holds
( z is normalized iff ( z is irreducible & z `2 is normalized ) );
registration
let L be non trivial right_complementable unital distributive add-associative right_zeroed doubleLoopStr ;
cluster normalized -> irreducible for rational_function of L;
coherence
for b1 being rational_function of L st b1 is normalized holds
b1 is irreducible by defnorm;
end;
registration
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ;
let z be rational_function of L;
cluster Leading-Coefficient (z `2) -> non zero ;
coherence
not LC (z `2) is zero ;
end;
definition
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ;
let z be rational_function of L;
func NormRationalFunction z -> rational_function of L equals :: RATFUNC1:def 12
[(((1. L) / (LC (z `2))) * (z `1)),(((1. L) / (LC (z `2))) * (z `2))];
coherence
[(((1. L) / (LC (z `2))) * (z `1)),(((1. L) / (LC (z `2))) * (z `2))] is rational_function of L ;
end;
:: deftheorem defines NormRationalFunction RATFUNC1:def_12_:_
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr
for z being rational_function of L holds NormRationalFunction z = [(((1. L) / (LC (z `2))) * (z `1)),(((1. L) / (LC (z `2))) * (z `2))];
notation
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ;
let z be rational_function of L;
synonym NormRatF z for NormRationalFunction z;
end;
registration
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ;
let z be non zero rational_function of L;
cluster NormRationalFunction z -> non zero ;
coherence
not NormRationalFunction z is zero
proof
z `1 <> 0_. L by defzerrat;
then reconsider z1 = z `1 as non zero Polynomial of L by defzer;
not ((1. L) / (LC (z `2))) * z1 is zero ;
then (NormRatF z) `1 <> 0_. L by XTUPLE_0:def_2;
hence not NormRationalFunction z is zero by defzerrat; ::_thesis: verum
end;
end;
definition
let L be non degenerated multLoopStr_0 ;
func 0._ L -> rational_function of L equals :: RATFUNC1:def 13
[(0_. L),(1_. L)];
coherence
[(0_. L),(1_. L)] is rational_function of L ;
func 1._ L -> rational_function of L equals :: RATFUNC1:def 14
[(1_. L),(1_. L)];
coherence
[(1_. L),(1_. L)] is rational_function of L ;
end;
:: deftheorem defines 0._ RATFUNC1:def_13_:_
for L being non degenerated multLoopStr_0 holds 0._ L = [(0_. L),(1_. L)];
:: deftheorem defines 1._ RATFUNC1:def_14_:_
for L being non degenerated multLoopStr_0 holds 1._ L = [(1_. L),(1_. L)];
registration
let L be non degenerated right_complementable associative well-unital distributive add-associative right_zeroed doubleLoopStr ;
cluster 0._ L -> normalized ;
coherence
0._ L is normalized
proof
set z = [(0_. L),(1_. L)];
set p1 = [(0_. L),(1_. L)] `1 ;
set p2 = [(0_. L),(1_. L)] `2 ;
now__::_thesis:_not_[(0_._L),(1_._L)]_`1_,[(0_._L),(1_._L)]_`2_have_a_common_root
assume [(0_. L),(1_. L)] `1 ,[(0_. L),(1_. L)] `2 have_a_common_root ; ::_thesis: contradiction
then consider x being Element of L such that
B: x is_a_common_root_of [(0_. L),(1_. L)] `1 ,[(0_. L),(1_. L)] `2 by root2;
x is_a_root_of [(0_. L),(1_. L)] `2 by B, root1;
then eval (([(0_. L),(1_. L)] `2),x) = 0. L by POLYNOM5:def_6;
hence contradiction by POLYNOM4:18; ::_thesis: verum
end;
then B: [(0_. L),(1_. L)] is irreducible by defirred;
C: len (1_. L) = 1 by POLYNOM4:4;
(len (1_. L)) -' 1 = 1 - 1 by C, XREAL_0:def_2;
then LC (1_. L) = 1. L by POLYNOM3:30;
then [(0_. L),(1_. L)] `2 is normalized by defnormp;
hence 0._ L is normalized by B, defnorm; ::_thesis: verum
end;
end;
registration
let L be non degenerated multLoopStr_0 ;
cluster 1._ L -> non zero ;
coherence
not 1._ L is zero
proof
(1._ L) `1 <> 0_. L by XTUPLE_0:def_2;
hence not 1._ L is zero by defzerrat; ::_thesis: verum
end;
end;
registration
let L be non degenerated right_complementable associative well-unital distributive add-associative right_zeroed doubleLoopStr ;
cluster 1._ L -> irreducible ;
coherence
1._ L is irreducible
proof
set z = [(1_. L),(1_. L)];
set p1 = [(1_. L),(1_. L)] `1 ;
set p2 = [(1_. L),(1_. L)] `2 ;
now__::_thesis:_not_[(1_._L),(1_._L)]_`1_,[(1_._L),(1_._L)]_`2_have_a_common_root
assume [(1_. L),(1_. L)] `1 ,[(1_. L),(1_. L)] `2 have_a_common_root ; ::_thesis: contradiction
then consider x being Element of L such that
B: x is_a_common_root_of [(1_. L),(1_. L)] `1 ,[(1_. L),(1_. L)] `2 by root2;
x is_a_root_of [(1_. L),(1_. L)] `2 by B, root1;
then eval (([(1_. L),(1_. L)] `2),x) = 0. L by POLYNOM5:def_6;
hence contradiction by POLYNOM4:18; ::_thesis: verum
end;
hence 1._ L is irreducible by defirred; ::_thesis: verum
end;
end;
registration
let L be non degenerated right_complementable associative well-unital distributive add-associative right_zeroed doubleLoopStr ;
cluster non zero irreducible for rational_function of L;
existence
ex b1 being rational_function of L st
( b1 is irreducible & not b1 is zero )
proof
take 1._ L ; ::_thesis: ( 1._ L is irreducible & not 1._ L is zero )
thus ( 1._ L is irreducible & not 1._ L is zero ) ; ::_thesis: verum
end;
end;
registration
let L be non degenerated right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let x be Element of L;
cluster[(rpoly (1,x)),(rpoly (1,x))] -> non zero reducible for rational_function of L;
coherence
for b1 being rational_function of L st b1 = [(rpoly (1,x)),(rpoly (1,x))] holds
( not b1 is irreducible & not b1 is zero )
proof
set z = [(rpoly (1,x)),(rpoly (1,x))];
C: [(rpoly (1,x)),(rpoly (1,x))] `1 = rpoly (1,x) ;
x is_a_root_of rpoly (1,x) by HURWITZ:30;
then x is_a_root_of [(rpoly (1,x)),(rpoly (1,x))] `1 ;
then x is_a_common_root_of [(rpoly (1,x)),(rpoly (1,x))] `1 ,[(rpoly (1,x)),(rpoly (1,x))] `2 by root1;
then [(rpoly (1,x)),(rpoly (1,x))] `1 ,[(rpoly (1,x)),(rpoly (1,x))] `2 have_common_roots by root2;
then [(rpoly (1,x)),(rpoly (1,x))] is reducible by defirred;
hence for b1 being rational_function of L st b1 = [(rpoly (1,x)),(rpoly (1,x))] holds
( not b1 is irreducible & not b1 is zero ) by C, defzerrat; ::_thesis: verum
end;
end;
registration
let L be non degenerated right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
cluster non zero reducible for rational_function of L;
existence
ex b1 being rational_function of L st
( b1 is reducible & not b1 is zero )
proof
set x = the Element of L;
take z = [(rpoly (1, the Element of L)),(rpoly (1, the Element of L))]; ::_thesis: ( z is reducible & not z is zero )
thus ( z is reducible & not z is zero ) ; ::_thesis: verum
end;
end;
registration
let L be non degenerated right_complementable associative well-unital distributive add-associative right_zeroed doubleLoopStr ;
cluster normalized for rational_function of L;
existence
ex b1 being rational_function of L st b1 is normalized
proof
take 0._ L ; ::_thesis: 0._ L is normalized
thus 0._ L is normalized ; ::_thesis: verum
end;
end;
registration
let L be non degenerated multLoopStr_0 ;
cluster 0._ L -> zero ;
coherence
0._ L is zero
proof
(0._ L) `1 = 0_. L by XTUPLE_0:def_2;
hence 0._ L is zero by defzerrat; ::_thesis: verum
end;
end;
registration
let L be non degenerated right_complementable associative well-unital distributive add-associative right_zeroed doubleLoopStr ;
cluster 1._ L -> normalized ;
coherence
1._ L is normalized
proof
len (1_. L) = 1 by POLYNOM4:4;
then (len (1_. L)) -' 1 = 1 - 1 by XREAL_0:def_2;
then LC (1_. L) = 1. L by POLYNOM3:30;
then [(1_. L),(1_. L)] `2 is normalized by defnormp;
hence 1._ L is normalized by defnorm; ::_thesis: verum
end;
end;
definition
let L be non trivial right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr ;
let p, q be rational_function of L;
funcp + q -> rational_function of L equals :: RATFUNC1:def 15
[(((p `1) *' (q `2)) + ((p `2) *' (q `1))),((p `2) *' (q `2))];
coherence
[(((p `1) *' (q `2)) + ((p `2) *' (q `1))),((p `2) *' (q `2))] is rational_function of L ;
end;
:: deftheorem defines + RATFUNC1:def_15_:_
for L being non trivial right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr
for p, q being rational_function of L holds p + q = [(((p `1) *' (q `2)) + ((p `2) *' (q `1))),((p `2) *' (q `2))];
definition
let L be non trivial right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr ;
let p, q be rational_function of L;
funcp *' q -> rational_function of L equals :: RATFUNC1:def 16
[((p `1) *' (q `1)),((p `2) *' (q `2))];
coherence
[((p `1) *' (q `1)),((p `2) *' (q `2))] is rational_function of L ;
end;
:: deftheorem defines *' RATFUNC1:def_16_:_
for L being non trivial right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr
for p, q being rational_function of L holds p *' q = [((p `1) *' (q `1)),((p `2) *' (q `2))];
theorem tw2: :: RATFUNC1:20
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for p being rational_function of L
for a being non zero Element of L holds
( [(a * (p `1)),(a * (p `2))] is irreducible iff p is irreducible )
proof
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being rational_function of L
for a being non zero Element of L holds
( [(a * (p `1)),(a * (p `2))] is irreducible iff p is irreducible )
let p be rational_function of L; ::_thesis: for a being non zero Element of L holds
( [(a * (p `1)),(a * (p `2))] is irreducible iff p is irreducible )
let a be non zero Element of L; ::_thesis: ( [(a * (p `1)),(a * (p `2))] is irreducible iff p is irreducible )
set ap = [(a * (p `1)),(a * (p `2))];
A: now__::_thesis:_(_p_is_irreducible_&_[(a_*_(p_`1)),(a_*_(p_`2))]_is_reducible_implies_[(a_*_(p_`1)),(a_*_(p_`2))]_is_irreducible_)
assume A0: p is irreducible ; ::_thesis: ( [(a * (p `1)),(a * (p `2))] is reducible implies [(a * (p `1)),(a * (p `2))] is irreducible )
assume [(a * (p `1)),(a * (p `2))] is reducible ; ::_thesis: [(a * (p `1)),(a * (p `2))] is irreducible
then [(a * (p `1)),(a * (p `2))] `1 ,[(a * (p `1)),(a * (p `2))] `2 have_common_roots by defirred;
then consider x being Element of L such that
A1: x is_a_common_root_of [(a * (p `1)),(a * (p `2))] `1 ,[(a * (p `1)),(a * (p `2))] `2 by root2;
( x is_a_root_of [(a * (p `1)),(a * (p `2))] `1 & x is_a_root_of [(a * (p `1)),(a * (p `2))] `2 ) by A1, root1;
then A2: ( eval (([(a * (p `1)),(a * (p `2))] `1),x) = 0. L & eval (([(a * (p `1)),(a * (p `2))] `2),x) = 0. L ) by POLYNOM5:def_6;
then eval ((a * (p `1)),x) = 0. L ;
then a * (eval ((p `1),x)) = 0. L by POLYNOM5:30;
then eval ((p `1),x) = 0. L by VECTSP_2:def_1;
then A3: x is_a_root_of p `1 by POLYNOM5:def_6;
eval ((a * (p `2)),x) = 0. L by A2;
then a * (eval ((p `2),x)) = 0. L by POLYNOM5:30;
then eval ((p `2),x) = 0. L by VECTSP_2:def_1;
then x is_a_root_of p `2 by POLYNOM5:def_6;
then x is_a_common_root_of p `1 ,p `2 by A3, root1;
then p `1 ,p `2 have_common_roots by root2;
hence [(a * (p `1)),(a * (p `2))] is irreducible by A0, defirred; ::_thesis: verum
end;
now__::_thesis:_(_[(a_*_(p_`1)),(a_*_(p_`2))]_is_irreducible_&_p_is_reducible_implies_p_is_irreducible_)
assume A0: [(a * (p `1)),(a * (p `2))] is irreducible ; ::_thesis: ( p is reducible implies p is irreducible )
assume p is reducible ; ::_thesis: p is irreducible
then p `1 ,p `2 have_common_roots by defirred;
then consider x being Element of L such that
A1: x is_a_common_root_of p `1 ,p `2 by root2;
( x is_a_root_of p `1 & x is_a_root_of p `2 ) by A1, root1;
then A2: ( eval ((p `1),x) = 0. L & eval ((p `2),x) = 0. L ) by POLYNOM5:def_6;
then a * (eval ((p `1),x)) = 0. L by VECTSP_1:6;
then eval ((a * (p `1)),x) = 0. L by POLYNOM5:30;
then eval (([(a * (p `1)),(a * (p `2))] `1),x) = 0. L ;
then A3: x is_a_root_of [(a * (p `1)),(a * (p `2))] `1 by POLYNOM5:def_6;
a * (eval ((p `2),x)) = 0. L by A2, VECTSP_1:6;
then eval ((a * (p `2)),x) = 0. L by POLYNOM5:30;
then eval (([(a * (p `1)),(a * (p `2))] `2),x) = 0. L ;
then x is_a_root_of [(a * (p `1)),(a * (p `2))] `2 by POLYNOM5:def_6;
then x is_a_common_root_of [(a * (p `1)),(a * (p `2))] `1 ,[(a * (p `1)),(a * (p `2))] `2 by A3, root1;
then [(a * (p `1)),(a * (p `2))] `1 ,[(a * (p `1)),(a * (p `2))] `2 have_common_roots by root2;
hence p is irreducible by A0, defirred; ::_thesis: verum
end;
hence ( [(a * (p `1)),(a * (p `2))] is irreducible iff p is irreducible ) by A; ::_thesis: verum
end;
begin
polynormirred: for L being non trivial right_complementable associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr
for z being rational_function of L st z is irreducible holds
ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )
proof
let L be non trivial right_complementable associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for z being rational_function of L st z is irreducible holds
ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )
let z be rational_function of L; ::_thesis: ( z is irreducible implies ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) )
assume AS: z is irreducible ; ::_thesis: ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )
take z ; ::_thesis: ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z `1)),(z2 *' (z `2))] & z is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )
reconsider e = 1_. L as non zero Polynomial of L ;
take e ; ::_thesis: ( z = [(e *' (z `1)),(e *' (z `2))] & z is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( e = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )
reconsider f = <*> the carrier of (Polynom-Ring L) as FinSequence of (Polynom-Ring L) ;
thus z = [(z `1),(z `2)] by ttt
.= [(e *' (z `1)),(z `2)] by POLYNOM3:35
.= [(e *' (z `1)),(e *' (z `2))] by POLYNOM3:35 ; ::_thesis: ( z is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( e = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )
thus z is irreducible by AS; ::_thesis: ex f being FinSequence of (Polynom-Ring L) st
( e = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) )
take f ; ::_thesis: ( e = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) )
Product f = 1_ (Polynom-Ring L) by GROUP_4:8;
hence ( e = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) by POLYNOM3:def_10; ::_thesis: verum
end;
theorem ratfuncNF: :: RATFUNC1:21
for L being non trivial right_complementable associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr
for z being rational_function of L ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )
proof
let L be non trivial right_complementable associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for z being rational_function of L ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )
let z be rational_function of L; ::_thesis: ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )
defpred S1[ Nat] means for z being rational_function of L st max ((deg (z `1)),(deg (z `2))) = $1 holds
ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) );
now__::_thesis:_for_z_being_rational_function_of_L_st_max_((deg_(z_`1)),(deg_(z_`2)))_=_0_holds_
ex_z1_being_rational_function_of_L_ex_z2_being_non_zero_Polynomial_of_L_st_
(_z_=_[(z2_*'_(z1_`1)),(z2_*'_(z1_`2))]_&_z1_is_irreducible_&_ex_f_being_FinSequence_of_(Polynom-Ring_L)_st_
(_z2_=_Product_f_&_(_for_i_being_Element_of_NAT_st_i_in_dom_f_holds_
ex_x_being_Element_of_L_st_
(_x_is_a_common_root_of_z_`1_,z_`2_&_f_._i_=_rpoly_(1,x)_)_)_)_)
let z be rational_function of L; ::_thesis: ( max ((deg (z `1)),(deg (z `2))) = 0 implies ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) )
assume max ((deg (z `1)),(deg (z `2))) = 0 ; ::_thesis: ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )
then deg (z `2) <= 0 by XXREAL_0:25;
then B: deg (z `2) = 0 ;
A: now__::_thesis:_for_x_being_Element_of_L_holds_not_x_is_a_root_of_z_`2
assume ex x being Element of L st x is_a_root_of z `2 ; ::_thesis: contradiction
then consider y being Element of L such that
H: y is_a_root_of z `2 ;
eval ((z `2),y) = 0. L by H, POLYNOM5:def_6;
hence contradiction by B, degrat2; ::_thesis: verum
end;
now__::_thesis:_not_z_is_reducible
assume z is reducible ; ::_thesis: contradiction
then z `1 ,z `2 have_common_roots by defirred;
then consider x being Element of L such that
H: x is_a_common_root_of z `1 ,z `2 by root2;
x is_a_root_of z `2 by H, root1;
hence contradiction by A; ::_thesis: verum
end;
hence ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) by polynormirred; ::_thesis: verum
end;
then IA: S1[ 0 ] ;
IS: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume AS: S1[n] ; ::_thesis: S1[n + 1]
for z being rational_function of L st max ((deg (z `1)),(deg (z `2))) = n + 1 holds
ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )
proof
let z be rational_function of L; ::_thesis: ( max ((deg (z `1)),(deg (z `2))) = n + 1 implies ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) )
assume AS1: max ((deg (z `1)),(deg (z `2))) = n + 1 ; ::_thesis: ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )
percases ( z is irreducible or z is reducible ) ;
suppose z is irreducible ; ::_thesis: ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )
hence ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) by polynormirred; ::_thesis: verum
end;
suppose z is reducible ; ::_thesis: ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )
then z `1 ,z `2 have_common_roots by defirred;
then consider x being Element of L such that
H: x is_a_common_root_of z `1 ,z `2 by root2;
H3: ( x is_a_root_of z `1 & x is_a_root_of z `2 ) by H, root1;
consider q2 being Polynomial of L such that
H2: z `2 = (rpoly (1,x)) *' q2 by H3, HURWITZ:33;
consider q1 being Polynomial of L such that
H1: z `1 = (rpoly (1,x)) *' q1 by H3, HURWITZ:33;
q2 <> 0_. L by H2, POLYNOM3:34;
then reconsider q2 = q2 as non zero Polynomial of L by defzer;
set q = [q1,q2];
max ((deg ([q1,q2] `1)),(deg ([q1,q2] `2))) = n
proof
A2: deg (z `2) = (deg (rpoly (1,x))) + (deg q2) by H2, HURWITZ:23
.= 1 + (deg q2) by HURWITZ:27 ;
percases ( max ((deg (z `1)),(deg (z `2))) = deg (z `1) or max ((deg (z `1)),(deg (z `2))) = deg (z `2) ) by XXREAL_0:16;
supposeA5: max ((deg (z `1)),(deg (z `2))) = deg (z `1) ; ::_thesis: max ((deg ([q1,q2] `1)),(deg ([q1,q2] `2))) = n
then z `1 <> 0_. L by AS1, HURWITZ:20;
then q1 <> 0_. L by H1, POLYNOM3:34;
then A3: deg (z `1) = (deg (rpoly (1,x))) + (deg q1) by H1, HURWITZ:23
.= 1 + (deg q1) by HURWITZ:27 ;
A6: deg (z `2) <= n + 1 by AS1, XXREAL_0:25;
((deg q2) + 1) - 1 <= (n + 1) - 1 by A2, A6, XREAL_1:9;
hence max ((deg ([q1,q2] `1)),(deg ([q1,q2] `2))) = n by A3, A5, AS1, XXREAL_0:def_10; ::_thesis: verum
end;
supposeA3: max ((deg (z `1)),(deg (z `2))) = deg (z `2) ; ::_thesis: max ((deg ([q1,q2] `1)),(deg ([q1,q2] `2))) = n
A6: deg (z `1) <= n + 1 by AS1, XXREAL_0:25;
now__::_thesis:_deg_q1_<=_deg_q2
percases ( q1 = 0_. L or q1 <> 0_. L ) ;
suppose q1 = 0_. L ; ::_thesis: deg q1 <= deg q2
hence deg q1 <= deg q2 by HURWITZ:20; ::_thesis: verum
end;
suppose q1 <> 0_. L ; ::_thesis: deg q1 <= deg q2
then deg (z `1) = (deg (rpoly (1,x))) + (deg q1) by H1, HURWITZ:23
.= 1 + (deg q1) by HURWITZ:27 ;
hence deg q1 <= deg q2 by A6, A2, A3, AS1, XREAL_1:9; ::_thesis: verum
end;
end;
end;
hence max ((deg ([q1,q2] `1)),(deg ([q1,q2] `2))) = n by A3, A2, AS1, XXREAL_0:def_10; ::_thesis: verum
end;
end;
end;
then consider z1q being rational_function of L, z2q being non zero Polynomial of L such that
IQ: ( [q1,q2] = [(z2q *' (z1q `1)),(z2q *' (z1q `2))] & z1q is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2q = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of [q1,q2] `1 ,[q1,q2] `2 & f . i = rpoly (1,x) ) ) ) ) by AS;
take z1 = z1q; ::_thesis: ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )
set z2 = (rpoly (1,x)) *' z2q;
reconsider z2 = (rpoly (1,x)) *' z2q as non zero Polynomial of L ;
take z2 ; ::_thesis: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )
consider fq being FinSequence of (Polynom-Ring L) such that
IQ2: ( z2q = Product fq & ( for i being Element of NAT st i in dom fq holds
ex x being Element of L st
( x is_a_common_root_of [q1,q2] `1 ,[q1,q2] `2 & fq . i = rpoly (1,x) ) ) ) by IQ;
reconsider rp = rpoly (1,x) as Element of (Polynom-Ring L) by POLYNOM3:def_10;
set f = <*rp*> ^ fq;
IQ3: Product (<*rp*> ^ fq) = rp * (Product fq) by GROUP_4:7
.= z2 by IQ2, POLYNOM3:def_10 ;
IQ4: z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))]
proof
X: q1 = z2q *' (z1q `1) by IQ, XTUPLE_0:def_2;
Z: q2 = z2q *' (z1q `2) by IQ, XTUPLE_0:def_3;
Y: z2 *' (z1 `1) = z `1 by X, H1, POLYNOM3:33;
A: z2 *' (z1 `2) = z `2 by Z, H2, POLYNOM3:33;
thus z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] by Y, A, ttt; ::_thesis: verum
end;
IQ5: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_(<*rp*>_^_fq)_holds_
ex_x_being_Element_of_L_st_
(_x_is_a_common_root_of_z_`1_,z_`2_&_(<*rp*>_^_fq)_._i_=_rpoly_(1,x)_)
let i be Element of NAT ; ::_thesis: ( i in dom (<*rp*> ^ fq) implies ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & (<*rp*> ^ fq) . i = rpoly (1,x) ) )
assume C1: i in dom (<*rp*> ^ fq) ; ::_thesis: ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & (<*rp*> ^ fq) . i = rpoly (1,x) )
now__::_thesis:_ex_x_being_Element_of_L_st_
(_x_is_a_common_root_of_z_`1_,z_`2_&_(<*rp*>_^_fq)_._i_=_rpoly_(1,x)_)
percases ( i in dom <*rp*> or ex n being Nat st
( n in dom fq & i = (len <*rp*>) + n ) ) by C1, FINSEQ_1:25;
supposeC2: i in dom <*rp*> ; ::_thesis: ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & (<*rp*> ^ fq) . i = rpoly (1,x) )
then C3: i in {1} by FINSEQ_1:2, FINSEQ_1:38;
(<*rp*> ^ fq) . i = <*rp*> . i by C2, FINSEQ_1:def_7
.= <*rp*> . 1 by C3, TARSKI:def_1
.= rpoly (1,x) by FINSEQ_1:40 ;
hence ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & (<*rp*> ^ fq) . i = rpoly (1,x) ) by H; ::_thesis: verum
end;
suppose ex n being Nat st
( n in dom fq & i = (len <*rp*>) + n ) ; ::_thesis: ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & (<*rp*> ^ fq) . i = rpoly (1,x) )
then consider n being Nat such that
C2: ( n in dom fq & i = (len <*rp*>) + n ) ;
(<*rp*> ^ fq) . i = fq . n by C2, FINSEQ_1:def_7;
then consider y being Element of L such that
C3: ( y is_a_common_root_of [q1,q2] `1 ,[q1,q2] `2 & (<*rp*> ^ fq) . i = rpoly (1,y) ) by C2, IQ2;
C4: ( y is_a_root_of [q1,q2] `1 & y is_a_root_of [q1,q2] `2 ) by C3, root1;
then C5: 0. L = eval (q1,y) by POLYNOM5:def_6;
C8: eval ((z `1),y) = (eval ((rpoly (1,x)),y)) * (eval (q1,y)) by H1, POLYNOM4:24
.= 0. L by C5, VECTSP_1:7 ;
C6: 0. L = eval (q2,y) by C4, POLYNOM5:def_6;
eval ((z `2),y) = (eval ((rpoly (1,x)),y)) * (eval (q2,y)) by H2, POLYNOM4:24
.= 0. L by C6, VECTSP_1:7 ;
then ( y is_a_root_of z `1 & y is_a_root_of z `2 ) by C8, POLYNOM5:def_6;
then y is_a_common_root_of z `1 ,z `2 by root1;
hence ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & (<*rp*> ^ fq) . i = rpoly (1,x) ) by C3; ::_thesis: verum
end;
end;
end;
hence ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & (<*rp*> ^ fq) . i = rpoly (1,x) ) ; ::_thesis: verum
end;
thus ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) by IQ, IQ3, IQ4, IQ5; ::_thesis: verum
end;
end;
end;
hence S1[n + 1] ; ::_thesis: verum
end;
I: for n being Nat holds S1[n] from NAT_1:sch_2(IA, IS);
max ((deg (z `1)),(deg (z `2))) >= deg (z `2) by XXREAL_0:25;
then max ((deg (z `1)),(deg (z `2))) >= 0 ;
then max ((deg (z `1)),(deg (z `2))) in NAT by INT_1:3;
hence ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) by I; ::_thesis: verum
end;
ratfuncNFunique1: for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr
for z being rational_function of L st z is irreducible holds
for z1 being rational_function of L
for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( g2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
( z2 = 1_. L & g2 = 1_. L & z1 = g1 )
proof
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for z being rational_function of L st z is irreducible holds
for z1 being rational_function of L
for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( g2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
( z2 = 1_. L & g2 = 1_. L & z1 = g1 )
let z be rational_function of L; ::_thesis: ( z is irreducible implies for z1 being rational_function of L
for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( g2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
( z2 = 1_. L & g2 = 1_. L & z1 = g1 ) )
assume AS: z is irreducible ; ::_thesis: for z1 being rational_function of L
for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( g2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
( z2 = 1_. L & g2 = 1_. L & z1 = g1 )
let z1 be rational_function of L; ::_thesis: for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( g2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
( z2 = 1_. L & g2 = 1_. L & z1 = g1 )
let z2 be non zero Polynomial of L; ::_thesis: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) implies for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( g2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
( z2 = 1_. L & g2 = 1_. L & z1 = g1 ) )
assume A: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ; ::_thesis: for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( g2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
( z2 = 1_. L & g2 = 1_. L & z1 = g1 )
let g1 be rational_function of L; ::_thesis: for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( g2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
( z2 = 1_. L & g2 = 1_. L & z1 = g1 )
let g2 be non zero Polynomial of L; ::_thesis: ( z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( g2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) implies ( z2 = 1_. L & g2 = 1_. L & z1 = g1 ) )
assume B: ( z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( g2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ; ::_thesis: ( z2 = 1_. L & g2 = 1_. L & z1 = g1 )
consider f being FinSequence of (Polynom-Ring L) such that
C: ( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) by A;
now__::_thesis:_(_f_<>_<*>_the_carrier_of_(Polynom-Ring_L)_implies_for_i_being_Element_of_dom_f_holds_contradiction_)
assume f <> <*> the carrier of (Polynom-Ring L) ; ::_thesis: for i being Element of dom f holds contradiction
then G: dom f <> {} ;
let i be Element of dom f; ::_thesis: contradiction
reconsider i = i as Nat ;
D1: i in dom f by G;
consider x being Element of L such that
D2: ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) by D1, C;
z `1 ,z `2 have_common_roots by D2, root2;
hence contradiction by AS, defirred; ::_thesis: verum
end;
hence D2: z2 = 1_ (Polynom-Ring L) by C, GROUP_4:8
.= 1_. L by POLYNOM3:def_10 ;
::_thesis: ( g2 = 1_. L & z1 = g1 )
then D1: z2 *' (z1 `1) = z1 `1 by POLYNOM3:35;
z2 *' (z1 `2) = z1 `2 by D2, POLYNOM3:35;
then D: z = z1 by D1, A, ttt;
consider h being FinSequence of (Polynom-Ring L) such that
E: ( g2 = Product h & ( for i being Element of NAT st i in dom h holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & h . i = rpoly (1,x) ) ) ) by B;
now__::_thesis:_(_h_<>_<*>_the_carrier_of_(Polynom-Ring_L)_implies_for_i_being_Element_of_dom_h_holds_contradiction_)
assume h <> <*> the carrier of (Polynom-Ring L) ; ::_thesis: for i being Element of dom h holds contradiction
then G: dom h <> {} ;
let i be Element of dom h; ::_thesis: contradiction
reconsider i = i as Nat ;
D1: i in dom h by G;
consider x being Element of L such that
D2: ( x is_a_common_root_of z `1 ,z `2 & h . i = rpoly (1,x) ) by D1, E;
z `1 ,z `2 have_common_roots by D2, root2;
hence contradiction by AS, defirred; ::_thesis: verum
end;
hence E2: g2 = 1_ (Polynom-Ring L) by E, GROUP_4:8
.= 1_. L by POLYNOM3:def_10 ;
::_thesis: z1 = g1
then E1: g2 *' (g1 `1) = g1 `1 by POLYNOM3:35;
g2 *' (g1 `2) = g1 `2 by E2, POLYNOM3:35;
hence z1 = g1 by D, E1, B, ttt; ::_thesis: verum
end;
ratfuncNFunique2: for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr
for z being non zero rational_function of L
for z1 being rational_function of L
for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds
z1 = g1
proof
let L be Field; ::_thesis: for z being non zero rational_function of L
for z1 being rational_function of L
for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds
z1 = g1
let z be non zero rational_function of L; ::_thesis: for z1 being rational_function of L
for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds
z1 = g1
let z1 be rational_function of L; ::_thesis: for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds
z1 = g1
let z2 be non zero Polynomial of L; ::_thesis: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) implies for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds
z1 = g1 )
assume H1: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ; ::_thesis: for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds
z1 = g1
let g1 be rational_function of L; ::_thesis: for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds
z1 = g1
let g2 be non zero Polynomial of L; ::_thesis: ( z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) implies z1 = g1 )
assume H2: ( z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) ) ; ::_thesis: z1 = g1
defpred S1[ Nat] means for z being non zero rational_function of L st max ((deg (z `1)),(deg (z `2))) = $1 holds
for z1 being rational_function of L
for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds
z1 = g1;
now__::_thesis:_for_z_being_non_zero_rational_function_of_L_st_max_((deg_(z_`1)),(deg_(z_`2)))_=_0_holds_
for_z1_being_rational_function_of_L
for_z2_being_non_zero_Polynomial_of_L_st_z_=_[(z2_*'_(z1_`1)),(z2_*'_(z1_`2))]_&_z1_is_irreducible_&_ex_f_being_FinSequence_of_(Polynom-Ring_L)_st_
(_z2_=_Product_f_&_(_for_i_being_Element_of_NAT_st_i_in_dom_f_holds_
ex_x_being_Element_of_L_st_
(_x_is_a_common_root_of_z_`1_,z_`2_&_f_._i_=_rpoly_(1,x)_)_)_)_holds_
for_g1_being_rational_function_of_L
for_g2_being_non_zero_Polynomial_of_L_st_z_=_[(g2_*'_(g1_`1)),(g2_*'_(g1_`2))]_&_g1_is_irreducible_&_ex_g_being_FinSequence_of_(Polynom-Ring_L)_st_
(_g2_=_Product_g_&_(_for_i_being_Element_of_NAT_st_i_in_dom_g_holds_
ex_x_being_Element_of_L_st_
(_x_is_a_common_root_of_z_`1_,z_`2_&_g_._i_=_rpoly_(1,x)_)_)_)_holds_
g1_=_z1
let z be non zero rational_function of L; ::_thesis: ( max ((deg (z `1)),(deg (z `2))) = 0 implies for z1 being rational_function of L
for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds
g1 = z1 )
assume max ((deg (z `1)),(deg (z `2))) = 0 ; ::_thesis: for z1 being rational_function of L
for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds
g1 = z1
then deg (z `2) <= 0 by XXREAL_0:25;
then B: deg (z `2) = 0 ;
let z1 be rational_function of L; ::_thesis: for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds
g1 = z1
let z2 be non zero Polynomial of L; ::_thesis: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) implies for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds
g1 = z1 )
assume H1: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ; ::_thesis: for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds
g1 = z1
let g1 be rational_function of L; ::_thesis: for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds
g1 = z1
let g2 be non zero Polynomial of L; ::_thesis: ( z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) implies g1 = z1 )
assume H2: ( z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) ) ; ::_thesis: g1 = z1
A: now__::_thesis:_for_x_being_Element_of_L_holds_not_x_is_a_root_of_z_`2
assume ex x being Element of L st x is_a_root_of z `2 ; ::_thesis: contradiction
then consider y being Element of L such that
H: y is_a_root_of z `2 ;
eval ((z `2),y) = 0. L by H, POLYNOM5:def_6;
hence contradiction by B, degrat2; ::_thesis: verum
end;
B: now__::_thesis:_not_z_is_reducible
assume z is reducible ; ::_thesis: contradiction
then z `1 ,z `2 have_common_roots by defirred;
then consider x being Element of L such that
H: x is_a_common_root_of z `1 ,z `2 by root2;
x is_a_root_of z `2 by H, root1;
hence contradiction by A; ::_thesis: verum
end;
thus g1 = z1 by B, H1, H2, ratfuncNFunique1; ::_thesis: verum
end;
then IA: S1[ 0 ] ;
IS: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume IV: S1[n] ; ::_thesis: S1[n + 1]
for z being non zero rational_function of L st max ((deg (z `1)),(deg (z `2))) = n + 1 holds
for z1 being rational_function of L
for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds
z1 = g1
proof
let z be non zero rational_function of L; ::_thesis: ( max ((deg (z `1)),(deg (z `2))) = n + 1 implies for z1 being rational_function of L
for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds
z1 = g1 )
assume AS1: max ((deg (z `1)),(deg (z `2))) = n + 1 ; ::_thesis: for z1 being rational_function of L
for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds
z1 = g1
let z1 be rational_function of L; ::_thesis: for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds
z1 = g1
let z2 be non zero Polynomial of L; ::_thesis: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) implies for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds
z1 = g1 )
assume H1: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ; ::_thesis: for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds
z1 = g1
consider f being FinSequence of (Polynom-Ring L) such that
H1a: ( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) by H1;
let g1 be rational_function of L; ::_thesis: for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds
z1 = g1
let g2 be non zero Polynomial of L; ::_thesis: ( z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) implies z1 = g1 )
assume H2: ( z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) ) ; ::_thesis: z1 = g1
consider g being FinSequence of (Polynom-Ring L) such that
H2a: ( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) by H2;
percases ( z is irreducible or z is reducible ) ;
supposeB: z is irreducible ; ::_thesis: z1 = g1
thus g1 = z1 by B, H1, H2, ratfuncNFunique1; ::_thesis: verum
end;
suppose z is reducible ; ::_thesis: z1 = g1
then z `1 ,z `2 have_common_roots by defirred;
then consider x being Element of L such that
H: x is_a_common_root_of z `1 ,z `2 by root2;
H3: ( x is_a_root_of z `1 & x is_a_root_of z `2 ) by H, root1;
consider q2 being Polynomial of L such that
HY: z `2 = (rpoly (1,x)) *' q2 by H3, HURWITZ:33;
consider q1 being Polynomial of L such that
HX: z `1 = (rpoly (1,x)) *' q1 by H3, HURWITZ:33;
q2 <> 0_. L by HY, POLYNOM3:34;
then reconsider q2 = q2 as non zero Polynomial of L by defzer;
set q = [q1,q2];
z `1 <> 0_. L by defzerrat;
then q1 <> 0_. L by HX, POLYNOM3:34;
then [q1,q2] `1 <> 0_. L ;
then reconsider q = [q1,q2] as non zero rational_function of L by defzerrat;
AS2: max ((deg (q `1)),(deg (q `2))) = n
proof
A2: deg (z `2) = (deg (rpoly (1,x))) + (deg q2) by HY, HURWITZ:23
.= 1 + (deg q2) by HURWITZ:27 ;
A7: max ((deg (q `1)),(deg (q `2))) = max ((deg q1),(deg (q `2))) by XTUPLE_0:def_2
.= max ((deg q1),(deg q2)) by XTUPLE_0:def_3 ;
percases ( max ((deg (z `1)),(deg (z `2))) = deg (z `1) or max ((deg (z `1)),(deg (z `2))) = deg (z `2) ) by XXREAL_0:16;
supposeA5: max ((deg (z `1)),(deg (z `2))) = deg (z `1) ; ::_thesis: max ((deg (q `1)),(deg (q `2))) = n
then z `1 <> 0_. L by AS1, HURWITZ:20;
then q1 <> 0_. L by HX, POLYNOM3:34;
then A3: deg (z `1) = (deg (rpoly (1,x))) + (deg q1) by HX, HURWITZ:23
.= 1 + (deg q1) by HURWITZ:27 ;
deg (z `2) <= n + 1 by AS1, XXREAL_0:25;
then ((deg q2) + 1) - 1 <= (n + 1) - 1 by A2, XREAL_1:9;
hence max ((deg (q `1)),(deg (q `2))) = n by A7, A3, A5, AS1, XXREAL_0:def_10; ::_thesis: verum
end;
supposeA3: max ((deg (z `1)),(deg (z `2))) = deg (z `2) ; ::_thesis: max ((deg (q `1)),(deg (q `2))) = n
A6: deg (z `1) <= n + 1 by AS1, XXREAL_0:25;
now__::_thesis:_deg_q1_<=_deg_q2
percases ( q1 = 0_. L or q1 <> 0_. L ) ;
suppose q1 = 0_. L ; ::_thesis: deg q1 <= deg q2
hence deg q1 <= deg q2 by HURWITZ:20; ::_thesis: verum
end;
suppose q1 <> 0_. L ; ::_thesis: deg q1 <= deg q2
then deg (z `1) = (deg (rpoly (1,x))) + (deg q1) by HX, HURWITZ:23
.= 1 + (deg q1) by HURWITZ:27 ;
hence deg q1 <= deg q2 by A6, A3, A2, AS1, XREAL_1:9; ::_thesis: verum
end;
end;
end;
hence max ((deg (q `1)),(deg (q `2))) = n by A7, A2, A3, AS1, XXREAL_0:def_10; ::_thesis: verum
end;
end;
end;
ZZ1: now__::_thesis:_for_i_being_Nat_st_i_in_dom_f_holds_
ex_z_being_Element_of_L_st_f_._i_=_rpoly_(1,z)
let i be Nat; ::_thesis: ( i in dom f implies ex z being Element of L st f . i = rpoly (1,z) )
assume i in dom f ; ::_thesis: ex z being Element of L st f . i = rpoly (1,z)
then ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) by H1a;
hence ex z being Element of L st f . i = rpoly (1,z) ; ::_thesis: verum
end;
ex i being Nat st
( i in dom f & f . i = rpoly (1,x) )
proof
z2 *' (z1 `1) = (rpoly (1,x)) *' q1 by HX, H1, XTUPLE_0:def_2;
then Z11: rpoly (1,x) divides z2 *' (z1 `1) by HURWITZ:34;
z2 *' (z1 `2) = (rpoly (1,x)) *' q2 by HY, H1, XTUPLE_0:def_3;
then Z11a: rpoly (1,x) divides z2 *' (z1 `2) by HURWITZ:34;
now__::_thesis:_(_(_rpoly_(1,x)_divides_z2_&_ex_i,_i_being_Nat_st_
(_i_in_dom_f_&_f_._i_=_rpoly_(1,x)_)_)_or_(_rpoly_(1,x)_divides_z1_`1_&_rpoly_(1,x)_divides_z1_`2_&_ex_i_being_Nat_st_
(_i_in_dom_f_&_f_._i_=_rpoly_(1,x)_)_)_)
percases ( rpoly (1,x) divides z2 or ( rpoly (1,x) divides z1 `1 & rpoly (1,x) divides z1 `2 ) ) by Z11, Z11a, div3;
case rpoly (1,x) divides z2 ; ::_thesis: ex i, i being Nat st
( i in dom f & f . i = rpoly (1,x) )
then eval (z2,x) = 0. L by div1;
then consider i being Nat such that
Z3: ( i in dom f & f . i = rpoly (1,x) ) by div2, H1a, ZZ1;
take i = i; ::_thesis: ex i being Nat st
( i in dom f & f . i = rpoly (1,x) )
thus ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) by Z3; ::_thesis: verum
end;
case ( rpoly (1,x) divides z1 `1 & rpoly (1,x) divides z1 `2 ) ; ::_thesis: ex i being Nat st
( i in dom f & f . i = rpoly (1,x) )
then ( eval ((z1 `1),x) = 0. L & eval ((z1 `2),x) = 0. L ) by div1;
then ( x is_a_root_of z1 `1 & x is_a_root_of z1 `2 ) by POLYNOM5:def_6;
then Z3: x is_a_common_root_of z1 `1 ,z1 `2 by root1;
z1 `1 ,z1 `2 have_no_common_roots by H1, defirred;
hence ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) by Z3, root2; ::_thesis: verum
end;
end;
end;
hence ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) ; ::_thesis: verum
end;
then consider i being Nat such that
H5: ( i in dom f & f . i = rpoly (1,x) ) ;
ZZ1a: now__::_thesis:_for_j_being_Nat_st_j_in_dom_g_holds_
ex_z_being_Element_of_L_st_g_._j_=_rpoly_(1,z)
let j be Nat; ::_thesis: ( j in dom g implies ex z being Element of L st g . j = rpoly (1,z) )
assume j in dom g ; ::_thesis: ex z being Element of L st g . j = rpoly (1,z)
then consider x being Element of L such that
A: ( x is_a_common_root_of z `1 ,z `2 & g . j = rpoly (1,x) ) by H2a;
thus ex z being Element of L st g . j = rpoly (1,z) by A; ::_thesis: verum
end;
ex j being Nat st
( j in dom g & g . j = rpoly (1,x) )
proof
g2 *' (g1 `1) = (rpoly (1,x)) *' q1 by HX, H2, XTUPLE_0:def_2;
then Z11: rpoly (1,x) divides g2 *' (g1 `1) by HURWITZ:34;
g2 *' (g1 `2) = (rpoly (1,x)) *' q2 by HY, H2, XTUPLE_0:def_3;
then Z11a: rpoly (1,x) divides g2 *' (g1 `2) by HURWITZ:34;
now__::_thesis:_(_(_rpoly_(1,x)_divides_g2_&_ex_i,_j_being_Nat_st_
(_j_in_dom_g_&_g_._j_=_rpoly_(1,x)_)_)_or_(_rpoly_(1,x)_divides_g1_`1_&_rpoly_(1,x)_divides_g1_`2_&_ex_j_being_Nat_st_
(_j_in_dom_g_&_g_._j_=_rpoly_(1,x)_)_)_)
percases ( rpoly (1,x) divides g2 or ( rpoly (1,x) divides g1 `1 & rpoly (1,x) divides g1 `2 ) ) by Z11, Z11a, div3;
case rpoly (1,x) divides g2 ; ::_thesis: ex i, j being Nat st
( j in dom g & g . j = rpoly (1,x) )
then eval (g2,x) = 0. L by div1;
then consider i being Nat such that
Z3: ( i in dom g & g . i = rpoly (1,x) ) by div2, H2a, ZZ1a;
take i = i; ::_thesis: ex j being Nat st
( j in dom g & g . j = rpoly (1,x) )
thus ex j being Nat st
( j in dom g & g . j = rpoly (1,x) ) by Z3; ::_thesis: verum
end;
case ( rpoly (1,x) divides g1 `1 & rpoly (1,x) divides g1 `2 ) ; ::_thesis: ex j being Nat st
( j in dom g & g . j = rpoly (1,x) )
then ( eval ((g1 `1),x) = 0. L & eval ((g1 `2),x) = 0. L ) by div1;
then ( x is_a_root_of g1 `1 & x is_a_root_of g1 `2 ) by POLYNOM5:def_6;
then Z3: x is_a_common_root_of g1 `1 ,g1 `2 by root1;
g1 `1 ,g1 `2 have_no_common_roots by H2, defirred;
hence ex j being Nat st
( j in dom g & g . j = rpoly (1,x) ) by Z3, root2; ::_thesis: verum
end;
end;
end;
hence ex j being Nat st
( j in dom g & g . j = rpoly (1,x) ) ; ::_thesis: verum
end;
then consider j being Nat such that
H6: ( j in dom g & g . j = rpoly (1,x) ) ;
reconsider fq = Del (f,i) as FinSequence of (Polynom-Ring L) by FINSEQ_3:105;
reconsider gq = Del (g,j) as FinSequence of (Polynom-Ring L) by FINSEQ_3:105;
X100: now__::_thesis:_for_k_being_Nat_st_k_in_dom_fq_holds_
ex_x_being_Element_of_L_st_fq_._k_=_rpoly_(1,x)
let k be Nat; ::_thesis: ( k in dom fq implies ex x being Element of L st fq . k = rpoly (1,x) )
assume H11: k in dom fq ; ::_thesis: ex x being Element of L st fq . k = rpoly (1,x)
consider m being Nat such that
H14: ( len f = m + 1 & len fq = m ) by H5, FINSEQ_3:104;
H14a: k in Seg m by H11, H14, FINSEQ_1:def_3;
Seg m c= Seg (m + 1) by FINSEQ_3:18;
then k in Seg (m + 1) by H14a;
then H13: k in dom f by H14, FINSEQ_1:def_3;
H14b: k <= m by H14a, FINSEQ_1:1;
then H14d: k + 1 <= m + 1 by XREAL_1:6;
1 <= k + 1 by NAT_1:11;
then k + 1 in Seg (m + 1) by H14d;
then H14c: k + 1 in dom f by H14, FINSEQ_1:def_3;
now__::_thesis:_ex_x_being_Element_of_L_st_fq_._k_=_rpoly_(1,x)
percases ( k < i or i <= k ) ;
supposeH12: k < i ; ::_thesis: ex x being Element of L st fq . k = rpoly (1,x)
ex y being Element of L st
( y is_a_common_root_of z `1 ,z `2 & f . k = rpoly (1,y) ) by H13, H1a;
hence ex x being Element of L st fq . k = rpoly (1,x) by H12, FINSEQ_3:110; ::_thesis: verum
end;
supposeH12: i <= k ; ::_thesis: ex x being Element of L st fq . k = rpoly (1,x)
ex y being Element of L st
( y is_a_common_root_of z `1 ,z `2 & f . (k + 1) = rpoly (1,y) ) by H1a, H14c;
hence ex x being Element of L st fq . k = rpoly (1,x) by H12, H14b, H5, H14, FINSEQ_3:111; ::_thesis: verum
end;
end;
end;
hence ex x being Element of L st fq . k = rpoly (1,x) ; ::_thesis: verum
end;
X101: now__::_thesis:_for_k_being_Nat_st_k_in_dom_gq_holds_
ex_x_being_Element_of_L_st_gq_._k_=_rpoly_(1,x)
let k be Nat; ::_thesis: ( k in dom gq implies ex x being Element of L st gq . k = rpoly (1,x) )
assume H11: k in dom gq ; ::_thesis: ex x being Element of L st gq . k = rpoly (1,x)
consider m being Nat such that
H14: ( len g = m + 1 & len gq = m ) by H6, FINSEQ_3:104;
H14a: k in Seg m by H11, H14, FINSEQ_1:def_3;
Seg m c= Seg (m + 1) by FINSEQ_3:18;
then k in Seg (m + 1) by H14a;
then H13: k in dom g by H14, FINSEQ_1:def_3;
H14b: k <= m by H14a, FINSEQ_1:1;
then H14d: k + 1 <= m + 1 by XREAL_1:6;
1 <= k + 1 by NAT_1:11;
then k + 1 in Seg (m + 1) by H14d;
then H14c: k + 1 in dom g by H14, FINSEQ_1:def_3;
now__::_thesis:_ex_x_being_Element_of_L_st_gq_._k_=_rpoly_(1,x)
percases ( k < j or j <= k ) ;
supposeH12: k < j ; ::_thesis: ex x being Element of L st gq . k = rpoly (1,x)
ex y being Element of L st
( y is_a_common_root_of z `1 ,z `2 & g . k = rpoly (1,y) ) by H13, H2a;
hence ex x being Element of L st gq . k = rpoly (1,x) by H12, FINSEQ_3:110; ::_thesis: verum
end;
supposeH12: j <= k ; ::_thesis: ex x being Element of L st gq . k = rpoly (1,x)
ex y being Element of L st
( y is_a_common_root_of z `1 ,z `2 & g . (k + 1) = rpoly (1,y) ) by H2a, H14c;
hence ex x being Element of L st gq . k = rpoly (1,x) by H12, H14b, H6, H14, FINSEQ_3:111; ::_thesis: verum
end;
end;
end;
hence ex x being Element of L st gq . k = rpoly (1,x) ; ::_thesis: verum
end;
reconsider z2q = Product fq as Polynomial of L by POLYNOM3:def_10;
z2q <> 0_. L by X100, div4;
then reconsider z2q = z2q as non zero Polynomial of L by defzer;
reconsider g2q = Product gq as Polynomial of L by POLYNOM3:def_10;
g2q <> 0_. L by X101, div4;
then reconsider g2q = g2q as non zero Polynomial of L by defzer;
H7: Product f = (f /. i) * (Product fq) by H5, del1;
H7a: Product g = (g /. j) * (Product gq) by H6, del1;
Seg (len f) = dom f by FINSEQ_1:def_3;
then ( 1 <= i & i <= len f ) by H5, FINSEQ_1:1;
then f /. i = rpoly (1,x) by H5, FINSEQ_4:15;
then H9: (rpoly (1,x)) *' z2q = Product f by H7, POLYNOM3:def_10;
then H8: (rpoly (1,x)) *' (z2q *' (z1 `1)) = z2 *' (z1 `1) by H1a, POLYNOM3:33
.= (rpoly (1,x)) *' q1 by HX, H1, XTUPLE_0:def_2
.= (rpoly (1,x)) *' (q `1) by XTUPLE_0:def_2 ;
then H8b: z2q *' (z1 `1) = q `1 by thequiv1;
H8a: (rpoly (1,x)) *' (z2q *' (z1 `2)) = z2 *' (z1 `2) by H9, H1a, POLYNOM3:33
.= (rpoly (1,x)) *' q2 by HY, H1, XTUPLE_0:def_3
.= (rpoly (1,x)) *' (q `2) by XTUPLE_0:def_3 ;
then z2q *' (z1 `2) = q `2 by thequiv1;
then I1: q = [(z2q *' (z1 `1)),(z2q *' (z1 `2))] by H8b, MCART_1:8;
I3: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_fq_holds_
ex_x_being_Element_of_L_st_
(_x_is_a_common_root_of_q_`1_,q_`2_&_fq_._k_=_rpoly_(1,x)_)
let k be Element of NAT ; ::_thesis: ( k in dom fq implies ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & fq . k = rpoly (1,x) ) )
assume H11: k in dom fq ; ::_thesis: ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & fq . k = rpoly (1,x) )
consider m being Nat such that
H14: ( len f = m + 1 & len fq = m ) by H5, FINSEQ_3:104;
H14a: k in Seg m by H11, H14, FINSEQ_1:def_3;
Seg m c= Seg (m + 1) by FINSEQ_3:18;
then k in Seg (m + 1) by H14a;
then H13: k in dom f by H14, FINSEQ_1:def_3;
H14b: k <= m by H14a, FINSEQ_1:1;
then H14d: k + 1 <= m + 1 by XREAL_1:6;
1 <= k + 1 by NAT_1:11;
then k + 1 in Seg (m + 1) by H14d;
then H14c: k + 1 in dom f by H14, FINSEQ_1:def_3;
now__::_thesis:_ex_x_being_Element_of_L_st_
(_x_is_a_common_root_of_q_`1_,q_`2_&_fq_._k_=_rpoly_(1,x)_)
percases ( k < i or i <= k ) ;
supposeH12: k < i ; ::_thesis: ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & fq . k = rpoly (1,x) )
then H12a: f . k = fq . k by FINSEQ_3:110;
consider y being Element of L such that
H10: ( y is_a_common_root_of z `1 ,z `2 & f . k = rpoly (1,y) ) by H13, H1a;
H25: eval (z2q,y) = 0. L by H12a, H10, H11, X100, div2;
then 0. L = (eval (z2q,y)) * (eval ((z1 `1),y)) by VECTSP_1:7
.= eval ((z2q *' (z1 `1)),y) by POLYNOM4:24
.= eval ((q `1),y) by H8, thequiv1 ;
then A1: y is_a_root_of q `1 by POLYNOM5:def_6;
0. L = (eval (z2q,y)) * (eval ((z1 `2),y)) by VECTSP_1:7, H25
.= eval ((z2q *' (z1 `2)),y) by POLYNOM4:24
.= eval ((q `2),y) by H8a, thequiv1 ;
then y is_a_root_of q `2 by POLYNOM5:def_6;
then y is_a_common_root_of q `1 ,q `2 by A1, root1;
hence ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & fq . k = rpoly (1,x) ) by H10, H12, FINSEQ_3:110; ::_thesis: verum
end;
supposeH12: i <= k ; ::_thesis: ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & fq . k = rpoly (1,x) )
then H12a: f . (k + 1) = fq . k by H14b, H5, H14, FINSEQ_3:111;
consider y being Element of L such that
H10: ( y is_a_common_root_of z `1 ,z `2 & f . (k + 1) = rpoly (1,y) ) by H1a, H14c;
H25: eval (z2q,y) = 0. L by H12a, H10, H11, X100, div2;
then 0. L = (eval (z2q,y)) * (eval ((z1 `1),y)) by VECTSP_1:7
.= eval ((z2q *' (z1 `1)),y) by POLYNOM4:24
.= eval ((q `1),y) by H8, thequiv1 ;
then A1: y is_a_root_of q `1 by POLYNOM5:def_6;
0. L = (eval (z2q,y)) * (eval ((z1 `2),y)) by VECTSP_1:7, H25
.= eval ((z2q *' (z1 `2)),y) by POLYNOM4:24
.= eval ((q `2),y) by H8a, thequiv1 ;
then y is_a_root_of q `2 by POLYNOM5:def_6;
then y is_a_common_root_of q `1 ,q `2 by A1, root1;
hence ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & fq . k = rpoly (1,x) ) by H10, H12, H14b, H5, H14, FINSEQ_3:111; ::_thesis: verum
end;
end;
end;
hence ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & fq . k = rpoly (1,x) ) ; ::_thesis: verum
end;
Seg (len g) = dom g by FINSEQ_1:def_3;
then ( 1 <= j & j <= len g ) by H6, FINSEQ_1:1;
then g /. j = rpoly (1,x) by H6, FINSEQ_4:15;
then H9: (rpoly (1,x)) *' g2q = Product g by H7a, POLYNOM3:def_10;
then H8: (rpoly (1,x)) *' (g2q *' (g1 `1)) = g2 *' (g1 `1) by H2a, POLYNOM3:33
.= z `1 by H2, XTUPLE_0:def_2
.= (rpoly (1,x)) *' (q `1) by HX, XTUPLE_0:def_2 ;
then H8b: g2q *' (g1 `1) = q `1 by thequiv1;
H8a: (rpoly (1,x)) *' (g2q *' (g1 `2)) = g2 *' (g1 `2) by H9, H2a, POLYNOM3:33
.= z `2 by H2, XTUPLE_0:def_3
.= (rpoly (1,x)) *' (q `2) by HY, XTUPLE_0:def_3 ;
then g2q *' (g1 `2) = q `2 by thequiv1;
then I2: q = [(g2q *' (g1 `1)),(g2q *' (g1 `2))] by H8b, MCART_1:8;
I4: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_gq_holds_
ex_x_being_Element_of_L_st_
(_x_is_a_common_root_of_q_`1_,q_`2_&_gq_._k_=_rpoly_(1,x)_)
let k be Element of NAT ; ::_thesis: ( k in dom gq implies ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & gq . k = rpoly (1,x) ) )
assume H11: k in dom gq ; ::_thesis: ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & gq . k = rpoly (1,x) )
consider m being Nat such that
H14: ( len g = m + 1 & len gq = m ) by H6, FINSEQ_3:104;
H14a: k in Seg m by H11, H14, FINSEQ_1:def_3;
Seg m c= Seg (m + 1) by FINSEQ_3:18;
then k in Seg (m + 1) by H14a;
then H13: k in dom g by H14, FINSEQ_1:def_3;
H14b: k <= m by H14a, FINSEQ_1:1;
then H14d: k + 1 <= m + 1 by XREAL_1:6;
1 <= k + 1 by NAT_1:11;
then k + 1 in Seg (m + 1) by H14d;
then H14c: k + 1 in dom g by H14, FINSEQ_1:def_3;
now__::_thesis:_ex_x_being_Element_of_L_st_
(_x_is_a_common_root_of_q_`1_,q_`2_&_gq_._k_=_rpoly_(1,x)_)
percases ( k < j or j <= k ) ;
supposeH12: k < j ; ::_thesis: ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & gq . k = rpoly (1,x) )
then H12a: g . k = gq . k by FINSEQ_3:110;
consider y being Element of L such that
H10: ( y is_a_common_root_of z `1 ,z `2 & g . k = rpoly (1,y) ) by H13, H2a;
H25: eval (g2q,y) = 0. L by H12a, H10, H11, X101, div2;
then 0. L = (eval (g2q,y)) * (eval ((g1 `1),y)) by VECTSP_1:7
.= eval ((g2q *' (g1 `1)),y) by POLYNOM4:24
.= eval ((q `1),y) by H8, thequiv1 ;
then A1: y is_a_root_of q `1 by POLYNOM5:def_6;
0. L = (eval (g2q,y)) * (eval ((g1 `2),y)) by VECTSP_1:7, H25
.= eval ((g2q *' (g1 `2)),y) by POLYNOM4:24
.= eval ((q `2),y) by H8a, thequiv1 ;
then y is_a_root_of q `2 by POLYNOM5:def_6;
then y is_a_common_root_of q `1 ,q `2 by A1, root1;
hence ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & gq . k = rpoly (1,x) ) by H10, H12, FINSEQ_3:110; ::_thesis: verum
end;
supposeH12: j <= k ; ::_thesis: ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & gq . k = rpoly (1,x) )
then H13: g . (k + 1) = gq . k by H14b, H6, H14, FINSEQ_3:111;
consider y being Element of L such that
H10: ( y is_a_common_root_of z `1 ,z `2 & g . (k + 1) = rpoly (1,y) ) by H2a, H14c;
H25: eval (g2q,y) = 0. L by H13, H10, H11, X101, div2;
then 0. L = (eval (g2q,y)) * (eval ((g1 `1),y)) by VECTSP_1:7
.= eval ((g2q *' (g1 `1)),y) by POLYNOM4:24
.= eval ((q `1),y) by H8, thequiv1 ;
then A1: y is_a_root_of q `1 by POLYNOM5:def_6;
0. L = (eval (g2q,y)) * (eval ((g1 `2),y)) by VECTSP_1:7, H25
.= eval ((g2q *' (g1 `2)),y) by POLYNOM4:24
.= eval ((q `2),y) by H8a, thequiv1 ;
then y is_a_root_of q `2 by POLYNOM5:def_6;
then y is_a_common_root_of q `1 ,q `2 by A1, root1;
hence ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & gq . k = rpoly (1,x) ) by H10, H12, H14b, H6, H14, FINSEQ_3:111; ::_thesis: verum
end;
end;
end;
hence ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & gq . k = rpoly (1,x) ) ; ::_thesis: verum
end;
thus z1 = g1 by H1, H2, I1, I2, I3, I4, AS2, IV; ::_thesis: verum
end;
end;
end;
hence S1[n + 1] ; ::_thesis: verum
end;
I: for n being Nat holds S1[n] from NAT_1:sch_2(IA, IS);
max ((deg (z `1)),(deg (z `2))) >= deg (z `2) by XXREAL_0:25;
then max ((deg (z `1)),(deg (z `2))) >= 0 ;
then max ((deg (z `1)),(deg (z `2))) in NAT by INT_1:3;
hence z1 = g1 by I, H1, H2; ::_thesis: verum
end;
definition
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ;
let z be rational_function of L;
func NF z -> rational_function of L means :defNF: :: RATFUNC1:def 17
ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & it = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) if not z is zero
otherwise it = 0._ L;
existence
( ( not z is zero implies ex b1, z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b1 = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ) & ( z is zero implies ex b1 being rational_function of L st b1 = 0._ L ) )
proof
percases ( not z is zero or z is zero ) ;
suppose not z is zero ; ::_thesis: ( ( not z is zero implies ex b1, z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b1 = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ) & ( z is zero implies ex b1 being rational_function of L st b1 = 0._ L ) )
consider z1 being rational_function of L, z2 being non zero Polynomial of L such that
H: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) by ratfuncNF;
reconsider nfz = NormRatF z1 as rational_function of L ;
ex zz1 being rational_function of L ex zz2 being non zero Polynomial of L st
( nfz = NormRatF zz1 & zz1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( zz2 = Product f & z = [(zz2 *' (zz1 `1)),(zz2 *' (zz1 `2))] & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) by H;
hence ( ( not z is zero implies ex b1, z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b1 = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ) & ( z is zero implies ex b1 being rational_function of L st b1 = 0._ L ) ) ; ::_thesis: verum
end;
suppose z is zero ; ::_thesis: ( ( not z is zero implies ex b1, z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b1 = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ) & ( z is zero implies ex b1 being rational_function of L st b1 = 0._ L ) )
hence ( ( not z is zero implies ex b1, z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b1 = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ) & ( z is zero implies ex b1 being rational_function of L st b1 = 0._ L ) ) ; ::_thesis: verum
end;
end;
end;
uniqueness
for b1, b2 being rational_function of L holds
( ( not z is zero & ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b1 = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) & ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b2 = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) implies b1 = b2 ) & ( z is zero & b1 = 0._ L & b2 = 0._ L implies b1 = b2 ) ) by ratfuncNFunique2;
consistency
for b1 being rational_function of L holds verum ;
end;
:: deftheorem defNF defines NF RATFUNC1:def_17_:_
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr
for z, b3 being rational_function of L holds
( ( not z is zero implies ( b3 = NF z iff ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b3 = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ) ) & ( z is zero implies ( b3 = NF z iff b3 = 0._ L ) ) );
registration
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ;
let z be rational_function of L;
cluster NF z -> irreducible normalized ;
coherence
( NF z is normalized & NF z is irreducible )
proof
percases ( not z is zero or z is zero ) ;
suppose not z is zero ; ::_thesis: ( NF z is normalized & NF z is irreducible )
then consider z1 being rational_function of L, z2 being non zero Polynomial of L such that
H: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & NF z = NormRatF z1 & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) by defNF;
A: NF z is irreducible by H, tw2;
(NF z) `2 = ((1. L) / (LC (z1 `2))) * (z1 `2) by H, XTUPLE_0:def_3;
hence ( NF z is normalized & NF z is irreducible ) by A, defnorm; ::_thesis: verum
end;
suppose z is zero ; ::_thesis: ( NF z is normalized & NF z is irreducible )
then NF z = 0._ L by defNF;
hence ( NF z is normalized & NF z is irreducible ) ; ::_thesis: verum
end;
end;
end;
end;
registration
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ;
let z be non zero rational_function of L;
cluster NF z -> non zero ;
coherence
not NF z is zero
proof
consider z1 being rational_function of L, z2 being non zero Polynomial of L such that
H: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & NF z = NormRatF z1 & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) by defNF;
now__::_thesis:_not_z1_`1_=_0_._L
assume z1 `1 = 0_. L ; ::_thesis: contradiction
then 0_. L = z2 *' (z1 `1) by POLYNOM3:34
.= z `1 by H, XTUPLE_0:def_2 ;
hence contradiction by defzerrat; ::_thesis: verum
end;
then not z1 is zero by defzerrat;
hence not NF z is zero by H; ::_thesis: verum
end;
end;
defnf1a: for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr
for z being non zero irreducible rational_function of L holds NF z = NormRationalFunction z
proof
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for z being non zero irreducible rational_function of L holds NF z = NormRationalFunction z
let z be non zero irreducible rational_function of L; ::_thesis: NF z = NormRationalFunction z
consider z1 being rational_function of L, z2 being non zero Polynomial of L such that
A1: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & NF z = NormRatF z1 & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) by defNF;
consider f being FinSequence of (Polynom-Ring L) such that
A2: ( z2 = Product f & z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) by A1;
now__::_thesis:_(_f_<>_<*>_the_carrier_of_(Polynom-Ring_L)_implies_for_i_being_Element_of_dom_f_holds_contradiction_)
assume AS: f <> <*> the carrier of (Polynom-Ring L) ; ::_thesis: for i being Element of dom f holds contradiction
let i be Element of dom f; ::_thesis: contradiction
dom f <> {} by AS;
then i in dom f ;
then reconsider i = i as Element of NAT ;
consider x being Element of L such that
A4: ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) by A2, AS;
z `1 ,z `2 have_common_roots by A4, root2;
hence contradiction by defirred; ::_thesis: verum
end;
then A5: Product f = 1_ (Polynom-Ring L) by GROUP_4:8
.= 1_. L by POLYNOM3:def_10 ;
then z = [(z1 `1),(z2 *' (z1 `2))] by A2, POLYNOM3:35
.= [(z1 `1),(z1 `2)] by A2, A5, POLYNOM3:35
.= z1 by ttt ;
hence NF z = NormRationalFunction z by A1; ::_thesis: verum
end;
theorem :: RATFUNC1:22
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr
for z being non zero rational_function of L
for z1 being rational_function of L
for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
NF z = NormRationalFunction z1 by defNF;
theorem :: RATFUNC1:23
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr holds NF (0._ L) = 0._ L by defNF;
theorem :: RATFUNC1:24
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr holds NF (1._ L) = 1._ L
proof
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: NF (1._ L) = 1._ L
set z = 1._ L;
B: NF (1._ L) = NormRatF (1._ L) by defnf1a
.= [(((1. L) / (LC ((1._ L) `2))) * ((1._ L) `1)),(((1. L) / (LC ((1._ L) `2))) * ((1._ L) `2))] ;
(1._ L) `2 is normalized by defnorm;
then D: LC ((1._ L) `2) = 1. L by defnormp;
C: (1. L) / (LC ((1._ L) `2)) = 1. L by D, VECTSP_1:def_10;
hence NF (1._ L) = [((1._ L) `1),(((1. L) / (LC ((1._ L) `2))) * ((1._ L) `2))] by B, POLYNOM5:27
.= [((1._ L) `1),((1._ L) `2)] by C, POLYNOM5:27
.= 1._ L by ttt ;
::_thesis: verum
end;
theorem :: RATFUNC1:25
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr
for z being non zero irreducible rational_function of L holds NF z = NormRationalFunction z by defnf1a;
tt2: for L being non trivial right_complementable unital distributive Abelian add-associative right_zeroed domRing-like left_zeroed doubleLoopStr
for p1, p2 being Polynomial of L holds
( not p1 *' p2 = 0_. L or p1 = 0_. L or p2 = 0_. L )
proof
let L be non trivial right_complementable unital distributive Abelian add-associative right_zeroed domRing-like left_zeroed doubleLoopStr ; ::_thesis: for p1, p2 being Polynomial of L holds
( not p1 *' p2 = 0_. L or p1 = 0_. L or p2 = 0_. L )
let p1, p2 be Polynomial of L; ::_thesis: ( not p1 *' p2 = 0_. L or p1 = 0_. L or p2 = 0_. L )
assume AS: p1 *' p2 = 0_. L ; ::_thesis: ( p1 = 0_. L or p2 = 0_. L )
now__::_thesis:_(_p1_<>_0_._L_implies_not_p2_<>_0_._L_)
assume ( p1 <> 0_. L & p2 <> 0_. L ) ; ::_thesis: contradiction
then reconsider x1 = p1, x2 = p2 as non zero Polynomial of L by defzer;
not x1 *' x2 is zero ;
hence contradiction by AS; ::_thesis: verum
end;
hence ( p1 = 0_. L or p2 = 0_. L ) ; ::_thesis: verum
end;
theorem nfequiv: :: RATFUNC1:26
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr
for z being rational_function of L
for x being Element of L holds NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = NF z
proof
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for z being rational_function of L
for x being Element of L holds NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = NF z
let z be rational_function of L; ::_thesis: for x being Element of L holds NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = NF z
let x be Element of L; ::_thesis: NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = NF z
percases ( not z is zero or z is zero ) ;
supposeA: not z is zero ; ::_thesis: NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = NF z
then consider z1 being rational_function of L, z2 being non zero Polynomial of L such that
A1: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & NF z = NormRatF z1 & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) by defNF;
consider f being FinSequence of (Polynom-Ring L) such that
A2: ( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) by A1;
set q = [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))];
now__::_thesis:_not_[((rpoly_(1,x))_*'_(z_`1)),((rpoly_(1,x))_*'_(z_`2))]_`1_=_0_._L
assume [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] `1 = 0_. L ; ::_thesis: contradiction
then (rpoly (1,x)) *' (z `1) = 0_. L ;
then z `1 = 0_. L by tt2;
hence contradiction by A, defzerrat; ::_thesis: verum
end;
then reconsider q = [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] as non zero rational_function of L by defzerrat;
reconsider rp = rpoly (1,x) as Element of (Polynom-Ring L) by POLYNOM3:def_10;
set g = <*rp*> ^ f;
reconsider g = <*rp*> ^ f as FinSequence of (Polynom-Ring L) ;
set g2 = Product g;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_g_holds_
ex_z_being_Element_of_L_st_g_._i_=_rpoly_(1,z)
let i be Nat; ::_thesis: ( i in dom g implies ex z being Element of L st g . i = rpoly (1,z) )
assume Y: i in dom g ; ::_thesis: ex z being Element of L st g . i = rpoly (1,z)
now__::_thesis:_ex_z_being_Element_of_L_st_g_._i_=_rpoly_(1,z)
percases ( i in dom <*rp*> or ex n being Nat st
( n in dom f & i = (len <*rp*>) + n ) ) by Y, FINSEQ_1:25;
supposeX: i in dom <*rp*> ; ::_thesis: ex z being Element of L st g . i = rpoly (1,z)
then i in {1} by FINSEQ_1:2, FINSEQ_1:38;
then i = 1 by TARSKI:def_1;
then g . i = <*rp*> . 1 by X, FINSEQ_1:def_7
.= rp by FINSEQ_1:40 ;
hence ex z being Element of L st g . i = rpoly (1,z) ; ::_thesis: verum
end;
suppose ex n being Nat st
( n in dom f & i = (len <*rp*>) + n ) ; ::_thesis: ex z being Element of L st g . i = rpoly (1,z)
then consider n being Nat such that
H: ( n in dom f & i = (len <*rp*>) + n ) ;
J: g . i = f . n by H, FINSEQ_1:def_7;
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . n = rpoly (1,x) ) by H, A2;
hence ex z being Element of L st g . i = rpoly (1,z) by J; ::_thesis: verum
end;
end;
end;
hence ex z being Element of L st g . i = rpoly (1,z) ; ::_thesis: verum
end;
then Product g <> 0_. L by div4;
then reconsider g2 = Product g as non zero Polynomial of L by defzer, POLYNOM3:def_10;
A3: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_g_holds_
ex_x_being_Element_of_L_st_
(_x_is_a_common_root_of_q_`1_,q_`2_&_g_._i_=_rpoly_(1,x)_)
let i be Element of NAT ; ::_thesis: ( i in dom g implies ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & g . i = rpoly (1,x) ) )
assume Y: i in dom g ; ::_thesis: ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & g . i = rpoly (1,x) )
now__::_thesis:_ex_z_being_Element_of_L_st_
(_z_is_a_common_root_of_q_`1_,q_`2_&_g_._i_=_rpoly_(1,z)_)
percases ( i in dom <*rp*> or ex n being Nat st
( n in dom f & i = (len <*rp*>) + n ) ) by Y, FINSEQ_1:25;
supposeX: i in dom <*rp*> ; ::_thesis: ex z being Element of L st
( z is_a_common_root_of q `1 ,q `2 & g . i = rpoly (1,z) )
then i in {1} by FINSEQ_1:2, FINSEQ_1:38;
then i = 1 by TARSKI:def_1;
then I: g . i = <*rp*> . 1 by X, FINSEQ_1:def_7
.= rp by FINSEQ_1:40 ;
H: eval ((rpoly (1,x)),x) = x - x by HURWITZ:29
.= 0. L by RLVECT_1:15 ;
then 0. L = (eval ((rpoly (1,x)),x)) * (eval ((z `1),x)) by VECTSP_1:7
.= eval (((rpoly (1,x)) *' (z `1)),x) by POLYNOM4:24 ;
then x is_a_root_of (rpoly (1,x)) *' (z `1) by POLYNOM5:def_6;
then J: x is_a_root_of q `1 by XTUPLE_0:def_2;
0. L = (eval ((rpoly (1,x)),x)) * (eval ((z `2),x)) by H, VECTSP_1:7
.= eval (((rpoly (1,x)) *' (z `2)),x) by POLYNOM4:24 ;
then x is_a_root_of (rpoly (1,x)) *' (z `2) by POLYNOM5:def_6;
then x is_a_root_of q `2 by XTUPLE_0:def_3;
then x is_a_common_root_of q `1 ,q `2 by J, root1;
hence ex z being Element of L st
( z is_a_common_root_of q `1 ,q `2 & g . i = rpoly (1,z) ) by I; ::_thesis: verum
end;
suppose ex n being Nat st
( n in dom f & i = (len <*rp*>) + n ) ; ::_thesis: ex z being Element of L st
( z is_a_common_root_of q `1 ,q `2 & g . i = rpoly (1,z) )
then consider n being Nat such that
H: ( n in dom f & i = (len <*rp*>) + n ) ;
J: g . i = f . n by H, FINSEQ_1:def_7;
consider y being Element of L such that
I: ( y is_a_common_root_of z `1 ,z `2 & f . n = rpoly (1,y) ) by H, A2;
y is_a_root_of z `1 by I, root1;
then eval ((z `1),y) = 0. L by POLYNOM5:def_6;
then 0. L = (eval ((rpoly (1,x)),y)) * (eval ((z `1),y)) by VECTSP_1:6
.= eval (((rpoly (1,x)) *' (z `1)),y) by POLYNOM4:24 ;
then y is_a_root_of (rpoly (1,x)) *' (z `1) by POLYNOM5:def_6;
then K: y is_a_root_of q `1 by XTUPLE_0:def_2;
y is_a_root_of z `2 by I, root1;
then eval ((z `2),y) = 0. L by POLYNOM5:def_6;
then 0. L = (eval ((rpoly (1,x)),y)) * (eval ((z `2),y)) by VECTSP_1:6
.= eval (((rpoly (1,x)) *' (z `2)),y) by POLYNOM4:24 ;
then y is_a_root_of (rpoly (1,x)) *' (z `2) by POLYNOM5:def_6;
then y is_a_root_of q `2 by XTUPLE_0:def_3;
then y is_a_common_root_of q `1 ,q `2 by K, root1;
hence ex z being Element of L st
( z is_a_common_root_of q `1 ,q `2 & g . i = rpoly (1,z) ) by J, I; ::_thesis: verum
end;
end;
end;
hence ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & g . i = rpoly (1,x) ) ; ::_thesis: verum
end;
A4: Product g = rp * (Product f) by GROUP_4:7;
A5: q `1 = (rpoly (1,x)) *' (z `1) by XTUPLE_0:def_2
.= (rpoly (1,x)) *' (z2 *' (z1 `1)) by A1, XTUPLE_0:def_2
.= ((rpoly (1,x)) *' z2) *' (z1 `1) by POLYNOM3:33
.= g2 *' (z1 `1) by A4, A2, POLYNOM3:def_10 ;
q `2 = (rpoly (1,x)) *' (z `2) by XTUPLE_0:def_3
.= (rpoly (1,x)) *' (z2 *' (z1 `2)) by A1, XTUPLE_0:def_3
.= ((rpoly (1,x)) *' z2) *' (z1 `2) by POLYNOM3:33
.= g2 *' (z1 `2) by A4, A2, POLYNOM3:def_10 ;
then q = [(g2 *' (z1 `1)),(g2 *' (z1 `2))] by A5, ttt;
hence NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = NF z by A1, A3, defNF; ::_thesis: verum
end;
supposeA: z is zero ; ::_thesis: NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = NF z
then z `1 = 0_. L by defzerrat;
then (rpoly (1,x)) *' (z `1) = 0_. L by POLYNOM3:34;
then [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] `1 = 0_. L ;
then [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] is zero by defzerrat;
then NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = 0._ L by defNF;
hence NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = NF z by A, defNF; ::_thesis: verum
end;
end;
end;
theorem :: RATFUNC1:27
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr
for z being rational_function of L holds NF (NF z) = NF z
proof
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for z being rational_function of L holds NF (NF z) = NF z
let z be rational_function of L; ::_thesis: NF (NF z) = NF z
set nfz = NF z;
percases ( z is zero or not z is zero ) ;
suppose z is zero ; ::_thesis: NF (NF z) = NF z
then A: NF z = 0._ L by defNF;
thus NF (NF z) = NF z by A, defNF; ::_thesis: verum
end;
supposeA: not z is zero ; ::_thesis: NF (NF z) = NF z
H: 1. L <> 0. L ;
B: NF (NF z) = NormRatF (NF z) by A, defnf1a
.= [(((1. L) / (LC ((NF z) `2))) * ((NF z) `1)),(((1. L) / (LC ((NF z) `2))) * ((NF z) `2))] ;
(NF z) `2 is normalized by defnorm;
then D: LC ((NF z) `2) = 1. L by defnormp;
C: (1. L) / (LC ((NF z) `2)) = 1. L by H, D, VECTSP_1:def_10;
then NF (NF z) = [((NF z) `1),(((1. L) / (LC ((NF z) `2))) * ((NF z) `2))] by B, POLYNOM5:27
.= [((NF z) `1),((NF z) `2)] by C, POLYNOM5:27
.= NF z by ttt ;
hence NF (NF z) = NF z ; ::_thesis: verum
end;
end;
end;
theorem th3: :: RATFUNC1:28
for L being non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr
for z being non zero rational_function of L holds
( z is irreducible iff ex a being Element of L st
( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) )
proof
let L be non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for z being non zero rational_function of L holds
( z is irreducible iff ex a being Element of L st
( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) )
let z be non zero rational_function of L; ::_thesis: ( z is irreducible iff ex a being Element of L st
( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) )
set q = z `2 ;
set a = (LC (z `2)) " ;
now__::_thesis:_not_(LC_(z_`2))_"_=_0._L
assume AB: (LC (z `2)) " = 0. L ; ::_thesis: contradiction
then AC: ((LC (z `2)) ") * (LC (z `2)) = 0. L by VECTSP_1:7;
(LC (z `2)) " <> 1. L by AB;
hence contradiction by AC, VECTSP_1:def_10; ::_thesis: verum
end;
then reconsider a = (LC (z `2)) " as non zero Element of L by STRUCT_0:def_12;
reconsider x = [(a * (z `1)),(a * (z `2))] as rational_function of L ;
A: now__::_thesis:_(_z_is_irreducible_implies_ex_a_being_Element_of_L_st_
(_a_<>_0._L_&_[(a_*_(z_`1)),(a_*_(z_`2))]_=_NF_z_)_)
assume z is irreducible ; ::_thesis: ex a being Element of L st
( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z )
then NF z = NormRatF z by defnf1a
.= [(((1. L) / (LC (z `2))) * (z `1)),(((1. L) / (LC (z `2))) * (z `2))] ;
hence ex a being Element of L st
( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) ; ::_thesis: verum
end;
now__::_thesis:_(_ex_a_being_Element_of_L_st_
(_a_<>_0._L_&_[(a_*_(z_`1)),(a_*_(z_`2))]_=_NF_z_)_implies_z_is_irreducible_)
assume ex a being Element of L st
( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) ; ::_thesis: z is irreducible
then consider a being Element of L such that
H0: ( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) ;
reconsider x = [(a * (z `1)),(a * (z `2))] as rational_function of L by H0;
H1: ( x `1 = a * (z `1) & x `2 = a * (z `2) ) by XTUPLE_0:def_2, XTUPLE_0:def_3;
now__::_thesis:_not_z_`1_,z_`2_have_a_common_root
assume z `1 ,z `2 have_a_common_root ; ::_thesis: contradiction
then consider u being Element of L such that
C1: u is_a_common_root_of z `1 ,z `2 by root2;
( u is_a_root_of z `1 & u is_a_root_of z `2 ) by root1, C1;
then C3: ( eval ((z `1),u) = 0. L & eval ((z `2),u) = 0. L ) by POLYNOM5:def_6;
eval ((x `1),u) = a * (eval ((z `1),u)) by H1, POLYNOM5:30;
then eval ((x `1),u) = 0. L by C3, VECTSP_1:6;
then C2: u is_a_root_of x `1 by POLYNOM5:def_6;
eval ((x `2),u) = a * (eval ((z `2),u)) by H1, POLYNOM5:30;
then eval ((x `2),u) = 0. L by C3, VECTSP_1:7;
then u is_a_root_of x `2 by POLYNOM5:def_6;
then u is_a_common_root_of x `1 ,x `2 by C2, root1;
then x `1 ,x `2 have_a_common_root by root2;
hence contradiction by defirred, H0; ::_thesis: verum
end;
hence z is irreducible by defirred; ::_thesis: verum
end;
hence ( z is irreducible iff ex a being Element of L st
( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) ) by A; ::_thesis: verum
end;
begin
definition
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ;
let z be rational_function of L;
func degree z -> Integer equals :: RATFUNC1:def 18
max ((degree ((NF z) `1)),(degree ((NF z) `2)));
coherence
max ((degree ((NF z) `1)),(degree ((NF z) `2))) is Integer ;
end;
:: deftheorem defines degree RATFUNC1:def_18_:_
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr
for z being rational_function of L holds degree z = max ((degree ((NF z) `1)),(degree ((NF z) `2)));
notation
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ;
let z be rational_function of L;
synonym deg z for degree z;
end;
th1a: for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr
for z being non zero rational_function of L st z is irreducible holds
degree z = max ((degree (z `1)),(degree (z `2)))
proof
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for z being non zero rational_function of L st z is irreducible holds
degree z = max ((degree (z `1)),(degree (z `2)))
let z be non zero rational_function of L; ::_thesis: ( z is irreducible implies degree z = max ((degree (z `1)),(degree (z `2))) )
assume z is irreducible ; ::_thesis: degree z = max ((degree (z `1)),(degree (z `2)))
then consider a being Element of L such that
H: ( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) by th3;
not a is zero by H, STRUCT_0:def_12;
then reconsider az2 = a * (z `2) as non zero Polynomial of L ;
H3: (NF z) `2 = a * (z `2) by H, XTUPLE_0:def_3;
thus degree z = max ((deg (a * (z `1))),(deg (a * (z `2)))) by H, XTUPLE_0:def_2, H3
.= max ((deg (z `1)),(deg az2)) by H, POLYNOM5:25
.= max ((degree (z `1)),(degree (z `2))) by H, POLYNOM5:25 ; ::_thesis: verum
end;
theorem th1: :: RATFUNC1:29
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr
for z being rational_function of L holds degree z <= max ((degree (z `1)),(degree (z `2)))
proof
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for z being rational_function of L holds degree z <= max ((degree (z `1)),(degree (z `2)))
let z be rational_function of L; ::_thesis: degree z <= max ((degree (z `1)),(degree (z `2)))
percases ( z is zero or not z is zero ) ;
supposeH: z is zero ; ::_thesis: degree z <= max ((degree (z `1)),(degree (z `2)))
then A: NF z = 0._ L by defNF
.= [(0_. L),(1_. L)] ;
z `1 = 0_. L by H, defzerrat;
then B: deg (z `1) = - 1 by HURWITZ:20;
E: deg (1_. L) = 1 - 1 by POLYNOM4:4;
deg z = max ((deg (0_. L)),(degree ((NF z) `2))) by A, XTUPLE_0:def_2
.= max ((deg (0_. L)),(deg (1_. L))) by A, XTUPLE_0:def_3
.= max ((- 1),(deg (1_. L))) by HURWITZ:20
.= 0 by E, XXREAL_0:def_10 ;
hence degree z <= max ((degree (z `1)),(degree (z `2))) by B, XXREAL_0:def_10; ::_thesis: verum
end;
supposeA: not z is zero ; ::_thesis: degree z <= max ((degree (z `1)),(degree (z `2)))
defpred S1[ Nat] means for z being non zero rational_function of L st max ((degree (z `1)),(degree (z `2))) = $1 holds
max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2)));
now__::_thesis:_for_z_being_non_zero_rational_function_of_L
for_z1_being_rational_function_of_L
for_z2_being_non_zero_Polynomial_of_L
for_f_being_FinSequence_of_(Polynom-Ring_L)_st_max_((degree_(z_`1)),(degree_(z_`2)))_=_0_holds_
max_((degree_((NF_z)_`1)),(degree_((NF_z)_`2)))_<=_max_((degree_(z_`1)),(degree_(z_`2)))
let z be non zero rational_function of L; ::_thesis: for z1 being rational_function of L
for z2 being non zero Polynomial of L
for f being FinSequence of (Polynom-Ring L) st max ((degree (z `1)),(degree (z `2))) = 0 holds
max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2)))
let z1 be rational_function of L; ::_thesis: for z2 being non zero Polynomial of L
for f being FinSequence of (Polynom-Ring L) st max ((degree (z `1)),(degree (z `2))) = 0 holds
max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2)))
let z2 be non zero Polynomial of L; ::_thesis: for f being FinSequence of (Polynom-Ring L) st max ((degree (z `1)),(degree (z `2))) = 0 holds
max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2)))
let f be FinSequence of (Polynom-Ring L); ::_thesis: ( max ((degree (z `1)),(degree (z `2))) = 0 implies max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2))) )
assume AS: max ((degree (z `1)),(degree (z `2))) = 0 ; ::_thesis: max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2)))
now__::_thesis:_z_`1_,z_`2_have_no_common_roots
percases ( degree (z `1) = 0 or degree (z `2) = 0 ) by AS, XXREAL_0:16;
supposeH: degree (z `1) = 0 ; ::_thesis: z `1 ,z `2 have_no_common_roots
now__::_thesis:_not_z_`1_,z_`2_have_common_roots
assume z `1 ,z `2 have_common_roots ; ::_thesis: contradiction
then consider x being Element of L such that
HH: x is_a_common_root_of z `1 ,z `2 by root2;
x is_a_root_of z `1 by HH, root1;
then z `1 is with_roots by POLYNOM5:def_7;
hence contradiction by HURWITZ:24, H; ::_thesis: verum
end;
hence z `1 ,z `2 have_no_common_roots ; ::_thesis: verum
end;
supposeH: degree (z `2) = 0 ; ::_thesis: z `1 ,z `2 have_no_common_roots
now__::_thesis:_not_z_`1_,z_`2_have_common_roots
assume z `1 ,z `2 have_common_roots ; ::_thesis: contradiction
then consider x being Element of L such that
HH: x is_a_common_root_of z `1 ,z `2 by root2;
x is_a_root_of z `2 by HH, root1;
then z `2 is with_roots by POLYNOM5:def_7;
hence contradiction by HURWITZ:24, H; ::_thesis: verum
end;
hence z `1 ,z `2 have_no_common_roots ; ::_thesis: verum
end;
end;
end;
then z is irreducible by defirred;
then degree z = max ((degree (z `1)),(degree (z `2))) by th1a;
hence max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2))) ; ::_thesis: verum
end;
then IA: S1[ 0 ] ;
IS: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume IV: S1[n] ; ::_thesis: S1[n + 1]
now__::_thesis:_for_z_being_non_zero_rational_function_of_L_st_max_((degree_(z_`1)),(degree_(z_`2)))_=_n_+_1_holds_
max_((degree_((NF_z)_`1)),(degree_((NF_z)_`2)))_<=_max_((degree_(z_`1)),(degree_(z_`2)))
let z be non zero rational_function of L; ::_thesis: ( max ((degree (z `1)),(degree (z `2))) = n + 1 implies max ((degree ((NF b1) `1)),(degree ((NF b1) `2))) <= max ((degree (b1 `1)),(degree (b1 `2))) )
assume AS: max ((degree (z `1)),(degree (z `2))) = n + 1 ; ::_thesis: max ((degree ((NF b1) `1)),(degree ((NF b1) `2))) <= max ((degree (b1 `1)),(degree (b1 `2)))
percases ( z is irreducible or z is reducible ) ;
suppose z is irreducible ; ::_thesis: max ((degree ((NF b1) `1)),(degree ((NF b1) `2))) <= max ((degree (b1 `1)),(degree (b1 `2)))
then degree z = max ((degree (z `1)),(degree (z `2))) by th1a;
hence max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2))) ; ::_thesis: verum
end;
suppose z is reducible ; ::_thesis: max ((degree ((NF b1) `1)),(degree ((NF b1) `2))) <= max ((degree (b1 `1)),(degree (b1 `2)))
then z `1 ,z `2 have_common_roots by defirred;
then consider x being Element of L such that
H: x is_a_common_root_of z `1 ,z `2 by root2;
H3: ( x is_a_root_of z `1 & x is_a_root_of z `2 ) by H, root1;
consider q2 being Polynomial of L such that
HY: z `2 = (rpoly (1,x)) *' q2 by H3, HURWITZ:33;
consider q1 being Polynomial of L such that
HX: z `1 = (rpoly (1,x)) *' q1 by H3, HURWITZ:33;
q1 <> 0_. L by defzerrat, HX, POLYNOM3:34;
then reconsider q1 = q1 as non zero Polynomial of L by defzer;
q2 <> 0_. L by HY, POLYNOM3:34;
then reconsider q2 = q2 as non zero Polynomial of L by defzer;
set q = [q1,q2];
now__::_thesis:_not_[q1,q2]_is_zero
assume [q1,q2] is zero ; ::_thesis: contradiction
then [q1,q2] `1 = 0_. L by defzerrat;
hence contradiction ; ::_thesis: verum
end;
then reconsider q = [q1,q2] as non zero rational_function of L ;
z = [((rpoly (1,x)) *' q1),((rpoly (1,x)) *' q2)] by ttt, HX, HY
.= [((rpoly (1,x)) *' (q `1)),((rpoly (1,x)) *' q2)] by XTUPLE_0:def_2
.= [((rpoly (1,x)) *' (q `1)),((rpoly (1,x)) *' (q `2))] by XTUPLE_0:def_3 ;
then HZ: NF z = NF q by nfequiv;
HV: n <= n + 1 by NAT_1:11;
W4: deg (z `1) = (deg (rpoly (1,x))) + (deg q1) by HX, HURWITZ:23
.= 1 + (deg q1) by HURWITZ:27
.= 1 + (deg (q `1)) by XTUPLE_0:def_2 ;
deg (z `2) = (deg (rpoly (1,x))) + (deg q2) by HY, HURWITZ:23
.= 1 + (deg q2) by HURWITZ:27
.= 1 + (deg (q `2)) by XTUPLE_0:def_3 ;
then HU: max ((degree (z `1)),(degree (z `2))) = 1 + (max ((degree (q `1)),(degree (q `2)))) by W4, maxx;
then max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (q `1)),(degree (q `2))) by IV, HZ, AS;
hence max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2))) by HV, HU, AS, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence S1[n + 1] ; ::_thesis: verum
end;
I: for n being Nat holds S1[n] from NAT_1:sch_2(IA, IS);
max ((degree (z `1)),(degree (z `2))) >= 0 by XXREAL_0:25;
then max ((degree (z `1)),(degree (z `2))) in NAT by INT_1:3;
hence degree z <= max ((degree (z `1)),(degree (z `2))) by A, I; ::_thesis: verum
end;
end;
end;
theorem :: RATFUNC1:30
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr
for z being non zero rational_function of L holds
( z is irreducible iff degree z = max ((degree (z `1)),(degree (z `2))) )
proof
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for z being non zero rational_function of L holds
( z is irreducible iff degree z = max ((degree (z `1)),(degree (z `2))) )
let z be non zero rational_function of L; ::_thesis: ( z is irreducible iff degree z = max ((degree (z `1)),(degree (z `2))) )
set p1 = z `1 ;
set p2 = z `2 ;
A: now__::_thesis:_(_z_is_irreducible_implies_degree_z_=_max_((degree_(z_`1)),(degree_(z_`2)))_)
assume z is irreducible ; ::_thesis: degree z = max ((degree (z `1)),(degree (z `2)))
then consider a being Element of L such that
A1: ( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) by th3;
A2: degree (a * (z `1)) = degree (z `1) by POLYNOM5:25, A1;
A3: degree (a * (z `2)) = degree (z `2) by POLYNOM5:25, A1;
degree ((NF z) `1) = degree (z `1) by A2, A1, XTUPLE_0:def_2;
hence degree z = max ((degree (z `1)),(degree (z `2))) by A3, A1, XTUPLE_0:def_3; ::_thesis: verum
end;
now__::_thesis:_(_degree_z_=_max_((degree_(z_`1)),(degree_(z_`2)))_implies_z_is_irreducible_)
assume AS: degree z = max ((degree (z `1)),(degree (z `2))) ; ::_thesis: z is irreducible
now__::_thesis:_z_is_irreducible
assume not z is irreducible ; ::_thesis: contradiction
then z `1 ,z `2 have_a_common_root by defirred;
then consider x being Element of L such that
A1: x is_a_common_root_of z `1 ,z `2 by root2;
A2: ( x is_a_root_of z `1 & x is_a_root_of z `2 ) by A1, root1;
then consider q1 being Polynomial of L such that
A3: z `1 = (rpoly (1,x)) *' q1 by HURWITZ:33;
consider q2 being Polynomial of L such that
A4: z `2 = (rpoly (1,x)) *' q2 by A2, HURWITZ:33;
q2 <> 0_. L by A4, POLYNOM3:34;
then reconsider q2 = q2 as non zero Polynomial of L by defzer;
set zz = [q1,q2];
H1: ( [q1,q2] `1 = q1 & [q1,q2] `2 = q2 ) ;
z = [((rpoly (1,x)) *' ([q1,q2] `1)),((rpoly (1,x)) *' ([q1,q2] `2))] by ttt, A3, A4;
then NF z = NF [q1,q2] by nfequiv;
then degree z = degree [q1,q2] ;
then A8: degree z <= max ((degree q1),(degree q2)) by th1, H1;
now__::_thesis:_contradiction
percases ( z `1 = 0_. L or z `1 <> 0_. L ) ;
supposeB0: z `1 = 0_. L ; ::_thesis: contradiction
B4: q1 = 0_. L by B0, A3, tt2;
(deg ((rpoly (1,x)) *' q2)) + 0 = (deg (rpoly (1,x))) + (deg q2) by HURWITZ:23
.= 1 + (deg q2) by HURWITZ:27 ;
then C: deg q2 < deg (z `2) by A4, XREAL_1:8;
deg (z `1) <= deg (z `2) by HURWITZ:20, B0;
then B3: max ((deg (z `1)),(deg (z `2))) = deg (z `2) by XXREAL_0:def_10;
deg q1 <= deg q2 by HURWITZ:20, B4;
hence contradiction by B3, C, AS, A8, XXREAL_0:def_10; ::_thesis: verum
end;
suppose z `1 <> 0_. L ; ::_thesis: contradiction
then reconsider p1 = z `1 as non zero Polynomial of L by defzer;
now__::_thesis:_not_q1_=_0_._L
assume q1 = 0_. L ; ::_thesis: contradiction
then p1 = 0_. L by A3, POLYNOM3:34;
hence contradiction ; ::_thesis: verum
end;
then reconsider q1 = q1 as non zero Polynomial of L by defzer;
(deg p1) + 0 = (deg (rpoly (1,x))) + (deg q1) by A3, HURWITZ:23
.= 1 + (deg q1) by HURWITZ:27 ;
then H2: deg q1 < deg p1 by XREAL_1:8;
(deg (z `2)) + 0 = (deg (rpoly (1,x))) + (deg q2) by A4, HURWITZ:23
.= 1 + (deg q2) by HURWITZ:27 ;
then deg q2 < deg (z `2) by XREAL_1:8;
hence contradiction by AS, A8, H2, XXREAL_0:27; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
hence z is irreducible ; ::_thesis: verum
end;
hence ( z is irreducible iff degree z = max ((degree (z `1)),(degree (z `2))) ) by A; ::_thesis: verum
end;
begin
definition
let L be Field;
let z be rational_function of L;
let x be Element of L;
func eval (z,x) -> Element of L equals :: RATFUNC1:def 19
(eval ((z `1),x)) / (eval ((z `2),x));
coherence
(eval ((z `1),x)) / (eval ((z `2),x)) is Element of L ;
end;
:: deftheorem defines eval RATFUNC1:def_19_:_
for L being Field
for z being rational_function of L
for x being Element of L holds eval (z,x) = (eval ((z `1),x)) / (eval ((z `2),x));
theorem ev0: :: RATFUNC1:31
for L being Field
for x being Element of L holds eval ((0._ L),x) = 0. L
proof
let L be Field; ::_thesis: for x being Element of L holds eval ((0._ L),x) = 0. L
let x be Element of L; ::_thesis: eval ((0._ L),x) = 0. L
thus eval ((0._ L),x) = (eval ((0_. L),x)) * ((eval (((0._ L) `2),x)) ") by XTUPLE_0:def_2
.= (0. L) * ((eval (((0._ L) `2),x)) ") by POLYNOM4:17
.= 0. L by VECTSP_1:7 ; ::_thesis: verum
end;
theorem :: RATFUNC1:32
for L being Field
for x being Element of L holds eval ((1._ L),x) = 1. L
proof
let L be Field; ::_thesis: for x being Element of L holds eval ((1._ L),x) = 1. L
let x be Element of L; ::_thesis: eval ((1._ L),x) = 1. L
A: 1. L <> 0. L ;
thus eval ((1._ L),x) = (eval ((1_. L),x)) * ((eval (((1._ L) `2),x)) ") by XTUPLE_0:def_2
.= (1. L) * ((eval (((1._ L) `2),x)) ") by POLYNOM4:18
.= (1. L) * ((eval ((1_. L),x)) ") by XTUPLE_0:def_3
.= (1. L) * ((1. L) ") by POLYNOM4:18
.= 1. L by A, VECTSP_1:def_10 ; ::_thesis: verum
end;
theorem :: RATFUNC1:33
for L being Field
for p, q being rational_function of L
for x being Element of L st eval ((p `2),x) <> 0. L & eval ((q `2),x) <> 0. L holds
eval ((p + q),x) = (eval (p,x)) + (eval (q,x))
proof
let L be Field; ::_thesis: for p, q being rational_function of L
for x being Element of L st eval ((p `2),x) <> 0. L & eval ((q `2),x) <> 0. L holds
eval ((p + q),x) = (eval (p,x)) + (eval (q,x))
let p, q be rational_function of L; ::_thesis: for x being Element of L st eval ((p `2),x) <> 0. L & eval ((q `2),x) <> 0. L holds
eval ((p + q),x) = (eval (p,x)) + (eval (q,x))
let x be Element of L; ::_thesis: ( eval ((p `2),x) <> 0. L & eval ((q `2),x) <> 0. L implies eval ((p + q),x) = (eval (p,x)) + (eval (q,x)) )
assume AS: ( eval ((p `2),x) <> 0. L & eval ((q `2),x) <> 0. L ) ; ::_thesis: eval ((p + q),x) = (eval (p,x)) + (eval (q,x))
thus eval ((p + q),x) = (eval ((((p `1) *' (q `2)) + ((p `2) *' (q `1))),x)) * ((eval (((p + q) `2),x)) ") by XTUPLE_0:def_2
.= (eval ((((p `1) *' (q `2)) + ((p `2) *' (q `1))),x)) * ((eval (((p `2) *' (q `2)),x)) ") by XTUPLE_0:def_3
.= (eval ((((p `1) *' (q `2)) + ((p `2) *' (q `1))),x)) * (((eval ((p `2),x)) * (eval ((q `2),x))) ") by POLYNOM4:24
.= (eval ((((p `1) *' (q `2)) + ((p `2) *' (q `1))),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) ")) by AS, VECTSP_2:11
.= ((eval (((p `1) *' (q `2)),x)) + (eval (((p `2) *' (q `1)),x))) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) ")) by POLYNOM4:19
.= ((eval (((p `1) *' (q `2)),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) "))) + ((eval (((p `2) *' (q `1)),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) "))) by VECTSP_1:def_3
.= (((eval ((p `1),x)) * (eval ((q `2),x))) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) "))) + ((eval (((p `2) *' (q `1)),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) "))) by POLYNOM4:24
.= ((eval ((p `1),x)) * ((eval ((q `2),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) ")))) + ((eval (((p `2) *' (q `1)),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) "))) by GROUP_1:def_3
.= ((eval ((p `1),x)) * (((eval ((q `2),x)) * ((eval ((q `2),x)) ")) * ((eval ((p `2),x)) "))) + ((eval (((p `2) *' (q `1)),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) "))) by GROUP_1:def_3
.= ((eval ((p `1),x)) * ((1. L) * ((eval ((p `2),x)) "))) + ((eval (((p `2) *' (q `1)),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) "))) by AS, VECTSP_1:def_10
.= ((eval ((p `1),x)) * ((eval ((p `2),x)) ")) + ((eval (((p `2) *' (q `1)),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) "))) by VECTSP_1:def_8
.= ((eval ((p `1),x)) * ((eval ((p `2),x)) ")) + (((eval ((p `2),x)) * (eval ((q `1),x))) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) "))) by POLYNOM4:24
.= ((eval ((p `1),x)) * ((eval ((p `2),x)) ")) + ((eval ((q `1),x)) * ((eval ((p `2),x)) * (((eval ((p `2),x)) ") * ((eval ((q `2),x)) ")))) by GROUP_1:def_3
.= ((eval ((p `1),x)) * ((eval ((p `2),x)) ")) + ((eval ((q `1),x)) * (((eval ((p `2),x)) * ((eval ((p `2),x)) ")) * ((eval ((q `2),x)) "))) by GROUP_1:def_3
.= ((eval ((p `1),x)) * ((eval ((p `2),x)) ")) + ((eval ((q `1),x)) * ((1. L) * ((eval ((q `2),x)) "))) by AS, VECTSP_1:def_10
.= (eval (p,x)) + (eval (q,x)) by VECTSP_1:def_8 ; ::_thesis: verum
end;
theorem :: RATFUNC1:34
for L being Field
for p, q being rational_function of L
for x being Element of L st eval ((p `2),x) <> 0. L & eval ((q `2),x) <> 0. L holds
eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))
proof
let L be Field; ::_thesis: for p, q being rational_function of L
for x being Element of L st eval ((p `2),x) <> 0. L & eval ((q `2),x) <> 0. L holds
eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))
let p, q be rational_function of L; ::_thesis: for x being Element of L st eval ((p `2),x) <> 0. L & eval ((q `2),x) <> 0. L holds
eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))
let x be Element of L; ::_thesis: ( eval ((p `2),x) <> 0. L & eval ((q `2),x) <> 0. L implies eval ((p *' q),x) = (eval (p,x)) * (eval (q,x)) )
assume AS: ( eval ((p `2),x) <> 0. L & eval ((q `2),x) <> 0. L ) ; ::_thesis: eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))
thus eval ((p *' q),x) = (eval (((p `1) *' (q `1)),x)) * ((eval (((p *' q) `2),x)) ") by XTUPLE_0:def_2
.= (eval (((p `1) *' (q `1)),x)) * ((eval (((p `2) *' (q `2)),x)) ") by XTUPLE_0:def_3
.= (eval (((p `1) *' (q `1)),x)) * (((eval ((p `2),x)) * (eval ((q `2),x))) ") by POLYNOM4:24
.= (eval (((p `1) *' (q `1)),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) ")) by AS, VECTSP_2:11
.= ((eval ((p `1),x)) * (eval ((q `1),x))) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) ")) by POLYNOM4:24
.= (eval ((p `1),x)) * ((eval ((q `1),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) "))) by GROUP_1:def_3
.= (eval ((p `1),x)) * (((eval ((p `2),x)) ") * (((eval ((q `2),x)) ") * (eval ((q `1),x)))) by GROUP_1:def_3
.= (eval (p,x)) * (eval (q,x)) by GROUP_1:def_3 ; ::_thesis: verum
end;
theorem ev4: :: RATFUNC1:35
for L being Field
for p being rational_function of L
for x being Element of L st eval ((p `2),x) <> 0. L holds
eval ((NormRationalFunction p),x) = eval (p,x)
proof
let L be Field; ::_thesis: for p being rational_function of L
for x being Element of L st eval ((p `2),x) <> 0. L holds
eval ((NormRationalFunction p),x) = eval (p,x)
let p be rational_function of L; ::_thesis: for x being Element of L st eval ((p `2),x) <> 0. L holds
eval ((NormRationalFunction p),x) = eval (p,x)
let x be Element of L; ::_thesis: ( eval ((p `2),x) <> 0. L implies eval ((NormRationalFunction p),x) = eval (p,x) )
assume AS: eval ((p `2),x) <> 0. L ; ::_thesis: eval ((NormRationalFunction p),x) = eval (p,x)
set np = NormRationalFunction p;
H: (1. L) / (LC (p `2)) <> 0. L ;
thus eval ((NormRationalFunction p),x) = (eval ((((1. L) / (LC (p `2))) * (p `1)),x)) * ((eval (((NormRationalFunction p) `2),x)) ") by XTUPLE_0:def_2
.= (eval ((((1. L) / (LC (p `2))) * (p `1)),x)) * ((eval ((((1. L) / (LC (p `2))) * (p `2)),x)) ") by XTUPLE_0:def_3
.= (((1. L) / (LC (p `2))) * (eval ((p `1),x))) * ((eval ((((1. L) / (LC (p `2))) * (p `2)),x)) ") by POLYNOM5:30
.= (((1. L) / (LC (p `2))) * (eval ((p `1),x))) * ((((1. L) / (LC (p `2))) * (eval ((p `2),x))) ") by POLYNOM5:30
.= (((1. L) / (LC (p `2))) * (eval ((p `1),x))) * ((((1. L) / (LC (p `2))) ") * ((eval ((p `2),x)) ")) by AS, VECTSP_2:11
.= (eval ((p `1),x)) * (((1. L) / (LC (p `2))) * ((((1. L) / (LC (p `2))) ") * ((eval ((p `2),x)) "))) by GROUP_1:def_3
.= (eval ((p `1),x)) * ((((1. L) / (LC (p `2))) * (((1. L) / (LC (p `2))) ")) * ((eval ((p `2),x)) ")) by GROUP_1:def_3
.= (eval ((p `1),x)) * ((1. L) * ((eval ((p `2),x)) ")) by H, VECTSP_1:def_10
.= eval (p,x) by VECTSP_1:def_8 ; ::_thesis: verum
end;
theorem :: RATFUNC1:36
for L being Field
for p being rational_function of L
for x being Element of L holds
( not eval ((p `2),x) <> 0. L or x is_a_common_root_of p `1 ,p `2 or eval ((NF p),x) = eval (p,x) )
proof
let L be Field; ::_thesis: for p being rational_function of L
for x being Element of L holds
( not eval ((p `2),x) <> 0. L or x is_a_common_root_of p `1 ,p `2 or eval ((NF p),x) = eval (p,x) )
let p be rational_function of L; ::_thesis: for x being Element of L holds
( not eval ((p `2),x) <> 0. L or x is_a_common_root_of p `1 ,p `2 or eval ((NF p),x) = eval (p,x) )
let x be Element of L; ::_thesis: ( not eval ((p `2),x) <> 0. L or x is_a_common_root_of p `1 ,p `2 or eval ((NF p),x) = eval (p,x) )
assume AS1: eval ((p `2),x) <> 0. L ; ::_thesis: ( x is_a_common_root_of p `1 ,p `2 or eval ((NF p),x) = eval (p,x) )
assume AS: not x is_a_common_root_of p `1 ,p `2 ; ::_thesis: eval ((NF p),x) = eval (p,x)
percases ( p is zero or not p is zero ) ;
supposeH: p is zero ; ::_thesis: eval ((NF p),x) = eval (p,x)
then H1: p `1 = 0_. L by defzerrat;
H2: NF p = 0._ L by H, defNF;
thus eval (p,x) = (0. L) * ((eval ((p `2),x)) ") by H1, POLYNOM4:17
.= 0. L by VECTSP_1:7
.= eval ((NF p),x) by H2, ev0 ; ::_thesis: verum
end;
suppose not p is zero ; ::_thesis: eval ((NF p),x) = eval (p,x)
then consider z1 being rational_function of L, z2 being non zero Polynomial of L such that
H: ( p = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & NF p = NormRatF z1 & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of p `1 ,p `2 & f . i = rpoly (1,x) ) ) ) ) by defNF;
H1: p `1 = z2 *' (z1 `1) by H, XTUPLE_0:def_2;
H2: p `2 = z2 *' (z1 `2) by H, XTUPLE_0:def_3;
H3: now__::_thesis:_not_eval_(z2,x)_=_0._L
assume A: eval (z2,x) = 0. L ; ::_thesis: contradiction
eval ((z2 *' (z1 `1)),x) = (eval (z2,x)) * (eval ((z1 `1),x)) by POLYNOM4:24
.= 0. L by A, VECTSP_1:7 ;
then B: x is_a_root_of p `1 by H1, POLYNOM5:def_6;
eval ((z2 *' (z1 `2)),x) = (eval (z2,x)) * (eval ((z1 `2),x)) by POLYNOM4:24
.= 0. L by A, VECTSP_1:7 ;
then x is_a_root_of p `2 by H2, POLYNOM5:def_6;
hence contradiction by AS, B, root1; ::_thesis: verum
end;
H6: now__::_thesis:_not_eval_((z1_`2),x)_=_0._L
assume eval ((z1 `2),x) = 0. L ; ::_thesis: contradiction
then 0. L = (eval (z2,x)) * (eval ((z1 `2),x)) by VECTSP_1:7
.= eval ((z2 *' (z1 `2)),x) by POLYNOM4:24 ;
hence contradiction by H, XTUPLE_0:def_3, AS1; ::_thesis: verum
end;
eval (p,x) = (eval ((z2 *' (z1 `1)),x)) * ((eval ((z2 *' (z1 `2)),x)) ") by H, XTUPLE_0:def_3, H1
.= ((eval (z2,x)) * (eval ((z1 `1),x))) * ((eval ((z2 *' (z1 `2)),x)) ") by POLYNOM4:24
.= ((eval (z2,x)) * (eval ((z1 `1),x))) * (((eval (z2,x)) * (eval ((z1 `2),x))) ") by POLYNOM4:24
.= ((eval (z2,x)) * (eval ((z1 `1),x))) * (((eval ((z1 `2),x)) ") * ((eval (z2,x)) ")) by H3, H6, VECTSP_2:11
.= (eval (z2,x)) * ((eval ((z1 `1),x)) * (((eval ((z1 `2),x)) ") * ((eval (z2,x)) "))) by GROUP_1:def_3
.= (eval (z2,x)) * (((eval ((z1 `1),x)) * ((eval ((z1 `2),x)) ")) * ((eval (z2,x)) ")) by GROUP_1:def_3
.= ((eval (z2,x)) * ((eval (z2,x)) ")) * ((eval ((z1 `1),x)) * ((eval ((z1 `2),x)) ")) by GROUP_1:def_3
.= (1. L) * ((eval ((z1 `1),x)) * ((eval ((z1 `2),x)) ")) by H3, VECTSP_1:def_10
.= eval (z1,x) by VECTSP_1:def_8 ;
hence eval ((NF p),x) = eval (p,x) by H, H6, ev4; ::_thesis: verum
end;
end;
end;