:: UPROOTS semantic presentation
begin
theorem Th1: :: UPROOTS:1
for f being FinSequence of NAT st ( for i being Element of NAT st i in dom f holds
f . i <> 0 ) holds
( Sum f = len f iff f = (len f) |-> 1 )
proof
defpred S1[ Element of NAT ] means for f being FinSequence of NAT st len f = $1 & ( for i being Element of NAT st i in dom f holds
f . i <> 0 ) holds
( Sum f = len f iff f = (len f) |-> 1 );
let f be FinSequence of NAT ; ::_thesis: ( ( for i being Element of NAT st i in dom f holds
f . i <> 0 ) implies ( Sum f = len f iff f = (len f) |-> 1 ) )
A1: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
let f be FinSequence of NAT ; ::_thesis: ( len f = n + 1 & ( for i being Element of NAT st i in dom f holds
f . i <> 0 ) implies ( Sum f = len f iff f = (len f) |-> 1 ) )
assume that
A3: len f = n + 1 and
A4: for i being Element of NAT st i in dom f holds
f . i <> 0 ; ::_thesis: ( Sum f = len f iff f = (len f) |-> 1 )
consider g being FinSequence of NAT , a being Element of NAT such that
A5: f = g ^ <*a*> by A3, FINSEQ_2:19;
A6: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_g_holds_
g_._i_<>_0
let i be Element of NAT ; ::_thesis: ( i in dom g implies g . i <> 0 )
A7: dom g c= dom f by A5, FINSEQ_1:26;
assume A8: i in dom g ; ::_thesis: g . i <> 0
then f . i = g . i by A5, FINSEQ_1:def_7;
hence g . i <> 0 by A4, A8, A7; ::_thesis: verum
end;
n + 1 = (len g) + (len <*a*>) by A3, A5, FINSEQ_1:22;
then A9: n + 1 = (len g) + 1 by FINSEQ_1:40;
then ( dom f = Seg (len f) & f . (len f) = a ) by A3, A5, FINSEQ_1:42, FINSEQ_1:def_3;
then a <> 0 by A3, A4, FINSEQ_1:4;
then A10: 0 + 1 <= a by NAT_1:13;
A11: g is FinSequence of REAL by FINSEQ_2:24;
hereby ::_thesis: ( f = (len f) |-> 1 implies Sum f = len f )
reconsider h = (len g) |-> 1 as FinSequence of REAL ;
reconsider h1 = h as Element of (len h) -tuples_on REAL by FINSEQ_2:92;
reconsider g1 = g as Element of (len g) -tuples_on REAL by A11, FINSEQ_2:92;
assume A12: Sum f = len f ; ::_thesis: f = (len f) |-> 1
A13: Sum g = ((Sum g) + a) - a
.= (n + 1) - a by A3, A5, A12, RVSUM_1:74 ;
A14: now__::_thesis:_for_j_being_Nat_st_j_in_Seg_(len_g)_holds_
h1_._j_<=_g1_._j
let j be Nat; ::_thesis: ( j in Seg (len g) implies h1 . j <= g1 . j )
reconsider a = j as Element of NAT by ORDINAL1:def_12;
assume A15: j in Seg (len g) ; ::_thesis: h1 . j <= g1 . j
then j in dom g by FINSEQ_1:def_3;
then g . j <> 0 by A6;
then 0 + 1 <= g . a by NAT_1:13;
hence h1 . j <= g1 . j by A15, FUNCOP_1:7; ::_thesis: verum
end;
A16: Sum h1 <= Sum g1 by A14, RVSUM_1:82;
Sum h = n * 1 by A9, RVSUM_1:80
.= n ;
then n + a <= ((n + 1) - a) + a by A16, A13, XREAL_1:6;
then a <= 1 by XREAL_1:6;
then A17: a = 1 by A10, XXREAL_0:1;
then g = (len g) |-> 1 by A2, A9, A6, A13;
hence f = (len f) |-> 1 by A3, A5, A9, A17, FINSEQ_2:60; ::_thesis: verum
end;
assume f = (len f) |-> 1 ; ::_thesis: Sum f = len f
then A18: f = (n |-> 1) ^ (1 |-> 1) by A3, FINSEQ_2:123
.= (n |-> 1) ^ <*1*> by FINSEQ_2:59 ;
then A19: a = 1 by A5, FINSEQ_2:17;
A20: Sum f = (Sum g) + a by A5, RVSUM_1:74;
g = (len g) |-> 1 by A5, A9, A18, FINSEQ_2:17;
hence Sum f = len f by A2, A3, A9, A6, A20, A19; ::_thesis: verum
end;
A21: S1[ 0 ]
proof
let f be FinSequence of NAT ; ::_thesis: ( len f = 0 & ( for i being Element of NAT st i in dom f holds
f . i <> 0 ) implies ( Sum f = len f iff f = (len f) |-> 1 ) )
assume that
A22: len f = 0 and
for i being Element of NAT st i in dom f holds
f . i <> 0 ; ::_thesis: ( Sum f = len f iff f = (len f) |-> 1 )
hereby ::_thesis: ( f = (len f) |-> 1 implies Sum f = len f )
assume Sum f = len f ; ::_thesis: f = (len f) |-> 1
thus f = {} by A22
.= (len f) |-> 1 by A22 ; ::_thesis: verum
end;
assume f = (len f) |-> 1 ; ::_thesis: Sum f = len f
f = {} by A22;
hence Sum f = len f by RVSUM_1:72; ::_thesis: verum
end;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A21, A1);
hence ( ( for i being Element of NAT st i in dom f holds
f . i <> 0 ) implies ( Sum f = len f iff f = (len f) |-> 1 ) ) ; ::_thesis: verum
end;
scheme :: UPROOTS:sch 1
IndFinSeq0{ F1() -> Nat, P1[ set ] } :
for i being Element of NAT st 1 <= i & i <= F1() holds
P1[i]
provided
A1: P1[1] and
A2: for i being Element of NAT st 1 <= i & i < F1() & P1[i] holds
P1[i + 1]
proof
defpred S1[ Nat] means ( 1 <= $1 & $1 <= F1() & P1[$1] );
assume ex i being Element of NAT st
( 1 <= i & i <= F1() & P1[i] ) ; ::_thesis: contradiction
then A3: ex k being Nat st S1[k] ;
consider k being Nat such that
A4: ( S1[k] & ( for k9 being Nat st S1[k9] holds
k <= k9 ) ) from NAT_1:sch_5(A3);
percases ( k = 1 or k <> 1 ) ;
suppose k = 1 ; ::_thesis: contradiction
hence contradiction by A1, A4; ::_thesis: verum
end;
supposeA5: k <> 1 ; ::_thesis: contradiction
1 - 1 <= k - 1 by A4, XREAL_1:9;
then reconsider k9 = k - 1 as Element of NAT by INT_1:3;
A6: (k - 1) + 1 = k + 0 ;
1 < k by A4, A5, XXREAL_0:1;
then A7: 1 <= k9 by A6, NAT_1:13;
( k9 <= k9 + 1 & k9 <> k9 + 1 ) by NAT_1:11;
then A8: k9 < k by XXREAL_0:1;
then k9 < F1() by A4, XXREAL_0:2;
hence contradiction by A2, A4, A6, A8, A7; ::_thesis: verum
end;
end;
end;
theorem Th2: :: UPROOTS:2
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for r being FinSequence of L st len r >= 2 & ( for k being Element of NAT st 2 < k & k in dom r holds
r . k = 0. L ) holds
Sum r = (r /. 1) + (r /. 2)
proof
let L be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for r being FinSequence of L st len r >= 2 & ( for k being Element of NAT st 2 < k & k in dom r holds
r . k = 0. L ) holds
Sum r = (r /. 1) + (r /. 2)
let r be FinSequence of L; ::_thesis: ( len r >= 2 & ( for k being Element of NAT st 2 < k & k in dom r holds
r . k = 0. L ) implies Sum r = (r /. 1) + (r /. 2) )
assume that
A1: len r >= 2 and
A2: for k being Element of NAT st 2 < k & k in dom r holds
r . k = 0. L ; ::_thesis: Sum r = (r /. 1) + (r /. 2)
A3: 2 in dom r by A1, FINSEQ_3:25;
1 <= len r by A1, XXREAL_0:2;
then A4: 1 in dom r by FINSEQ_3:25;
not r is empty by A1;
then consider a being Element of L, r1 being FinSequence of L such that
A5: a = r . 1 and
A6: r = <*a*> ^ r1 by FINSEQ_3:102;
A7: len <*a*> = 1 by FINSEQ_1:40;
then A8: r . 2 = r1 . (2 - 1) by A1, A6, FINSEQ_1:24
.= r1 . 1 ;
A9: len r = 1 + (len r1) by A6, A7, FINSEQ_1:22;
now__::_thesis:_not_r1_is_empty
assume r1 is empty ; ::_thesis: contradiction
then len r1 = 0 ;
hence contradiction by A1, A9; ::_thesis: verum
end;
then consider b being Element of L, r2 being FinSequence of L such that
A10: b = r1 . 1 and
A11: r1 = <*b*> ^ r2 by FINSEQ_3:102;
A12: len <*b*> = 1 by FINSEQ_1:40;
A13: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_r2_holds_
r2_._i_=_0._L
let i be Element of NAT ; ::_thesis: ( i in dom r2 implies r2 . i = 0. L )
assume A14: i in dom r2 ; ::_thesis: r2 . i = 0. L
A15: 1 + i in dom r1 by A11, A12, A14, FINSEQ_1:28;
1 <= i by A14, FINSEQ_3:25;
then 1 < 1 + i by NAT_1:13;
then A16: 1 + 1 < 1 + (1 + i) by XREAL_1:8;
thus r2 . i = r1 . (1 + i) by A11, A12, A14, FINSEQ_1:def_7
.= r . (1 + (1 + i)) by A6, A7, A15, FINSEQ_1:def_7
.= 0. L by A2, A6, A7, A15, A16, FINSEQ_1:28 ; ::_thesis: verum
end;
thus Sum r = a + (Sum r1) by A6, FVSUM_1:72
.= a + (b + (Sum r2)) by A11, FVSUM_1:72
.= a + (b + (0. L)) by A13, POLYNOM3:1
.= a + b by RLVECT_1:def_4
.= (r /. 1) + b by A5, A4, PARTFUN1:def_6
.= (r /. 1) + (r /. 2) by A10, A3, A8, PARTFUN1:def_6 ; ::_thesis: verum
end;
begin
registration
let A be finite set ;
cluster Relation-like NAT -defined A -valued Function-like one-to-one onto finite FinSequence-like FinSubsequence-like finite-support for FinSequence of A;
existence
ex b1 being FinSequence of A st
( b1 is one-to-one & b1 is onto )
proof
defpred S1[ Element of NAT , set , set ] means c3 = [(choose (c2 `2)),((c2 `2) \ {(choose (c2 `2))})];
set cA = card A;
A1: for n being Element of NAT st 1 <= n & n < card A holds
for x being set ex y being set st S1[n,x,y] ;
consider f being FinSequence such that
A2: len f = card A and
A3: ( f . 1 = [(choose A),(A \ {(choose A)})] or card A = 0 ) and
A4: for n being Element of NAT st 1 <= n & n < card A holds
S1[n,f . n,f . (n + 1)] from RECDEF_1:sch_3(A1);
defpred S2[ Element of NAT ] means ( A in dom f implies ( f . A in [:A,(bool A):] & ex X being finite set st
( X = (f . A) `2 & (card X) + A = card A ) ) );
A5: for i being Element of NAT st 1 <= i & i < len f & S2[i] holds
S2[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len f & S2[i] implies S2[i + 1] )
assume that
A6: 1 <= i and
A7: i < len f and
A8: S2[i] and
i + 1 in dom f ; ::_thesis: ( f . (i + 1) in [:A,(bool A):] & ex X being finite set st
( X = (f . (i + 1)) `2 & (card X) + (i + 1) = card A ) )
A9: f . (i + 1) = [(choose ((f . i) `2)),(((f . i) `2) \ {(choose ((f . i) `2))})] by A2, A4, A6, A7;
consider a, ba being set such that
a in A and
A10: ba in bool A and
A11: f . i = [a,ba] by A6, A7, A8, FINSEQ_3:25, ZFMISC_1:def_2;
A12: (f . i) `2 = ba by A11, MCART_1:7;
then A13: ((f . i) `2) \ {(choose ((f . i) `2))} c= A by A10, XBOOLE_1:1;
A14: now__::_thesis:_not_choose_((f_._i)_`2)_in_((f_._i)_`2)_\_{(choose_((f_._i)_`2))}
assume choose ((f . i) `2) in ((f . i) `2) \ {(choose ((f . i) `2))} ; ::_thesis: contradiction
then not choose ((f . i) `2) in {(choose ((f . i) `2))} by XBOOLE_0:def_5;
hence contradiction by TARSKI:def_1; ::_thesis: verum
end;
consider X being finite set such that
A15: X = (f . i) `2 and
A16: (card X) + i = card A by A6, A7, A8, FINSEQ_3:25;
A17: X <> {} by A2, A7, A16, CARD_1:27;
then choose ((f . i) `2) in (f . i) `2 by A15;
hence f . (i + 1) in [:A,(bool A):] by A10, A9, A12, A13, ZFMISC_1:def_2; ::_thesis: ex X being finite set st
( X = (f . (i + 1)) `2 & (card X) + (i + 1) = card A )
reconsider XX = ((f . i) `2) \ {(choose ((f . i) `2))} as finite set by A15;
take XX ; ::_thesis: ( XX = (f . (i + 1)) `2 & (card XX) + (i + 1) = card A )
thus XX = (f . (i + 1)) `2 by A9, MCART_1:7; ::_thesis: (card XX) + (i + 1) = card A
{(choose ((f . i) `2))} c= (f . i) `2 by A15, A17, ZFMISC_1:31;
then (f . i) `2 = {(choose ((f . i) `2))} \/ (((f . i) `2) \ {(choose ((f . i) `2))}) by XBOOLE_1:45;
then card X = (card XX) + 1 by A15, A14, CARD_2:41;
hence (card XX) + (i + 1) = card A by A16; ::_thesis: verum
end;
A18: S2[1]
proof
reconsider X = A \ {(choose A)} as finite set ;
A19: now__::_thesis:_not_choose_A_in_A_\_{(choose_A)}
assume choose A in A \ {(choose A)} ; ::_thesis: contradiction
then not choose A in {(choose A)} by XBOOLE_0:def_5;
hence contradiction by TARSKI:def_1; ::_thesis: verum
end;
assume A20: 1 in dom f ; ::_thesis: ( f . 1 in [:A,(bool A):] & ex X being finite set st
( X = (f . 1) `2 & (card X) + 1 = card A ) )
then A <> {} by A2, FINSEQ_3:25;
hence f . 1 in [:A,(bool A):] by A3, ZFMISC_1:def_2; ::_thesis: ex X being finite set st
( X = (f . 1) `2 & (card X) + 1 = card A )
take X ; ::_thesis: ( X = (f . 1) `2 & (card X) + 1 = card A )
thus X = (f . 1) `2 by A2, A3, A20, FINSEQ_3:25, MCART_1:7; ::_thesis: (card X) + 1 = card A
0 + 1 <= len f by A20, FINSEQ_3:25;
then {(choose A)} c= A by A2, CARD_1:27, ZFMISC_1:31;
then A = {(choose A)} \/ (A \ {(choose A)}) by XBOOLE_1:45;
hence (card X) + 1 = card A by A19, CARD_2:41; ::_thesis: verum
end;
A21: for i being Element of NAT st 1 <= i & i <= len f holds
S2[i] from UPROOTS:sch_1(A18, A5);
rng f c= [:A,(bool A):]
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in [:A,(bool A):] )
assume y in rng f ; ::_thesis: y in [:A,(bool A):]
then consider i being Nat such that
A22: i in dom f and
A23: y = f . i by FINSEQ_2:10;
( 1 <= i & i <= len f ) by A22, FINSEQ_3:25;
hence y in [:A,(bool A):] by A21, A22, A23; ::_thesis: verum
end;
then reconsider f = f as FinSequence of [:A,(bool A):] by FINSEQ_1:def_4;
deffunc H1( Nat) -> set = (f . A) `1 ;
consider p being FinSequence such that
A24: len p = card A and
A25: for k being Nat st k in dom p holds
p . k = H1(k) from FINSEQ_1:sch_2();
A26: dom p = dom f by A2, A24, FINSEQ_3:29;
rng p c= A
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng p or y in A )
assume y in rng p ; ::_thesis: y in A
then consider i being Nat such that
A27: i in dom p and
A28: p . i = y by FINSEQ_2:10;
( p . i = (f . i) `1 & f . i in [:A,(bool A):] ) by A25, A26, A27, FINSEQ_2:11;
hence y in A by A28, MCART_1:10; ::_thesis: verum
end;
then reconsider p = p as FinSequence of A by FINSEQ_1:def_4;
A29: rng p = A
proof
set F = p;
percases ( A = {} or A <> {} ) ;
suppose A = {} ; ::_thesis: rng p = A
hence rng p = A ; ::_thesis: verum
end;
supposeA30: A <> {} ; ::_thesis: rng p = A
defpred S3[ Element of NAT ] means ( (rng (p | (Seg A))) \/ ((f . A) `2) = A & ex X being finite set st
( X = (f . A) `2 & (card X) + A = card A ) );
A31: for i being Element of NAT st 1 <= i & i < len f & S3[i] holds
S3[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len f & S3[i] implies S3[i + 1] )
assume that
A32: 1 <= i and
A33: i < len f and
A34: S3[i] ; ::_thesis: S3[i + 1]
A35: f . (i + 1) = [(choose ((f . i) `2)),(((f . i) `2) \ {(choose ((f . i) `2))})] by A2, A4, A32, A33;
consider X being finite set such that
A36: X = (f . i) `2 and
A37: (card X) + i = card A by A34;
reconsider XX = ((f . i) `2) \ {(choose ((f . i) `2))} as finite set by A36;
not (f . i) `2 is empty by A2, A33, A36, A37, CARD_1:27;
then {(choose ((f . i) `2))} c= (f . i) `2 by ZFMISC_1:31;
then A38: (f . i) `2 = {(choose ((f . i) `2))} \/ (((f . i) `2) \ {(choose ((f . i) `2))}) by XBOOLE_1:45;
reconsider Fi = p | (Seg i), Fi1 = p | (Seg (i + 1)) as FinSequence of A by FINSEQ_1:18;
A39: i + 1 <= len p by A2, A24, A33, NAT_1:13;
then consider a being Element of A such that
A40: Fi1 = Fi ^ <*a*> by A30, TREES_9:33;
1 <= i + 1 by NAT_1:12;
then A41: i + 1 in dom p by A39, FINSEQ_3:25;
A42: rng Fi1 = (rng Fi) \/ (rng <*a*>) by A40, FINSEQ_1:31
.= (rng Fi) \/ {a} by FINSEQ_1:39 ;
( p . (i + 1) = Fi1 . (i + 1) & i = len Fi ) by A2, A24, A33, FINSEQ_1:4, FINSEQ_1:17, FUNCT_1:49;
then A43: a = p . (i + 1) by A40, FINSEQ_1:42
.= (f . (i + 1)) `1 by A25, A41
.= choose ((f . i) `2) by A35, MCART_1:7 ;
then (f . (i + 1)) `2 = ((f . i) `2) \ {a} by A35, MCART_1:7;
hence (rng (p | (Seg (i + 1)))) \/ ((f . (i + 1)) `2) = A by A34, A38, A42, A43, XBOOLE_1:4; ::_thesis: ex X being finite set st
( X = (f . (i + 1)) `2 & (card X) + (i + 1) = card A )
take XX ; ::_thesis: ( XX = (f . (i + 1)) `2 & (card XX) + (i + 1) = card A )
thus XX = (f . (i + 1)) `2 by A35, MCART_1:7; ::_thesis: (card XX) + (i + 1) = card A
now__::_thesis:_not_choose_((f_._i)_`2)_in_((f_._i)_`2)_\_{(choose_((f_._i)_`2))}
assume choose ((f . i) `2) in ((f . i) `2) \ {(choose ((f . i) `2))} ; ::_thesis: contradiction
then not choose ((f . i) `2) in {(choose ((f . i) `2))} by XBOOLE_0:def_5;
hence contradiction by TARSKI:def_1; ::_thesis: verum
end;
then card X = (card XX) + 1 by A36, A38, CARD_2:41;
hence (card XX) + (i + 1) = card A by A37; ::_thesis: verum
end;
A44: 0 + 1 <= len p by A24, A30, NAT_1:13;
then A45: 1 in dom p by FINSEQ_3:25;
A46: S3[1]
proof
reconsider X = A \ {(choose A)} as finite set ;
reconsider F1 = p | (Seg 1) as FinSequence of A by FINSEQ_1:18;
A47: now__::_thesis:_not_choose_A_in_A_\_{(choose_A)}
assume choose A in A \ {(choose A)} ; ::_thesis: contradiction
then not choose A in {(choose A)} by XBOOLE_0:def_5;
hence contradiction by TARSKI:def_1; ::_thesis: verum
end;
1 in Seg (0 + 1) by FINSEQ_1:4;
then A48: F1 . 1 = p . 1 by FUNCT_1:49
.= (f . 1) `1 by A25, A45
.= choose A by A3, A30, MCART_1:7 ;
ex a being Element of A st F1 = <*a*> by A30, A44, TREES_9:34;
then p | (Seg 1) = <*(choose A)*> by A48, FINSEQ_1:40;
then A49: rng (p | (Seg 1)) = {(choose A)} by FINSEQ_1:39;
(f . 1) `2 = A \ {(choose A)} by A3, A30, MCART_1:7;
hence (rng (p | (Seg 1))) \/ ((f . 1) `2) = A by A49, XBOOLE_1:45; ::_thesis: ex X being finite set st
( X = (f . 1) `2 & (card X) + 1 = card A )
take X ; ::_thesis: ( X = (f . 1) `2 & (card X) + 1 = card A )
thus X = (f . 1) `2 by A3, A30, MCART_1:7; ::_thesis: (card X) + 1 = card A
{(choose A)} c= A by A30, ZFMISC_1:31;
then A = {(choose A)} \/ (A \ {(choose A)}) by XBOOLE_1:45;
hence (card X) + 1 = card A by A47, CARD_2:41; ::_thesis: verum
end;
A50: for i being Element of NAT st 1 <= i & i <= len f holds
S3[i] from UPROOTS:sch_1(A46, A31);
A51: len p >= 1 by A24, A30, NAT_1:14;
then consider X being finite set such that
A52: X = (f . (len p)) `2 and
A53: (card X) + (len f) = card A by A2, A24, A50;
p = p | (Seg (len p)) by FINSEQ_3:49;
then A54: (rng p) \/ ((f . (len p)) `2) = A by A2, A24, A50, A51;
X = {} by A2, A53;
hence rng p = A by A54, A52; ::_thesis: verum
end;
end;
end;
then A55: p is onto by FUNCT_2:def_3;
take p ; ::_thesis: ( p is one-to-one & p is onto )
p is one-to-one by A24, A29, FINSEQ_4:62;
hence ( p is one-to-one & p is onto ) by A55; ::_thesis: verum
end;
end;
definition
let A be finite set ;
func canFS A -> FinSequence of A equals :: UPROOTS:def 1
the one-to-one onto FinSequence of A;
coherence
the one-to-one onto FinSequence of A is FinSequence of A ;
end;
:: deftheorem defines canFS UPROOTS:def_1_:_
for A being finite set holds canFS A = the one-to-one onto FinSequence of A;
registration
let A be finite set ;
cluster canFS A -> one-to-one onto ;
coherence
( canFS A is one-to-one & canFS A is onto ) ;
end;
theorem Th3: :: UPROOTS:3
for A being finite set holds len (canFS A) = card A
proof
let A be finite set ; ::_thesis: len (canFS A) = card A
rng (canFS A) = A by FUNCT_2:def_3;
hence len (canFS A) = card A by FINSEQ_4:62; ::_thesis: verum
end;
registration
let A be non empty finite set ;
cluster canFS A -> non empty ;
coherence
not canFS A is empty
proof
len (canFS A) = card A by Th3;
hence not canFS A is empty ; ::_thesis: verum
end;
end;
theorem Th4: :: UPROOTS:4
for a being set holds canFS {a} = <*a*>
proof
let a be set ; ::_thesis: canFS {a} = <*a*>
A1: rng (canFS {a}) = {a} by FUNCT_2:def_3;
len (canFS {a}) = card {a} by Th3
.= 1 by CARD_1:30 ;
hence canFS {a} = <*a*> by A1, FINSEQ_1:39; ::_thesis: verum
end;
theorem Th5: :: UPROOTS:5
for A being finite set holds (canFS A) " is Function of A,(Seg (card A))
proof
let A be finite set ; ::_thesis: (canFS A) " is Function of A,(Seg (card A))
len (canFS A) = card A by Th3;
then dom (canFS A) = Seg (card A) by FINSEQ_1:def_3;
then A1: rng ((canFS A) ") = Seg (card A) by FUNCT_1:33;
rng (canFS A) = A by FUNCT_2:def_3;
then dom ((canFS A) ") = A by FUNCT_1:33;
hence (canFS A) " is Function of A,(Seg (card A)) by A1, FUNCT_2:1; ::_thesis: verum
end;
begin
definition
let X be set ;
let S be finite Subset of X;
let n be Element of NAT ;
func(S,n) -bag -> Element of Bags X equals :: UPROOTS:def 2
(EmptyBag X) +* (S --> n);
correctness
coherence
(EmptyBag X) +* (S --> n) is Element of Bags X;
proof
set b = (EmptyBag X) +* (S --> n);
A1: EmptyBag X = X --> 0 by PRE_POLY:def_13;
A2: dom (S --> n) = S by FUNCOP_1:13;
A3: now__::_thesis:_for_i_being_set_st_not_i_in_S_holds_
((EmptyBag_X)_+*_(S_-->_n))_._i_=_0
let i be set ; ::_thesis: ( not i in S implies ((EmptyBag X) +* (S --> n)) . i = 0 )
assume not i in S ; ::_thesis: ((EmptyBag X) +* (S --> n)) . i = 0
hence ((EmptyBag X) +* (S --> n)) . i = (EmptyBag X) . i by A2, FUNCT_4:11
.= 0 by PRE_POLY:52 ;
::_thesis: verum
end;
A4: now__::_thesis:_for_i_being_set_st_i_in_S_holds_
((EmptyBag_X)_+*_(S_-->_n))_._i_=_n
let i be set ; ::_thesis: ( i in S implies ((EmptyBag X) +* (S --> n)) . i = n )
assume A5: i in S ; ::_thesis: ((EmptyBag X) +* (S --> n)) . i = n
thus ((EmptyBag X) +* (S --> n)) . i = (S --> n) . i by A2, A5, FUNCT_4:13
.= n by A5, FUNCOP_1:7 ; ::_thesis: verum
end;
A6: support ((EmptyBag X) +* (S --> n)) is finite
proof
percases ( S is empty or ( not S is empty & n = 0 ) or ( not S is empty & n <> 0 ) ) ;
supposeA7: S is empty ; ::_thesis: support ((EmptyBag X) +* (S --> n)) is finite
now__::_thesis:_support_((EmptyBag_X)_+*_(S_-->_n))_is_empty
assume not support ((EmptyBag X) +* (S --> n)) is empty ; ::_thesis: contradiction
then consider x being set such that
A8: x in support ((EmptyBag X) +* (S --> n)) by XBOOLE_0:def_1;
((EmptyBag X) +* (S --> n)) . x <> 0 by A8, PRE_POLY:def_7;
hence contradiction by A3, A7; ::_thesis: verum
end;
hence support ((EmptyBag X) +* (S --> n)) is finite ; ::_thesis: verum
end;
supposeA9: ( not S is empty & n = 0 ) ; ::_thesis: support ((EmptyBag X) +* (S --> n)) is finite
now__::_thesis:_support_((EmptyBag_X)_+*_(S_-->_n))_is_empty
assume not support ((EmptyBag X) +* (S --> n)) is empty ; ::_thesis: contradiction
then consider x being set such that
A10: x in support ((EmptyBag X) +* (S --> n)) by XBOOLE_0:def_1;
A11: ((EmptyBag X) +* (S --> n)) . x <> 0 by A10, PRE_POLY:def_7;
then ((EmptyBag X) +* (S --> n)) . x = (S --> n) . x by A2, A3, FUNCT_4:13
.= 0 by A3, A9, A11, FUNCOP_1:7 ;
hence contradiction by A10, PRE_POLY:def_7; ::_thesis: verum
end;
hence support ((EmptyBag X) +* (S --> n)) is finite ; ::_thesis: verum
end;
suppose ( not S is empty & n <> 0 ) ; ::_thesis: support ((EmptyBag X) +* (S --> n)) is finite
then for x being set holds
( x in S iff ((EmptyBag X) +* (S --> n)) . x <> 0 ) by A3, A4;
hence support ((EmptyBag X) +* (S --> n)) is finite by PRE_POLY:def_7; ::_thesis: verum
end;
end;
end;
dom ((EmptyBag X) +* (S --> n)) = (dom (EmptyBag X)) \/ (dom (S --> n)) by FUNCT_4:def_1
.= X \/ (dom (S --> n)) by A1, FUNCOP_1:13
.= X \/ S by FUNCOP_1:13
.= X by XBOOLE_1:12 ;
then (EmptyBag X) +* (S --> n) is bag of X by A6, PARTFUN1:def_2, PRE_POLY:def_8, RELAT_1:def_18;
hence (EmptyBag X) +* (S --> n) is Element of Bags X by PRE_POLY:def_12; ::_thesis: verum
end;
end;
:: deftheorem defines -bag UPROOTS:def_2_:_
for X being set
for S being finite Subset of X
for n being Element of NAT holds (S,n) -bag = (EmptyBag X) +* (S --> n);
theorem Th6: :: UPROOTS:6
for X being set
for S being finite Subset of X
for n being Element of NAT
for i being set st not i in S holds
((S,n) -bag) . i = 0
proof
let X be set ; ::_thesis: for S being finite Subset of X
for n being Element of NAT
for i being set st not i in S holds
((S,n) -bag) . i = 0
let S be finite Subset of X; ::_thesis: for n being Element of NAT
for i being set st not i in S holds
((S,n) -bag) . i = 0
let n be Element of NAT ; ::_thesis: for i being set st not i in S holds
((S,n) -bag) . i = 0
let i be set ; ::_thesis: ( not i in S implies ((S,n) -bag) . i = 0 )
assume A1: not i in S ; ::_thesis: ((S,n) -bag) . i = 0
dom (S --> n) = S by FUNCOP_1:13;
hence ((S,n) -bag) . i = (EmptyBag X) . i by A1, FUNCT_4:11
.= 0 by PRE_POLY:52 ;
::_thesis: verum
end;
theorem Th7: :: UPROOTS:7
for X being set
for S being finite Subset of X
for n being Element of NAT
for i being set st i in S holds
((S,n) -bag) . i = n
proof
let X be set ; ::_thesis: for S being finite Subset of X
for n being Element of NAT
for i being set st i in S holds
((S,n) -bag) . i = n
let S be finite Subset of X; ::_thesis: for n being Element of NAT
for i being set st i in S holds
((S,n) -bag) . i = n
let n be Element of NAT ; ::_thesis: for i being set st i in S holds
((S,n) -bag) . i = n
let i be set ; ::_thesis: ( i in S implies ((S,n) -bag) . i = n )
assume A1: i in S ; ::_thesis: ((S,n) -bag) . i = n
dom (S --> n) = S by FUNCOP_1:13;
hence ((S,n) -bag) . i = (S --> n) . i by A1, FUNCT_4:13
.= n by A1, FUNCOP_1:7 ;
::_thesis: verum
end;
theorem Th8: :: UPROOTS:8
for X being set
for S being finite Subset of X
for n being Element of NAT st n <> 0 holds
support ((S,n) -bag) = S
proof
let X be set ; ::_thesis: for S being finite Subset of X
for n being Element of NAT st n <> 0 holds
support ((S,n) -bag) = S
let S be finite Subset of X; ::_thesis: for n being Element of NAT st n <> 0 holds
support ((S,n) -bag) = S
let n be Element of NAT ; ::_thesis: ( n <> 0 implies support ((S,n) -bag) = S )
assume n <> 0 ; ::_thesis: support ((S,n) -bag) = S
then for x being set holds
( x in S iff ((S,n) -bag) . x <> 0 ) by Th6, Th7;
hence support ((S,n) -bag) = S by PRE_POLY:def_7; ::_thesis: verum
end;
theorem :: UPROOTS:9
for X being set
for S being finite Subset of X
for n being Element of NAT st ( S is empty or n = 0 ) holds
(S,n) -bag = EmptyBag X
proof
let X be set ; ::_thesis: for S being finite Subset of X
for n being Element of NAT st ( S is empty or n = 0 ) holds
(S,n) -bag = EmptyBag X
let S be finite Subset of X; ::_thesis: for n being Element of NAT st ( S is empty or n = 0 ) holds
(S,n) -bag = EmptyBag X
let n be Element of NAT ; ::_thesis: ( ( S is empty or n = 0 ) implies (S,n) -bag = EmptyBag X )
assume A1: ( S is empty or n = 0 ) ; ::_thesis: (S,n) -bag = EmptyBag X
now__::_thesis:_for_i_being_set_st_i_in_X_holds_
((S,n)_-bag)_._i_=_(EmptyBag_X)_._i
let i be set ; ::_thesis: ( i in X implies ((S,n) -bag) . b1 = (EmptyBag X) . b1 )
assume i in X ; ::_thesis: ((S,n) -bag) . b1 = (EmptyBag X) . b1
percases ( i in S or not i in S ) ;
suppose i in S ; ::_thesis: ((S,n) -bag) . b1 = (EmptyBag X) . b1
hence ((S,n) -bag) . i = 0 by A1, Th7
.= (EmptyBag X) . i by PRE_POLY:52 ;
::_thesis: verum
end;
suppose not i in S ; ::_thesis: ((S,n) -bag) . b1 = (EmptyBag X) . b1
hence ((S,n) -bag) . i = 0 by Th6
.= (EmptyBag X) . i by PRE_POLY:52 ;
::_thesis: verum
end;
end;
end;
hence (S,n) -bag = EmptyBag X by PBOOLE:3; ::_thesis: verum
end;
theorem Th10: :: UPROOTS:10
for X being set
for S, T being finite Subset of X
for n being Element of NAT st S misses T holds
((S \/ T),n) -bag = ((S,n) -bag) + ((T,n) -bag)
proof
let X be set ; ::_thesis: for S, T being finite Subset of X
for n being Element of NAT st S misses T holds
((S \/ T),n) -bag = ((S,n) -bag) + ((T,n) -bag)
let S, T be finite Subset of X; ::_thesis: for n being Element of NAT st S misses T holds
((S \/ T),n) -bag = ((S,n) -bag) + ((T,n) -bag)
let n be Element of NAT ; ::_thesis: ( S misses T implies ((S \/ T),n) -bag = ((S,n) -bag) + ((T,n) -bag) )
assume S misses T ; ::_thesis: ((S \/ T),n) -bag = ((S,n) -bag) + ((T,n) -bag)
then A1: S /\ T = {} by XBOOLE_0:def_7;
now__::_thesis:_for_i_being_set_st_i_in_X_holds_
(((S_\/_T),n)_-bag)_._i_=_(((S,n)_-bag)_+_((T,n)_-bag))_._i
let i be set ; ::_thesis: ( i in X implies (((S \/ T),n) -bag) . b1 = (((S,n) -bag) + ((T,n) -bag)) . b1 )
assume i in X ; ::_thesis: (((S \/ T),n) -bag) . b1 = (((S,n) -bag) + ((T,n) -bag)) . b1
percases ( not i in S \/ T or i in S or i in T ) by XBOOLE_0:def_3;
supposeA2: not i in S \/ T ; ::_thesis: (((S \/ T),n) -bag) . b1 = (((S,n) -bag) + ((T,n) -bag)) . b1
then A3: not i in T by XBOOLE_0:def_3;
A4: not i in S by A2, XBOOLE_0:def_3;
thus (((S \/ T),n) -bag) . i = 0 by A2, Th6
.= (((S,n) -bag) . i) + 0 by A4, Th6
.= (((S,n) -bag) . i) + (((T,n) -bag) . i) by A3, Th6
.= (((S,n) -bag) + ((T,n) -bag)) . i by PRE_POLY:def_5 ; ::_thesis: verum
end;
supposeA5: i in S ; ::_thesis: (((S \/ T),n) -bag) . b1 = (((S,n) -bag) + ((T,n) -bag)) . b1
then A6: not i in T by A1, XBOOLE_0:def_4;
i in S \/ T by A5, XBOOLE_0:def_3;
hence (((S \/ T),n) -bag) . i = n by Th7
.= (((S,n) -bag) . i) + 0 by A5, Th7
.= (((S,n) -bag) . i) + (((T,n) -bag) . i) by A6, Th6
.= (((S,n) -bag) + ((T,n) -bag)) . i by PRE_POLY:def_5 ;
::_thesis: verum
end;
supposeA7: i in T ; ::_thesis: (((S \/ T),n) -bag) . b1 = (((S,n) -bag) + ((T,n) -bag)) . b1
then A8: not i in S by A1, XBOOLE_0:def_4;
i in S \/ T by A7, XBOOLE_0:def_3;
hence (((S \/ T),n) -bag) . i = n by Th7
.= (((T,n) -bag) . i) + 0 by A7, Th7
.= (((S,n) -bag) . i) + (((T,n) -bag) . i) by A8, Th6
.= (((S,n) -bag) + ((T,n) -bag)) . i by PRE_POLY:def_5 ;
::_thesis: verum
end;
end;
end;
hence ((S \/ T),n) -bag = ((S,n) -bag) + ((T,n) -bag) by PBOOLE:3; ::_thesis: verum
end;
definition
let X be set ;
mode Rbag of X is real-valued finite-support ManySortedSet of X;
end;
definition
let A be set ;
let b be Rbag of A;
func Sum b -> real number means :Def3: :: UPROOTS:def 3
ex f being FinSequence of REAL st
( it = Sum f & f = b * (canFS (support b)) );
existence
ex b1 being real number ex f being FinSequence of REAL st
( b1 = Sum f & f = b * (canFS (support b)) )
proof
set cS = canFS (support b);
set f = b * (canFS (support b));
A1: rng (b * (canFS (support b))) c= REAL ;
( support b c= dom b & rng (canFS (support b)) = support b ) by FUNCT_2:def_3, PRE_POLY:37;
then dom (b * (canFS (support b))) = dom (canFS (support b)) by RELAT_1:27;
then dom (b * (canFS (support b))) = Seg (len (canFS (support b))) by FINSEQ_1:def_3;
then b * (canFS (support b)) is FinSequence by FINSEQ_1:def_2;
then reconsider f = b * (canFS (support b)) as FinSequence of REAL by A1, FINSEQ_1:def_4;
take Sum f ; ::_thesis: ex f being FinSequence of REAL st
( Sum f = Sum f & f = b * (canFS (support b)) )
thus ex f being FinSequence of REAL st
( Sum f = Sum f & f = b * (canFS (support b)) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being real number st ex f being FinSequence of REAL st
( b1 = Sum f & f = b * (canFS (support b)) ) & ex f being FinSequence of REAL st
( b2 = Sum f & f = b * (canFS (support b)) ) holds
b1 = b2 ;
end;
:: deftheorem Def3 defines Sum UPROOTS:def_3_:_
for A being set
for b being Rbag of A
for b3 being real number holds
( b3 = Sum b iff ex f being FinSequence of REAL st
( b3 = Sum f & f = b * (canFS (support b)) ) );
notation
let A be set ;
let b be bag of A;
synonym degree b for Sum b;
end;
definition
let A be set ;
let b be bag of A;
:: original: Sum
redefine func degree b -> Element of NAT means :Def4: :: UPROOTS:def 4
ex f being FinSequence of NAT st
( it = Sum f & f = b * (canFS (support b)) );
coherence
Sum b is Element of NAT
proof
consider f being FinSequence of REAL such that
A1: degree b = Sum f and
A2: f = b * (canFS (support b)) by Def3;
rng f c= NAT
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in NAT )
assume y in rng f ; ::_thesis: y in NAT
then consider x being set such that
A3: x in dom f and
A4: y = f . x by FUNCT_1:def_3;
f . x = b . ((canFS (support b)) . x) by A2, A3, FUNCT_1:12;
hence y in NAT by A4; ::_thesis: verum
end;
then reconsider f = f as FinSequence of NAT by FINSEQ_1:def_4;
Sum f is Element of NAT ;
hence Sum b is Element of NAT by A1; ::_thesis: verum
end;
compatibility
for b1 being Element of NAT holds
( b1 = Sum b iff ex f being FinSequence of NAT st
( b1 = Sum f & f = b * (canFS (support b)) ) )
proof
set cS = canFS (support b);
let n be Element of NAT ; ::_thesis: ( n = Sum b iff ex f being FinSequence of NAT st
( n = Sum f & f = b * (canFS (support b)) ) )
hereby ::_thesis: ( ex f being FinSequence of NAT st
( n = Sum f & f = b * (canFS (support b)) ) implies n = Sum b )
consider f being FinSequence of REAL such that
A5: degree b = Sum f and
A6: f = b * (canFS (support b)) by Def3;
A7: rng f c= NAT
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in NAT )
assume y in rng f ; ::_thesis: y in NAT
then consider x being set such that
A8: x in dom f and
A9: y = f . x by FUNCT_1:def_3;
f . x = b . ((canFS (support b)) . x) by A6, A8, FUNCT_1:12;
hence y in NAT by A9; ::_thesis: verum
end;
assume A10: n = degree b ; ::_thesis: ex f being FinSequence of NAT st
( n = Sum f & f = b * (canFS (support b)) )
reconsider f = f as FinSequence of NAT by A7, FINSEQ_1:def_4;
take f = f; ::_thesis: ( n = Sum f & f = b * (canFS (support b)) )
thus ( n = Sum f & f = b * (canFS (support b)) ) by A10, A5, A6; ::_thesis: verum
end;
given f being FinSequence of NAT such that A11: ( n = Sum f & f = b * (canFS (support b)) ) ; ::_thesis: n = Sum b
rng f c= REAL ;
then reconsider f = f as FinSequence of REAL by FINSEQ_1:def_4;
f = f ;
hence n = Sum b by A11, Def3; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines degree UPROOTS:def_4_:_
for A being set
for b being bag of A
for b3 being Element of NAT holds
( b3 = degree b iff ex f being FinSequence of NAT st
( b3 = Sum f & f = b * (canFS (support b)) ) );
theorem Th11: :: UPROOTS:11
for A being set
for b being Rbag of A st b = EmptyBag A holds
Sum b = 0
proof
let A be set ; ::_thesis: for b being Rbag of A st b = EmptyBag A holds
Sum b = 0
let b be Rbag of A; ::_thesis: ( b = EmptyBag A implies Sum b = 0 )
set cS = canFS (support b);
assume b = EmptyBag A ; ::_thesis: Sum b = 0
then support b = {} by BAGORDER:18;
then b * (canFS (support b)) = <*> NAT ;
hence Sum b = 0 by Def3, RVSUM_1:72; ::_thesis: verum
end;
theorem Th12: :: UPROOTS:12
for A being set
for b being bag of A st Sum b = 0 holds
b = EmptyBag A
proof
let A be set ; ::_thesis: for b being bag of A st Sum b = 0 holds
b = EmptyBag A
let b be bag of A; ::_thesis: ( Sum b = 0 implies b = EmptyBag A )
set cS = canFS (support b);
consider f being FinSequence of NAT such that
A1: degree b = Sum f and
A2: f = b * (canFS (support b)) by Def4;
assume A3: degree b = 0 ; ::_thesis: b = EmptyBag A
now__::_thesis:_not_support_b_<>_{}
assume A4: support b <> {} ; ::_thesis: contradiction
A5: now__::_thesis:_ex_i_being_Nat_st_
(_i_in_dom_f_&_0_<_f_._i_)
consider x being set such that
A6: x in support b by A4, XBOOLE_0:def_1;
x in rng (canFS (support b)) by A6, FUNCT_2:def_3;
then consider i being Nat such that
A7: i in dom (canFS (support b)) and
A8: (canFS (support b)) . i = x by FINSEQ_2:10;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
f . i = b . ((canFS (support b)) . i) by A2, A7, FUNCT_1:13;
then A9: f . i <> 0 by A6, A8, PRE_POLY:def_7;
support b c= dom b by PRE_POLY:37;
then i in dom f by A2, A6, A7, A8, FUNCT_1:11;
hence ex i being Nat st
( i in dom f & 0 < f . i ) by A9; ::_thesis: verum
end;
for i being Nat st i in dom f holds
0 <= f . i ;
hence contradiction by A3, A1, A5, RVSUM_1:85; ::_thesis: verum
end;
hence b = EmptyBag A by BAGORDER:19; ::_thesis: verum
end;
theorem Th13: :: UPROOTS:13
for A being set
for S being finite Subset of A
for b being bag of A holds
( ( S = support b & degree b = card S ) iff b = (S,1) -bag )
proof
let A be set ; ::_thesis: for S being finite Subset of A
for b being bag of A holds
( ( S = support b & degree b = card S ) iff b = (S,1) -bag )
let S be finite Subset of A; ::_thesis: for b being bag of A holds
( ( S = support b & degree b = card S ) iff b = (S,1) -bag )
let b be bag of A; ::_thesis: ( ( S = support b & degree b = card S ) iff b = (S,1) -bag )
set cS = canFS S;
set f = b * (canFS S);
A1: dom b = A by PARTFUN1:def_2;
set g = (card S) |-> 1;
A2: len (canFS S) = card S by Th3;
A3: rng (canFS S) = S by FUNCT_2:def_3;
then A4: dom (b * (canFS S)) = dom (canFS S) by A1, RELAT_1:27;
then dom (b * (canFS S)) = Seg (len (canFS S)) by FINSEQ_1:def_3;
then reconsider f = b * (canFS S) as FinSequence by FINSEQ_1:def_2;
A5: len (canFS S) = len f by A4, FINSEQ_3:29;
hereby ::_thesis: ( b = (S,1) -bag implies ( S = support b & degree b = card S ) )
set sb = (S,1) -bag ;
assume that
A6: S = support b and
A7: degree b = card S ; ::_thesis: b = (S,1) -bag
consider F being FinSequence of NAT such that
A8: degree b = Sum F and
A9: F = b * (canFS S) by A6, Def4;
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_F_holds_
F_._i_<>_0
let i be Element of NAT ; ::_thesis: ( i in dom F implies F . i <> 0 )
assume i in dom F ; ::_thesis: F . i <> 0
then ( F . i = b . ((canFS S) . i) & (canFS S) . i in rng (canFS S) ) by A4, A9, FUNCT_1:3, FUNCT_1:12;
hence F . i <> 0 by A6, PRE_POLY:def_7; ::_thesis: verum
end;
then A10: F = (len F) |-> 1 by A2, A5, A7, A8, A9, Th1;
A11: support b = support ((S,1) -bag) by A6, Th8;
now__::_thesis:_(_dom_b_=_dom_((S,1)_-bag)_&_(_for_x_being_set_st_x_in_dom_b_holds_
b_._x_=_((S,1)_-bag)_._x_)_)
thus dom b = dom ((S,1) -bag) by A1, PARTFUN1:def_2; ::_thesis: for x being set st x in dom b holds
b . b2 = ((S,1) -bag) . b2
let x be set ; ::_thesis: ( x in dom b implies b . b1 = ((S,1) -bag) . b1 )
assume x in dom b ; ::_thesis: b . b1 = ((S,1) -bag) . b1
percases ( x in support b or not x in support b ) ;
supposeA12: x in support b ; ::_thesis: b . b1 = ((S,1) -bag) . b1
then A13: ((canFS S) ") . x in dom (canFS S) by A3, A6, FUNCT_1:32;
then A14: ((canFS S) ") . x in Seg (len F) by A4, A9, FINSEQ_1:def_3;
rng (canFS S) = support b by A6, FUNCT_2:def_3;
hence b . x = b . ((canFS S) . (((canFS S) ") . x)) by A12, FUNCT_1:35
.= F . (((canFS S) ") . x) by A9, A13, FUNCT_1:13
.= 1 by A10, A14, FUNCOP_1:7
.= ((S,1) -bag) . x by A6, A12, Th7 ;
::_thesis: verum
end;
supposeA15: not x in support b ; ::_thesis: b . b1 = ((S,1) -bag) . b1
hence b . x = 0 by PRE_POLY:def_7
.= ((S,1) -bag) . x by A11, A15, PRE_POLY:def_7 ;
::_thesis: verum
end;
end;
end;
hence b = (S,1) -bag by FUNCT_1:2; ::_thesis: verum
end;
rng f c= NAT
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in NAT )
assume y in rng f ; ::_thesis: y in NAT
then consider x being set such that
A16: x in dom f and
A17: y = f . x by FUNCT_1:def_3;
f . x = b . ((canFS S) . x) by A16, FUNCT_1:12;
hence y in NAT by A17; ::_thesis: verum
end;
then reconsider f = f as FinSequence of NAT by FINSEQ_1:def_4;
assume A18: b = (S,1) -bag ; ::_thesis: ( S = support b & degree b = card S )
A19: rng (canFS S) = S by FUNCT_2:def_3;
now__::_thesis:_(_len_f_=_card_S_&_len_((card_S)_|->_1)_=_card_S_&_(_for_i_being_Nat_st_i_in_dom_f_holds_
f_._i_=_((card_S)_|->_1)_._i_)_)
thus len f = card S by A4, A2, FINSEQ_3:29; ::_thesis: ( len ((card S) |-> 1) = card S & ( for i being Nat st i in dom f holds
f . i = ((card S) |-> 1) . i ) )
thus len ((card S) |-> 1) = card S by CARD_1:def_7; ::_thesis: for i being Nat st i in dom f holds
f . i = ((card S) |-> 1) . i
let i be Nat; ::_thesis: ( i in dom f implies f . i = ((card S) |-> 1) . i )
A20: dom f = Seg (card S) by A4, A2, FINSEQ_1:def_3;
assume A21: i in dom f ; ::_thesis: f . i = ((card S) |-> 1) . i
hence f . i = b . ((canFS S) . i) by FUNCT_1:12
.= 1 by A4, A19, A18, A21, Th7, FUNCT_1:3
.= ((card S) |-> 1) . i by A20, A21, FUNCOP_1:7 ;
::_thesis: verum
end;
then A22: f = (card S) |-> 1 by FINSEQ_2:9;
thus S = support b by A18, Th8; ::_thesis: degree b = card S
then degree b = Sum f by Def4;
hence degree b = (card S) * 1 by A22, RVSUM_1:80
.= card S ;
::_thesis: verum
end;
theorem Th14: :: UPROOTS:14
for A being set
for S being finite Subset of A
for b being Rbag of A st support b c= S holds
ex f being FinSequence of REAL st
( f = b * (canFS S) & Sum b = Sum f )
proof
let A be set ; ::_thesis: for S being finite Subset of A
for b being Rbag of A st support b c= S holds
ex f being FinSequence of REAL st
( f = b * (canFS S) & Sum b = Sum f )
let S be finite Subset of A; ::_thesis: for b being Rbag of A st support b c= S holds
ex f being FinSequence of REAL st
( f = b * (canFS S) & Sum b = Sum f )
let b be Rbag of A; ::_thesis: ( support b c= S implies ex f being FinSequence of REAL st
( f = b * (canFS S) & Sum b = Sum f ) )
assume A1: support b c= S ; ::_thesis: ex f being FinSequence of REAL st
( f = b * (canFS S) & Sum b = Sum f )
A2: card (support b) <= card S by A1, NAT_1:43;
set cs = canFS (support b);
A3: rng (canFS (support b)) = support b by FUNCT_2:def_3;
set cS = canFS S;
set f = b * (canFS S);
len (canFS S) = card S by Th3;
then A4: dom (canFS S) = Seg (card S) by FINSEQ_1:def_3;
len (canFS (support b)) = card (support b) by Th3;
then A5: dom (canFS (support b)) = Seg (card (support b)) by FINSEQ_1:def_3;
consider g being FinSequence of REAL such that
A6: Sum b = Sum g and
A7: g = b * (canFS (support b)) by Def3;
A8: dom b = A by PARTFUN1:def_2;
then A9: dom g = Seg (card (support b)) by A1, A7, A5, A3, RELAT_1:27, XBOOLE_1:1;
then A10: len g = card (support b) by FINSEQ_1:def_3;
A11: rng (canFS S) = S by FUNCT_2:def_3;
then A12: dom (b * (canFS S)) = Seg (card S) by A4, A8, RELAT_1:27;
then reconsider f = b * (canFS S) as FinSequence by FINSEQ_1:def_2;
rng f c= rng b by RELAT_1:26;
then rng f c= REAL by XBOOLE_1:1;
then reconsider f = f as FinSequence of REAL by FINSEQ_1:def_4;
take f ; ::_thesis: ( f = b * (canFS S) & Sum b = Sum f )
thus f = b * (canFS S) ; ::_thesis: Sum b = Sum f
percases ( card (support b) < card S or card (support b) = card S ) by A2, XXREAL_0:1;
supposeA13: card (support b) < card S ; ::_thesis: Sum b = Sum f
set dd = { j where j is Element of NAT : ( j in dom f & f . j = 0 ) } ;
A14: now__::_thesis:_not__{__j_where_j_is_Element_of_NAT_:_(_j_in_dom_f_&_f_._j_=_0_)__}__is_empty
consider x being set such that
A15: ( ( x in support b & not x in S ) or ( x in S & not x in support b ) ) by A13, TARSKI:1;
consider j being set such that
A16: j in dom (canFS S) and
A17: (canFS S) . j = x by A1, A11, A15, FUNCT_1:def_3;
reconsider j = j as Element of NAT by A16;
f . j = b . x by A16, A17, FUNCT_1:13;
then f . j = 0 by A1, A15, PRE_POLY:def_7;
then j in { j where j is Element of NAT : ( j in dom f & f . j = 0 ) } by A4, A12, A16;
hence not { j where j is Element of NAT : ( j in dom f & f . j = 0 ) } is empty ; ::_thesis: verum
end;
reconsider gr = g as FinSequence of REAL ;
A18: { j where j is Element of NAT : ( j in dom f & f . j = 0 ) } c= dom f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { j where j is Element of NAT : ( j in dom f & f . j = 0 ) } or x in dom f )
assume x in { j where j is Element of NAT : ( j in dom f & f . j = 0 ) } ; ::_thesis: x in dom f
then ex j being Element of NAT st
( x = j & j in dom f & f . j = 0 ) ;
hence x in dom f ; ::_thesis: verum
end;
then reconsider dd = { j where j is Element of NAT : ( j in dom f & f . j = 0 ) } as non empty finite set by A14;
consider d being Element of NAT such that
A19: card S = (card (support b)) + d and
1 <= d by A13, FINSEQ_4:84;
set h = d |-> 0;
set F = gr ^ (d |-> 0);
( rng (canFS dd) = dd & dd c= NAT ) by A18, FUNCT_2:def_3, XBOOLE_1:1;
then reconsider cdd = canFS dd as FinSequence of NAT by FINSEQ_1:def_4;
set cdi = cdd " ;
reconsider cdi = cdd " as Function of dd,(Seg (card dd)) by Th5;
reconsider cdi = cdi as Function of dd,NAT by FUNCT_2:7;
deffunc H1( set ) -> Element of NAT = (cdi /. $1) + (card (support b));
consider z being Function such that
A20: dom z = dd and
A21: for x being set st x in dd holds
z . x = H1(x) from FUNCT_1:sch_3();
set p = (((canFS (support b)) ") * (canFS S)) +* z;
A22: dom cdi = dd by FUNCT_2:def_1;
set cSr = (canFS S) | ((dom f) \ dd);
now__::_thesis:_for_y_being_set_holds_
(_(_y_in_rng_((canFS_S)_|_((dom_f)_\_dd))_implies_y_in_support_b_)_&_(_y_in_support_b_implies_y_in_rng_((canFS_S)_|_((dom_f)_\_dd))_)_)
let y be set ; ::_thesis: ( ( y in rng ((canFS S) | ((dom f) \ dd)) implies y in support b ) & ( y in support b implies y in rng ((canFS S) | ((dom f) \ dd)) ) )
hereby ::_thesis: ( y in support b implies y in rng ((canFS S) | ((dom f) \ dd)) )
assume y in rng ((canFS S) | ((dom f) \ dd)) ; ::_thesis: y in support b
then consider x being set such that
A23: x in dom ((canFS S) | ((dom f) \ dd)) and
A24: y = ((canFS S) | ((dom f) \ dd)) . x by FUNCT_1:def_3;
A25: ((canFS S) | ((dom f) \ dd)) . x = (canFS S) . x by A23, FUNCT_1:47;
x in dom (canFS S) by A23, RELAT_1:57;
then reconsider j = x as Element of NAT ;
A26: x in (findom f) \ dd by A23;
then not j in dd by XBOOLE_0:def_5;
then A27: f . j <> 0 by A26;
x in dom (canFS S) by A23, RELAT_1:57;
then b . ((canFS S) . j) <> 0 by A27, FUNCT_1:13;
hence y in support b by A24, A25, PRE_POLY:def_7; ::_thesis: verum
end;
assume A28: y in support b ; ::_thesis: y in rng ((canFS S) | ((dom f) \ dd))
then consider x being set such that
A29: x in dom (canFS S) and
A30: y = (canFS S) . x by A1, A11, FUNCT_1:def_3;
now__::_thesis:_not_x_in_dd
assume x in dd ; ::_thesis: contradiction
then consider j being Element of NAT such that
A31: j = x and
A32: ( j in dom f & f . j = 0 ) ;
0 = b . ((canFS S) . j) by A4, A12, A32, FUNCT_1:13;
hence contradiction by A28, A30, A31, PRE_POLY:def_7; ::_thesis: verum
end;
then x in (dom f) \ dd by A4, A12, A29, XBOOLE_0:def_5;
hence y in rng ((canFS S) | ((dom f) \ dd)) by A29, A30, FUNCT_1:50; ::_thesis: verum
end;
then A33: rng ((canFS S) | ((dom f) \ dd)) = support b by TARSKI:1;
((findom f) \ dd) /\ (dom f) = (dom f) \ dd by XBOOLE_1:28;
then ( (canFS S) | ((dom f) \ dd) is one-to-one & dom ((canFS S) | ((dom f) \ dd)) = (dom f) \ dd ) by A4, A12, FUNCT_1:52, RELAT_1:61;
then support b,(dom f) \ dd are_equipotent by A33, WELLORD2:def_4;
then A34: card (support b) = card ((dom f) \ dd) by CARD_1:5;
card ((dom f) \ dd) = (card (dom f)) - (card dd) by A18, CARD_2:44;
then A35: (card (support b)) + (card dd) = card S by A12, A34, FINSEQ_1:57;
A36: now__::_thesis:_not_(dom_(((canFS_(support_b))_")_*_(canFS_S)))_/\_(dom_z)_<>_{}
A37: dom ((canFS (support b)) ") = support b by A3, FUNCT_1:33;
assume (dom (((canFS (support b)) ") * (canFS S))) /\ (dom z) <> {} ; ::_thesis: contradiction
then consider x being set such that
A38: x in (dom (((canFS (support b)) ") * (canFS S))) /\ (dom z) by XBOOLE_0:def_1;
x in dom z by A38, XBOOLE_0:def_4;
then consider j being Element of NAT such that
A39: j = x and
j in dom f and
A40: f . j = 0 by A20;
A41: x in dom (((canFS (support b)) ") * (canFS S)) by A38, XBOOLE_0:def_4;
then j in dom (canFS S) by A39, FUNCT_1:11;
then f . j = b . ((canFS S) . j) by FUNCT_1:13;
then not (canFS S) . j in support b by A40, PRE_POLY:def_7;
hence contradiction by A41, A39, A37, FUNCT_1:11; ::_thesis: verum
end;
len (gr ^ (d |-> 0)) = (len g) + (len (d |-> 0)) by FINSEQ_1:22
.= card S by A10, A19, CARD_1:def_7 ;
then A42: dom (gr ^ (d |-> 0)) = Seg (card S) by FINSEQ_1:def_3;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(dom_(((canFS_(support_b))_")_*_(canFS_S)))_\/_(dom_z)_implies_x_in_dom_(gr_^_(d_|->_0))_)_&_(_x_in_dom_(gr_^_(d_|->_0))_implies_x_in_(dom_(((canFS_(support_b))_")_*_(canFS_S)))_\/_(dom_z)_)_)
let x be set ; ::_thesis: ( ( x in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) implies x in dom (gr ^ (d |-> 0)) ) & ( x in dom (gr ^ (d |-> 0)) implies b1 in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) ) )
hereby ::_thesis: ( x in dom (gr ^ (d |-> 0)) implies b1 in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) )
assume A43: x in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) ; ::_thesis: x in dom (gr ^ (d |-> 0))
percases ( x in dom (((canFS (support b)) ") * (canFS S)) or x in dom z ) by A43, XBOOLE_0:def_3;
suppose x in dom (((canFS (support b)) ") * (canFS S)) ; ::_thesis: x in dom (gr ^ (d |-> 0))
hence x in dom (gr ^ (d |-> 0)) by A4, A42, FUNCT_1:11; ::_thesis: verum
end;
suppose x in dom z ; ::_thesis: x in dom (gr ^ (d |-> 0))
hence x in dom (gr ^ (d |-> 0)) by A12, A42, A18, A20; ::_thesis: verum
end;
end;
end;
assume A44: x in dom (gr ^ (d |-> 0)) ; ::_thesis: b1 in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z)
then reconsider i = x as Element of NAT ;
percases ( f . x = 0 or f . x <> 0 ) ;
suppose f . x = 0 ; ::_thesis: b1 in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z)
then i in dom z by A12, A42, A20, A44;
hence x in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) by XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA45: f . x <> 0 ; ::_thesis: b1 in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z)
f . i = b . ((canFS S) . i) by A4, A42, A44, FUNCT_1:13;
then (canFS S) . i in support b by A45, PRE_POLY:def_7;
then (canFS S) . i in dom ((canFS (support b)) ") by A3, FUNCT_1:33;
then i in dom (((canFS (support b)) ") * (canFS S)) by A4, A42, A44, FUNCT_1:11;
hence x in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
then A46: (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) = dom (gr ^ (d |-> 0)) by TARSKI:1;
then A47: dom ((((canFS (support b)) ") * (canFS S)) +* z) = dom (gr ^ (d |-> 0)) by FUNCT_4:def_1;
len cdd = card dd by Th3;
then A48: dom cdd = Seg d by A19, A35, FINSEQ_1:def_3;
then A49: rng cdi = Seg d by FUNCT_1:33;
A50: rng z c= Seg (card S)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng z or y in Seg (card S) )
assume y in rng z ; ::_thesis: y in Seg (card S)
then consider x being set such that
A51: x in dom z and
A52: y = z . x by FUNCT_1:def_3;
A53: ( cdi /. x = cdi . x & cdi . x in Seg d ) by A22, A49, A20, A51, FUNCT_1:3, PARTFUN1:def_6;
then 1 <= cdi /. x by FINSEQ_1:1;
then A54: 1 <= (cdi /. x) + (card (support b)) by NAT_1:12;
cdi /. x <= d by A53, FINSEQ_1:1;
then A55: (cdi /. x) + (card (support b)) <= d + (card (support b)) by XREAL_1:6;
y = (cdi /. x) + (card (support b)) by A20, A21, A51, A52;
hence y in Seg (card S) by A19, A54, A55, FINSEQ_1:1; ::_thesis: verum
end;
A56: now__::_thesis:_for_x_being_set_st_x_in_dom_(gr_^_(d_|->_0))_holds_
((((canFS_(support_b))_")_*_(canFS_S))_+*_z)_._x_in_dom_(gr_^_(d_|->_0))
let x be set ; ::_thesis: ( x in dom (gr ^ (d |-> 0)) implies ((((canFS (support b)) ") * (canFS S)) +* z) . b1 in dom (gr ^ (d |-> 0)) )
assume A57: x in dom (gr ^ (d |-> 0)) ; ::_thesis: ((((canFS (support b)) ") * (canFS S)) +* z) . b1 in dom (gr ^ (d |-> 0))
percases ( x in dom (((canFS (support b)) ") * (canFS S)) or x in dom z ) by A46, A57, XBOOLE_0:def_3;
supposeA58: x in dom (((canFS (support b)) ") * (canFS S)) ; ::_thesis: ((((canFS (support b)) ") * (canFS S)) +* z) . b1 in dom (gr ^ (d |-> 0))
then (((canFS (support b)) ") * (canFS S)) . x in rng (((canFS (support b)) ") * (canFS S)) by FUNCT_1:3;
then (((canFS (support b)) ") * (canFS S)) . x in rng ((canFS (support b)) ") by FUNCT_1:14;
then A59: (((canFS (support b)) ") * (canFS S)) . x in dom (canFS (support b)) by FUNCT_1:33;
not x in dom z by A36, A58, XBOOLE_0:def_4;
then A60: ((((canFS (support b)) ") * (canFS S)) +* z) . x = (((canFS (support b)) ") * (canFS S)) . x by FUNCT_4:11;
Seg (card (support b)) c= Seg (card S) by A2, FINSEQ_1:5;
hence ((((canFS (support b)) ") * (canFS S)) +* z) . x in dom (gr ^ (d |-> 0)) by A5, A42, A60, A59; ::_thesis: verum
end;
suppose x in dom z ; ::_thesis: ((((canFS (support b)) ") * (canFS S)) +* z) . b1 in dom (gr ^ (d |-> 0))
then ( ((((canFS (support b)) ") * (canFS S)) +* z) . x = z . x & z . x in rng z ) by FUNCT_1:3, FUNCT_4:13;
hence ((((canFS (support b)) ") * (canFS S)) +* z) . x in dom (gr ^ (d |-> 0)) by A42, A50; ::_thesis: verum
end;
end;
end;
A61: dom ((((canFS (support b)) ") * (canFS S)) +* z) = (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) by FUNCT_4:def_1;
reconsider p = (((canFS (support b)) ") * (canFS S)) +* z as Function of (dom (gr ^ (d |-> 0))),(dom (gr ^ (d |-> 0))) by A47, A56, FUNCT_2:3;
len (d |-> 0) = d by CARD_1:def_7;
then A62: dom (d |-> 0) = Seg d by FINSEQ_1:def_3;
A63: rng cdd = dd by FUNCT_2:def_3;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_rng_p_implies_x_in_dom_(gr_^_(d_|->_0))_)_&_(_x_in_dom_(gr_^_(d_|->_0))_implies_x_in_rng_p_)_)
let x be set ; ::_thesis: ( ( x in rng p implies x in dom (gr ^ (d |-> 0)) ) & ( x in dom (gr ^ (d |-> 0)) implies b1 in rng p ) )
hereby ::_thesis: ( x in dom (gr ^ (d |-> 0)) implies b1 in rng p )
assume x in rng p ; ::_thesis: x in dom (gr ^ (d |-> 0))
then consider a being set such that
A64: a in dom p and
A65: x = p . a by FUNCT_1:def_3;
percases ( a in dom (((canFS (support b)) ") * (canFS S)) or a in dom z ) by A64, FUNCT_4:12;
supposeA66: a in dom (((canFS (support b)) ") * (canFS S)) ; ::_thesis: x in dom (gr ^ (d |-> 0))
then (canFS S) . a in dom ((canFS (support b)) ") by FUNCT_1:11;
then ((canFS (support b)) ") . ((canFS S) . a) in rng ((canFS (support b)) ") by FUNCT_1:3;
then A67: ((canFS (support b)) ") . ((canFS S) . a) in dom (canFS (support b)) by FUNCT_1:33;
not a in dom z by A36, A66, XBOOLE_0:def_4;
then A68: p . a = (((canFS (support b)) ") * (canFS S)) . a by FUNCT_4:11
.= ((canFS (support b)) ") . ((canFS S) . a) by A66, FUNCT_1:12 ;
dom (canFS (support b)) c= dom (gr ^ (d |-> 0)) by A5, A2, A42, FINSEQ_1:5;
hence x in dom (gr ^ (d |-> 0)) by A65, A68, A67; ::_thesis: verum
end;
suppose a in dom z ; ::_thesis: x in dom (gr ^ (d |-> 0))
then ( z . a in rng z & p . a = z . a ) by FUNCT_1:3, FUNCT_4:13;
hence x in dom (gr ^ (d |-> 0)) by A42, A50, A65; ::_thesis: verum
end;
end;
end;
assume A69: x in dom (gr ^ (d |-> 0)) ; ::_thesis: b1 in rng p
then reconsider j = x as Element of NAT ;
percases ( j in dom gr or ex n being Nat st
( n in dom (d |-> 0) & j = (len gr) + n ) ) by A69, FINSEQ_1:25;
supposeA70: j in dom gr ; ::_thesis: b1 in rng p
then A71: (canFS (support b)) . j in support b by A5, A3, A9, FUNCT_1:3;
then A72: ((canFS S) ") . ((canFS (support b)) . j) in Seg (card S) by A1, A4, A11, FUNCT_1:32;
now__::_thesis:_not_((canFS_S)_")_._((canFS_(support_b))_._j)_in_dom_z
assume ((canFS S) ") . ((canFS (support b)) . j) in dom z ; ::_thesis: contradiction
then A73: ex k being Element of NAT st
( k = ((canFS S) ") . ((canFS (support b)) . j) & k in dom f & f . k = 0 ) by A20;
(b * (canFS S)) . (((canFS S) ") . ((canFS (support b)) . j)) = b . ((canFS S) . (((canFS S) ") . ((canFS (support b)) . j))) by A4, A72, FUNCT_1:13
.= b . ((canFS (support b)) . j) by A1, A11, A71, FUNCT_1:35 ;
hence contradiction by A71, A73, PRE_POLY:def_7; ::_thesis: verum
end;
then p . (((canFS S) ") . ((canFS (support b)) . j)) = (((canFS (support b)) ") * (canFS S)) . (((canFS S) ") . ((canFS (support b)) . j)) by FUNCT_4:11
.= ((canFS (support b)) ") . ((canFS S) . (((canFS S) ") . ((canFS (support b)) . j))) by A4, A72, FUNCT_1:13
.= ((canFS (support b)) ") . ((canFS (support b)) . j) by A1, A11, A71, FUNCT_1:35
.= j by A5, A9, A70, FUNCT_1:34 ;
hence x in rng p by A42, A47, A72, FUNCT_1:3; ::_thesis: verum
end;
suppose ex n being Nat st
( n in dom (d |-> 0) & j = (len gr) + n ) ; ::_thesis: b1 in rng p
then consider n being Nat such that
A74: n in dom (d |-> 0) and
A75: j = (len gr) + n ;
A76: cdd . n in dd by A62, A48, A63, A74, FUNCT_1:3;
p . (cdd . n) = z . (cdd . n) by A62, A48, A63, A20, A74, FUNCT_1:3, FUNCT_4:13
.= (cdi /. (cdd . n)) + (card (support b)) by A62, A48, A63, A21, A74, FUNCT_1:3
.= (cdi . (cdd . n)) + (card (support b)) by A62, A48, A63, A22, A74, FUNCT_1:3, PARTFUN1:def_6
.= n + (card (support b)) by A62, A48, A74, FUNCT_1:34
.= j by A9, A75, FINSEQ_1:def_3 ;
hence x in rng p by A12, A42, A18, A47, A76, FUNCT_1:3; ::_thesis: verum
end;
end;
end;
then A77: rng p = dom (gr ^ (d |-> 0)) by TARSKI:1;
then A78: dom ((gr ^ (d |-> 0)) * p) = dom (gr ^ (d |-> 0)) by A47, RELAT_1:27;
now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
f_._x_=_((gr_^_(d_|->_0))_*_p)_._x
let x be set ; ::_thesis: ( x in dom f implies f . b1 = ((gr ^ (d |-> 0)) * p) . b1 )
assume A79: x in dom f ; ::_thesis: f . b1 = ((gr ^ (d |-> 0)) * p) . b1
percases ( f . x = 0 or f . x <> 0 ) ;
supposeA80: f . x = 0 ; ::_thesis: f . b1 = ((gr ^ (d |-> 0)) * p) . b1
reconsider cdix = cdi /. x as Element of NAT ;
reconsider px = p . x as Element of NAT ;
reconsider j = x as Element of NAT by A79;
A81: j in dom z by A20, A79, A80;
then A82: p . x = z . x by FUNCT_4:13
.= (cdi /. x) + (card (support b)) by A20, A21, A81 ;
A83: cdi . x in Seg (card dd) by A20, A81, FUNCT_2:5;
dom cdi = dd by FUNCT_2:def_1;
then A84: cdi /. x = cdi . x by A20, A81, PARTFUN1:def_6;
thus f . x = (d |-> 0) . cdix by A80
.= (gr ^ (d |-> 0)) . px by A10, A19, A62, A35, A82, A84, A83, FINSEQ_1:def_7
.= ((gr ^ (d |-> 0)) * p) . x by A12, A42, A78, A79, FUNCT_1:12 ; ::_thesis: verum
end;
supposeA85: f . x <> 0 ; ::_thesis: f . b1 = ((gr ^ (d |-> 0)) * p) . b1
reconsider px = p . x as Element of NAT ;
f . x = b . ((canFS S) . x) by A79, FUNCT_1:12;
then (canFS S) . x in support b by A85, PRE_POLY:def_7;
then A86: (canFS S) . x in rng (canFS (support b)) by FUNCT_2:def_3;
then A87: ((canFS (support b)) ") . ((canFS S) . x) in dom (canFS (support b)) by FUNCT_1:32;
now__::_thesis:_not_x_in_dd
assume x in dd ; ::_thesis: contradiction
then ex j being Element of NAT st
( j = x & j in dom f & f . j = 0 ) ;
hence contradiction by A85; ::_thesis: verum
end;
then A88: p . x = (((canFS (support b)) ") * (canFS S)) . x by A20, FUNCT_4:11
.= ((canFS (support b)) ") . ((canFS S) . x) by A4, A12, A79, FUNCT_1:13 ;
thus f . x = b . ((canFS S) . x) by A79, FUNCT_1:12
.= b . ((canFS (support b)) . px) by A86, A88, FUNCT_1:32
.= g . px by A7, A87, A88, FUNCT_1:13
.= (gr ^ (d |-> 0)) . px by A5, A9, A87, A88, FINSEQ_1:def_7
.= ((gr ^ (d |-> 0)) * p) . x by A12, A42, A78, A79, FUNCT_1:12 ; ::_thesis: verum
end;
end;
end;
then A89: f = (gr ^ (d |-> 0)) * p by A4, A11, A8, A42, A78, FUNCT_1:2, RELAT_1:27;
A90: p is one-to-one
proof
let a, c be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not a in proj1 p or not c in proj1 p or not p . a = p . c or a = c )
assume that
A91: ( a in dom p & c in dom p ) and
A92: p . a = p . c ; ::_thesis: a = c
percases ( ( a in dom (((canFS (support b)) ") * (canFS S)) & c in dom (((canFS (support b)) ") * (canFS S)) ) or ( a in dom (((canFS (support b)) ") * (canFS S)) & c in dom z ) or ( a in dom z & c in dom (((canFS (support b)) ") * (canFS S)) ) or ( a in dom z & c in dom z ) ) by A61, A91, XBOOLE_0:def_3;
supposeA93: ( a in dom (((canFS (support b)) ") * (canFS S)) & c in dom (((canFS (support b)) ") * (canFS S)) ) ; ::_thesis: a = c
then (canFS S) . a in dom ((canFS (support b)) ") by FUNCT_1:11;
then (canFS S) . a in rng (canFS (support b)) by FUNCT_1:33;
then A94: (canFS (support b)) . (((canFS (support b)) ") . ((canFS S) . a)) = (canFS S) . a by FUNCT_1:35;
a in dom (canFS S) by A93, FUNCT_1:11;
then A95: ((canFS S) ") . ((canFS S) . a) = a by FUNCT_1:34;
(canFS S) . c in dom ((canFS (support b)) ") by A93, FUNCT_1:11;
then A96: (canFS S) . c in rng (canFS (support b)) by FUNCT_1:33;
not c in dom z by A36, A93, XBOOLE_0:def_4;
then A97: p . c = (((canFS (support b)) ") * (canFS S)) . c by FUNCT_4:11
.= ((canFS (support b)) ") . ((canFS S) . c) by A93, FUNCT_1:12 ;
A98: c in dom (canFS S) by A93, FUNCT_1:11;
not a in dom z by A36, A93, XBOOLE_0:def_4;
then p . a = (((canFS (support b)) ") * (canFS S)) . a by FUNCT_4:11
.= ((canFS (support b)) ") . ((canFS S) . a) by A93, FUNCT_1:12 ;
then ((canFS S) ") . ((canFS S) . a) = ((canFS S) ") . ((canFS S) . c) by A92, A97, A94, A96, FUNCT_1:35;
hence a = c by A95, A98, FUNCT_1:34; ::_thesis: verum
end;
supposeA99: ( a in dom (((canFS (support b)) ") * (canFS S)) & c in dom z ) ; ::_thesis: a = c
then (canFS S) . a in dom ((canFS (support b)) ") by FUNCT_1:11;
then ((canFS (support b)) ") . ((canFS S) . a) in rng ((canFS (support b)) ") by FUNCT_1:3;
then A100: ((canFS (support b)) ") . ((canFS S) . a) in dom (canFS (support b)) by FUNCT_1:33;
not a in dom z by A36, A99, XBOOLE_0:def_4;
then A101: p . a = (((canFS (support b)) ") * (canFS S)) . a by FUNCT_4:11
.= ((canFS (support b)) ") . ((canFS S) . a) by A99, FUNCT_1:12 ;
p . c = z . c by A99, FUNCT_4:13
.= (cdi /. c) + (card (support b)) by A20, A21, A99 ;
then (cdi /. c) + (card (support b)) <= 0 + (card (support b)) by A5, A92, A101, A100, FINSEQ_1:1;
then cdi /. c = 0 by XREAL_1:6;
then A102: cdi . c = 0 by A22, A20, A99, PARTFUN1:def_6;
cdi . c in rng cdi by A22, A20, A99, FUNCT_1:3;
hence a = c by A49, A102, FINSEQ_1:1; ::_thesis: verum
end;
supposeA103: ( a in dom z & c in dom (((canFS (support b)) ") * (canFS S)) ) ; ::_thesis: a = c
then (canFS S) . c in dom ((canFS (support b)) ") by FUNCT_1:11;
then ((canFS (support b)) ") . ((canFS S) . c) in rng ((canFS (support b)) ") by FUNCT_1:3;
then A104: ((canFS (support b)) ") . ((canFS S) . c) in dom (canFS (support b)) by FUNCT_1:33;
not c in dom z by A36, A103, XBOOLE_0:def_4;
then A105: p . c = (((canFS (support b)) ") * (canFS S)) . c by FUNCT_4:11
.= ((canFS (support b)) ") . ((canFS S) . c) by A103, FUNCT_1:12 ;
p . a = z . a by A103, FUNCT_4:13
.= (cdi /. a) + (card (support b)) by A20, A21, A103 ;
then (cdi /. a) + (card (support b)) <= 0 + (card (support b)) by A5, A92, A105, A104, FINSEQ_1:1;
then cdi /. a = 0 by XREAL_1:6;
then A106: cdi . a = 0 by A22, A20, A103, PARTFUN1:def_6;
cdi . a in rng cdi by A22, A20, A103, FUNCT_1:3;
hence a = c by A49, A106, FINSEQ_1:1; ::_thesis: verum
end;
supposeA107: ( a in dom z & c in dom z ) ; ::_thesis: a = c
then A108: ( cdi /. a = cdi . a & cdi /. c = cdi . c ) by A22, A20, PARTFUN1:def_6;
A109: p . c = z . c by A107, FUNCT_4:13
.= (cdi /. c) + (card (support b)) by A20, A21, A107 ;
p . a = z . a by A107, FUNCT_4:13
.= (cdi /. a) + (card (support b)) by A20, A21, A107 ;
hence a = c by A22, A20, A92, A107, A109, A108, FUNCT_1:def_4; ::_thesis: verum
end;
end;
end;
Sum (d |-> 0) = 0 by RVSUM_1:81;
then A110: Sum gr = (Sum gr) + (Sum (d |-> 0))
.= Sum (gr ^ (d |-> 0)) by RVSUM_1:75 ;
p is onto by A77, FUNCT_2:def_3;
hence Sum b = Sum f by A6, A90, A89, A110, FINSOP_1:7; ::_thesis: verum
end;
suppose card (support b) = card S ; ::_thesis: Sum b = Sum f
hence Sum b = Sum f by A1, A6, A7, PRE_POLY:8; ::_thesis: verum
end;
end;
end;
theorem Th15: :: UPROOTS:15
for A being set
for b, b1, b2 being Rbag of A st b = b1 + b2 holds
Sum b = (Sum b1) + (Sum b2)
proof
let A be set ; ::_thesis: for b, b1, b2 being Rbag of A st b = b1 + b2 holds
Sum b = (Sum b1) + (Sum b2)
let b, b1, b2 be Rbag of A; ::_thesis: ( b = b1 + b2 implies Sum b = (Sum b1) + (Sum b2) )
set S = support b;
set SS = (support b1) \/ (support b2);
A1: dom b2 = A by PARTFUN1:def_2;
then A2: support b2 c= A by PRE_POLY:37;
A3: dom b1 = A by PARTFUN1:def_2;
then support b1 c= A by PRE_POLY:37;
then reconsider SS = (support b1) \/ (support b2) as finite Subset of A by A2, XBOOLE_1:8;
set cS = canFS SS;
consider f1r being FinSequence of REAL such that
A4: f1r = b1 * (canFS SS) and
A5: Sum b1 = Sum f1r by Th14, XBOOLE_1:7;
A6: rng (canFS SS) = SS by FUNCT_2:def_3;
then A7: dom f1r = dom (canFS SS) by A3, A4, RELAT_1:27;
assume A8: b = b1 + b2 ; ::_thesis: Sum b = (Sum b1) + (Sum b2)
then support b c= SS by PRE_POLY:75;
then consider f being FinSequence of REAL such that
A9: f = b * (canFS SS) and
A10: Sum b = Sum f by Th14;
dom b = A by PARTFUN1:def_2;
then A11: dom f = dom (canFS SS) by A9, A6, RELAT_1:27;
then A12: len f1r = len f by A7, FINSEQ_3:29;
consider f2r being FinSequence of REAL such that
A13: f2r = b2 * (canFS SS) and
A14: Sum b2 = Sum f2r by Th14, XBOOLE_1:7;
A15: dom f2r = dom (canFS SS) by A1, A13, A6, RELAT_1:27;
A16: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_f1r_holds_
f_._k_=_(f1r_/._k)_+_(f2r_/._k)
let k be Element of NAT ; ::_thesis: ( k in dom f1r implies f . k = (f1r /. k) + (f2r /. k) )
assume A17: k in dom f1r ; ::_thesis: f . k = (f1r /. k) + (f2r /. k)
A18: f1r /. k = f1r . k by A17, PARTFUN1:def_6
.= b1 . ((canFS SS) . k) by A4, A17, FUNCT_1:12 ;
A19: f . k = b . ((canFS SS) . k) by A9, A11, A7, A17, FUNCT_1:12;
f2r /. k = f2r . k by A7, A15, A17, PARTFUN1:def_6
.= b2 . ((canFS SS) . k) by A13, A7, A15, A17, FUNCT_1:12 ;
hence f . k = (f1r /. k) + (f2r /. k) by A8, A18, A19, PRE_POLY:def_5; ::_thesis: verum
end;
len f1r = len f2r by A7, A15, FINSEQ_3:29;
hence Sum b = (Sum b1) + (Sum b2) by A10, A5, A14, A12, A16, INTEGRA1:21; ::_thesis: verum
end;
theorem Th16: :: UPROOTS:16
for L being non empty unital associative commutative multMagma
for f, g being FinSequence of L
for p being Permutation of (dom f) st g = f * p holds
Product g = Product f
proof
let L be non empty unital associative commutative multMagma ; ::_thesis: for f, g being FinSequence of L
for p being Permutation of (dom f) st g = f * p holds
Product g = Product f
let f, g be FinSequence of L; ::_thesis: for p being Permutation of (dom f) st g = f * p holds
Product g = Product f
let p be Permutation of (dom f); ::_thesis: ( g = f * p implies Product g = Product f )
assume A1: g = f * p ; ::_thesis: Product g = Product f
set mL = the multF of L;
( the multF of L is commutative & the multF of L is associative ) by MONOID_0:def_11;
hence Product g = Product f by A1, FINSOP_1:7; ::_thesis: verum
end;
begin
definition
let L be non empty ZeroStr ;
let p be Polynomial of L;
attrp is non-zero means :Def5: :: UPROOTS:def 5
p <> 0_. L;
end;
:: deftheorem Def5 defines non-zero UPROOTS:def_5_:_
for L being non empty ZeroStr
for p being Polynomial of L holds
( p is non-zero iff p <> 0_. L );
theorem Th17: :: UPROOTS:17
for L being non empty ZeroStr
for p being Polynomial of L holds
( p is non-zero iff len p > 0 )
proof
let L be non empty ZeroStr ; ::_thesis: for p being Polynomial of L holds
( p is non-zero iff len p > 0 )
let p be Polynomial of L; ::_thesis: ( p is non-zero iff len p > 0 )
hereby ::_thesis: ( len p > 0 implies p is non-zero )
assume p is non-zero ; ::_thesis: len p > 0
then p <> 0_. L by Def5;
then len p <> 0 by POLYNOM4:5;
hence len p > 0 ; ::_thesis: verum
end;
assume len p > 0 ; ::_thesis: p is non-zero
then p <> 0_. L by POLYNOM4:3;
hence p is non-zero by Def5; ::_thesis: verum
end;
registration
let L be non trivial ZeroStr ;
cluster Relation-like NAT -defined the carrier of L -valued Function-like non empty total quasi_total finite-Support non-zero for Element of bool [:NAT, the carrier of L:];
existence
ex b1 being Polynomial of L st b1 is non-zero
proof
set a = the Element of NonZero L;
reconsider a = the Element of NonZero L as Element of L ;
take p = <%a%>; ::_thesis: p is non-zero
A1: ( not a in {(0. L)} & (0_. L) . 0 = 0. L ) by FUNCOP_1:7, XBOOLE_0:def_5;
p . 0 = a by POLYNOM5:32;
then p <> 0_. L by A1, TARSKI:def_1;
hence p is non-zero by Def5; ::_thesis: verum
end;
end;
registration
let L be non empty non degenerated multLoopStr_0 ;
let x be Element of L;
cluster<%x,(1. L)%> -> non-zero ;
correctness
coherence
<%x,(1. L)%> is non-zero ;
proof
len <%x,(1. L)%> = 2 by POLYNOM5:40;
hence <%x,(1. L)%> is non-zero by Th17; ::_thesis: verum
end;
end;
theorem Th18: :: UPROOTS:18
for L being non empty ZeroStr
for p being Polynomial of L st len p > 0 holds
p . ((len p) -' 1) <> 0. L
proof
let L be non empty ZeroStr ; ::_thesis: for p being Polynomial of L st len p > 0 holds
p . ((len p) -' 1) <> 0. L
let p be Polynomial of L; ::_thesis: ( len p > 0 implies p . ((len p) -' 1) <> 0. L )
assume len p > 0 ; ::_thesis: p . ((len p) -' 1) <> 0. L
then ex k being Nat st len p = k + 1 by NAT_1:6;
then len p = ((len p) -' 1) + 1 by NAT_D:34;
hence p . ((len p) -' 1) <> 0. L by ALGSEQ_1:10; ::_thesis: verum
end;
theorem Th19: :: UPROOTS:19
for L being non empty ZeroStr
for p being AlgSequence of L st len p = 1 holds
( p = <%(p . 0)%> & p . 0 <> 0. L )
proof
let L be non empty ZeroStr ; ::_thesis: for p being AlgSequence of L st len p = 1 holds
( p = <%(p . 0)%> & p . 0 <> 0. L )
let p be AlgSequence of L; ::_thesis: ( len p = 1 implies ( p = <%(p . 0)%> & p . 0 <> 0. L ) )
assume A1: len p = 1 ; ::_thesis: ( p = <%(p . 0)%> & p . 0 <> 0. L )
thus p = <%(p . 0)%> by A1, ALGSEQ_1:def_5; ::_thesis: p . 0 <> 0. L
hence p . 0 <> 0. L by A1, ALGSEQ_1:14; ::_thesis: verum
end;
theorem Th20: :: UPROOTS:20
for L being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of L holds p *' (0_. L) = 0_. L
proof
let L be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being Polynomial of L holds p *' (0_. L) = 0_. L
let p be Polynomial of L; ::_thesis: p *' (0_. L) = 0_. L
now__::_thesis:_for_i_being_Element_of_NAT_holds_(p_*'_(0_._L))_._i_=_(0_._L)_._i
let i be Element of NAT ; ::_thesis: (p *' (0_. L)) . i = (0_. L) . i
consider r being FinSequence of L such that
len r = i + 1 and
A1: (p *' (0_. L)) . i = Sum r and
A2: for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * ((0_. L) . ((i + 1) -' k)) by POLYNOM3:def_9;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_r_holds_
r_._k_=_0._L
let k be Element of NAT ; ::_thesis: ( k in dom r implies r . k = 0. L )
assume k in dom r ; ::_thesis: r . k = 0. L
hence r . k = (p . (k -' 1)) * ((0_. L) . ((i + 1) -' k)) by A2
.= (p . (k -' 1)) * (0. L) by FUNCOP_1:7
.= 0. L by VECTSP_1:6 ;
::_thesis: verum
end;
hence (p *' (0_. L)) . i = 0. L by A1, POLYNOM3:1
.= (0_. L) . i by FUNCOP_1:7 ;
::_thesis: verum
end;
hence p *' (0_. L) = 0_. L by FUNCT_2:63; ::_thesis: verum
end;
registration
cluster non empty non degenerated right_complementable unital associative commutative distributive Abelian add-associative right_zeroed domRing-like algebraic-closed for doubleLoopStr ;
existence
ex b1 being non empty unital doubleLoopStr st
( b1 is algebraic-closed & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is Abelian & b1 is commutative & b1 is associative & b1 is distributive & b1 is domRing-like & not b1 is degenerated )
proof
take F_Complex ; ::_thesis: ( F_Complex is algebraic-closed & F_Complex is add-associative & F_Complex is right_zeroed & F_Complex is right_complementable & F_Complex is Abelian & F_Complex is commutative & F_Complex is associative & F_Complex is distributive & F_Complex is domRing-like & not F_Complex is degenerated )
thus ( F_Complex is algebraic-closed & F_Complex is add-associative & F_Complex is right_zeroed & F_Complex is right_complementable & F_Complex is Abelian & F_Complex is commutative & F_Complex is associative & F_Complex is distributive & F_Complex is domRing-like & not F_Complex is degenerated ) ; ::_thesis: verum
end;
end;
theorem Th21: :: UPROOTS:21
for L being non empty right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr
for p, q being Polynomial of L holds
( not p *' q = 0_. L or p = 0_. L or q = 0_. L )
proof
let L be non empty right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for p, q being Polynomial of L holds
( not p *' q = 0_. L or p = 0_. L or q = 0_. L )
let p, q be Polynomial of L; ::_thesis: ( not p *' q = 0_. L or p = 0_. L or q = 0_. L )
assume that
A1: p *' q = 0_. L and
A2: p <> 0_. L and
A3: q <> 0_. L ; ::_thesis: contradiction
consider lp1 being Nat such that
A4: len p = lp1 + 1 by A2, NAT_1:6, POLYNOM4:5;
len p <> 0 by A2, POLYNOM4:5;
then A5: 0 + 1 <= len p by NAT_1:13;
consider lq1 being Nat such that
A6: len q = lq1 + 1 by A3, NAT_1:6, POLYNOM4:5;
reconsider lp1 = lp1, lq1 = lq1 as Element of NAT by ORDINAL1:def_12;
A7: p . lp1 <> 0. L by A4, ALGSEQ_1:10;
A8: q . lq1 <> 0. L by A6, ALGSEQ_1:10;
set lpq = lp1 + lq1;
consider r being FinSequence of L such that
A9: len r = (lp1 + lq1) + 1 and
A10: (p *' q) . (lp1 + lq1) = Sum r and
A11: for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . (((lp1 + lq1) + 1) -' k)) by POLYNOM3:def_9;
A12: ((lp1 + lq1) + 1) -' (len p) = (lq1 + (lp1 + 1)) -' (len p)
.= lq1 by A4, NAT_D:34 ;
len p <= (lp1 + 1) + lq1 by A4, NAT_1:12;
then A13: len p in dom r by A9, A5, FINSEQ_3:25;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_r_&_k_<>_len_p_holds_
r_._k_=_0._L
let k be Nat; ::_thesis: ( k in dom r & k <> len p implies r . b1 = 0. L )
assume that
A14: k in dom r and
A15: k <> len p ; ::_thesis: r . b1 = 0. L
reconsider k1 = k as Element of NAT by ORDINAL1:def_12;
A16: r . k1 = (p . (k1 -' 1)) * (q . (((lp1 + lq1) + 1) -' k1)) by A11, A14;
percases ( k < len p or k > len p ) by A15, XXREAL_0:1;
suppose k < len p ; ::_thesis: r . b1 = 0. L
then consider d being Element of NAT such that
A17: len p = k1 + d and
A18: 1 <= d by FINSEQ_4:84;
A19: len q <= lq1 + d by A6, A18, XREAL_1:6;
((lp1 + lq1) + 1) -' k = ((lq1 + d) + k) -' k by A4, A17
.= lq1 + d by NAT_D:34 ;
hence r . k = (p . (k -' 1)) * (0. L) by A16, A19, ALGSEQ_1:8
.= 0. L by VECTSP_1:6 ;
::_thesis: verum
end;
suppose k > len p ; ::_thesis: r . b1 = 0. L
then k >= (len p) + 1 by NAT_1:13;
then k -' 1 >= ((len p) + 1) -' 1 by NAT_D:42;
then k -' 1 >= len p by NAT_D:34;
hence r . k = (0. L) * (q . (((lp1 + lq1) + 1) -' k)) by A16, ALGSEQ_1:8
.= 0. L by VECTSP_1:7 ;
::_thesis: verum
end;
end;
end;
then Sum r = r . (len p) by A13, MATRIX_3:12
.= (p . ((len p) -' 1)) * (q . (((lp1 + lq1) + 1) -' (len p))) by A11, A13
.= (p . lp1) * (q . lq1) by A4, A12, NAT_D:34 ;
then Sum r <> 0. L by A7, A8, VECTSP_2:def_1;
hence contradiction by A1, A10, FUNCOP_1:7; ::_thesis: verum
end;
registration
let L be non empty right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr ;
cluster Polynom-Ring L -> domRing-like ;
correctness
coherence
Polynom-Ring L is domRing-like ;
proof
set PRL = 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) )
reconsider xp = x, yp = y as Polynomial of L by POLYNOM3:def_10;
A1: 0_. L = 0. (Polynom-Ring L) by POLYNOM3:def_10;
assume x * y = 0. (Polynom-Ring L) ; ::_thesis: ( x = 0. (Polynom-Ring L) or y = 0. (Polynom-Ring L) )
then xp *' yp = 0_. L by A1, POLYNOM3:def_10;
hence ( x = 0. (Polynom-Ring L) or y = 0. (Polynom-Ring L) ) by A1, Th21; ::_thesis: verum
end;
end;
registration
let L be domRing;
let p, q be non-zero Polynomial of L;
clusterp *' q -> non-zero ;
correctness
coherence
p *' q is non-zero ;
proof
( p <> 0_. L & q <> 0_. L ) by Def5;
then p *' q <> 0_. L by Th21;
hence p *' q is non-zero by Def5; ::_thesis: verum
end;
end;
theorem :: UPROOTS:22
for L being non degenerated comRing
for p, q being Polynomial of L holds (Roots p) \/ (Roots q) c= Roots (p *' q)
proof
let L be non degenerated comRing; ::_thesis: for p, q being Polynomial of L holds (Roots p) \/ (Roots q) c= Roots (p *' q)
let p, q be Polynomial of L; ::_thesis: (Roots p) \/ (Roots q) c= Roots (p *' q)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Roots p) \/ (Roots q) or x in Roots (p *' q) )
assume A1: x in (Roots p) \/ (Roots q) ; ::_thesis: x in Roots (p *' q)
percases ( x in Roots p or x in Roots q ) by A1, XBOOLE_0:def_3;
supposeA2: x in Roots p ; ::_thesis: x in Roots (p *' q)
then reconsider a = x as Element of L ;
a is_a_root_of p by A2, POLYNOM5:def_9;
then eval (p,a) = 0. L by POLYNOM5:def_6;
then (eval (p,a)) * (eval (q,a)) = 0. L by VECTSP_1:7;
then eval ((p *' q),a) = 0. L by POLYNOM4:24;
then a is_a_root_of p *' q by POLYNOM5:def_6;
hence x in Roots (p *' q) by POLYNOM5:def_9; ::_thesis: verum
end;
supposeA3: x in Roots q ; ::_thesis: x in Roots (p *' q)
then reconsider a = x as Element of L ;
a is_a_root_of q by A3, POLYNOM5:def_9;
then eval (q,a) = 0. L by POLYNOM5:def_6;
then (eval (p,a)) * (eval (q,a)) = 0. L by VECTSP_1:6;
then eval ((p *' q),a) = 0. L by POLYNOM4:24;
then a is_a_root_of p *' q by POLYNOM5:def_6;
hence x in Roots (p *' q) by POLYNOM5:def_9; ::_thesis: verum
end;
end;
end;
theorem Th23: :: UPROOTS:23
for L being domRing
for p, q being Polynomial of L holds Roots (p *' q) = (Roots p) \/ (Roots q)
proof
let L be domRing; ::_thesis: for p, q being Polynomial of L holds Roots (p *' q) = (Roots p) \/ (Roots q)
let p, q be Polynomial of L; ::_thesis: Roots (p *' q) = (Roots p) \/ (Roots q)
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_Roots_(p_*'_q)_implies_x_in_(Roots_p)_\/_(Roots_q)_)_&_(_x_in_(Roots_p)_\/_(Roots_q)_implies_x_in_Roots_(p_*'_q)_)_)
let x be set ; ::_thesis: ( ( x in Roots (p *' q) implies x in (Roots p) \/ (Roots q) ) & ( x in (Roots p) \/ (Roots q) implies b1 in Roots (p *' q) ) )
hereby ::_thesis: ( x in (Roots p) \/ (Roots q) implies b1 in Roots (p *' q) )
assume A1: x in Roots (p *' q) ; ::_thesis: x in (Roots p) \/ (Roots q)
then reconsider a = x as Element of L ;
a is_a_root_of p *' q by A1, POLYNOM5:def_9;
then eval ((p *' q),a) = 0. L by POLYNOM5:def_6;
then A2: (eval (p,a)) * (eval (q,a)) = 0. L by POLYNOM4:24;
percases ( eval (p,a) = 0. L or eval (q,a) = 0. L ) by A2, VECTSP_2:def_1;
suppose eval (p,a) = 0. L ; ::_thesis: x in (Roots p) \/ (Roots q)
then a is_a_root_of p by POLYNOM5:def_6;
then a in Roots p by POLYNOM5:def_9;
hence x in (Roots p) \/ (Roots q) by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose eval (q,a) = 0. L ; ::_thesis: x in (Roots p) \/ (Roots q)
then a is_a_root_of q by POLYNOM5:def_6;
then a in Roots q by POLYNOM5:def_9;
hence x in (Roots p) \/ (Roots q) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
assume A3: x in (Roots p) \/ (Roots q) ; ::_thesis: b1 in Roots (p *' q)
percases ( x in Roots p or x in Roots q ) by A3, XBOOLE_0:def_3;
supposeA4: x in Roots p ; ::_thesis: b1 in Roots (p *' q)
then reconsider a = x as Element of L ;
a is_a_root_of p by A4, POLYNOM5:def_9;
then eval (p,a) = 0. L by POLYNOM5:def_6;
then (eval (p,a)) * (eval (q,a)) = 0. L by VECTSP_1:7;
then eval ((p *' q),a) = 0. L by POLYNOM4:24;
then a is_a_root_of p *' q by POLYNOM5:def_6;
hence x in Roots (p *' q) by POLYNOM5:def_9; ::_thesis: verum
end;
supposeA5: x in Roots q ; ::_thesis: b1 in Roots (p *' q)
then reconsider a = x as Element of L ;
a is_a_root_of q by A5, POLYNOM5:def_9;
then eval (q,a) = 0. L by POLYNOM5:def_6;
then (eval (p,a)) * (eval (q,a)) = 0. L by VECTSP_1:6;
then eval ((p *' q),a) = 0. L by POLYNOM4:24;
then a is_a_root_of p *' q by POLYNOM5:def_6;
hence x in Roots (p *' q) by POLYNOM5:def_9; ::_thesis: verum
end;
end;
end;
hence Roots (p *' q) = (Roots p) \/ (Roots q) by TARSKI:1; ::_thesis: verum
end;
theorem Th24: :: UPROOTS:24
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of L
for pc being Element of (Polynom-Ring L) st p = pc holds
- p = - pc
proof
let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being Polynomial of L
for pc being Element of (Polynom-Ring L) st p = pc holds
- p = - pc
let p be Polynomial of L; ::_thesis: for pc being Element of (Polynom-Ring L) st p = pc holds
- p = - pc
let pc be Element of (Polynom-Ring L); ::_thesis: ( p = pc implies - p = - pc )
assume A1: p = pc ; ::_thesis: - p = - pc
set PRL = Polynom-Ring L;
reconsider mpc = - p as Element of (Polynom-Ring L) by POLYNOM3:def_10;
p + (- p) = p - p
.= 0_. L by POLYNOM3:29 ;
then pc + mpc = 0_. L by A1, POLYNOM3:def_10
.= 0. (Polynom-Ring L) by POLYNOM3:def_10 ;
hence - p = - pc by RLVECT_1:def_10; ::_thesis: verum
end;
theorem Th25: :: UPROOTS:25
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of L
for pc, qc being Element of (Polynom-Ring L) st p = pc & q = qc holds
p - q = pc - qc
proof
let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q being Polynomial of L
for pc, qc being Element of (Polynom-Ring L) st p = pc & q = qc holds
p - q = pc - qc
let p, q be Polynomial of L; ::_thesis: for pc, qc being Element of (Polynom-Ring L) st p = pc & q = qc holds
p - q = pc - qc
let pc, qc be Element of (Polynom-Ring L); ::_thesis: ( p = pc & q = qc implies p - q = pc - qc )
assume that
A1: p = pc and
A2: q = qc ; ::_thesis: p - q = pc - qc
- q = - qc by A2, Th24;
hence p - q = pc - qc by A1, POLYNOM3:def_10; ::_thesis: verum
end;
theorem Th26: :: UPROOTS:26
for L being non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr
for p, q, r being Polynomial of L holds (p *' q) - (p *' r) = p *' (q - r)
proof
let L be non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q, r being Polynomial of L holds (p *' q) - (p *' r) = p *' (q - r)
let p, q, r be Polynomial of L; ::_thesis: (p *' q) - (p *' r) = p *' (q - r)
set PRL = Polynom-Ring L;
reconsider pc = p, qc = q, rc = r as Element of (Polynom-Ring L) by POLYNOM3:def_10;
A1: qc - rc = q - r by Th25;
( p *' q = pc * qc & p *' r = pc * rc ) by POLYNOM3:def_10;
hence (p *' q) - (p *' r) = (pc * qc) - (pc * rc) by Th25
.= pc * (qc - rc) by VECTSP_1:11
.= p *' (q - r) by A1, POLYNOM3:def_10 ;
::_thesis: verum
end;
theorem Th27: :: UPROOTS:27
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of L st p - q = 0_. L holds
p = q
proof
let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q being Polynomial of L st p - q = 0_. L holds
p = q
let q, r be Polynomial of L; ::_thesis: ( q - r = 0_. L implies q = r )
set PRL = Polynom-Ring L;
reconsider qc = q, rc = r as Element of (Polynom-Ring L) by POLYNOM3:def_10;
assume A1: q - r = 0_. L ; ::_thesis: q = r
0_. L = 0. (Polynom-Ring L) by POLYNOM3:def_10;
then qc - rc = 0. (Polynom-Ring L) by A1, Th25;
hence q = r by VECTSP_1:27; ::_thesis: verum
end;
theorem Th28: :: UPROOTS:28
for L being non empty right_complementable distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr
for p, q, r being Polynomial of L st p <> 0_. L & p *' q = p *' r holds
q = r
proof
let L be non empty right_complementable distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for p, q, r being Polynomial of L st p <> 0_. L & p *' q = p *' r holds
q = r
let p, q, r be Polynomial of L; ::_thesis: ( p <> 0_. L & p *' q = p *' r implies q = r )
assume A1: p <> 0_. L ; ::_thesis: ( not p *' q = p *' r or q = r )
assume p *' q = p *' r ; ::_thesis: q = r
then (p *' q) - (p *' r) = 0_. L by POLYNOM3:29;
then p *' (q - r) = 0_. L by Th26;
then q - r = 0_. L by A1, Th21;
hence q = r by Th27; ::_thesis: verum
end;
theorem Th29: :: UPROOTS:29
for L being domRing
for n being Element of NAT
for p being Polynomial of L st p <> 0_. L holds
p `^ n <> 0_. L
proof
let L be domRing; ::_thesis: for n being Element of NAT
for p being Polynomial of L st p <> 0_. L holds
p `^ n <> 0_. L
let n be Element of NAT ; ::_thesis: for p being Polynomial of L st p <> 0_. L holds
p `^ n <> 0_. L
let p be Polynomial of L; ::_thesis: ( p <> 0_. L implies p `^ n <> 0_. L )
defpred S1[ Element of NAT ] means p `^ $1 <> 0_. L;
assume A1: p <> 0_. L ; ::_thesis: p `^ n <> 0_. L
A2: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A3: S1[n] ; ::_thesis: S1[n + 1]
p `^ (n + 1) = (p `^ n) *' p by POLYNOM5:19;
hence S1[n + 1] by A1, A3, Th21; ::_thesis: verum
end;
( (1_. L) . 0 = 1. L & (0_. L) . 0 = 0. L ) by FUNCOP_1:7, POLYNOM3:30;
then A4: S1[ 0 ] by POLYNOM5:15;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2);
hence p `^ n <> 0_. L ; ::_thesis: verum
end;
theorem Th30: :: UPROOTS:30
for L being comRing
for i, j being Element of NAT
for p being Polynomial of L holds (p `^ i) *' (p `^ j) = p `^ (i + j)
proof
let L be comRing; ::_thesis: for i, j being Element of NAT
for p being Polynomial of L holds (p `^ i) *' (p `^ j) = p `^ (i + j)
let i, j be Element of NAT ; ::_thesis: for p being Polynomial of L holds (p `^ i) *' (p `^ j) = p `^ (i + j)
let p be Polynomial of L; ::_thesis: (p `^ i) *' (p `^ j) = p `^ (i + j)
defpred S1[ Element of NAT ] means (p `^ i) *' (p `^ $1) = p `^ (i + $1);
A1: for j being Element of NAT st S1[j] holds
S1[j + 1]
proof
let j be Element of NAT ; ::_thesis: ( S1[j] implies S1[j + 1] )
assume A2: S1[j] ; ::_thesis: S1[j + 1]
(p `^ i) *' (p `^ (j + 1)) = (p `^ i) *' ((p `^ j) *' p) by POLYNOM5:19
.= (p `^ (i + j)) *' p by A2, POLYNOM3:33
.= p `^ ((i + j) + 1) by POLYNOM5:19
.= p `^ (i + (j + 1)) ;
hence S1[j + 1] ; ::_thesis: verum
end;
(p `^ i) *' (p `^ 0) = (p `^ i) *' (1_. L) by POLYNOM5:15
.= p `^ (i + 0) by POLYNOM3:35 ;
then A3: S1[ 0 ] ;
for j being Element of NAT holds S1[j] from NAT_1:sch_1(A3, A1);
hence (p `^ i) *' (p `^ j) = p `^ (i + j) ; ::_thesis: verum
end;
theorem Th31: :: UPROOTS:31
for L being non empty multLoopStr_0 holds 1_. L = <%(1. L)%>
proof
let L be non empty multLoopStr_0 ; ::_thesis: 1_. L = <%(1. L)%>
A1: dom (0_. L) = NAT by FUNCT_2:def_1;
now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
(1_._L)_._x_=_<%(1._L)%>_._x
let x be set ; ::_thesis: ( x in NAT implies (1_. L) . b1 = <%(1. L)%> . b1 )
assume x in NAT ; ::_thesis: (1_. L) . b1 = <%(1. L)%> . b1
then reconsider n = x as Element of NAT ;
percases ( x = 0 or n <> 0 ) ;
supposeA2: x = 0 ; ::_thesis: (1_. L) . b1 = <%(1. L)%> . b1
hence (1_. L) . x = 1. L by A1, FUNCT_7:31
.= <%(1. L)%> . x by A2, ALGSEQ_1:def_5 ;
::_thesis: verum
end;
supposeA3: n <> 0 ; ::_thesis: (1_. L) . b1 = <%(1. L)%> . b1
then A4: ( n = 1 or n > 1 ) by NAT_1:53;
thus (1_. L) . x = (0_. L) . n by A3, FUNCT_7:32
.= 0. L by FUNCOP_1:7
.= <%(1. L)%> . x by A4, POLYNOM5:32 ; ::_thesis: verum
end;
end;
end;
hence 1_. L = <%(1. L)%> by FUNCT_2:12; ::_thesis: verum
end;
theorem :: UPROOTS:32
for L being non empty right_complementable right-distributive well-unital add-associative right_zeroed doubleLoopStr
for p being Polynomial of L holds p *' <%(1. L)%> = p
proof
let L be non empty right_complementable right-distributive well-unital add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being Polynomial of L holds p *' <%(1. L)%> = p
let p be Polynomial of L; ::_thesis: p *' <%(1. L)%> = p
thus p *' <%(1. L)%> = p *' (1_. L) by Th31
.= p by POLYNOM3:35 ; ::_thesis: verum
end;
theorem Th33: :: UPROOTS:33
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of L st ( len p = 0 or len q = 0 ) holds
len (p *' q) = 0
proof
let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q being Polynomial of L st ( len p = 0 or len q = 0 ) holds
len (p *' q) = 0
let p, q be Polynomial of L; ::_thesis: ( ( len p = 0 or len q = 0 ) implies len (p *' q) = 0 )
assume A1: ( len p = 0 or len q = 0 ) ; ::_thesis: len (p *' q) = 0
percases ( len p = 0 or len q = 0 ) by A1;
suppose len p = 0 ; ::_thesis: len (p *' q) = 0
then p = 0_. L by POLYNOM4:5;
then p *' q = 0_. L by POLYNOM4:2;
hence len (p *' q) = 0 by POLYNOM4:3; ::_thesis: verum
end;
suppose len q = 0 ; ::_thesis: len (p *' q) = 0
then q = 0_. L by POLYNOM4:5;
then p *' q = 0_. L by Th20;
hence len (p *' q) = 0 by POLYNOM4:3; ::_thesis: verum
end;
end;
end;
theorem Th34: :: UPROOTS:34
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of L st p *' q is non-zero holds
( p is non-zero & q is non-zero )
proof
let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q being Polynomial of L st p *' q is non-zero holds
( p is non-zero & q is non-zero )
let p, q be Polynomial of L; ::_thesis: ( p *' q is non-zero implies ( p is non-zero & q is non-zero ) )
assume that
A1: p *' q is non-zero and
A2: ( not p is non-zero or not q is non-zero ) ; ::_thesis: contradiction
( len p = 0 or len q = 0 ) by A2, Th17;
then len (p *' q) = 0 by Th33;
hence contradiction by A1, Th17; ::_thesis: verum
end;
theorem :: UPROOTS:35
for L being non empty right_complementable associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of L st (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. L holds
0 < len (p *' q)
proof
let L be non empty right_complementable associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q being Polynomial of L st (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. L holds
0 < len (p *' q)
let p, q be Polynomial of L; ::_thesis: ( (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. L implies 0 < len (p *' q) )
assume A1: (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. L ; ::_thesis: 0 < len (p *' q)
now__::_thesis:_not_len_q_<=_0
assume len q <= 0 ; ::_thesis: contradiction
then len q = 0 ;
then q = 0_. L by POLYNOM4:5;
then q . ((len q) -' 1) = 0. L by FUNCOP_1:7;
hence contradiction by A1, VECTSP_1:6; ::_thesis: verum
end;
then A2: 0 + 1 <= len q by NAT_1:13;
now__::_thesis:_not_len_p_<=_0
assume len p <= 0 ; ::_thesis: contradiction
then len p = 0 ;
then p = 0_. L by POLYNOM4:5;
then p . ((len p) -' 1) = 0. L by FUNCOP_1:7;
hence contradiction by A1, VECTSP_1:7; ::_thesis: verum
end;
then 0 + 1 <= len p by NAT_1:13;
then (len p) + (len q) >= 1 + 1 by A2, XREAL_1:7;
then ((len p) + (len q)) - 1 >= (1 + 1) - 1 by XREAL_1:9;
hence 0 < len (p *' q) by A1, POLYNOM4:10; ::_thesis: verum
end;
theorem Th36: :: UPROOTS:36
for L being non empty right_complementable associative commutative well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p, q being Polynomial of L st 1 < len p & 1 < len q holds
len p < len (p *' q)
proof
let L be non empty right_complementable associative commutative well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for p, q being Polynomial of L st 1 < len p & 1 < len q holds
len p < len (p *' q)
let p, q be Polynomial of L; ::_thesis: ( 1 < len p & 1 < len q implies len p < len (p *' q) )
assume that
A1: 1 < len p and
A2: 1 < len q ; ::_thesis: len p < len (p *' q)
( p . ((len p) -' 1) <> 0. L & q . ((len q) -' 1) <> 0. L ) by A1, A2, Th18;
then (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. L by VECTSP_2:def_1;
then A3: len (p *' q) = ((len p) + (len q)) - 1 by POLYNOM4:10;
(len q) - 1 > 1 - 1 by A2, XREAL_1:14;
then (len p) + ((len q) - 1) > 0 + (len p) by XREAL_1:8;
hence len p < len (p *' q) by A3; ::_thesis: verum
end;
theorem Th37: :: UPROOTS:37
for L being non empty right_complementable left-distributive add-associative right_zeroed doubleLoopStr
for a, b being Element of L
for p being Polynomial of L holds
( (<%a,b%> *' p) . 0 = a * (p . 0) & ( for i being Nat holds (<%a,b%> *' p) . (i + 1) = (a * (p . (i + 1))) + (b * (p . i)) ) )
proof
let L be non empty right_complementable left-distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for a, b being Element of L
for p being Polynomial of L holds
( (<%a,b%> *' p) . 0 = a * (p . 0) & ( for i being Nat holds (<%a,b%> *' p) . (i + 1) = (a * (p . (i + 1))) + (b * (p . i)) ) )
let a, b be Element of L; ::_thesis: for p being Polynomial of L holds
( (<%a,b%> *' p) . 0 = a * (p . 0) & ( for i being Nat holds (<%a,b%> *' p) . (i + 1) = (a * (p . (i + 1))) + (b * (p . i)) ) )
let q be Polynomial of L; ::_thesis: ( (<%a,b%> *' q) . 0 = a * (q . 0) & ( for i being Nat holds (<%a,b%> *' q) . (i + 1) = (a * (q . (i + 1))) + (b * (q . i)) ) )
set p = <%a,b%>;
consider r being FinSequence of L such that
A1: len r = 0 + 1 and
A2: (<%a,b%> *' q) . 0 = Sum r and
A3: for k being Element of NAT st k in dom r holds
r . k = (<%a,b%> . (k -' 1)) * (q . ((0 + 1) -' k)) by POLYNOM3:def_9;
A4: 1 in dom r by A1, FINSEQ_3:25;
then reconsider r1 = r . 1 as Element of L by FINSEQ_2:11;
r = <*r1*> by A1, FINSEQ_1:40;
then Sum r = r1 by RLVECT_1:44
.= (<%a,b%> . (1 -' 1)) * (q . ((0 + 1) -' 1)) by A3, A4
.= (<%a,b%> . 0) * (q . ((0 + 1) -' 1)) by XREAL_1:232
.= (<%a,b%> . 0) * (q . 0) by NAT_D:34 ;
hence (<%a,b%> *' q) . 0 = a * (q . 0) by A2, POLYNOM5:38; ::_thesis: for i being Nat holds (<%a,b%> *' q) . (i + 1) = (a * (q . (i + 1))) + (b * (q . i))
let i be Nat; ::_thesis: (<%a,b%> *' q) . (i + 1) = (a * (q . (i + 1))) + (b * (q . i))
consider r being FinSequence of L such that
A5: len r = (i + 1) + 1 and
A6: (<%a,b%> *' q) . (i + 1) = Sum r and
A7: for k being Element of NAT st k in dom r holds
r . k = (<%a,b%> . (k -' 1)) * (q . (((i + 1) + 1) -' k)) by POLYNOM3:def_9;
len r = i + 2 by A5;
then A8: 0 + 2 <= len r by XREAL_1:6;
then A9: 2 in dom r by FINSEQ_3:25;
then A10: r /. 2 = r . 2 by PARTFUN1:def_6
.= (<%a,b%> . ((1 + 1) -' 1)) * (q . (((i + 1) + 1) -' 2)) by A7, A9
.= (<%a,b%> . 1) * (q . (((i + 1) + 1) -' 2)) by NAT_D:34
.= b * (q . ((i + (1 + 1)) -' 2)) by POLYNOM5:38
.= b * (q . i) by NAT_D:34 ;
A11: now__::_thesis:_for_k_being_Element_of_NAT_st_2_<_k_&_k_in_dom_r_holds_
r_._k_=_0._L
let k be Element of NAT ; ::_thesis: ( 2 < k & k in dom r implies r . k = 0. L )
assume that
A12: 2 < k and
A13: k in dom r ; ::_thesis: r . k = 0. L
consider k1 being Nat such that
A14: k = k1 + 1 by A12, NAT_1:6;
A15: 2 <= k1 by A12, A14, NAT_1:13;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def_12;
thus r . k = (<%a,b%> . (k -' 1)) * (q . (((i + 1) + 1) -' k)) by A7, A13
.= (<%a,b%> . k1) * (q . (((i + 1) + 1) -' k)) by A14, NAT_D:34
.= (0. L) * (q . (((i + 1) + 1) -' k)) by A15, POLYNOM5:38
.= 0. L by VECTSP_1:7 ; ::_thesis: verum
end;
1 <= len r by A8, XXREAL_0:2;
then A16: 1 in dom r by FINSEQ_3:25;
then r /. 1 = r . 1 by PARTFUN1:def_6
.= (<%a,b%> . (1 -' 1)) * (q . (((i + 1) + 1) -' 1)) by A7, A16
.= (<%a,b%> . 0) * (q . (((i + 1) + 1) -' 1)) by XREAL_1:232
.= (<%a,b%> . 0) * (q . (i + 1)) by NAT_D:34
.= a * (q . (i + 1)) by POLYNOM5:38 ;
hence (<%a,b%> *' q) . (i + 1) = (a * (q . (i + 1))) + (b * (q . i)) by A6, A8, A10, A11, Th2; ::_thesis: verum
end;
theorem Th38: :: UPROOTS:38
for L being non empty non degenerated right_complementable associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for r being Element of L
for q being non-zero Polynomial of L holds len (<%r,(1. L)%> *' q) = (len q) + 1
proof
let L be non empty non degenerated right_complementable associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for r being Element of L
for q being non-zero Polynomial of L holds len (<%r,(1. L)%> *' q) = (len q) + 1
let r be Element of L; ::_thesis: for q being non-zero Polynomial of L holds len (<%r,(1. L)%> *' q) = (len q) + 1
let q be non-zero Polynomial of L; ::_thesis: len (<%r,(1. L)%> *' q) = (len q) + 1
set p = <%r,(1. L)%>;
A1: (<%r,(1. L)%> . ((len <%r,(1. L)%>) -' 1)) * (q . ((len q) -' 1)) = (<%r,(1. L)%> . ((1 + 1) -' 1)) * (q . ((len q) -' 1)) by POLYNOM5:40
.= (<%r,(1. L)%> . 1) * (q . ((len q) -' 1)) by NAT_D:34
.= (1. L) * (q . ((len q) -' 1)) by POLYNOM5:38
.= q . ((len q) -' 1) by VECTSP_1:def_8 ;
( len <%r,(1. L)%> = 2 & len q > 0 ) by Th17, POLYNOM5:40;
hence len (<%r,(1. L)%> *' q) = ((len q) + (1 + 1)) - 1 by A1, Th18, POLYNOM4:10
.= (len q) + 1 ;
::_thesis: verum
end;
theorem Th39: :: UPROOTS:39
for L being non degenerated comRing
for x being Element of L
for i being Element of NAT holds len (<%x,(1. L)%> `^ i) = i + 1
proof
let L be non degenerated comRing; ::_thesis: for x being Element of L
for i being Element of NAT holds len (<%x,(1. L)%> `^ i) = i + 1
let x be Element of L; ::_thesis: for i being Element of NAT holds len (<%x,(1. L)%> `^ i) = i + 1
defpred S1[ Element of NAT ] means len (<%x,(1. L)%> `^ $1) = $1 + 1;
set r = <%x,(1. L)%>;
A1: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A2: S1[i] ; ::_thesis: S1[i + 1]
reconsider ri = <%x,(1. L)%> `^ i as non-zero Polynomial of L by A2, Th17;
thus len (<%x,(1. L)%> `^ (i + 1)) = len ((<%x,(1. L)%> `^ 1) *' ri) by Th30
.= len (<%x,(1. L)%> *' ri) by POLYNOM5:16
.= (i + 1) + 1 by A2, Th38 ; ::_thesis: verum
end;
<%x,(1. L)%> `^ 0 = 1_. L by POLYNOM5:15;
then A3: S1[ 0 ] by POLYNOM4:4;
thus for i being Element of NAT holds S1[i] from NAT_1:sch_1(A3, A1); ::_thesis: verum
end;
registration
let L be non degenerated comRing;
let x be Element of L;
let n be Element of NAT ;
cluster<%x,(1. L)%> `^ n -> non-zero ;
correctness
coherence
<%x,(1. L)%> `^ n is non-zero ;
proof
len (<%x,(1. L)%> `^ n) = n + 1 by Th39;
hence <%x,(1. L)%> `^ n is non-zero by Th17; ::_thesis: verum
end;
end;
theorem Th40: :: UPROOTS:40
for L being non degenerated comRing
for x being Element of L
for q being non-zero Polynomial of L
for i being Element of NAT holds len ((<%x,(1. L)%> `^ i) *' q) = i + (len q)
proof
let L be non degenerated comRing; ::_thesis: for x being Element of L
for q being non-zero Polynomial of L
for i being Element of NAT holds len ((<%x,(1. L)%> `^ i) *' q) = i + (len q)
let x be Element of L; ::_thesis: for q being non-zero Polynomial of L
for i being Element of NAT holds len ((<%x,(1. L)%> `^ i) *' q) = i + (len q)
let q be non-zero Polynomial of L; ::_thesis: for i being Element of NAT holds len ((<%x,(1. L)%> `^ i) *' q) = i + (len q)
set r = <%x,(1. L)%>;
defpred S1[ Element of NAT ] means len ((<%x,(1. L)%> `^ $1) *' q) = $1 + (len q);
A1: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A2: S1[i] ; ::_thesis: S1[i + 1]
len q > 0 by Th17;
then A3: (<%x,(1. L)%> `^ i) *' q is non-zero by A2, Th17;
thus len ((<%x,(1. L)%> `^ (i + 1)) *' q) = len (((<%x,(1. L)%> `^ 1) *' (<%x,(1. L)%> `^ i)) *' q) by Th30
.= len ((<%x,(1. L)%> *' (<%x,(1. L)%> `^ i)) *' q) by POLYNOM5:16
.= len (<%x,(1. L)%> *' ((<%x,(1. L)%> `^ i) *' q)) by POLYNOM3:33
.= (i + (len q)) + 1 by A2, A3, Th38
.= (i + 1) + (len q) ; ::_thesis: verum
end;
len ((<%x,(1. L)%> `^ 0) *' q) = len ((1_. L) *' q) by POLYNOM5:15
.= 0 + (len q) by POLYNOM3:35 ;
then A4: S1[ 0 ] ;
thus for i being Element of NAT holds S1[i] from NAT_1:sch_1(A4, A1); ::_thesis: verum
end;
theorem Th41: :: UPROOTS:41
for L being non empty non degenerated right_complementable associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for r being Element of L
for p, q being Polynomial of L st p = <%r,(1. L)%> *' q & p . ((len p) -' 1) = 1. L holds
q . ((len q) -' 1) = 1. L
proof
let L be non empty non degenerated right_complementable associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for r being Element of L
for p, q being Polynomial of L st p = <%r,(1. L)%> *' q & p . ((len p) -' 1) = 1. L holds
q . ((len q) -' 1) = 1. L
let x be Element of L; ::_thesis: for p, q being Polynomial of L st p = <%x,(1. L)%> *' q & p . ((len p) -' 1) = 1. L holds
q . ((len q) -' 1) = 1. L
let p, q be Polynomial of L; ::_thesis: ( p = <%x,(1. L)%> *' q & p . ((len p) -' 1) = 1. L implies q . ((len q) -' 1) = 1. L )
assume that
A1: p = <%x,(1. L)%> *' q and
A2: p . ((len p) -' 1) = 1. L ; ::_thesis: q . ((len q) -' 1) = 1. L
set lp1 = (len p) -' 1;
A3: now__::_thesis:_not_q_=_0_._L
assume q = 0_. L ; ::_thesis: contradiction
then p = 0_. L by A1, POLYNOM3:34;
hence contradiction by A2, FUNCOP_1:7; ::_thesis: verum
end;
then q is non-zero by Def5;
then len p = (len q) + 1 by A1, Th38;
then A4: (len p) -' 1 = len q by NAT_D:34;
then consider lp2 being Nat such that
A5: (len p) -' 1 = lp2 + 1 by A3, NAT_1:6, POLYNOM4:5;
reconsider lp2 = lp2 as Element of NAT by ORDINAL1:def_12;
A6: q . ((len p) -' 1) = 0. L by A4, ALGSEQ_1:8;
(<%x,(1. L)%> *' q) . ((len p) -' 1) = (x * (q . ((len p) -' 1))) + ((1. L) * (q . lp2)) by A5, Th37
.= (0. L) + ((1. L) * (q . lp2)) by A6, VECTSP_1:6
.= (1. L) * (q . lp2) by RLVECT_1:4
.= q . lp2 by VECTSP_1:def_8 ;
hence q . ((len q) -' 1) = 1. L by A1, A2, A4, A5, NAT_D:34; ::_thesis: verum
end;
begin
definition
let L be non empty ZeroStr ;
let p be Polynomial of L;
let n be Nat;
func poly_shift (p,n) -> Polynomial of L means :Def6: :: UPROOTS:def 6
for i being Nat holds it . i = p . (n + i);
existence
ex b1 being Polynomial of L st
for i being Nat holds b1 . i = p . (n + i)
proof
deffunc H1( Nat) -> Element of the carrier of L = p . (n + $1);
consider ps being AlgSequence of L such that
A1: len ps <= len p and
A2: for k being Nat st k < len p holds
ps . k = H1(k) from ALGSEQ_1:sch_1();
take ps ; ::_thesis: for i being Nat holds ps . i = p . (n + i)
let i be Nat; ::_thesis: ps . i = p . (n + i)
percases ( i < len p or i >= len p ) ;
suppose i < len p ; ::_thesis: ps . i = p . (n + i)
hence ps . i = p . (n + i) by A2; ::_thesis: verum
end;
supposeA3: i >= len p ; ::_thesis: ps . i = p . (n + i)
hence ps . i = 0. L by A1, ALGSEQ_1:8, XXREAL_0:2
.= p . (n + i) by A3, ALGSEQ_1:8, NAT_1:12 ;
::_thesis: verum
end;
end;
end;
uniqueness
for b1, b2 being Polynomial of L st ( for i being Nat holds b1 . i = p . (n + i) ) & ( for i being Nat holds b2 . i = p . (n + i) ) holds
b1 = b2
proof
let it1, it2 be Polynomial of L; ::_thesis: ( ( for i being Nat holds it1 . i = p . (n + i) ) & ( for i being Nat holds it2 . i = p . (n + i) ) implies it1 = it2 )
assume that
A4: for i being Nat holds it1 . i = p . (n + i) and
A5: for i being Nat holds it2 . i = p . (n + i) ; ::_thesis: it1 = it2
now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
it1_._x_=_it2_._x
let x be set ; ::_thesis: ( x in NAT implies it1 . x = it2 . x )
assume x in NAT ; ::_thesis: it1 . x = it2 . x
then reconsider i = x as Element of NAT ;
thus it1 . x = p . (n + i) by A4
.= it2 . x by A5 ; ::_thesis: verum
end;
hence it1 = it2 by FUNCT_2:12; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines poly_shift UPROOTS:def_6_:_
for L being non empty ZeroStr
for p being Polynomial of L
for n being Nat
for b4 being Polynomial of L holds
( b4 = poly_shift (p,n) iff for i being Nat holds b4 . i = p . (n + i) );
theorem Th42: :: UPROOTS:42
for L being non empty ZeroStr
for p being Polynomial of L holds poly_shift (p,0) = p
proof
let L be non empty ZeroStr ; ::_thesis: for p being Polynomial of L holds poly_shift (p,0) = p
let p be Polynomial of L; ::_thesis: poly_shift (p,0) = p
set ps = poly_shift (p,0);
now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
(poly_shift_(p,0))_._x_=_p_._x
let x be set ; ::_thesis: ( x in NAT implies (poly_shift (p,0)) . x = p . x )
assume x in NAT ; ::_thesis: (poly_shift (p,0)) . x = p . x
then reconsider i = x as Element of NAT ;
thus (poly_shift (p,0)) . x = p . (0 + i) by Def6
.= p . x ; ::_thesis: verum
end;
hence poly_shift (p,0) = p by FUNCT_2:12; ::_thesis: verum
end;
theorem Th43: :: UPROOTS:43
for L being non empty ZeroStr
for n being Element of NAT
for p being Polynomial of L st n >= len p holds
poly_shift (p,n) = 0_. L
proof
let L be non empty ZeroStr ; ::_thesis: for n being Element of NAT
for p being Polynomial of L st n >= len p holds
poly_shift (p,n) = 0_. L
let n be Element of NAT ; ::_thesis: for p being Polynomial of L st n >= len p holds
poly_shift (p,n) = 0_. L
let p be Polynomial of L; ::_thesis: ( n >= len p implies poly_shift (p,n) = 0_. L )
set ps = poly_shift (p,n);
assume A1: n >= len p ; ::_thesis: poly_shift (p,n) = 0_. L
A2: now__::_thesis:_for_z_being_set_st_z_in_dom_(poly_shift_(p,n))_holds_
(poly_shift_(p,n))_._z_=_0._L
let z be set ; ::_thesis: ( z in dom (poly_shift (p,n)) implies (poly_shift (p,n)) . z = 0. L )
assume z in dom (poly_shift (p,n)) ; ::_thesis: (poly_shift (p,n)) . z = 0. L
then reconsider i = z as Element of NAT ;
thus (poly_shift (p,n)) . z = p . (n + i) by Def6
.= 0. L by A1, ALGSEQ_1:8, NAT_1:12 ; ::_thesis: verum
end;
dom (poly_shift (p,n)) = NAT by FUNCT_2:def_1;
hence poly_shift (p,n) = 0_. L by A2, FUNCOP_1:11; ::_thesis: verum
end;
theorem Th44: :: UPROOTS:44
for L being non empty non degenerated multLoopStr_0
for n being Element of NAT
for p being Polynomial of L st n <= len p holds
(len (poly_shift (p,n))) + n = len p
proof
let L be non empty non degenerated multLoopStr_0 ; ::_thesis: for n being Element of NAT
for p being Polynomial of L st n <= len p holds
(len (poly_shift (p,n))) + n = len p
let n be Element of NAT ; ::_thesis: for p being Polynomial of L st n <= len p holds
(len (poly_shift (p,n))) + n = len p
let p be Polynomial of L; ::_thesis: ( n <= len p implies (len (poly_shift (p,n))) + n = len p )
assume A1: n <= len p ; ::_thesis: (len (poly_shift (p,n))) + n = len p
set ps = poly_shift (p,n);
set lpn = (len p) - n;
n - n <= (len p) - n by A1, XREAL_1:9;
then reconsider lpn = (len p) - n as Element of NAT by INT_1:3;
A2: now__::_thesis:_for_m_being_Nat_st_m_is_at_least_length_of_poly_shift_(p,n)_holds_
not_lpn_>_m
let m be Nat; ::_thesis: ( m is_at_least_length_of poly_shift (p,n) implies not lpn > m )
assume that
A3: m is_at_least_length_of poly_shift (p,n) and
A4: lpn > m ; ::_thesis: contradiction
lpn >= m + 1 by A4, NAT_1:13;
then A5: lpn - 1 >= (m + 1) - 1 by XREAL_1:9;
then reconsider lpn1 = lpn - 1 as Element of NAT by INT_1:3;
(n + lpn1) + 1 = len p ;
then A6: p . (n + lpn1) <> 0. L by ALGSEQ_1:10;
(poly_shift (p,n)) . lpn1 = p . (n + lpn1) by Def6;
hence contradiction by A3, A5, A6, ALGSEQ_1:def_2; ::_thesis: verum
end;
now__::_thesis:_for_i_being_Nat_st_i_>=_lpn_holds_
(poly_shift_(p,n))_._i_=_0._L
let i be Nat; ::_thesis: ( i >= lpn implies (poly_shift (p,n)) . i = 0. L )
assume i >= lpn ; ::_thesis: (poly_shift (p,n)) . i = 0. L
then A7: i + n >= len p by XREAL_1:20;
thus (poly_shift (p,n)) . i = p . (n + i) by Def6
.= 0. L by A7, ALGSEQ_1:8 ; ::_thesis: verum
end;
then lpn is_at_least_length_of poly_shift (p,n) by ALGSEQ_1:def_2;
hence (len (poly_shift (p,n))) + n = lpn + n by A2, ALGSEQ_1:def_3
.= len p ;
::_thesis: verum
end;
theorem Th45: :: UPROOTS:45
for L being non degenerated comRing
for x being Element of L
for n being Element of NAT
for p being Polynomial of L st n < len p holds
eval ((poly_shift (p,n)),x) = (x * (eval ((poly_shift (p,(n + 1))),x))) + (p . n)
proof
let L be non degenerated comRing; ::_thesis: for x being Element of L
for n being Element of NAT
for p being Polynomial of L st n < len p holds
eval ((poly_shift (p,n)),x) = (x * (eval ((poly_shift (p,(n + 1))),x))) + (p . n)
let x be Element of L; ::_thesis: for n being Element of NAT
for p being Polynomial of L st n < len p holds
eval ((poly_shift (p,n)),x) = (x * (eval ((poly_shift (p,(n + 1))),x))) + (p . n)
let n be Element of NAT ; ::_thesis: for p being Polynomial of L st n < len p holds
eval ((poly_shift (p,n)),x) = (x * (eval ((poly_shift (p,(n + 1))),x))) + (p . n)
let p be Polynomial of L; ::_thesis: ( n < len p implies eval ((poly_shift (p,n)),x) = (x * (eval ((poly_shift (p,(n + 1))),x))) + (p . n) )
assume A1: n < len p ; ::_thesis: eval ((poly_shift (p,n)),x) = (x * (eval ((poly_shift (p,(n + 1))),x))) + (p . n)
set ps = poly_shift (p,n);
set ps1 = poly_shift (p,(n + 1));
consider f being FinSequence of L such that
A2: eval ((poly_shift (p,n)),x) = Sum f and
A3: len f = len (poly_shift (p,n)) and
A4: for k being Element of NAT st k in dom f holds
f . k = ((poly_shift (p,n)) . (k -' 1)) * ((power L) . (x,(k -' 1))) by POLYNOM4:def_2;
consider f1 being FinSequence of L such that
A5: eval ((poly_shift (p,(n + 1))),x) = Sum f1 and
A6: len f1 = len (poly_shift (p,(n + 1))) and
A7: for k being Element of NAT st k in dom f1 holds
f1 . k = ((poly_shift (p,(n + 1))) . (k -' 1)) * ((power L) . (x,(k -' 1))) by POLYNOM4:def_2;
( rng f1 c= the carrier of L & dom (x multfield) = the carrier of L ) by FUNCT_2:def_1;
then A8: ( x * f1 = (x multfield) * f1 & dom ((x multfield) * f1) = dom f1 ) by FVSUM_1:def_6, RELAT_1:27;
A9: 1_ L = 1. L ;
now__::_thesis:_(_len_f_=_len_f_&_len_(<*(p_._n)*>_^_(x_*_f1))_=_len_f_&_(_for_j_being_Nat_st_j_in_dom_f_holds_
f_._j_=_(<*(p_._n)*>_^_(x_*_f1))_._j_)_)
A10: n + 1 <= len p by A1, NAT_1:13;
A11: ((len (poly_shift (p,(n + 1)))) + 1) + n = (len (poly_shift (p,(n + 1)))) + (n + 1)
.= len p by A10, Th44
.= (len (poly_shift (p,n))) + n by A1, Th44 ;
thus len f = len f ; ::_thesis: ( len (<*(p . n)*> ^ (x * f1)) = len f & ( for j being Nat st j in dom f holds
f . b2 = (<*(p . n)*> ^ (x * f1)) . b2 ) )
A12: len <*(p . n)*> = 1 by FINSEQ_1:40;
A13: len (x * f1) = len f1 by A8, FINSEQ_3:29;
hence len (<*(p . n)*> ^ (x * f1)) = len f by A3, A6, A11, A12, FINSEQ_1:22; ::_thesis: for j being Nat st j in dom f holds
f . b2 = (<*(p . n)*> ^ (x * f1)) . b2
let j be Nat; ::_thesis: ( j in dom f implies f . b1 = (<*(p . n)*> ^ (x * f1)) . b1 )
assume A14: j in dom f ; ::_thesis: f . b1 = (<*(p . n)*> ^ (x * f1)) . b1
A15: 1 <= j by A14, FINSEQ_3:25;
A16: j <= len f by A14, FINSEQ_3:25;
percases ( j = 1 or 1 < j ) by A15, XXREAL_0:1;
supposeA17: j = 1 ; ::_thesis: f . b1 = (<*(p . n)*> ^ (x * f1)) . b1
A18: 1 in dom <*(p . n)*> by A12, FINSEQ_3:25;
thus f . j = ((poly_shift (p,n)) . (1 -' 1)) * ((power L) . (x,(1 -' 1))) by A4, A14, A17
.= ((poly_shift (p,n)) . 0) * ((power L) . (x,(1 -' 1))) by XREAL_1:232
.= ((poly_shift (p,n)) . 0) * ((power L) . (x,0)) by XREAL_1:232
.= ((poly_shift (p,n)) . 0) * (1. L) by A9, GROUP_1:def_7
.= (poly_shift (p,n)) . 0 by A9, GROUP_1:def_4
.= p . (n + 0) by Def6
.= <*(p . n)*> . 1 by FINSEQ_1:40
.= (<*(p . n)*> ^ (x * f1)) . j by A17, A18, FINSEQ_1:def_7 ; ::_thesis: verum
end;
supposeA19: 1 < j ; ::_thesis: f . b1 = (<*(p . n)*> ^ (x * f1)) . b1
1 - 1 <= j - 1 by A15, XREAL_1:9;
then reconsider j1 = j - 1 as Element of NAT by INT_1:3;
A20: 1 + 1 <= j by A19, NAT_1:13;
then A21: (1 + 1) - 1 <= j - 1 by XREAL_1:9;
then ex j2 being Nat st j1 = j2 + 1 by NAT_1:6;
then A22: (j1 -' 1) + 1 = j1 by NAT_D:34;
j = j1 + 1 ;
then A23: j1 = j -' 1 by NAT_D:34;
j - 1 <= ((len f1) + 1) - 1 by A3, A6, A11, A16, XREAL_1:9;
then A24: j1 in dom f1 by A21, FINSEQ_3:25;
then reconsider f1j = f1 . j1 as Element of L by FINSEQ_2:11;
thus f . j = ((poly_shift (p,n)) . (j -' 1)) * ((power L) . (x,(j -' 1))) by A4, A14
.= (p . (n + j1)) * ((power L) . (x,j1)) by A23, Def6
.= (p . ((n + 1) + (j1 -' 1))) * (((power L) . (x,(j1 -' 1))) * x) by A22, GROUP_1:def_7
.= x * ((p . ((n + 1) + (j1 -' 1))) * ((power L) . (x,(j1 -' 1)))) by GROUP_1:def_3
.= x * (((poly_shift (p,(n + 1))) . (j1 -' 1)) * ((power L) . (x,(j1 -' 1)))) by Def6
.= x * f1j by A7, A24
.= (x * f1) . j1 by A8, A24, FVSUM_1:50
.= (<*(p . n)*> ^ (x * f1)) . j by A3, A6, A11, A12, A13, A16, A20, FINSEQ_1:23 ; ::_thesis: verum
end;
end;
end;
then ( x * (Sum f1) = Sum (x * f1) & f = <*(p . n)*> ^ (x * f1) ) by FINSEQ_2:9, FVSUM_1:73;
hence eval ((poly_shift (p,n)),x) = (x * (eval ((poly_shift (p,(n + 1))),x))) + (p . n) by A2, A5, FVSUM_1:72; ::_thesis: verum
end;
theorem Th46: :: UPROOTS:46
for L being non degenerated comRing
for p being Polynomial of L st len p = 1 holds
Roots p = {}
proof
let L be non degenerated comRing; ::_thesis: for p being Polynomial of L st len p = 1 holds
Roots p = {}
let p be Polynomial of L; ::_thesis: ( len p = 1 implies Roots p = {} )
assume len p = 1 ; ::_thesis: Roots p = {}
then A1: ( p = <%(p . 0)%> & p . 0 <> 0. L ) by Th19;
assume Roots p <> {} ; ::_thesis: contradiction
then consider x being set such that
A2: x in Roots p by XBOOLE_0:def_1;
reconsider x = x as Element of L by A2;
x is_a_root_of p by A2, POLYNOM5:def_9;
then eval (p,x) = 0. L by POLYNOM5:def_6;
hence contradiction by A1, POLYNOM5:37; ::_thesis: verum
end;
definition
let L be non degenerated comRing;
let r be Element of L;
let p be Polynomial of L;
assume A1: r is_a_root_of p ;
func poly_quotient (p,r) -> Polynomial of L means :Def7: :: UPROOTS:def 7
( (len it) + 1 = len p & ( for i being Nat holds it . i = eval ((poly_shift (p,(i + 1))),r) ) ) if len p > 0
otherwise it = 0_. L;
existence
( ( len p > 0 implies ex b1 being Polynomial of L st
( (len b1) + 1 = len p & ( for i being Nat holds b1 . i = eval ((poly_shift (p,(i + 1))),r) ) ) ) & ( not len p > 0 implies ex b1 being Polynomial of L st b1 = 0_. L ) )
proof
hereby ::_thesis: ( not len p > 0 implies ex b1 being Polynomial of L st b1 = 0_. L )
r in Roots p by A1, POLYNOM5:def_9;
then A1: len p <> 1 by Th46;
deffunc H1( Nat) -> Element of the carrier of L = eval ((poly_shift (p,($1 + 1))),r);
set lq = (len p) -' 1;
consider q being sequence of L such that
A2: for k being Element of NAT holds q . k = H1(k) from FUNCT_2:sch_4();
reconsider q = q as sequence of L ;
assume A3: len p > 0 ; ::_thesis: ex q being AlgSequence of L st
( (len q) + 1 = len p & ( for k being Nat holds q . k = H1(k) ) )
then consider p1 being Nat such that
A4: len p = p1 + 1 by NAT_1:6;
A5: (len p) -' 1 = p1 by A4, NAT_D:34;
then A6: (len p) -' 1 < len p by A4, NAT_1:13;
len p >= 0 + 1 by A3, NAT_1:13;
then consider lq1 being Nat such that
A7: (len p) -' 1 = lq1 + 1 by A4, A5, A1, NAT_1:6;
A8: now__::_thesis:_for_i_being_Nat_st_i_>=_(len_p)_-'_1_holds_
q_._i_=_0._L
let i be Nat; ::_thesis: ( i >= (len p) -' 1 implies q . i = 0. L )
assume i >= (len p) -' 1 ; ::_thesis: q . i = 0. L
then i >= p1 by A4, NAT_D:34;
then A9: i + 1 >= len p by A4, XREAL_1:6;
i in NAT by ORDINAL1:def_12;
hence q . i = eval ((poly_shift (p,(i + 1))),r) by A2
.= eval ((0_. L),r) by A9, Th43
.= 0. L by POLYNOM4:17 ;
::_thesis: verum
end;
reconsider lq1 = lq1 as Element of NAT by ORDINAL1:def_12;
q . lq1 = eval ((poly_shift (p,(lq1 + 1))),r) by A2
.= (r * (eval ((poly_shift (p,(len p))),r))) + (p . ((len p) -' 1)) by A4, A5, A7, A6, Th45
.= (r * (eval ((0_. L),r))) + (p . ((len p) -' 1)) by Th43
.= (r * (0. L)) + (p . ((len p) -' 1)) by POLYNOM4:17
.= (0. L) + (p . ((len p) -' 1)) by VECTSP_1:6
.= p . ((len p) -' 1) by RLVECT_1:4 ;
then A10: q . lq1 <> 0. L by A4, A5, ALGSEQ_1:10;
reconsider q = q as AlgSequence of L by A8, ALGSEQ_1:def_1;
A11: lq1 = ((len p) -' 1) -' 1 by A7, NAT_D:34;
A12: now__::_thesis:_for_m_being_Nat_st_m_is_at_least_length_of_q_holds_
not_(len_p)_-'_1_>_m
let m be Nat; ::_thesis: ( m is_at_least_length_of q implies not (len p) -' 1 > m )
assume A13: m is_at_least_length_of q ; ::_thesis: not (len p) -' 1 > m
assume A14: (len p) -' 1 > m ; ::_thesis: contradiction
then consider lq1 being Nat such that
A15: (len p) -' 1 = lq1 + 1 by NAT_1:6;
lq1 >= m by A14, A15, NAT_1:13;
then ((len p) -' 1) -' 1 >= m by A15, NAT_D:34;
hence contradiction by A11, A10, A13, ALGSEQ_1:def_2; ::_thesis: verum
end;
take q = q; ::_thesis: ( (len q) + 1 = len p & ( for k being Nat holds q . k = H1(k) ) )
(len p) -' 1 is_at_least_length_of q by A8, ALGSEQ_1:def_2;
hence (len q) + 1 = ((p1 + 1) -' 1) + 1 by A4, A12, ALGSEQ_1:def_3
.= len p by A4, NAT_D:34 ;
::_thesis: for k being Nat holds q . k = H1(k)
let k be Nat; ::_thesis: q . k = H1(k)
k in NAT by ORDINAL1:def_12;
hence q . k = H1(k) by A2; ::_thesis: verum
end;
thus ( not len p > 0 implies ex b1 being Polynomial of L st b1 = 0_. L ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Polynomial of L holds
( ( len p > 0 & (len b1) + 1 = len p & ( for i being Nat holds b1 . i = eval ((poly_shift (p,(i + 1))),r) ) & (len b2) + 1 = len p & ( for i being Nat holds b2 . i = eval ((poly_shift (p,(i + 1))),r) ) implies b1 = b2 ) & ( not len p > 0 & b1 = 0_. L & b2 = 0_. L implies b1 = b2 ) )
proof
let it1, it2 be Polynomial of L; ::_thesis: ( ( len p > 0 & (len it1) + 1 = len p & ( for i being Nat holds it1 . i = eval ((poly_shift (p,(i + 1))),r) ) & (len it2) + 1 = len p & ( for i being Nat holds it2 . i = eval ((poly_shift (p,(i + 1))),r) ) implies it1 = it2 ) & ( not len p > 0 & it1 = 0_. L & it2 = 0_. L implies it1 = it2 ) )
hereby ::_thesis: ( not len p > 0 & it1 = 0_. L & it2 = 0_. L implies it1 = it2 )
assume len p > 0 ; ::_thesis: ( (len it1) + 1 = len p & ( for i being Nat holds it1 . i = eval ((poly_shift (p,(i + 1))),r) ) & (len it2) + 1 = len p & ( for i being Nat holds it2 . i = eval ((poly_shift (p,(i + 1))),r) ) implies it1 = it2 )
assume that
A16: (len it1) + 1 = len p and
A17: for i being Nat holds it1 . i = eval ((poly_shift (p,(i + 1))),r) and
A18: (len it2) + 1 = len p and
A19: for i being Nat holds it2 . i = eval ((poly_shift (p,(i + 1))),r) ; ::_thesis: it1 = it2
now__::_thesis:_for_k_being_Nat_st_k_<_len_it1_holds_
it1_._k_=_it2_._k
let k be Nat; ::_thesis: ( k < len it1 implies it1 . k = it2 . k )
assume k < len it1 ; ::_thesis: it1 . k = it2 . k
thus it1 . k = eval ((poly_shift (p,(k + 1))),r) by A17
.= it2 . k by A19 ; ::_thesis: verum
end;
hence it1 = it2 by A16, A18, ALGSEQ_1:12; ::_thesis: verum
end;
thus ( not len p > 0 & it1 = 0_. L & it2 = 0_. L implies it1 = it2 ) ; ::_thesis: verum
end;
consistency
for b1 being Polynomial of L holds verum ;
end;
:: deftheorem Def7 defines poly_quotient UPROOTS:def_7_:_
for L being non degenerated comRing
for r being Element of L
for p being Polynomial of L st r is_a_root_of p holds
for b4 being Polynomial of L holds
( ( len p > 0 implies ( b4 = poly_quotient (p,r) iff ( (len b4) + 1 = len p & ( for i being Nat holds b4 . i = eval ((poly_shift (p,(i + 1))),r) ) ) ) ) & ( not len p > 0 implies ( b4 = poly_quotient (p,r) iff b4 = 0_. L ) ) );
theorem Th47: :: UPROOTS:47
for L being non degenerated comRing
for r being Element of L
for p being non-zero Polynomial of L st r is_a_root_of p holds
len (poly_quotient (p,r)) > 0
proof
let L be non degenerated comRing; ::_thesis: for r being Element of L
for p being non-zero Polynomial of L st r is_a_root_of p holds
len (poly_quotient (p,r)) > 0
let r be Element of L; ::_thesis: for p being non-zero Polynomial of L st r is_a_root_of p holds
len (poly_quotient (p,r)) > 0
let p be non-zero Polynomial of L; ::_thesis: ( r is_a_root_of p implies len (poly_quotient (p,r)) > 0 )
assume A1: r is_a_root_of p ; ::_thesis: len (poly_quotient (p,r)) > 0
assume len (poly_quotient (p,r)) <= 0 ; ::_thesis: contradiction
then A2: len (poly_quotient (p,r)) = 0 ;
len p > 0 by Th17;
then (len (poly_quotient (p,r))) + 1 = len p by A1, Def7;
then Roots p = {} by A2, Th46;
hence contradiction by A1, POLYNOM5:def_9; ::_thesis: verum
end;
theorem Th48: :: UPROOTS:48
for L being non empty right_complementable left-distributive well-unital add-associative right_zeroed doubleLoopStr
for x being Element of L holds Roots <%(- x),(1. L)%> = {x}
proof
let L be non empty right_complementable left-distributive well-unital add-associative right_zeroed doubleLoopStr ; ::_thesis: for x being Element of L holds Roots <%(- x),(1. L)%> = {x}
let x be Element of L; ::_thesis: Roots <%(- x),(1. L)%> = {x}
now__::_thesis:_for_a_being_set_holds_
(_(_a_in_Roots_<%(-_x),(1._L)%>_implies_x_=_a_)_&_(_a_=_x_implies_a_in_Roots_<%(-_x),(1._L)%>_)_)
let a be set ; ::_thesis: ( ( a in Roots <%(- x),(1. L)%> implies x = a ) & ( a = x implies a in Roots <%(- x),(1. L)%> ) )
hereby ::_thesis: ( a = x implies a in Roots <%(- x),(1. L)%> )
assume A1: a in Roots <%(- x),(1. L)%> ; ::_thesis: x = a
then reconsider b = a as Element of L ;
b is_a_root_of <%(- x),(1. L)%> by A1, POLYNOM5:def_9;
then 0. L = eval (<%(- x),(1. L)%>,b) by POLYNOM5:def_6
.= (- x) + b by POLYNOM5:47 ;
then - x = - b by RLVECT_1:6;
hence x = a by RLVECT_1:18; ::_thesis: verum
end;
eval (<%(- x),(1. L)%>,x) = (- x) + x by POLYNOM5:47
.= 0. L by RLVECT_1:5 ;
then A2: x is_a_root_of <%(- x),(1. L)%> by POLYNOM5:def_6;
assume a = x ; ::_thesis: a in Roots <%(- x),(1. L)%>
hence a in Roots <%(- x),(1. L)%> by A2, POLYNOM5:def_9; ::_thesis: verum
end;
hence Roots <%(- x),(1. L)%> = {x} by TARSKI:def_1; ::_thesis: verum
end;
theorem Th49: :: UPROOTS:49
for L being non trivial comRing
for x being Element of L
for p, q being Polynomial of L st p = <%(- x),(1. L)%> *' q holds
x is_a_root_of p
proof
let L be non trivial comRing; ::_thesis: for x being Element of L
for p, q being Polynomial of L st p = <%(- x),(1. L)%> *' q holds
x is_a_root_of p
let x be Element of L; ::_thesis: for p, q being Polynomial of L st p = <%(- x),(1. L)%> *' q holds
x is_a_root_of p
let p, q be Polynomial of L; ::_thesis: ( p = <%(- x),(1. L)%> *' q implies x is_a_root_of p )
assume A1: p = <%(- x),(1. L)%> *' q ; ::_thesis: x is_a_root_of p
A2: eval (<%(- x),(1. L)%>,x) = (- x) + x by POLYNOM5:47
.= 0. L by RLVECT_1:5 ;
thus eval (p,x) = (eval (<%(- x),(1. L)%>,x)) * (eval (q,x)) by A1, POLYNOM4:24
.= 0. L by A2, VECTSP_1:7 ; :: according to POLYNOM5:def_6 ::_thesis: verum
end;
theorem Th50: :: UPROOTS:50
for L being non degenerated comRing
for r being Element of L
for p being Polynomial of L st r is_a_root_of p holds
p = <%(- r),(1. L)%> *' (poly_quotient (p,r))
proof
let L be non degenerated comRing; ::_thesis: for r being Element of L
for p being Polynomial of L st r is_a_root_of p holds
p = <%(- r),(1. L)%> *' (poly_quotient (p,r))
let x be Element of L; ::_thesis: for p being Polynomial of L st x is_a_root_of p holds
p = <%(- x),(1. L)%> *' (poly_quotient (p,x))
let p be Polynomial of L; ::_thesis: ( x is_a_root_of p implies p = <%(- x),(1. L)%> *' (poly_quotient (p,x)) )
assume A1: x is_a_root_of p ; ::_thesis: p = <%(- x),(1. L)%> *' (poly_quotient (p,x))
set r = <%(- x),(1. L)%>;
set pq = poly_quotient (p,x);
percases ( len p > 0 or len p = 0 ) ;
supposeA2: len p > 0 ; ::_thesis: p = <%(- x),(1. L)%> *' (poly_quotient (p,x))
<%(- x),(1. L)%> . ((len <%(- x),(1. L)%>) -' 1) = <%(- x),(1. L)%> . ((1 + 1) -' 1) by POLYNOM5:40
.= <%(- x),(1. L)%> . 1 by NAT_D:34
.= 1. L by POLYNOM5:38 ;
then A3: (<%(- x),(1. L)%> . ((len <%(- x),(1. L)%>) -' 1)) * ((poly_quotient (p,x)) . ((len (poly_quotient (p,x))) -' 1)) = (poly_quotient (p,x)) . ((len (poly_quotient (p,x))) -' 1) by VECTSP_1:def_8;
p is non-zero by A2, Th17;
then A4: len (poly_quotient (p,x)) > 0 by A1, Th47;
now__::_thesis:_(_len_p_=_len_(<%(-_x),(1._L)%>_*'_(poly_quotient_(p,x)))_&_(_for_k_being_Nat_st_k_<_len_p_holds_
p_._k_=_(<%(-_x),(1._L)%>_*'_(poly_quotient_(p,x)))_._k_)_)
len (<%(- x),(1. L)%> *' (poly_quotient (p,x))) = ((len <%(- x),(1. L)%>) + (len (poly_quotient (p,x)))) - 1 by A4, A3, Th18, POLYNOM4:10
.= ((len (poly_quotient (p,x))) + (1 + 1)) - 1 by POLYNOM5:40
.= (len (poly_quotient (p,x))) + 1
.= len p by A1, A2, Def7 ;
hence len p = len (<%(- x),(1. L)%> *' (poly_quotient (p,x))) ; ::_thesis: for k being Nat st k < len p holds
p . k = (<%(- x),(1. L)%> *' (poly_quotient (p,x))) . k
defpred S1[ Nat] means p . $1 = (<%(- x),(1. L)%> *' (poly_quotient (p,x))) . $1;
let k be Nat; ::_thesis: ( k < len p implies p . k = (<%(- x),(1. L)%> *' (poly_quotient (p,x))) . k )
assume k < len p ; ::_thesis: p . k = (<%(- x),(1. L)%> *' (poly_quotient (p,x))) . k
A5: 0. L = eval (p,x) by A1, POLYNOM5:def_6
.= eval ((poly_shift (p,0)),x) by Th42
.= (x * (eval ((poly_shift (p,(0 + 1))),x))) + (p . 0) by A2, Th45 ;
A6: (- x) * (eval ((poly_shift (p,(0 + 1))),x)) = ((- x) * (eval ((poly_shift (p,(0 + 1))),x))) + (0. L) by RLVECT_1:def_4
.= (((- x) * (eval ((poly_shift (p,(0 + 1))),x))) + (x * (eval ((poly_shift (p,1)),x)))) + (p . 0) by A5, RLVECT_1:def_3
.= ((- (x * (eval ((poly_shift (p,(0 + 1))),x)))) + (x * (eval ((poly_shift (p,1)),x)))) + (p . 0) by VECTSP_1:9
.= (0. L) + (p . 0) by RLVECT_1:5
.= p . 0 by RLVECT_1:4 ;
A7: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; ::_thesis: S1[k + 1]
A8: (poly_quotient (p,x)) . (k + 1) = eval ((poly_shift (p,((k + 1) + 1))),x) by A1, A2, Def7;
A9: (poly_quotient (p,x)) . k = eval ((poly_shift (p,(k + 1))),x) by A1, A2, Def7;
percases ( k + 1 >= len p or k + 1 < len p ) ;
supposeA10: k + 1 >= len p ; ::_thesis: S1[k + 1]
then A11: (poly_quotient (p,x)) . (k + 1) = eval ((0_. L),x) by A8, Th43, NAT_1:12
.= 0. L by POLYNOM4:17 ;
A12: (poly_quotient (p,x)) . k = eval ((0_. L),x) by A9, A10, Th43
.= 0. L by POLYNOM4:17 ;
(<%(- x),(1. L)%> *' (poly_quotient (p,x))) . (k + 1) = ((- x) * ((poly_quotient (p,x)) . (k + 1))) + ((1. L) * ((poly_quotient (p,x)) . k)) by Th37
.= (0. L) + ((1. L) * ((poly_quotient (p,x)) . k)) by A11, VECTSP_1:6
.= (0. L) + (0. L) by A12, VECTSP_1:6
.= 0. L by RLVECT_1:4 ;
hence S1[k + 1] by A10, ALGSEQ_1:8; ::_thesis: verum
end;
suppose k + 1 < len p ; ::_thesis: S1[k + 1]
then (poly_quotient (p,x)) . k = (x * (eval ((poly_shift (p,((k + 1) + 1))),x))) + (p . (k + 1)) by A9, Th45;
then A13: (- (x * ((poly_quotient (p,x)) . (k + 1)))) + ((poly_quotient (p,x)) . k) = ((- (x * ((poly_quotient (p,x)) . (k + 1)))) + (x * (eval ((poly_shift (p,((k + 1) + 1))),x)))) + (p . (k + 1)) by RLVECT_1:def_3
.= (0. L) + (p . (k + 1)) by A8, RLVECT_1:5 ;
(<%(- x),(1. L)%> *' (poly_quotient (p,x))) . (k + 1) = ((- x) * ((poly_quotient (p,x)) . (k + 1))) + ((1. L) * ((poly_quotient (p,x)) . k)) by Th37
.= ((- x) * ((poly_quotient (p,x)) . (k + 1))) + ((poly_quotient (p,x)) . k) by VECTSP_1:def_8
.= (- (x * ((poly_quotient (p,x)) . (k + 1)))) + ((poly_quotient (p,x)) . k) by VECTSP_1:9 ;
hence S1[k + 1] by A13, RLVECT_1:4; ::_thesis: verum
end;
end;
end;
(<%(- x),(1. L)%> *' (poly_quotient (p,x))) . 0 = (- x) * ((poly_quotient (p,x)) . 0) by Th37
.= (- x) * (eval ((poly_shift (p,(0 + 1))),x)) by A1, A2, Def7 ;
then A14: S1[ 0 ] by A6;
for k being Nat holds S1[k] from NAT_1:sch_2(A14, A7);
hence p . k = (<%(- x),(1. L)%> *' (poly_quotient (p,x))) . k ; ::_thesis: verum
end;
hence p = <%(- x),(1. L)%> *' (poly_quotient (p,x)) by ALGSEQ_1:12; ::_thesis: verum
end;
suppose len p = 0 ; ::_thesis: p = <%(- x),(1. L)%> *' (poly_quotient (p,x))
then ( poly_quotient (p,x) = 0_. L & p = 0_. L ) by A1, Def7, POLYNOM4:5;
hence p = <%(- x),(1. L)%> *' (poly_quotient (p,x)) by POLYNOM3:34; ::_thesis: verum
end;
end;
end;
theorem :: UPROOTS:51
for L being non degenerated comRing
for r being Element of L
for p, q being Polynomial of L st p = <%(- r),(1. L)%> *' q holds
r is_a_root_of p
proof
let L be non degenerated comRing; ::_thesis: for r being Element of L
for p, q being Polynomial of L st p = <%(- r),(1. L)%> *' q holds
r is_a_root_of p
let r be Element of L; ::_thesis: for p, q being Polynomial of L st p = <%(- r),(1. L)%> *' q holds
r is_a_root_of p
let p, q be Polynomial of L; ::_thesis: ( p = <%(- r),(1. L)%> *' q implies r is_a_root_of p )
assume p = <%(- r),(1. L)%> *' q ; ::_thesis: r is_a_root_of p
then eval (p,r) = (eval (<%(- r),(1. L)%>,r)) * (eval (q,r)) by POLYNOM4:24
.= ((- r) + r) * (eval (q,r)) by POLYNOM5:47
.= (0. L) * (eval (q,r)) by RLVECT_1:def_10
.= 0. L by VECTSP_1:7 ;
hence r is_a_root_of p by POLYNOM5:def_6; ::_thesis: verum
end;
Lm1: now__::_thesis:_for_L_being_domRing
for_p_being_non-zero_Polynomial_of_L_holds_
(_Roots_p_is_finite_&_ex_n_being_Element_of_NAT_st_
(_n_=_card_(Roots_p)_&_n_<_len_p_)_)
let L be domRing; ::_thesis: for p being non-zero Polynomial of L holds
( Roots p is finite & ex n being Element of NAT st
( n = card (Roots p) & n < len p ) )
let p be non-zero Polynomial of L; ::_thesis: ( Roots p is finite & ex n being Element of NAT st
( n = card (Roots p) & n < len p ) )
defpred S1[ Nat] means for p being Polynomial of L st len p = $1 holds
( Roots p is finite & ex n being Element of NAT st
( n = card (Roots p) & n < len p ) );
p <> 0_. L by Def5;
then len p <> 0 by POLYNOM4:5;
then A1: len p >= 0 + 1 by NAT_1:13;
A2: for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] )
assume that
n >= 1 and
A3: S1[n] ; ::_thesis: S1[n + 1]
let p be Polynomial of L; ::_thesis: ( len p = n + 1 implies ( Roots p is finite & ex n being Element of NAT st
( n = card (Roots p) & n < len p ) ) )
assume A4: len p = n + 1 ; ::_thesis: ( Roots p is finite & ex n being Element of NAT st
( n = card (Roots p) & n < len p ) )
percases ( p is with_roots or not p is with_roots ) ;
suppose p is with_roots ; ::_thesis: ( Roots p is finite & ex n being Element of NAT st
( n = card (Roots p) & n < len p ) )
then consider x being Element of L such that
A5: x is_a_root_of p by POLYNOM5:def_7;
set r = <%(- x),(1. L)%>;
set pq = poly_quotient (p,x);
A6: p = <%(- x),(1. L)%> *' (poly_quotient (p,x)) by A5, Th50;
then A7: Roots p = (Roots <%(- x),(1. L)%>) \/ (Roots (poly_quotient (p,x))) by Th23;
A8: Roots <%(- x),(1. L)%> = {x} by Th48;
then reconsider Rr = Roots <%(- x),(1. L)%> as finite set ;
A9: (len (poly_quotient (p,x))) + 1 = len p by A4, A5, Def7;
then consider k being Element of NAT such that
A10: k = card (Roots (poly_quotient (p,x))) and
A11: k < len (poly_quotient (p,x)) by A3, A4;
reconsider Rpq = Roots (poly_quotient (p,x)) as finite set by A3, A4, A9;
reconsider Rp = Rpq \/ Rr as finite set ;
card Rr = 1 by A8, CARD_1:30;
then A12: card Rp <= k + 1 by A10, CARD_2:43;
Roots (poly_quotient (p,x)) is finite by A3, A4, A9;
hence Roots p is finite by A8, A7; ::_thesis: ex n being Element of NAT st
( n = card (Roots p) & n < len p )
take m = card Rp; ::_thesis: ( m = card (Roots p) & m < len p )
thus m = card (Roots p) by A6, Th23; ::_thesis: m < len p
k + 1 < n + 1 by A4, A9, A11, XREAL_1:8;
hence m < len p by A4, A12, XXREAL_0:2; ::_thesis: verum
end;
supposeA13: not p is with_roots ; ::_thesis: ( Roots p is finite & ex n being Element of NAT st
( n = card (Roots p) & n < len p ) )
A14: now__::_thesis:_not_Roots_p_<>_{}
assume Roots p <> {} ; ::_thesis: contradiction
then consider x being set such that
A15: x in Roots p by XBOOLE_0:def_1;
reconsider x = x as Element of L by A15;
x is_a_root_of p by A15, POLYNOM5:def_9;
hence contradiction by A13, POLYNOM5:def_7; ::_thesis: verum
end;
hence Roots p is finite ; ::_thesis: ex n being Element of NAT st
( n = card (Roots p) & n < len p )
take 0 ; ::_thesis: ( 0 = card (Roots p) & 0 < len p )
thus 0 = card (Roots p) by A14; ::_thesis: 0 < len p
thus 0 < len p by A4; ::_thesis: verum
end;
end;
end;
A16: S1[1]
proof
let p be Polynomial of L; ::_thesis: ( len p = 1 implies ( Roots p is finite & ex n being Element of NAT st
( n = card (Roots p) & n < len p ) ) )
assume A17: len p = 1 ; ::_thesis: ( Roots p is finite & ex n being Element of NAT st
( n = card (Roots p) & n < len p ) )
hence Roots p is finite by Th46; ::_thesis: ex n being Element of NAT st
( n = card (Roots p) & n < len p )
take 0 ; ::_thesis: ( 0 = card (Roots p) & 0 < len p )
thus 0 = card (Roots p) by A17, Th46, CARD_1:27; ::_thesis: 0 < len p
thus 0 < len p by A17; ::_thesis: verum
end;
for n being Nat st n >= 1 holds
S1[n] from NAT_1:sch_8(A16, A2);
hence ( Roots p is finite & ex n being Element of NAT st
( n = card (Roots p) & n < len p ) ) by A1; ::_thesis: verum
end;
begin
registration
let L be domRing;
let p be non-zero Polynomial of L;
cluster Roots p -> finite ;
correctness
coherence
Roots p is finite ;
by Lm1;
end;
definition
let L be non degenerated comRing;
let x be Element of L;
let p be non-zero Polynomial of L;
func multiplicity (p,x) -> Element of NAT means :Def8: :: UPROOTS:def 8
ex F being non empty finite Subset of NAT st
( F = { k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q } & it = max F );
existence
ex b1 being Element of NAT ex F being non empty finite Subset of NAT st
( F = { k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q } & b1 = max F )
proof
set r = <%(- x),(1. L)%>;
defpred S1[ Element of NAT ] means ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ $1) *' q;
set F = { k where k is Element of NAT : S1[k] } ;
A1: { k where k is Element of NAT : S1[k] } c= NAT from FRAENKEL:sch_10();
p = (1_. L) *' p by POLYNOM3:35
.= (<%(- x),(1. L)%> `^ 0) *' p by POLYNOM5:15 ;
then A2: 0 in { k where k is Element of NAT : S1[k] } ;
A3: len p > 0 by Th17;
{ k where k is Element of NAT : S1[k] } c= len p
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { k where k is Element of NAT : S1[k] } or a in len p )
assume a in { k where k is Element of NAT : S1[k] } ; ::_thesis: a in len p
then consider k being Element of NAT such that
A4: a = k and
A5: S1[k] ;
consider q being Polynomial of L such that
A6: p = (<%(- x),(1. L)%> `^ k) *' q by A5;
A7: now__::_thesis:_not_len_q_=_0
assume len q = 0 ; ::_thesis: contradiction
then q = 0_. L by POLYNOM4:5;
then p = 0_. L by A6, POLYNOM4:2;
hence contradiction by A3, POLYNOM4:3; ::_thesis: verum
end;
then reconsider q = q as non-zero Polynomial of L by Th17;
now__::_thesis:_not_k_>=_len_p
assume k >= len p ; ::_thesis: contradiction
then k + (len q) > (len p) + 0 by A7, XREAL_1:8;
hence contradiction by A6, Th40; ::_thesis: verum
end;
then k in { i where i is Element of NAT : i < len p } ;
hence a in len p by A4, AXIOMS:4; ::_thesis: verum
end;
then reconsider F = { k where k is Element of NAT : S1[k] } as non empty finite Subset of NAT by A2, A1;
reconsider FF = F as non empty finite natural-membered set ;
reconsider m = max FF as Element of NAT by ORDINAL1:def_12;
take m ; ::_thesis: ex F being non empty finite Subset of NAT st
( F = { k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q } & m = max F )
thus ex F being non empty finite Subset of NAT st
( F = { k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q } & m = max F ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of NAT st ex F being non empty finite Subset of NAT st
( F = { k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q } & b1 = max F ) & ex F being non empty finite Subset of NAT st
( F = { k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q } & b2 = max F ) holds
b1 = b2 ;
end;
:: deftheorem Def8 defines multiplicity UPROOTS:def_8_:_
for L being non degenerated comRing
for x being Element of L
for p being non-zero Polynomial of L
for b4 being Element of NAT holds
( b4 = multiplicity (p,x) iff ex F being non empty finite Subset of NAT st
( F = { k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q } & b4 = max F ) );
theorem Th52: :: UPROOTS:52
for L being non degenerated comRing
for p being non-zero Polynomial of L
for x being Element of L holds
( x is_a_root_of p iff multiplicity (p,x) >= 1 )
proof
let L be non degenerated comRing; ::_thesis: for p being non-zero Polynomial of L
for x being Element of L holds
( x is_a_root_of p iff multiplicity (p,x) >= 1 )
let p be non-zero Polynomial of L; ::_thesis: for x being Element of L holds
( x is_a_root_of p iff multiplicity (p,x) >= 1 )
let x be Element of L; ::_thesis: ( x is_a_root_of p iff multiplicity (p,x) >= 1 )
set r = <%(- x),(1. L)%>;
set m = multiplicity (p,x);
consider F being non empty finite Subset of NAT such that
A1: F = { k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q } and
A2: multiplicity (p,x) = max F by Def8;
multiplicity (p,x) in F by A2, XXREAL_2:def_8;
then consider k being Element of NAT such that
A3: multiplicity (p,x) = k and
A4: ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q by A1;
hereby ::_thesis: ( multiplicity (p,x) >= 1 implies x is_a_root_of p )
assume x is_a_root_of p ; ::_thesis: multiplicity (p,x) >= 1
then A5: p = <%(- x),(1. L)%> *' (poly_quotient (p,x)) by Th50;
<%(- x),(1. L)%> `^ 1 = <%(- x),(1. L)%> by POLYNOM5:16;
then 1 in F by A1, A5;
hence multiplicity (p,x) >= 1 by A2, XXREAL_2:def_8; ::_thesis: verum
end;
consider q being Polynomial of L such that
A6: p = (<%(- x),(1. L)%> `^ k) *' q by A4;
assume multiplicity (p,x) >= 1 ; ::_thesis: x is_a_root_of p
then consider k1 being Nat such that
A7: k = k1 + 1 by A3, NAT_1:6;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def_12;
p = (<%(- x),(1. L)%> *' (<%(- x),(1. L)%> `^ k1)) *' q by A6, A7, POLYNOM5:19
.= <%(- x),(1. L)%> *' ((<%(- x),(1. L)%> `^ k1) *' q) by POLYNOM3:33 ;
hence x is_a_root_of p by Th49; ::_thesis: verum
end;
theorem Th53: :: UPROOTS:53
for L being non degenerated comRing
for x being Element of L holds multiplicity (<%(- x),(1. L)%>,x) = 1
proof
let L be non degenerated comRing; ::_thesis: for x being Element of L holds multiplicity (<%(- x),(1. L)%>,x) = 1
let x be Element of L; ::_thesis: multiplicity (<%(- x),(1. L)%>,x) = 1
set r = <%(- x),(1. L)%>;
set j = multiplicity (<%(- x),(1. L)%>,x);
consider F being non empty finite Subset of NAT such that
A1: F = { k where k is Element of NAT : ex q being Polynomial of L st <%(- x),(1. L)%> = (<%(- x),(1. L)%> `^ k) *' q } and
A2: multiplicity (<%(- x),(1. L)%>,x) = max F by Def8;
multiplicity (<%(- x),(1. L)%>,x) in F by A2, XXREAL_2:def_8;
then consider k being Element of NAT such that
A3: k = multiplicity (<%(- x),(1. L)%>,x) and
A4: ex q being Polynomial of L st <%(- x),(1. L)%> = (<%(- x),(1. L)%> `^ k) *' q by A1;
consider q being Polynomial of L such that
A5: <%(- x),(1. L)%> = (<%(- x),(1. L)%> `^ k) *' q by A4;
A6: len <%(- x),(1. L)%> = 2 by POLYNOM5:40;
A7: now__::_thesis:_not_len_q_=_0
assume len q = 0 ; ::_thesis: contradiction
then q = 0_. L by POLYNOM4:5;
then <%(- x),(1. L)%> = 0_. L by A5, POLYNOM4:2;
hence contradiction by A6, POLYNOM4:3; ::_thesis: verum
end;
then A8: q is non-zero by Th17;
A9: now__::_thesis:_not_k_>_1
assume k > 1 ; ::_thesis: contradiction
then k >= 1 + 1 by NAT_1:13;
then k + (len q) > 2 + 0 by A7, XREAL_1:8;
hence contradiction by A6, A5, A8, Th40; ::_thesis: verum
end;
<%(- x),(1. L)%> = <%(- x),(1. L)%> `^ 1 by POLYNOM5:16;
then <%(- x),(1. L)%> = (<%(- x),(1. L)%> `^ 1) *' (1_. L) by POLYNOM3:35;
then 1 in F by A1;
then multiplicity (<%(- x),(1. L)%>,x) >= 1 by A2, XXREAL_2:def_8;
hence multiplicity (<%(- x),(1. L)%>,x) = 1 by A3, A9, XXREAL_0:1; ::_thesis: verum
end;
definition
let L be domRing;
let p be non-zero Polynomial of L;
func BRoots p -> bag of the carrier of L means :Def9: :: UPROOTS:def 9
( support it = Roots p & ( for x being Element of L holds it . x = multiplicity (p,x) ) );
existence
ex b1 being bag of the carrier of L st
( support b1 = Roots p & ( for x being Element of L holds b1 . x = multiplicity (p,x) ) )
proof
deffunc H1( Element of L) -> Element of NAT = multiplicity (p,$1);
consider b being Function of the carrier of L,NAT such that
A1: for x being Element of L holds b . x = H1(x) from FUNCT_2:sch_4();
dom b = the carrier of L by FUNCT_2:def_1;
then A2: support b c= the carrier of L by PRE_POLY:37;
A3: now__::_thesis:_for_x_being_set_holds_
(_(_x_in_support_b_implies_x_in_Roots_p_)_&_(_x_in_Roots_p_implies_x_in_support_b_)_)
let x be set ; ::_thesis: ( ( x in support b implies x in Roots p ) & ( x in Roots p implies x in support b ) )
hereby ::_thesis: ( x in Roots p implies x in support b )
assume A4: x in support b ; ::_thesis: x in Roots p
then reconsider xx = x as Element of L by A2;
b . x <> 0 by A4, PRE_POLY:def_7;
then A5: b . xx >= 0 + 1 by NAT_1:13;
b . x = H1(xx) by A1;
then xx is_a_root_of p by A5, Th52;
hence x in Roots p by POLYNOM5:def_9; ::_thesis: verum
end;
assume A6: x in Roots p ; ::_thesis: x in support b
then reconsider xx = x as Element of L ;
xx is_a_root_of p by A6, POLYNOM5:def_9;
then multiplicity (p,xx) >= 1 by Th52;
then b . xx >= 1 by A1;
hence x in support b by PRE_POLY:def_7; ::_thesis: verum
end;
then support b = Roots p by TARSKI:1;
then reconsider b = b as bag of the carrier of L by PRE_POLY:def_8;
take b ; ::_thesis: ( support b = Roots p & ( for x being Element of L holds b . x = multiplicity (p,x) ) )
thus ( support b = Roots p & ( for x being Element of L holds b . x = multiplicity (p,x) ) ) by A1, A3, TARSKI:1; ::_thesis: verum
end;
uniqueness
for b1, b2 being bag of the carrier of L st support b1 = Roots p & ( for x being Element of L holds b1 . x = multiplicity (p,x) ) & support b2 = Roots p & ( for x being Element of L holds b2 . x = multiplicity (p,x) ) holds
b1 = b2
proof
let it1, it2 be bag of the carrier of L; ::_thesis: ( support it1 = Roots p & ( for x being Element of L holds it1 . x = multiplicity (p,x) ) & support it2 = Roots p & ( for x being Element of L holds it2 . x = multiplicity (p,x) ) implies it1 = it2 )
assume that
support it1 = Roots p and
A7: for x being Element of L holds it1 . x = multiplicity (p,x) and
support it2 = Roots p and
A8: for x being Element of L holds it2 . x = multiplicity (p,x) ; ::_thesis: it1 = it2
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_L_holds_
it1_._x_=_it2_._x
let x be set ; ::_thesis: ( x in the carrier of L implies it1 . x = it2 . x )
assume x in the carrier of L ; ::_thesis: it1 . x = it2 . x
then reconsider xx = x as Element of L ;
thus it1 . x = multiplicity (p,xx) by A7
.= it2 . x by A8 ; ::_thesis: verum
end;
hence it1 = it2 by PBOOLE:3; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines BRoots UPROOTS:def_9_:_
for L being domRing
for p being non-zero Polynomial of L
for b3 being bag of the carrier of L holds
( b3 = BRoots p iff ( support b3 = Roots p & ( for x being Element of L holds b3 . x = multiplicity (p,x) ) ) );
theorem Th54: :: UPROOTS:54
for L being domRing
for x being Element of L holds BRoots <%(- x),(1. L)%> = ({x},1) -bag
proof
let L be domRing; ::_thesis: for x being Element of L holds BRoots <%(- x),(1. L)%> = ({x},1) -bag
let x be Element of L; ::_thesis: BRoots <%(- x),(1. L)%> = ({x},1) -bag
set r = <%(- x),(1. L)%>;
Roots <%(- x),(1. L)%> = {x} by Th48;
then A1: support (BRoots <%(- x),(1. L)%>) = {x} by Def9;
A2: x in {x} by TARSKI:def_1;
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_L_holds_
(BRoots_<%(-_x),(1._L)%>)_._i_=_(({x},1)_-bag)_._i
let i be set ; ::_thesis: ( i in the carrier of L implies (BRoots <%(- x),(1. L)%>) . b1 = (({x},1) -bag) . b1 )
assume i in the carrier of L ; ::_thesis: (BRoots <%(- x),(1. L)%>) . b1 = (({x},1) -bag) . b1
then reconsider i1 = i as Element of L ;
percases ( i = x or i <> x ) ;
supposeA3: i = x ; ::_thesis: (BRoots <%(- x),(1. L)%>) . b1 = (({x},1) -bag) . b1
thus (BRoots <%(- x),(1. L)%>) . i = multiplicity (<%(- x),(1. L)%>,i1) by Def9
.= 1 by A3, Th53
.= (({x},1) -bag) . i by A2, A3, Th7 ; ::_thesis: verum
end;
suppose i <> x ; ::_thesis: (BRoots <%(- x),(1. L)%>) . b1 = (({x},1) -bag) . b1
then A4: not i in {x} by TARSKI:def_1;
hence (BRoots <%(- x),(1. L)%>) . i = 0 by A1, PRE_POLY:def_7
.= (({x},1) -bag) . i by A4, Th6 ;
::_thesis: verum
end;
end;
end;
hence BRoots <%(- x),(1. L)%> = ({x},1) -bag by PBOOLE:3; ::_thesis: verum
end;
theorem Th55: :: UPROOTS:55
for L being domRing
for x being Element of L
for p, q being non-zero Polynomial of L holds multiplicity ((p *' q),x) = (multiplicity (p,x)) + (multiplicity (q,x))
proof
let L be domRing; ::_thesis: for x being Element of L
for p, q being non-zero Polynomial of L holds multiplicity ((p *' q),x) = (multiplicity (p,x)) + (multiplicity (q,x))
let x be Element of L; ::_thesis: for p, q being non-zero Polynomial of L holds multiplicity ((p *' q),x) = (multiplicity (p,x)) + (multiplicity (q,x))
let p, q be non-zero Polynomial of L; ::_thesis: multiplicity ((p *' q),x) = (multiplicity (p,x)) + (multiplicity (q,x))
set r = <%(- x),(1. L)%>;
consider F being non empty finite Subset of NAT such that
A1: F = { k where k is Element of NAT : ex pqq being Polynomial of L st p *' q = (<%(- x),(1. L)%> `^ k) *' pqq } and
A2: multiplicity ((p *' q),x) = max F by Def8;
consider f being non empty finite Subset of NAT such that
A3: f = { k where k is Element of NAT : ex pq being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' pq } and
A4: multiplicity (p,x) = max f by Def8;
max f in f by XXREAL_2:def_8;
then consider i being Element of NAT such that
A5: i = max f and
A6: ex pq being Polynomial of L st p = (<%(- x),(1. L)%> `^ i) *' pq by A3;
consider pq being Polynomial of L such that
A7: p = (<%(- x),(1. L)%> `^ i) *' pq by A6;
consider g being non empty finite Subset of NAT such that
A8: g = { k where k is Element of NAT : ex qq being Polynomial of L st q = (<%(- x),(1. L)%> `^ k) *' qq } and
A9: multiplicity (q,x) = max g by Def8;
max F in F by XXREAL_2:def_8;
then consider k being Element of NAT such that
A10: k = max F and
A11: ex pqq being Polynomial of L st p *' q = (<%(- x),(1. L)%> `^ k) *' pqq by A1;
consider pqq being Polynomial of L such that
A12: p *' q = (<%(- x),(1. L)%> `^ k) *' pqq by A11;
max g in g by XXREAL_2:def_8;
then consider j being Element of NAT such that
A13: j = max g and
A14: ex qq being Polynomial of L st q = (<%(- x),(1. L)%> `^ j) *' qq by A8;
consider qq being Polynomial of L such that
A15: q = (<%(- x),(1. L)%> `^ j) *' qq by A14;
A16: p *' q = (((<%(- x),(1. L)%> `^ i) *' pq) *' (<%(- x),(1. L)%> `^ j)) *' qq by A7, A15, POLYNOM3:33
.= (((<%(- x),(1. L)%> `^ i) *' (<%(- x),(1. L)%> `^ j)) *' pq) *' qq by POLYNOM3:33
.= ((<%(- x),(1. L)%> `^ (i + j)) *' pq) *' qq by Th30
.= (<%(- x),(1. L)%> `^ (i + j)) *' (pq *' qq) by POLYNOM3:33 ;
A17: now__::_thesis:_not_i_+_j_<_k
assume i + j < k ; ::_thesis: contradiction
then 0 + (i + j) < k ;
then A18: 0 < k - (i + j) by XREAL_1:20;
then reconsider kij = k - (i + j) as Element of NAT by INT_1:3;
consider kk being Nat such that
A19: kij = kk + 1 by A18, NAT_1:6;
reconsider kk = kk as Element of NAT by ORDINAL1:def_12;
<%(- x),(1. L)%> `^ kij = (<%(- x),(1. L)%> `^ 1) *' (<%(- x),(1. L)%> `^ kk) by A19, Th30
.= <%(- x),(1. L)%> *' (<%(- x),(1. L)%> `^ kk) by POLYNOM5:16 ;
then A20: (<%(- x),(1. L)%> `^ kij) *' pqq = <%(- x),(1. L)%> *' ((<%(- x),(1. L)%> `^ kk) *' pqq) by POLYNOM3:33;
( (0_. L) . 1 = 0. L & <%(- x),(1. L)%> . 1 = 1. L ) by FUNCOP_1:7, POLYNOM5:38;
then A21: <%(- x),(1. L)%> `^ (i + j) <> 0_. L by Th29;
k = kij + (i + j) ;
then p *' q = ((<%(- x),(1. L)%> `^ (i + j)) *' (<%(- x),(1. L)%> `^ kij)) *' pqq by A12, Th30
.= (<%(- x),(1. L)%> `^ (i + j)) *' ((<%(- x),(1. L)%> `^ kij) *' pqq) by POLYNOM3:33 ;
then x is_a_root_of pq *' qq by A16, A21, A20, Th28, Th49;
then x in Roots (pq *' qq) by POLYNOM5:def_9;
then A22: x in (Roots pq) \/ (Roots qq) by Th23;
percases ( x in Roots pq or x in Roots qq ) by A22, XBOOLE_0:def_3;
suppose x in Roots pq ; ::_thesis: contradiction
then x is_a_root_of pq by POLYNOM5:def_9;
then pq = <%(- x),(1. L)%> *' (poly_quotient (pq,x)) by Th50;
then p = ((<%(- x),(1. L)%> `^ i) *' <%(- x),(1. L)%>) *' (poly_quotient (pq,x)) by A7, POLYNOM3:33
.= ((<%(- x),(1. L)%> `^ i) *' (<%(- x),(1. L)%> `^ 1)) *' (poly_quotient (pq,x)) by POLYNOM5:16
.= (<%(- x),(1. L)%> `^ (i + 1)) *' (poly_quotient (pq,x)) by Th30 ;
then i + 1 in f by A3;
then i + 1 <= i by A5, XXREAL_2:def_8;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
suppose x in Roots qq ; ::_thesis: contradiction
then x is_a_root_of qq by POLYNOM5:def_9;
then qq = <%(- x),(1. L)%> *' (poly_quotient (qq,x)) by Th50;
then q = ((<%(- x),(1. L)%> `^ j) *' <%(- x),(1. L)%>) *' (poly_quotient (qq,x)) by A15, POLYNOM3:33
.= ((<%(- x),(1. L)%> `^ j) *' (<%(- x),(1. L)%> `^ 1)) *' (poly_quotient (qq,x)) by POLYNOM5:16
.= (<%(- x),(1. L)%> `^ (j + 1)) *' (poly_quotient (qq,x)) by Th30 ;
then j + 1 in g by A8;
then j + 1 <= j by A13, XXREAL_2:def_8;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
end;
end;
i + j in F by A1, A16;
then i + j <= k by A10, XXREAL_2:def_8;
hence multiplicity ((p *' q),x) = (multiplicity (p,x)) + (multiplicity (q,x)) by A2, A4, A9, A10, A5, A13, A17, XXREAL_0:1; ::_thesis: verum
end;
theorem Th56: :: UPROOTS:56
for L being domRing
for p, q being non-zero Polynomial of L holds BRoots (p *' q) = (BRoots p) + (BRoots q)
proof
let L be domRing; ::_thesis: for p, q being non-zero Polynomial of L holds BRoots (p *' q) = (BRoots p) + (BRoots q)
let p, q be non-zero Polynomial of L; ::_thesis: BRoots (p *' q) = (BRoots p) + (BRoots q)
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_L_holds_
(BRoots_(p_*'_q))_._i_=_((BRoots_p)_+_(BRoots_q))_._i
let i be set ; ::_thesis: ( i in the carrier of L implies (BRoots (p *' q)) . i = ((BRoots p) + (BRoots q)) . i )
assume i in the carrier of L ; ::_thesis: (BRoots (p *' q)) . i = ((BRoots p) + (BRoots q)) . i
then reconsider x = i as Element of L ;
thus (BRoots (p *' q)) . i = multiplicity ((p *' q),x) by Def9
.= (multiplicity (p,x)) + (multiplicity (q,x)) by Th55
.= ((BRoots p) . i) + (multiplicity (q,x)) by Def9
.= ((BRoots p) . i) + ((BRoots q) . i) by Def9
.= ((BRoots p) + (BRoots q)) . i by PRE_POLY:def_5 ; ::_thesis: verum
end;
hence BRoots (p *' q) = (BRoots p) + (BRoots q) by PBOOLE:3; ::_thesis: verum
end;
Lm2: now__::_thesis:_for_L_being_domRing
for_p,_q_being_non-zero_Polynomial_of_L_holds_degree_(BRoots_(p_*'_q))_=_(degree_(BRoots_p))_+_(degree_(BRoots_q))
let L be domRing; ::_thesis: for p, q being non-zero Polynomial of L holds degree (BRoots (p *' q)) = (degree (BRoots p)) + (degree (BRoots q))
let p, q be non-zero Polynomial of L; ::_thesis: degree (BRoots (p *' q)) = (degree (BRoots p)) + (degree (BRoots q))
BRoots (p *' q) = (BRoots p) + (BRoots q) by Th56;
hence degree (BRoots (p *' q)) = (degree (BRoots p)) + (degree (BRoots q)) by Th15; ::_thesis: verum
end;
theorem Th57: :: UPROOTS:57
for L being domRing
for p being non-zero Polynomial of L st len p = 1 holds
degree (BRoots p) = 0
proof
let L be domRing; ::_thesis: for p being non-zero Polynomial of L st len p = 1 holds
degree (BRoots p) = 0
let p be non-zero Polynomial of L; ::_thesis: ( len p = 1 implies degree (BRoots p) = 0 )
assume len p = 1 ; ::_thesis: degree (BRoots p) = 0
then Roots p = {} by Th46;
then support (BRoots p) = {} by Def9;
then BRoots p = EmptyBag the carrier of L by BAGORDER:19;
hence degree (BRoots p) = 0 by Th11; ::_thesis: verum
end;
theorem Th58: :: UPROOTS:58
for L being domRing
for x being Element of L
for n being Element of NAT holds degree (BRoots (<%(- x),(1. L)%> `^ n)) = n
proof
let L be domRing; ::_thesis: for x being Element of L
for n being Element of NAT holds degree (BRoots (<%(- x),(1. L)%> `^ n)) = n
let x be Element of L; ::_thesis: for n being Element of NAT holds degree (BRoots (<%(- x),(1. L)%> `^ n)) = n
set r = <%(- x),(1. L)%>;
defpred S1[ Element of NAT ] means degree (BRoots (<%(- x),(1. L)%> `^ $1)) = $1;
A1: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
<%(- x),(1. L)%> `^ (n + 1) = (<%(- x),(1. L)%> `^ n) *' <%(- x),(1. L)%> by POLYNOM5:19;
then A3: degree (BRoots (<%(- x),(1. L)%> `^ (n + 1))) = (degree (BRoots (<%(- x),(1. L)%> `^ n))) + (degree (BRoots <%(- x),(1. L)%>)) by Lm2
.= n + (degree (({x},1) -bag)) by A2, Th54 ;
card {x} = 1 by CARD_1:30;
hence S1[n + 1] by A3, Th13; ::_thesis: verum
end;
( len (1_. L) = 1 & <%(- x),(1. L)%> `^ 0 = 1_. L ) by POLYNOM4:4, POLYNOM5:15;
then A4: S1[ 0 ] by Th57;
thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A1); ::_thesis: verum
end;
theorem :: UPROOTS:59
for L being algebraic-closed domRing
for p being non-zero Polynomial of L holds degree (BRoots p) = (len p) -' 1
proof
let L be algebraic-closed domRing; ::_thesis: for p being non-zero Polynomial of L holds degree (BRoots p) = (len p) -' 1
let p be non-zero Polynomial of L; ::_thesis: degree (BRoots p) = (len p) -' 1
defpred S1[ Nat] means for p being non-zero Polynomial of L st len p = $1 & $1 > 0 holds
degree (BRoots p) = (len p) -' 1;
A1: for k being Nat st ( for n being Nat st n < k holds
S1[n] ) holds
S1[k]
proof
let k be Nat; ::_thesis: ( ( for n being Nat st n < k holds
S1[n] ) implies S1[k] )
assume A2: for n being Nat st n < k holds
S1[n] ; ::_thesis: S1[k]
let p be non-zero Polynomial of L; ::_thesis: ( len p = k & k > 0 implies degree (BRoots p) = (len p) -' 1 )
assume that
A3: len p = k and
A4: k > 0 ; ::_thesis: degree (BRoots p) = (len p) -' 1
A5: k >= 0 + 1 by A4, NAT_1:13;
thus degree (BRoots p) = (len p) -' 1 ::_thesis: verum
proof
percases ( k = 1 or k > 1 ) by A5, XXREAL_0:1;
supposeA6: k = 1 ; ::_thesis: degree (BRoots p) = (len p) -' 1
hence degree (BRoots p) = 1 - 1 by A3, Th57
.= (len p) -' 1 by A3, A6, XREAL_1:233 ;
::_thesis: verum
end;
supposeA7: k > 1 ; ::_thesis: degree (BRoots p) = (len p) -' 1
then p is with_roots by A3, POLYNOM5:def_8;
then consider x being Element of L such that
A8: x is_a_root_of p by POLYNOM5:def_7;
A9: multiplicity (p,x) >= 1 by A8, Th52;
set r = <%(- x),(1. L)%>;
consider F being non empty finite Subset of NAT such that
A10: F = { l where l is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ l) *' q } and
A11: multiplicity (p,x) = max F by Def8;
max F in F by XXREAL_2:def_8;
then consider l being Element of NAT such that
A12: l = max F and
A13: ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ l) *' q by A10;
set rr = <%(- x),(1. L)%> `^ l;
consider q being Polynomial of L such that
A14: p = (<%(- x),(1. L)%> `^ l) *' q by A13;
reconsider q = q as non-zero Polynomial of L by A14, Th34;
len q > 0 by Th17;
then A15: len q >= 0 + 1 by NAT_1:13;
thus degree (BRoots p) = (len p) -' 1 ::_thesis: verum
proof
len q > 0 by Th17;
then A16: q . ((len q) -' 1) <> 0. L by Th18;
len (<%(- x),(1. L)%> `^ l) > 0 by Th17;
then (<%(- x),(1. L)%> `^ l) . ((len (<%(- x),(1. L)%> `^ l)) -' 1) <> 0. L by Th18;
then A17: ((<%(- x),(1. L)%> `^ l) . ((len (<%(- x),(1. L)%> `^ l)) -' 1)) * (q . ((len q) -' 1)) <> 0. L by A16, VECTSP_2:def_1;
A18: ((l * 2) - l) + 1 = l + 1 ;
A19: len <%(- x),(1. L)%> = 2 by POLYNOM5:40;
then A20: len (<%(- x),(1. L)%> `^ l) = ((l * 2) - l) + 1 by POLYNOM5:23;
then A21: len (<%(- x),(1. L)%> `^ l) > 1 by A9, A11, A12, NAT_1:13;
percases ( len q = 1 or len q > 1 ) by A15, XXREAL_0:1;
supposeA22: len q = 1 ; ::_thesis: degree (BRoots p) = (len p) -' 1
A23: len p = ((len (<%(- x),(1. L)%> `^ l)) + (len q)) - 1 by A14, A17, POLYNOM4:10
.= len (<%(- x),(1. L)%> `^ l) by A22 ;
thus degree (BRoots p) = (degree (BRoots (<%(- x),(1. L)%> `^ l))) + (degree (BRoots q)) by A14, Lm2
.= (degree (BRoots (<%(- x),(1. L)%> `^ l))) + 0 by A22, Th57
.= (((2 * l) - l) + 1) - 1 by Th58
.= (len p) -' 1 by A3, A5, A20, A23, XREAL_1:233 ; ::_thesis: verum
end;
supposeA24: len q > 1 ; ::_thesis: degree (BRoots p) = (len p) -' 1
then A25: ( degree (BRoots (<%(- x),(1. L)%> `^ l)) = (l + 1) -' 1 & degree (BRoots q) = (len q) -' 1 ) by A2, A3, A14, A20, A21, Th36;
thus degree (BRoots p) = (degree (BRoots (<%(- x),(1. L)%> `^ l))) + (degree (BRoots q)) by A14, Lm2
.= ((len (<%(- x),(1. L)%> `^ l)) -' 1) + ((len q) -' 1) by A19, A18, A25, POLYNOM5:23
.= ((len (<%(- x),(1. L)%> `^ l)) - 1) + ((len q) -' 1) by A21, XREAL_1:233
.= ((len (<%(- x),(1. L)%> `^ l)) - 1) + ((len q) - 1) by A24, XREAL_1:233
.= (((len (<%(- x),(1. L)%> `^ l)) + (len q)) - 1) - 1
.= (len p) - 1 by A14, A17, POLYNOM4:10
.= (len p) -' 1 by A3, A7, XREAL_1:233 ; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
A26: for n being Nat holds S1[n] from NAT_1:sch_4(A1);
len p > 0 by Th17;
hence degree (BRoots p) = (len p) -' 1 by A26; ::_thesis: verum
end;
definition
let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ;
let c be Element of L;
let n be Element of NAT ;
func fpoly_mult_root (c,n) -> FinSequence of (Polynom-Ring L) means :Def10: :: UPROOTS:def 10
( len it = n & ( for i being Element of NAT st i in dom it holds
it . i = <%(- c),(1. L)%> ) );
existence
ex b1 being FinSequence of (Polynom-Ring L) st
( len b1 = n & ( for i being Element of NAT st i in dom b1 holds
b1 . i = <%(- c),(1. L)%> ) )
proof
<%(- c),(1. L)%> is Element of (Polynom-Ring L) by POLYNOM3:def_10;
then reconsider f = n |-> <%(- c),(1. L)%> as FinSequence of (Polynom-Ring L) by FINSEQ_2:63;
take f ; ::_thesis: ( len f = n & ( for i being Element of NAT st i in dom f holds
f . i = <%(- c),(1. L)%> ) )
thus A1: len f = n by CARD_1:def_7; ::_thesis: for i being Element of NAT st i in dom f holds
f . i = <%(- c),(1. L)%>
let i be Element of NAT ; ::_thesis: ( i in dom f implies f . i = <%(- c),(1. L)%> )
assume i in dom f ; ::_thesis: f . i = <%(- c),(1. L)%>
then i in Seg n by A1, FINSEQ_1:def_3;
hence f . i = <%(- c),(1. L)%> by FUNCOP_1:7; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence of (Polynom-Ring L) st len b1 = n & ( for i being Element of NAT st i in dom b1 holds
b1 . i = <%(- c),(1. L)%> ) & len b2 = n & ( for i being Element of NAT st i in dom b2 holds
b2 . i = <%(- c),(1. L)%> ) holds
b1 = b2
proof
let it1, it2 be FinSequence of (Polynom-Ring L); ::_thesis: ( len it1 = n & ( for i being Element of NAT st i in dom it1 holds
it1 . i = <%(- c),(1. L)%> ) & len it2 = n & ( for i being Element of NAT st i in dom it2 holds
it2 . i = <%(- c),(1. L)%> ) implies it1 = it2 )
assume that
A2: len it1 = n and
A3: for i being Element of NAT st i in dom it1 holds
it1 . i = <%(- c),(1. L)%> and
A4: len it2 = n and
A5: for i being Element of NAT st i in dom it2 holds
it2 . i = <%(- c),(1. L)%> ; ::_thesis: it1 = it2
A6: dom it1 = dom it2 by A2, A4, FINSEQ_3:29;
now__::_thesis:_for_x_being_Nat_st_x_in_dom_it1_holds_
it1_._x_=_it2_._x
let x be Nat; ::_thesis: ( x in dom it1 implies it1 . x = it2 . x )
assume A7: x in dom it1 ; ::_thesis: it1 . x = it2 . x
hence it1 . x = <%(- c),(1. L)%> by A3
.= it2 . x by A5, A6, A7 ;
::_thesis: verum
end;
hence it1 = it2 by A6, FINSEQ_1:13; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines fpoly_mult_root UPROOTS:def_10_:_
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for c being Element of L
for n being Element of NAT
for b4 being FinSequence of (Polynom-Ring L) holds
( b4 = fpoly_mult_root (c,n) iff ( len b4 = n & ( for i being Element of NAT st i in dom b4 holds
b4 . i = <%(- c),(1. L)%> ) ) );
definition
let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ;
let b be bag of the carrier of L;
func poly_with_roots b -> Polynomial of L means :Def11: :: UPROOTS:def 11
ex f being FinSequence of the carrier of (Polynom-Ring L) * ex s being FinSequence of L st
( len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & it = Product (FlattenSeq f) );
existence
ex b1 being Polynomial of L ex f being FinSequence of the carrier of (Polynom-Ring L) * ex s being FinSequence of L st
( len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & b1 = Product (FlattenSeq f) )
proof
( support b c= dom b & dom b = the carrier of L ) by PARTFUN1:def_2, PRE_POLY:37;
then rng (canFS (support b)) c= the carrier of L by XBOOLE_1:1;
then reconsider s = canFS (support b) as FinSequence of L by FINSEQ_1:def_4;
deffunc H1( set ) -> FinSequence of (Polynom-Ring L) = fpoly_mult_root ((s /. $1),(b . (s /. $1)));
consider f being FinSequence such that
A1: len f = card (support b) and
A2: for k being Nat st k in dom f holds
f . k = H1(k) from FINSEQ_1:sch_2();
rng f c= the carrier of (Polynom-Ring L) *
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in the carrier of (Polynom-Ring L) * )
assume x in rng f ; ::_thesis: x in the carrier of (Polynom-Ring L) *
then consider i being Nat such that
A3: ( i in dom f & f . i = x ) by FINSEQ_2:10;
x = H1(i) by A2, A3;
hence x in the carrier of (Polynom-Ring L) * by FINSEQ_1:def_11; ::_thesis: verum
end;
then reconsider f = f as FinSequence of the carrier of (Polynom-Ring L) * by FINSEQ_1:def_4;
reconsider it1 = Product (FlattenSeq f) as Polynomial of L by POLYNOM3:def_10;
take it1 ; ::_thesis: ex f being FinSequence of the carrier of (Polynom-Ring L) * ex s being FinSequence of L st
( len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & it1 = Product (FlattenSeq f) )
take f ; ::_thesis: ex s being FinSequence of L st
( len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & it1 = Product (FlattenSeq f) )
take s ; ::_thesis: ( len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & it1 = Product (FlattenSeq f) )
thus len f = card (support b) by A1; ::_thesis: ( s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & it1 = Product (FlattenSeq f) )
thus s = canFS (support b) ; ::_thesis: ( ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & it1 = Product (FlattenSeq f) )
thus for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) by A2; ::_thesis: it1 = Product (FlattenSeq f)
thus it1 = Product (FlattenSeq f) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Polynomial of L st ex f being FinSequence of the carrier of (Polynom-Ring L) * ex s being FinSequence of L st
( len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & b1 = Product (FlattenSeq f) ) & ex f being FinSequence of the carrier of (Polynom-Ring L) * ex s being FinSequence of L st
( len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & b2 = Product (FlattenSeq f) ) holds
b1 = b2
proof
let it1, it2 be Polynomial of L; ::_thesis: ( ex f being FinSequence of the carrier of (Polynom-Ring L) * ex s being FinSequence of L st
( len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & it1 = Product (FlattenSeq f) ) & ex f being FinSequence of the carrier of (Polynom-Ring L) * ex s being FinSequence of L st
( len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & it2 = Product (FlattenSeq f) ) implies it1 = it2 )
given f1 being FinSequence of the carrier of (Polynom-Ring L) * , s1 being FinSequence of L such that A4: len f1 = card (support b) and
A5: s1 = canFS (support b) and
A6: for i being Element of NAT st i in dom f1 holds
f1 . i = fpoly_mult_root ((s1 /. i),(b . (s1 /. i))) and
A7: it1 = Product (FlattenSeq f1) ; ::_thesis: ( for f being FinSequence of the carrier of (Polynom-Ring L) *
for s being FinSequence of L holds
( not len f = card (support b) or not s = canFS (support b) or ex i being Element of NAT st
( i in dom f & not f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) or not it2 = Product (FlattenSeq f) ) or it1 = it2 )
given f2 being FinSequence of the carrier of (Polynom-Ring L) * , s2 being FinSequence of L such that A8: len f2 = card (support b) and
A9: ( s2 = canFS (support b) & ( for i being Element of NAT st i in dom f2 holds
f2 . i = fpoly_mult_root ((s2 /. i),(b . (s2 /. i))) ) ) and
A10: it2 = Product (FlattenSeq f2) ; ::_thesis: it1 = it2
A11: dom f1 = dom f2 by A4, A8, FINSEQ_3:29;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_f1_holds_
f1_._i_=_f2_._i
let i be Nat; ::_thesis: ( i in dom f1 implies f1 . i = f2 . i )
assume A12: i in dom f1 ; ::_thesis: f1 . i = f2 . i
hence f1 . i = fpoly_mult_root ((s1 /. i),(b . (s1 /. i))) by A6
.= f2 . i by A5, A9, A11, A12 ;
::_thesis: verum
end;
hence it1 = it2 by A4, A7, A8, A10, FINSEQ_2:9; ::_thesis: verum
end;
end;
:: deftheorem Def11 defines poly_with_roots UPROOTS:def_11_:_
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for b being bag of the carrier of L
for b3 being Polynomial of L holds
( b3 = poly_with_roots b iff ex f being FinSequence of the carrier of (Polynom-Ring L) * ex s being FinSequence of L st
( len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & b3 = Product (FlattenSeq f) ) );
theorem Th60: :: UPROOTS:60
for L being non empty right_complementable commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr holds poly_with_roots (EmptyBag the carrier of L) = <%(1. L)%>
proof
let L be non empty right_complementable commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: poly_with_roots (EmptyBag the carrier of L) = <%(1. L)%>
set b = EmptyBag the carrier of L;
consider f being FinSequence of the carrier of (Polynom-Ring L) * , s being FinSequence of L such that
A1: len f = card (support (EmptyBag the carrier of L)) and
s = canFS (support (EmptyBag the carrier of L)) and
for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),((EmptyBag the carrier of L) . (s /. i))) and
A2: poly_with_roots (EmptyBag the carrier of L) = Product (FlattenSeq f) by Def11;
f = <*> ( the carrier of (Polynom-Ring L) *) by A1, BAGORDER:18, CARD_1:27;
then ( 1_ (Polynom-Ring L) = 1. (Polynom-Ring L) & FlattenSeq f = <*> the carrier of (Polynom-Ring L) ) ;
then Product (FlattenSeq f) = 1. (Polynom-Ring L) by GROUP_4:8
.= 1_. L by POLYNOM3:36 ;
hence poly_with_roots (EmptyBag the carrier of L) = <%(1. L)%> by A2, Th31; ::_thesis: verum
end;
theorem Th61: :: UPROOTS:61
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for c being Element of L holds poly_with_roots (({c},1) -bag) = <%(- c),(1. L)%>
proof
let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for c being Element of L holds poly_with_roots (({c},1) -bag) = <%(- c),(1. L)%>
let c be Element of L; ::_thesis: poly_with_roots (({c},1) -bag) = <%(- c),(1. L)%>
set b = ({c},1) -bag ;
consider f being FinSequence of the carrier of (Polynom-Ring L) * , s being FinSequence of L such that
A1: len f = card (support (({c},1) -bag)) and
A2: s = canFS (support (({c},1) -bag)) and
A3: for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),((({c},1) -bag) . (s /. i))) and
A4: poly_with_roots (({c},1) -bag) = Product (FlattenSeq f) by Def11;
A5: support (({c},1) -bag) = {c} by Th8;
then A6: s = <*c*> by A2, Th4;
A7: card (support (({c},1) -bag)) = 1 by A5, CARD_1:30;
then A8: 1 in dom f by A1, FINSEQ_3:25;
then A9: f . 1 = f /. 1 by PARTFUN1:def_6;
len s = 1 by A2, A7, Th3;
then 1 in dom s by FINSEQ_3:25;
then A10: s /. 1 = s . 1 by PARTFUN1:def_6
.= c by A6, FINSEQ_1:40 ;
set f1 = fpoly_mult_root ((s /. 1),((({c},1) -bag) . (s /. 1)));
c in {c} by TARSKI:def_1;
then (({c},1) -bag) . (s /. 1) = 1 by A10, Th7;
then A11: len (fpoly_mult_root ((s /. 1),((({c},1) -bag) . (s /. 1)))) = 1 by Def10;
then A12: 1 in dom (fpoly_mult_root ((s /. 1),((({c},1) -bag) . (s /. 1)))) by FINSEQ_3:25;
f = <*(f /. 1)*> by A1, A5, CARD_1:30, FINSEQ_5:14;
then A13: FlattenSeq f = f . 1 by A9, PRE_POLY:1;
A14: f . 1 = fpoly_mult_root ((s /. 1),((({c},1) -bag) . (s /. 1))) by A3, A8;
fpoly_mult_root ((s /. 1),((({c},1) -bag) . (s /. 1))) = <*((fpoly_mult_root ((s /. 1),((({c},1) -bag) . (s /. 1)))) /. 1)*> by A11, FINSEQ_5:14;
hence poly_with_roots (({c},1) -bag) = (fpoly_mult_root ((s /. 1),((({c},1) -bag) . (s /. 1)))) /. 1 by A4, A13, A14, FINSOP_1:11
.= (fpoly_mult_root ((s /. 1),((({c},1) -bag) . (s /. 1)))) . 1 by A12, PARTFUN1:def_6
.= <%(- c),(1. L)%> by A10, A12, Def10 ;
::_thesis: verum
end;
theorem Th62: :: UPROOTS:62
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for b being bag of the carrier of L
for f being FinSequence of the carrier of (Polynom-Ring L) *
for s being FinSequence of L st len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds
len (FlattenSeq f) = degree b
proof
let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for b being bag of the carrier of L
for f being FinSequence of the carrier of (Polynom-Ring L) *
for s being FinSequence of L st len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds
len (FlattenSeq f) = degree b
let b be bag of the carrier of L; ::_thesis: for f being FinSequence of the carrier of (Polynom-Ring L) *
for s being FinSequence of L st len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds
len (FlattenSeq f) = degree b
let f be FinSequence of the carrier of (Polynom-Ring L) * ; ::_thesis: for s being FinSequence of L st len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds
len (FlattenSeq f) = degree b
let s be FinSequence of L; ::_thesis: ( len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) implies len (FlattenSeq f) = degree b )
assume that
A1: len f = card (support b) and
A2: s = canFS (support b) and
A3: for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ; ::_thesis: len (FlattenSeq f) = degree b
reconsider Cf = Card f as FinSequence of NAT ;
consider g being FinSequence of NAT such that
A4: degree b = Sum g and
A5: g = b * (canFS (support b)) by Def4;
len s = card (support b) by A2, Th3;
then A6: dom f = dom s by A1, FINSEQ_3:29;
A7: now__::_thesis:_(_dom_(Card_f)_=_dom_g_&_(_for_i_being_Nat_st_i_in_dom_(Card_f)_holds_
Cf_._i_=_g_._i_)_)
A8: rng s c= dom b
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng s or x in dom b )
assume x in rng s ; ::_thesis: x in dom b
then A9: x in support b by A2, FUNCT_2:def_3;
support b c= dom b by PRE_POLY:37;
hence x in dom b by A9; ::_thesis: verum
end;
thus dom (Card f) = dom f by CARD_3:def_2
.= dom g by A2, A6, A5, A8, RELAT_1:27 ; ::_thesis: for i being Nat st i in dom (Card f) holds
Cf . i = g . i
let i be Nat; ::_thesis: ( i in dom (Card f) implies Cf . i = g . i )
assume i in dom (Card f) ; ::_thesis: Cf . i = g . i
then A10: i in dom f by CARD_3:def_2;
then A11: g . i = b . (s . i) by A2, A6, A5, FUNCT_1:13;
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) by A3, A10;
then A12: len (f . i) = b . (s /. i) by Def10;
thus Cf . i = card (f . i) by A10, CARD_3:def_2
.= g . i by A6, A10, A12, A11, PARTFUN1:def_6 ; ::_thesis: verum
end;
len (FlattenSeq f) = Sum Cf by PRE_POLY:27;
hence len (FlattenSeq f) = degree b by A4, A7, FINSEQ_1:13; ::_thesis: verum
end;
theorem Th63: :: UPROOTS:63
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for b being bag of the carrier of L
for f being FinSequence of the carrier of (Polynom-Ring L) *
for s being FinSequence of L
for c being Element of L st len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds
( ( c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = b . c ) & ( not c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = 0 ) )
proof
let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for b being bag of the carrier of L
for f being FinSequence of the carrier of (Polynom-Ring L) *
for s being FinSequence of L
for c being Element of L st len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds
( ( c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = b . c ) & ( not c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = 0 ) )
let b be bag of the carrier of L; ::_thesis: for f being FinSequence of the carrier of (Polynom-Ring L) *
for s being FinSequence of L
for c being Element of L st len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds
( ( c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = b . c ) & ( not c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = 0 ) )
let f be FinSequence of the carrier of (Polynom-Ring L) * ; ::_thesis: for s being FinSequence of L
for c being Element of L st len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds
( ( c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = b . c ) & ( not c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = 0 ) )
let s be FinSequence of L; ::_thesis: for c being Element of L st len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds
( ( c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = b . c ) & ( not c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = 0 ) )
let c be Element of L; ::_thesis: ( len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) implies ( ( c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = b . c ) & ( not c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = 0 ) ) )
assume that
A1: len f = card (support b) and
A2: s = canFS (support b) and
A3: for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ; ::_thesis: ( ( c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = b . c ) & ( not c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = 0 ) )
len f = len s by A1, A2, Th3;
then A4: dom f = dom s by FINSEQ_3:29;
hereby ::_thesis: ( not c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = 0 )
set X = { k where k is Element of NAT : k < b . c } ;
set ff = FlattenSeq f;
set Y = (FlattenSeq f) " {<%(- c),(1. L)%>};
assume c in support b ; ::_thesis: card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = b . c
then c in rng s by A2, FUNCT_2:def_3;
then consider i being Nat such that
A5: i in dom s and
A6: s . i = c by FINSEQ_2:10;
defpred S1[ set , set ] means ex n being Element of NAT st
( n = $1 & $2 = (Sum (Card (f | (i -' 1)))) + (1 + n) );
A7: for x being set st x in { k where k is Element of NAT : k < b . c } holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in { k where k is Element of NAT : k < b . c } implies ex y being set st S1[x,y] )
assume x in { k where k is Element of NAT : k < b . c } ; ::_thesis: ex y being set st S1[x,y]
then consider k being Element of NAT such that
A8: x = k and
k < b . c ;
take (Sum (Card (f | (i -' 1)))) + (1 + k) ; ::_thesis: S1[x,(Sum (Card (f | (i -' 1)))) + (1 + k)]
thus S1[x,(Sum (Card (f | (i -' 1)))) + (1 + k)] by A8; ::_thesis: verum
end;
consider g being Function such that
A9: dom g = { k where k is Element of NAT : k < b . c } and
A10: for x being set st x in { k where k is Element of NAT : k < b . c } holds
S1[x,g . x] from CLASSES1:sch_1(A7);
A11: s /. i = c by A5, A6, PARTFUN1:def_6;
now__::_thesis:_for_y_being_set_holds_
(_(_y_in_rng_g_implies_y_in_(FlattenSeq_f)_"_{<%(-_c),(1._L)%>}_)_&_(_y_in_(FlattenSeq_f)_"_{<%(-_c),(1._L)%>}_implies_y_in_rng_g_)_)
let y be set ; ::_thesis: ( ( y in rng g implies y in (FlattenSeq f) " {<%(- c),(1. L)%>} ) & ( y in (FlattenSeq f) " {<%(- c),(1. L)%>} implies y in rng g ) )
A12: <%(- c),(1. L)%> . 0 = - c by POLYNOM5:38;
hereby ::_thesis: ( y in (FlattenSeq f) " {<%(- c),(1. L)%>} implies y in rng g )
assume y in rng g ; ::_thesis: y in (FlattenSeq f) " {<%(- c),(1. L)%>}
then consider x being set such that
A13: x in dom g and
A14: y = g . x by FUNCT_1:def_3;
consider n being Element of NAT such that
A15: n = x and
A16: g . x = (Sum (Card (f | (i -' 1)))) + (1 + n) by A9, A10, A13;
ex k being Element of NAT st
( x = k & k < b . c ) by A9, A13;
then A17: ( 1 <= 1 + n & 1 + n <= b . c ) by A15, NAT_1:12, NAT_1:13;
A18: f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) by A3, A4, A5;
then len (f . i) = b . c by A11, Def10;
then A19: 1 + n in dom (f . i) by A17, FINSEQ_3:25;
then (f . i) . (1 + n) = <%(- c),(1. L)%> by A11, A18, Def10;
then A20: (f . i) . (1 + n) in {<%(- c),(1. L)%>} by TARSKI:def_1;
( (Sum (Card (f | (i -' 1)))) + (1 + n) in dom (FlattenSeq f) & (f . i) . (1 + n) = (FlattenSeq f) . ((Sum (Card (f | (i -' 1)))) + (1 + n)) ) by A4, A5, A19, PRE_POLY:30;
hence y in (FlattenSeq f) " {<%(- c),(1. L)%>} by A14, A16, A20, FUNCT_1:def_7; ::_thesis: verum
end;
assume A21: y in (FlattenSeq f) " {<%(- c),(1. L)%>} ; ::_thesis: y in rng g
then reconsider yn = y as Element of NAT ;
A22: (FlattenSeq f) . y in {<%(- c),(1. L)%>} by A21, FUNCT_1:def_7;
y in dom (FlattenSeq f) by A21, FUNCT_1:def_7;
then consider i1, j being Element of NAT such that
A23: i1 in dom f and
A24: j in dom (f . i1) and
A25: yn = (Sum (Card (f | (i1 -' 1)))) + j and
A26: (f . i1) . j = (FlattenSeq f) . yn by PRE_POLY:29;
A27: f . i1 = fpoly_mult_root ((s /. i1),(b . (s /. i1))) by A3, A23;
then (f . i1) . j = <%(- (s /. i1)),(1. L)%> by A24, Def10;
then <%(- c),(1. L)%> = <%(- (s /. i1)),(1. L)%> by A22, A26, TARSKI:def_1;
then A28: c = s /. i1 by A12, POLYNOM5:38, RLVECT_1:18;
( i1 in dom s & s /. i1 = s . i1 ) by A4, A23, PARTFUN1:def_6;
then A29: i1 = i by A2, A5, A6, A28, FUNCT_1:def_4;
consider j1 being Nat such that
A30: j = j1 + 1 by A24, FINSEQ_3:24, NAT_1:6;
reconsider j1 = j1 as Element of NAT by ORDINAL1:def_12;
len (f . i1) = b . c by A27, A28, Def10;
then j <= b . c by A24, FINSEQ_3:25;
then j1 < b . c by A30, NAT_1:13;
then A31: j1 in { k where k is Element of NAT : k < b . c } ;
then ex n being Element of NAT st
( n = j1 & g . j1 = (Sum (Card (f | (i -' 1)))) + (1 + n) ) by A10;
hence y in rng g by A9, A25, A30, A29, A31, FUNCT_1:3; ::_thesis: verum
end;
then A32: rng g = (FlattenSeq f) " {<%(- c),(1. L)%>} by TARSKI:1;
g is one-to-one
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in proj1 g or not x2 in proj1 g or not g . x1 = g . x2 or x1 = x2 )
assume that
A33: ( x1 in dom g & x2 in dom g ) and
A34: g . x1 = g . x2 ; ::_thesis: x1 = x2
( ex n1 being Element of NAT st
( n1 = x1 & g . x1 = (Sum (Card (f | (i -' 1)))) + (1 + n1) ) & ex n2 being Element of NAT st
( n2 = x2 & g . x2 = (Sum (Card (f | (i -' 1)))) + (1 + n2) ) ) by A9, A10, A33;
hence x1 = x2 by A34; ::_thesis: verum
end;
then ( b . c = { k where k is Element of NAT : k < b . c } & { k where k is Element of NAT : k < b . c } ,(FlattenSeq f) " {<%(- c),(1. L)%>} are_equipotent ) by A9, A32, AXIOMS:4, WELLORD2:def_4;
hence card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = b . c by CARD_1:def_2; ::_thesis: verum
end;
assume that
A35: not c in support b and
A36: card ((FlattenSeq f) " {<%(- c),(1. L)%>}) <> 0 ; ::_thesis: contradiction
consider x being set such that
A37: x in (FlattenSeq f) " {<%(- c),(1. L)%>} by A36, CARD_1:27, XBOOLE_0:def_1;
A38: x in dom (FlattenSeq f) by A37, FUNCT_1:def_7;
reconsider x = x as Element of NAT by A37;
consider i, j being Element of NAT such that
A39: i in dom f and
A40: j in dom (f . i) and
x = (Sum (Card (f | (i -' 1)))) + j and
A41: (f . i) . j = (FlattenSeq f) . x by A38, PRE_POLY:29;
A42: ( s /. i = s . i & s . i in rng s ) by A4, A39, FUNCT_1:3, PARTFUN1:def_6;
(FlattenSeq f) . x in {<%(- c),(1. L)%>} by A37, FUNCT_1:def_7;
then A43: (FlattenSeq f) . x = <%(- c),(1. L)%> by TARSKI:def_1;
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) by A3, A39;
then A44: (f . i) . j = <%(- (s /. i)),(1. L)%> by A40, Def10;
<%(- c),(1. L)%> . 0 = - c by POLYNOM5:38;
then c = s /. i by A41, A43, A44, POLYNOM5:38, RLVECT_1:18;
hence contradiction by A2, A35, A42, FUNCT_2:def_3; ::_thesis: verum
end;
theorem Th64: :: UPROOTS:64
for L being comRing
for b1, b2 being bag of the carrier of L holds poly_with_roots (b1 + b2) = (poly_with_roots b1) *' (poly_with_roots b2)
proof
let L be comRing; ::_thesis: for b1, b2 being bag of the carrier of L holds poly_with_roots (b1 + b2) = (poly_with_roots b1) *' (poly_with_roots b2)
let b1, b2 be bag of the carrier of L; ::_thesis: poly_with_roots (b1 + b2) = (poly_with_roots b1) *' (poly_with_roots b2)
set b = b1 + b2;
A1: support (b1 + b2) = (support b1) \/ (support b2) by PRE_POLY:38;
consider f2 being FinSequence of the carrier of (Polynom-Ring L) * , s2 being FinSequence of L such that
A2: len f2 = card (support b2) and
A3: s2 = canFS (support b2) and
A4: for i being Element of NAT st i in dom f2 holds
f2 . i = fpoly_mult_root ((s2 /. i),(b2 . (s2 /. i))) and
A5: poly_with_roots b2 = Product (FlattenSeq f2) by Def11;
consider f1 being FinSequence of the carrier of (Polynom-Ring L) * , s1 being FinSequence of L such that
A6: len f1 = card (support b1) and
A7: s1 = canFS (support b1) and
A8: for i being Element of NAT st i in dom f1 holds
f1 . i = fpoly_mult_root ((s1 /. i),(b1 . (s1 /. i))) and
A9: poly_with_roots b1 = Product (FlattenSeq f1) by Def11;
consider f being FinSequence of the carrier of (Polynom-Ring L) * , s being FinSequence of L such that
A10: len f = card (support (b1 + b2)) and
A11: s = canFS (support (b1 + b2)) and
A12: for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),((b1 + b2) . (s /. i))) and
A13: poly_with_roots (b1 + b2) = Product (FlattenSeq f) by Def11;
set ff = FlattenSeq f;
set ff1 = FlattenSeq f1;
set ff2 = FlattenSeq f2;
A14: len (FlattenSeq f) = degree (b1 + b2) by A10, A11, A12, Th62;
A15: len (FlattenSeq f2) = degree b2 by A2, A3, A4, Th62;
set g = (FlattenSeq f1) ^ (FlattenSeq f2);
len ((FlattenSeq f1) ^ (FlattenSeq f2)) = (len (FlattenSeq f1)) + (len (FlattenSeq f2)) by FINSEQ_1:22
.= (degree b1) + (degree b2) by A6, A7, A8, A15, Th62
.= degree (b1 + b2) by Th15 ;
then A16: dom (FlattenSeq f) = dom ((FlattenSeq f1) ^ (FlattenSeq f2)) by A14, FINSEQ_3:29;
A17: len s = card (support (b1 + b2)) by A11, Th3;
now__::_thesis:_for_x_being_set_holds_card_(Coim_((FlattenSeq_f),x))_=_card_(Coim_(((FlattenSeq_f1)_^_(FlattenSeq_f2)),x))
let x be set ; ::_thesis: card (Coim ((FlattenSeq f),b1)) = card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),b1))
percases ( x in rng (FlattenSeq f) or not x in rng (FlattenSeq f) ) ;
suppose x in rng (FlattenSeq f) ; ::_thesis: card (Coim ((FlattenSeq f),b1)) = card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),b1))
then consider k being Nat such that
A18: k in dom (FlattenSeq f) and
A19: (FlattenSeq f) . k = x by FINSEQ_2:10;
consider i, j being Element of NAT such that
A20: i in dom f and
A21: j in dom (f . i) and
k = (Sum (Card (f | (i -' 1)))) + j and
A22: (f . i) . j = (FlattenSeq f) . k by A18, PRE_POLY:29;
f . i = fpoly_mult_root ((s /. i),((b1 + b2) . (s /. i))) by A12, A20;
then A23: (f . i) . j = <%(- (s /. i)),(1. L)%> by A21, Def10;
i in dom s by A10, A17, A20, FINSEQ_3:29;
then ( s . i = s /. i & s . i in rng s ) by FUNCT_1:3, PARTFUN1:def_6;
then A24: s /. i in support (b1 + b2) by A11, FUNCT_2:def_3;
A25: card (((FlattenSeq f1) ^ (FlattenSeq f2)) " {x}) = (card ((FlattenSeq f1) " {x})) + (card ((FlattenSeq f2) " {x})) by FINSEQ_3:57;
percases ( ( s /. i in support b1 & not s /. i in support b2 ) or ( not s /. i in support b1 & s /. i in support b2 ) or ( s /. i in support b1 & s /. i in support b2 ) ) by A1, A24, XBOOLE_0:def_3;
supposeA26: ( s /. i in support b1 & not s /. i in support b2 ) ; ::_thesis: card (Coim ((FlattenSeq f),b1)) = card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),b1))
then A27: card ((FlattenSeq f2) " {x}) = 0 by A2, A3, A4, A19, A22, A23, Th63;
thus card (Coim ((FlattenSeq f),x)) = (b1 + b2) . (s /. i) by A10, A11, A12, A19, A22, A23, A24, Th63
.= (b1 . (s /. i)) + (b2 . (s /. i)) by PRE_POLY:def_5
.= (b1 . (s /. i)) + 0 by A26, PRE_POLY:def_7
.= card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),x)) by A6, A7, A8, A19, A22, A23, A25, A26, A27, Th63 ; ::_thesis: verum
end;
supposeA28: ( not s /. i in support b1 & s /. i in support b2 ) ; ::_thesis: card (Coim ((FlattenSeq f),b1)) = card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),b1))
then A29: card ((FlattenSeq f2) " {x}) = b2 . (s /. i) by A2, A3, A4, A19, A22, A23, Th63;
thus card (Coim ((FlattenSeq f),x)) = (b1 + b2) . (s /. i) by A10, A11, A12, A19, A22, A23, A24, Th63
.= (b1 . (s /. i)) + (b2 . (s /. i)) by PRE_POLY:def_5
.= 0 + (b2 . (s /. i)) by A28, PRE_POLY:def_7
.= card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),x)) by A6, A7, A8, A19, A22, A23, A25, A28, A29, Th63 ; ::_thesis: verum
end;
supposeA30: ( s /. i in support b1 & s /. i in support b2 ) ; ::_thesis: card (Coim ((FlattenSeq f),b1)) = card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),b1))
then A31: card ((FlattenSeq f2) " {x}) = b2 . (s /. i) by A2, A3, A4, A19, A22, A23, Th63;
thus card (Coim ((FlattenSeq f),x)) = (b1 + b2) . (s /. i) by A10, A11, A12, A19, A22, A23, A24, Th63
.= (b1 . (s /. i)) + (b2 . (s /. i)) by PRE_POLY:def_5
.= card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),x)) by A6, A7, A8, A19, A22, A23, A25, A30, A31, Th63 ; ::_thesis: verum
end;
end;
end;
supposeA32: not x in rng (FlattenSeq f) ; ::_thesis: card (Coim ((FlattenSeq f),b1)) = card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),b1))
now__::_thesis:_not_x_in_rng_((FlattenSeq_f1)_^_(FlattenSeq_f2))
assume x in rng ((FlattenSeq f1) ^ (FlattenSeq f2)) ; ::_thesis: contradiction
then A33: x in (rng (FlattenSeq f1)) \/ (rng (FlattenSeq f2)) by FINSEQ_1:31;
percases ( x in rng (FlattenSeq f1) or x in rng (FlattenSeq f2) ) by A33, XBOOLE_0:def_3;
suppose x in rng (FlattenSeq f1) ; ::_thesis: contradiction
then consider k being Nat such that
A34: k in dom (FlattenSeq f1) and
A35: (FlattenSeq f1) . k = x by FINSEQ_2:10;
consider i, j being Element of NAT such that
A36: i in dom f1 and
A37: j in dom (f1 . i) and
k = (Sum (Card (f1 | (i -' 1)))) + j and
A38: (f1 . i) . j = (FlattenSeq f1) . k by A34, PRE_POLY:29;
f1 . i = fpoly_mult_root ((s1 /. i),(b1 . (s1 /. i))) by A8, A36;
then A39: (f1 . i) . j = <%(- (s1 /. i)),(1. L)%> by A37, Def10;
len s1 = card (support b1) by A7, Th3;
then i in dom s1 by A6, A36, FINSEQ_3:29;
then ( s1 . i = s1 /. i & s1 . i in rng s1 ) by FUNCT_1:3, PARTFUN1:def_6;
then s1 /. i in support b1 by A7, FUNCT_2:def_3;
then A40: s1 /. i in support (b1 + b2) by A1, XBOOLE_0:def_3;
then (b1 + b2) . (s1 /. i) <> 0 by PRE_POLY:def_7;
then A41: 0 + 1 <= (b1 + b2) . (s1 /. i) by NAT_1:13;
s1 /. i in rng s by A11, A40, FUNCT_2:def_3;
then consider l being Nat such that
A42: l in dom s and
A43: s . l = s1 /. i by FINSEQ_2:10;
A44: s . l = s /. l by A42, PARTFUN1:def_6;
A45: l in dom f by A10, A17, A42, FINSEQ_3:29;
then A46: f . l = fpoly_mult_root ((s /. l),((b1 + b2) . (s /. l))) by A12;
then len (f . l) = (b1 + b2) . (s /. l) by Def10;
then A47: 1 in dom (f . l) by A43, A44, A41, FINSEQ_3:25;
then ( (Sum (Card (f | (l -' 1)))) + 1 in dom (FlattenSeq f) & (f . l) . 1 = (FlattenSeq f) . ((Sum (Card (f | (l -' 1)))) + 1) ) by A45, PRE_POLY:30;
then (f . l) . 1 in rng (FlattenSeq f) by FUNCT_1:3;
hence contradiction by A32, A35, A38, A39, A43, A46, A44, A47, Def10; ::_thesis: verum
end;
suppose x in rng (FlattenSeq f2) ; ::_thesis: contradiction
then consider k being Nat such that
A48: k in dom (FlattenSeq f2) and
A49: (FlattenSeq f2) . k = x by FINSEQ_2:10;
consider i, j being Element of NAT such that
A50: i in dom f2 and
A51: j in dom (f2 . i) and
k = (Sum (Card (f2 | (i -' 1)))) + j and
A52: (f2 . i) . j = (FlattenSeq f2) . k by A48, PRE_POLY:29;
f2 . i = fpoly_mult_root ((s2 /. i),(b2 . (s2 /. i))) by A4, A50;
then A53: (f2 . i) . j = <%(- (s2 /. i)),(1. L)%> by A51, Def10;
len s2 = card (support b2) by A3, Th3;
then i in dom s2 by A2, A50, FINSEQ_3:29;
then ( s2 . i = s2 /. i & s2 . i in rng s2 ) by FUNCT_1:3, PARTFUN1:def_6;
then s2 /. i in support b2 by A3, FUNCT_2:def_3;
then A54: s2 /. i in support (b1 + b2) by A1, XBOOLE_0:def_3;
then (b1 + b2) . (s2 /. i) <> 0 by PRE_POLY:def_7;
then A55: 0 + 1 <= (b1 + b2) . (s2 /. i) by NAT_1:13;
s2 /. i in rng s by A11, A54, FUNCT_2:def_3;
then consider l being Nat such that
A56: l in dom s and
A57: s . l = s2 /. i by FINSEQ_2:10;
A58: s . l = s /. l by A56, PARTFUN1:def_6;
A59: l in dom f by A10, A17, A56, FINSEQ_3:29;
then A60: f . l = fpoly_mult_root ((s /. l),((b1 + b2) . (s /. l))) by A12;
then len (f . l) = (b1 + b2) . (s /. l) by Def10;
then A61: 1 in dom (f . l) by A57, A58, A55, FINSEQ_3:25;
then ( (Sum (Card (f | (l -' 1)))) + 1 in dom (FlattenSeq f) & (f . l) . 1 = (FlattenSeq f) . ((Sum (Card (f | (l -' 1)))) + 1) ) by A59, PRE_POLY:30;
then (f . l) . 1 in rng (FlattenSeq f) by FUNCT_1:3;
hence contradiction by A32, A49, A52, A53, A57, A60, A58, A61, Def10; ::_thesis: verum
end;
end;
end;
then ((FlattenSeq f1) ^ (FlattenSeq f2)) " {x} = {} by FUNCT_1:72;
hence card (Coim ((FlattenSeq f),x)) = card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),x)) by A32, FUNCT_1:72; ::_thesis: verum
end;
end;
end;
then FlattenSeq f,(FlattenSeq f1) ^ (FlattenSeq f2) are_fiberwise_equipotent by CLASSES1:def_9;
then ex p being Permutation of (dom (FlattenSeq f)) st FlattenSeq f = ((FlattenSeq f1) ^ (FlattenSeq f2)) * p by A16, RFINSEQ:4;
hence poly_with_roots (b1 + b2) = Product ((FlattenSeq f1) ^ (FlattenSeq f2)) by A13, A16, Th16
.= (Product (FlattenSeq f1)) * (Product (FlattenSeq f2)) by GROUP_4:5
.= (poly_with_roots b1) *' (poly_with_roots b2) by A9, A5, POLYNOM3:def_10 ;
::_thesis: verum
end;
theorem :: UPROOTS:65
for L being algebraic-closed domRing
for p being non-zero Polynomial of L st p . ((len p) -' 1) = 1. L holds
p = poly_with_roots (BRoots p)
proof
let L be algebraic-closed domRing; ::_thesis: for p being non-zero Polynomial of L st p . ((len p) -' 1) = 1. L holds
p = poly_with_roots (BRoots p)
let p be non-zero Polynomial of L; ::_thesis: ( p . ((len p) -' 1) = 1. L implies p = poly_with_roots (BRoots p) )
assume A1: p . ((len p) -' 1) = 1. L ; ::_thesis: p = poly_with_roots (BRoots p)
defpred S1[ Nat] means for p being non-zero Polynomial of L st len p = $1 & $1 >= 1 & p . ((len p) -' 1) = 1. L holds
p = poly_with_roots (BRoots p);
len p > 0 by Th17;
then A2: len p >= 0 + 1 by NAT_1:13;
A3: for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] )
assume that
A4: n >= 1 and
A5: S1[n] ; ::_thesis: S1[n + 1]
let p be non-zero Polynomial of L; ::_thesis: ( len p = n + 1 & n + 1 >= 1 & p . ((len p) -' 1) = 1. L implies p = poly_with_roots (BRoots p) )
assume that
A6: len p = n + 1 and
n + 1 >= 1 and
A7: p . ((len p) -' 1) = 1. L ; ::_thesis: p = poly_with_roots (BRoots p)
n + 1 > 1 by A4, NAT_1:13;
then p is with_roots by A6, POLYNOM5:def_8;
then consider x being Element of L such that
A8: x is_a_root_of p by POLYNOM5:def_7;
set r = <%(- x),(1. L)%>;
set q = poly_quotient (p,x);
A9: p = <%(- x),(1. L)%> *' (poly_quotient (p,x)) by A8, Th50;
then reconsider q = poly_quotient (p,x) as non-zero Polynomial of L by Th34;
A10: len <%(- x),(1. L)%> = 2 by POLYNOM5:40;
then A11: <%(- x),(1. L)%> . ((len <%(- x),(1. L)%>) -' 1) <> 0. L by Th18;
len q > 0 by Th17;
then q . ((len q) -' 1) <> 0. L by Th18;
then (<%(- x),(1. L)%> . ((len <%(- x),(1. L)%>) -' 1)) * (q . ((len q) -' 1)) <> 0. L by A11, VECTSP_2:def_1;
then A12: len p = ((len q) + (1 + 1)) - 1 by A9, A10, POLYNOM4:10;
q . ((len q) -' 1) = 1. L by A7, A9, Th41;
then A13: q = poly_with_roots (BRoots q) by A4, A5, A6, A12;
A14: poly_with_roots (({x},1) -bag) = <%(- x),(1. L)%> by Th61;
BRoots <%(- x),(1. L)%> = ({x},1) -bag by Th54;
then BRoots p = (({x},1) -bag) + (BRoots q) by A9, Th56;
hence p = poly_with_roots (BRoots p) by A9, A13, A14, Th64; ::_thesis: verum
end;
A15: S1[1]
proof
let p be non-zero Polynomial of L; ::_thesis: ( len p = 1 & 1 >= 1 & p . ((len p) -' 1) = 1. L implies p = poly_with_roots (BRoots p) )
assume that
A16: len p = 1 and
1 >= 1 and
A17: p . ((len p) -' 1) = 1. L ; ::_thesis: p = poly_with_roots (BRoots p)
degree (BRoots p) = 0 by A16, Th57;
then A18: BRoots p = EmptyBag the carrier of L by Th12;
(len p) -' 1 = 0 by A16, XREAL_1:232;
hence p = <%(1. L)%> by A16, A17, ALGSEQ_1:def_5
.= poly_with_roots (BRoots p) by A18, Th60 ;
::_thesis: verum
end;
for n being Nat st n >= 1 holds
S1[n] from NAT_1:sch_8(A15, A3);
hence p = poly_with_roots (BRoots p) by A1, A2; ::_thesis: verum
end;
theorem :: UPROOTS:66
for L being comRing
for s being non empty finite Subset of L
for f being FinSequence of (Polynom-Ring L) st len f = card s & ( for i being Element of NAT
for c being Element of L st i in dom f & c = (canFS s) . i holds
f . i = <%(- c),(1. L)%> ) holds
poly_with_roots ((s,1) -bag) = Product f
proof
let L be comRing; ::_thesis: for s being non empty finite Subset of L
for f being FinSequence of (Polynom-Ring L) st len f = card s & ( for i being Element of NAT
for c being Element of L st i in dom f & c = (canFS s) . i holds
f . i = <%(- c),(1. L)%> ) holds
poly_with_roots ((s,1) -bag) = Product f
set cL = the carrier of L;
set cPRL = the carrier of (Polynom-Ring L);
let s be non empty finite Subset of the carrier of L; ::_thesis: for f being FinSequence of (Polynom-Ring L) st len f = card s & ( for i being Element of NAT
for c being Element of L st i in dom f & c = (canFS s) . i holds
f . i = <%(- c),(1. L)%> ) holds
poly_with_roots ((s,1) -bag) = Product f
let f be FinSequence of the carrier of (Polynom-Ring L); ::_thesis: ( len f = card s & ( for i being Element of NAT
for c being Element of L st i in dom f & c = (canFS s) . i holds
f . i = <%(- c),(1. L)%> ) implies poly_with_roots ((s,1) -bag) = Product f )
assume that
A1: len f = card s and
A2: for i being Element of NAT
for c being Element of the carrier of L st i in dom f & c = (canFS s) . i holds
f . i = <%(- c),(1. L)%> ; ::_thesis: poly_with_roots ((s,1) -bag) = Product f
set cs = canFS s;
A3: rng (canFS s) = s by FUNCT_2:def_3;
defpred S1[ Element of NAT ] means ex t being finite Subset of the carrier of L ex g being FinSequence of the carrier of (Polynom-Ring L) st
( t = rng ((canFS s) | (Seg $1)) & g = f | (Seg $1) & poly_with_roots ((t,1) -bag) = Product g );
A4: len (canFS s) = card s by Th3;
then A5: dom f = dom (canFS s) by A1, FINSEQ_3:29;
A6: for j being Element of NAT st 1 <= j & j < len f & S1[j] holds
S1[j + 1]
proof
let j be Element of NAT ; ::_thesis: ( 1 <= j & j < len f & S1[j] implies S1[j + 1] )
assume that
A7: 1 <= j and
A8: j < len f ; ::_thesis: ( not S1[j] or S1[j + 1] )
reconsider g1 = f | (Seg (j + 1)) as FinSequence of the carrier of (Polynom-Ring L) by FINSEQ_1:18;
A9: j + 1 <= len f by A8, NAT_1:13;
then ex l being Nat st len f = (j + 1) + l by NAT_1:10;
then A10: len g1 = j + 1 by FINSEQ_3:53;
1 <= j + 1 by A7, NAT_1:13;
then A11: j + 1 in dom (canFS s) by A1, A4, A9, FINSEQ_3:25;
then (canFS s) . (j + 1) in s by FINSEQ_2:11;
then reconsider csj1 = (canFS s) . (j + 1) as Element of the carrier of L ;
A12: g1 . (j + 1) = f . (j + 1) by FINSEQ_1:4, FUNCT_1:49
.= <%(- csj1),(1. L)%> by A2, A5, A11 ;
reconsider csja1 = (canFS s) | (Seg (j + 1)) as FinSequence of s by FINSEQ_1:18;
reconsider csja = (canFS s) | (Seg j) as FinSequence of s by FINSEQ_1:18;
given t being finite Subset of the carrier of L, g being FinSequence of the carrier of (Polynom-Ring L) such that A13: t = rng ((canFS s) | (Seg j)) and
A14: g = f | (Seg j) and
A15: poly_with_roots ((t,1) -bag) = Product g ; ::_thesis: S1[j + 1]
j <= j + 1 by NAT_1:12;
then Seg j c= Seg (j + 1) by FINSEQ_1:5;
then g = g1 | (Seg j) by A14, RELAT_1:74;
then A16: g1 = g ^ <*<%(- csj1),(1. L)%>*> by A10, A12, FINSEQ_3:55;
reconsider pt = poly_with_roots ((t,1) -bag) as Polynomial of L ;
set t1 = rng csja1;
Seg (j + 1) = (Seg j) \/ {(j + 1)} by FINSEQ_1:9;
then A17: csja1 = csja \/ ((canFS s) | {(j + 1)}) by RELAT_1:78;
(canFS s) | {(j + 1)} = (j + 1) .--> csj1 by A11, FUNCT_7:6;
then rng ((canFS s) | {(j + 1)}) = {csj1} by FUNCOP_1:8;
then A18: rng csja1 = t \/ {csj1} by A13, A17, RELAT_1:12;
reconsider epj1 = <%(- csj1),(1. L)%> as Element of the carrier of (Polynom-Ring L) by POLYNOM3:def_10;
reconsider pj1 = poly_with_roots (({csj1},1) -bag) as Polynomial of L ;
A19: pj1 = epj1 by Th61;
reconsider t1 = rng csja1 as finite Subset of the carrier of L by A18;
take t1 ; ::_thesis: ex g being FinSequence of the carrier of (Polynom-Ring L) st
( t1 = rng ((canFS s) | (Seg (j + 1))) & g = f | (Seg (j + 1)) & poly_with_roots ((t1,1) -bag) = Product g )
take g1 ; ::_thesis: ( t1 = rng ((canFS s) | (Seg (j + 1))) & g1 = f | (Seg (j + 1)) & poly_with_roots ((t1,1) -bag) = Product g1 )
thus ( t1 = rng ((canFS s) | (Seg (j + 1))) & g1 = f | (Seg (j + 1)) ) ; ::_thesis: poly_with_roots ((t1,1) -bag) = Product g1
t misses {csj1}
proof
assume not t misses {csj1} ; ::_thesis: contradiction
then t /\ {csj1} <> {} by XBOOLE_0:def_7;
then consider x being set such that
A20: x in t /\ {csj1} by XBOOLE_0:def_1;
x in {csj1} by A20, XBOOLE_0:def_4;
then A21: x = csj1 by TARSKI:def_1;
x in t by A20, XBOOLE_0:def_4;
then consider i being set such that
A22: i in dom ((canFS s) | (Seg j)) and
A23: x = ((canFS s) | (Seg j)) . i by A13, FUNCT_1:def_3;
A24: i in Seg j by A22, RELAT_1:57;
reconsider i = i as Element of NAT by A22;
A25: 1 <= i by A24, FINSEQ_1:1;
i <= j by A24, FINSEQ_1:1;
then A26: i < j + 1 by NAT_1:13;
x = (canFS s) . i by A22, A23, FUNCT_1:47;
hence contradiction by A1, A4, A3, A9, A21, A25, A26, GRAPH_5:7; ::_thesis: verum
end;
then (t1,1) -bag = ((t,1) -bag) + (({csj1},1) -bag) by A18, Th10;
hence poly_with_roots ((t1,1) -bag) = pt *' pj1 by Th64
.= (Product g) * epj1 by A15, A19, POLYNOM3:def_10
.= Product g1 by A16, GROUP_4:6 ;
::_thesis: verum
end;
f | (Seg (len f)) is FinSequence by FINSEQ_1:18;
then A27: ( (canFS s) | (Seg (len f)) is FinSequence & f | (Seg (len f)) = f ) by FINSEQ_1:18, FINSEQ_2:20;
A28: 0 + 1 <= len f by A1, NAT_1:13;
A29: S1[1]
proof
1 in dom (canFS s) by A1, A4, A28, FINSEQ_3:25;
then reconsider cs1 = (canFS s) . 1 as Element of s by FINSEQ_2:11;
reconsider g = f | (Seg 1) as FinSequence of the carrier of (Polynom-Ring L) by FINSEQ_1:18;
reconsider cs1a = (canFS s) | (Seg 1) as FinSequence of s by FINSEQ_1:18;
A30: cs1 in the carrier of L ;
A31: 1 in Seg 1 by FINSEQ_1:1;
then A32: cs1a . 1 = cs1 by FUNCT_1:49;
reconsider cs1 = (canFS s) . 1 as Element of the carrier of L by A30;
reconsider t = {cs1} as finite Subset of the carrier of L ;
take t ; ::_thesis: ex g being FinSequence of the carrier of (Polynom-Ring L) st
( t = rng ((canFS s) | (Seg 1)) & g = f | (Seg 1) & poly_with_roots ((t,1) -bag) = Product g )
take g ; ::_thesis: ( t = rng ((canFS s) | (Seg 1)) & g = f | (Seg 1) & poly_with_roots ((t,1) -bag) = Product g )
consider s1 being Element of s such that
A33: cs1a = <*s1*> by A1, A4, A28, TREES_9:34;
cs1a . 1 = s1 by A33, FINSEQ_1:40;
hence ( t = rng ((canFS s) | (Seg 1)) & g = f | (Seg 1) ) by A33, A32, FINSEQ_1:39; ::_thesis: poly_with_roots ((t,1) -bag) = Product g
consider p1 being Element of the carrier of (Polynom-Ring L) such that
A34: g = <*p1*> by A28, TREES_9:34;
A35: ( g . 1 = p1 & Product g = p1 ) by A34, FINSEQ_1:40, FINSOP_1:11;
A36: 1 in dom f by A28, FINSEQ_3:25;
then reconsider f1 = f . 1 as Element of the carrier of (Polynom-Ring L) by FINSEQ_2:11;
A37: g . 1 = f1 by A31, FUNCT_1:49;
f1 = <%(- cs1),(1. L)%> by A2, A36;
hence poly_with_roots ((t,1) -bag) = Product g by A37, A35, Th61; ::_thesis: verum
end;
for i being Element of NAT st 1 <= i & i <= len f holds
S1[i] from INT_1:sch_7(A29, A6);
then ex t being finite Subset of the carrier of L ex g being FinSequence of the carrier of (Polynom-Ring L) st
( t = rng ((canFS s) | (Seg (len f))) & g = f | (Seg (len f)) & poly_with_roots ((t,1) -bag) = Product g ) by A28;
hence poly_with_roots ((s,1) -bag) = Product f by A1, A4, A27, A3, FINSEQ_2:20; ::_thesis: verum
end;
theorem :: UPROOTS:67
for L being non trivial comRing
for s being non empty finite Subset of L
for x being Element of L
for f being FinSequence of L st len f = card s & ( for i being Element of NAT
for c being Element of L st i in dom f & c = (canFS s) . i holds
f . i = eval (<%(- c),(1. L)%>,x) ) holds
eval ((poly_with_roots ((s,1) -bag)),x) = Product f
proof
let L be non trivial comRing; ::_thesis: for s being non empty finite Subset of L
for x being Element of L
for f being FinSequence of L st len f = card s & ( for i being Element of NAT
for c being Element of L st i in dom f & c = (canFS s) . i holds
f . i = eval (<%(- c),(1. L)%>,x) ) holds
eval ((poly_with_roots ((s,1) -bag)),x) = Product f
set cL = the carrier of L;
let s be non empty finite Subset of the carrier of L; ::_thesis: for x being Element of L
for f being FinSequence of L st len f = card s & ( for i being Element of NAT
for c being Element of L st i in dom f & c = (canFS s) . i holds
f . i = eval (<%(- c),(1. L)%>,x) ) holds
eval ((poly_with_roots ((s,1) -bag)),x) = Product f
let x be Element of the carrier of L; ::_thesis: for f being FinSequence of L st len f = card s & ( for i being Element of NAT
for c being Element of L st i in dom f & c = (canFS s) . i holds
f . i = eval (<%(- c),(1. L)%>,x) ) holds
eval ((poly_with_roots ((s,1) -bag)),x) = Product f
let f be FinSequence of L; ::_thesis: ( len f = card s & ( for i being Element of NAT
for c being Element of L st i in dom f & c = (canFS s) . i holds
f . i = eval (<%(- c),(1. L)%>,x) ) implies eval ((poly_with_roots ((s,1) -bag)),x) = Product f )
assume that
A1: len f = card s and
A2: for i being Element of NAT
for c being Element of the carrier of L st i in dom f & c = (canFS s) . i holds
f . i = eval (<%(- c),(1. L)%>,x) ; ::_thesis: eval ((poly_with_roots ((s,1) -bag)),x) = Product f
set cs = canFS s;
A3: rng (canFS s) = s by FUNCT_2:def_3;
defpred S1[ Element of NAT ] means ex t being finite Subset of the carrier of L ex g being FinSequence of the carrier of L st
( t = rng ((canFS s) | (Seg $1)) & g = f | (Seg $1) & eval ((poly_with_roots ((t,1) -bag)),x) = Product g );
A4: len (canFS s) = card s by Th3;
then A5: dom f = dom (canFS s) by A1, FINSEQ_3:29;
A6: for j being Element of NAT st 1 <= j & j < len f & S1[j] holds
S1[j + 1]
proof
let j be Element of NAT ; ::_thesis: ( 1 <= j & j < len f & S1[j] implies S1[j + 1] )
assume that
A7: 1 <= j and
A8: j < len f ; ::_thesis: ( not S1[j] or S1[j + 1] )
reconsider g1 = f | (Seg (j + 1)) as FinSequence of the carrier of L by FINSEQ_1:18;
A9: j + 1 <= len f by A8, NAT_1:13;
then ex l being Nat st len f = (j + 1) + l by NAT_1:10;
then A10: len g1 = j + 1 by FINSEQ_3:53;
1 <= j + 1 by A7, NAT_1:13;
then A11: j + 1 in dom (canFS s) by A1, A4, A9, FINSEQ_3:25;
then (canFS s) . (j + 1) in s by FINSEQ_2:11;
then reconsider csj1 = (canFS s) . (j + 1) as Element of the carrier of L ;
A12: g1 . (j + 1) = f . (j + 1) by FINSEQ_1:4, FUNCT_1:49
.= eval (<%(- csj1),(1. L)%>,x) by A2, A5, A11 ;
reconsider csja1 = (canFS s) | (Seg (j + 1)) as FinSequence of s by FINSEQ_1:18;
reconsider csja = (canFS s) | (Seg j) as FinSequence of s by FINSEQ_1:18;
given t being finite Subset of the carrier of L, g being FinSequence of the carrier of L such that A13: t = rng ((canFS s) | (Seg j)) and
A14: g = f | (Seg j) and
A15: eval ((poly_with_roots ((t,1) -bag)),x) = Product g ; ::_thesis: S1[j + 1]
j <= j + 1 by NAT_1:12;
then Seg j c= Seg (j + 1) by FINSEQ_1:5;
then g = g1 | (Seg j) by A14, RELAT_1:74;
then A16: g1 = g ^ <*(eval (<%(- csj1),(1. L)%>,x))*> by A10, A12, FINSEQ_3:55;
reconsider pt = poly_with_roots ((t,1) -bag) as Polynomial of L ;
set t1 = rng csja1;
Seg (j + 1) = (Seg j) \/ {(j + 1)} by FINSEQ_1:9;
then A17: csja1 = csja \/ ((canFS s) | {(j + 1)}) by RELAT_1:78;
(canFS s) | {(j + 1)} = (j + 1) .--> csj1 by A11, FUNCT_7:6;
then rng ((canFS s) | {(j + 1)}) = {csj1} by FUNCOP_1:8;
then A18: rng csja1 = t \/ {csj1} by A13, A17, RELAT_1:12;
then reconsider t1 = rng csja1 as finite Subset of the carrier of L ;
take t1 ; ::_thesis: ex g being FinSequence of the carrier of L st
( t1 = rng ((canFS s) | (Seg (j + 1))) & g = f | (Seg (j + 1)) & eval ((poly_with_roots ((t1,1) -bag)),x) = Product g )
take g1 ; ::_thesis: ( t1 = rng ((canFS s) | (Seg (j + 1))) & g1 = f | (Seg (j + 1)) & eval ((poly_with_roots ((t1,1) -bag)),x) = Product g1 )
thus ( t1 = rng ((canFS s) | (Seg (j + 1))) & g1 = f | (Seg (j + 1)) ) ; ::_thesis: eval ((poly_with_roots ((t1,1) -bag)),x) = Product g1
reconsider pj1 = poly_with_roots (({csj1},1) -bag) as Polynomial of L ;
A19: pj1 = <%(- csj1),(1. L)%> by Th61;
t misses {csj1}
proof
assume not t misses {csj1} ; ::_thesis: contradiction
then t /\ {csj1} <> {} by XBOOLE_0:def_7;
then consider x being set such that
A20: x in t /\ {csj1} by XBOOLE_0:def_1;
x in {csj1} by A20, XBOOLE_0:def_4;
then A21: x = csj1 by TARSKI:def_1;
x in t by A20, XBOOLE_0:def_4;
then consider i being set such that
A22: i in dom ((canFS s) | (Seg j)) and
A23: x = ((canFS s) | (Seg j)) . i by A13, FUNCT_1:def_3;
A24: i in Seg j by A22, RELAT_1:57;
reconsider i = i as Element of NAT by A22;
A25: 1 <= i by A24, FINSEQ_1:1;
i <= j by A24, FINSEQ_1:1;
then A26: i < j + 1 by NAT_1:13;
x = (canFS s) . i by A22, A23, FUNCT_1:47;
hence contradiction by A1, A4, A3, A9, A21, A25, A26, GRAPH_5:7; ::_thesis: verum
end;
then (t1,1) -bag = ((t,1) -bag) + (({csj1},1) -bag) by A18, Th10;
then poly_with_roots ((t1,1) -bag) = pt *' pj1 by Th64;
hence eval ((poly_with_roots ((t1,1) -bag)),x) = (Product g) * (eval (pj1,x)) by A15, POLYNOM4:24
.= Product g1 by A16, A19, GROUP_4:6 ;
::_thesis: verum
end;
f | (Seg (len f)) is FinSequence by FINSEQ_1:18;
then A27: ( (canFS s) | (Seg (len f)) is FinSequence & f | (Seg (len f)) = f ) by FINSEQ_1:18, FINSEQ_2:20;
A28: 0 + 1 <= len f by A1, NAT_1:13;
A29: S1[1]
proof
1 in dom (canFS s) by A1, A4, A28, FINSEQ_3:25;
then reconsider cs1 = (canFS s) . 1 as Element of s by FINSEQ_2:11;
reconsider g = f | (Seg 1) as FinSequence of the carrier of L by FINSEQ_1:18;
reconsider cs1a = (canFS s) | (Seg 1) as FinSequence of s by FINSEQ_1:18;
A30: cs1 in the carrier of L ;
A31: 1 in Seg 1 by FINSEQ_1:1;
then A32: cs1a . 1 = cs1 by FUNCT_1:49;
reconsider cs1 = (canFS s) . 1 as Element of the carrier of L by A30;
reconsider t = {cs1} as finite Subset of the carrier of L ;
take t ; ::_thesis: ex g being FinSequence of the carrier of L st
( t = rng ((canFS s) | (Seg 1)) & g = f | (Seg 1) & eval ((poly_with_roots ((t,1) -bag)),x) = Product g )
take g ; ::_thesis: ( t = rng ((canFS s) | (Seg 1)) & g = f | (Seg 1) & eval ((poly_with_roots ((t,1) -bag)),x) = Product g )
consider s1 being Element of s such that
A33: cs1a = <*s1*> by A1, A4, A28, TREES_9:34;
cs1a . 1 = s1 by A33, FINSEQ_1:40;
hence ( t = rng ((canFS s) | (Seg 1)) & g = f | (Seg 1) ) by A33, A32, FINSEQ_1:39; ::_thesis: eval ((poly_with_roots ((t,1) -bag)),x) = Product g
consider p1 being Element of the carrier of L such that
A34: g = <*p1*> by A28, TREES_9:34;
A35: ( g . 1 = p1 & Product g = p1 ) by A34, FINSEQ_1:40, FINSOP_1:11;
A36: 1 in dom f by A28, FINSEQ_3:25;
then reconsider f1 = f . 1 as Element of the carrier of L by FINSEQ_2:11;
A37: g . 1 = f1 by A31, FUNCT_1:49;
f1 = eval (<%(- cs1),(1. L)%>,x) by A2, A36;
hence eval ((poly_with_roots ((t,1) -bag)),x) = Product g by A37, A35, Th61; ::_thesis: verum
end;
for i being Element of NAT st 1 <= i & i <= len f holds
S1[i] from INT_1:sch_7(A29, A6);
then ex t being finite Subset of the carrier of L ex g being FinSequence of the carrier of L st
( t = rng ((canFS s) | (Seg (len f))) & g = f | (Seg (len f)) & eval ((poly_with_roots ((t,1) -bag)),x) = Product g ) by A28;
hence eval ((poly_with_roots ((s,1) -bag)),x) = Product f by A1, A4, A27, A3, FINSEQ_2:20; ::_thesis: verum
end;