:: POLYNOM8 semantic presentation
begin
Lm1: for j being Integer holds
( j >= 0 or j = - 1 or j < - 1 )
proof
let j be Integer; ::_thesis: ( j >= 0 or j = - 1 or j < - 1 )
percases ( j >= 0 or j < 0 ) ;
suppose j >= 0 ; ::_thesis: ( j >= 0 or j = - 1 or j < - 1 )
hence ( j >= 0 or j = - 1 or j < - 1 ) ; ::_thesis: verum
end;
supposeA1: j < 0 ; ::_thesis: ( j >= 0 or j = - 1 or j < - 1 )
then reconsider n = - j as Element of NAT by INT_1:3;
n <> - 0 by A1;
then n >= 1 by NAT_1:14;
then ( n > 1 or n = 1 ) by XXREAL_0:1;
then ( - 1 > - (- j) or - 1 = j ) by XREAL_1:24;
hence ( j >= 0 or j = - 1 or j < - 1 ) ; ::_thesis: verum
end;
end;
end;
Lm2: for j being Integer holds
( j >= 1 or j = 0 or j < 0 )
proof
let j be Integer; ::_thesis: ( j >= 1 or j = 0 or j < 0 )
( j < 0 or ( j is Element of NAT & ( j <> 0 or j = 0 ) ) ) by INT_1:3;
hence ( j >= 1 or j = 0 or j < 0 ) by NAT_1:14; ::_thesis: verum
end;
theorem Th1: :: POLYNOM8:1
for n being Element of NAT
for L being non empty non degenerated well-unital domRing-like doubleLoopStr
for x being Element of L st x <> 0. L holds
x |^ n <> 0. L
proof
let n be Element of NAT ; ::_thesis: for L being non empty non degenerated well-unital domRing-like doubleLoopStr
for x being Element of L st x <> 0. L holds
x |^ n <> 0. L
let L be non empty non degenerated well-unital domRing-like doubleLoopStr ; ::_thesis: for x being Element of L st x <> 0. L holds
x |^ n <> 0. L
let x be Element of L; ::_thesis: ( x <> 0. L implies x |^ n <> 0. L )
defpred S1[ Element of NAT ] means x |^ $1 <> 0. L;
assume A1: x <> 0. L ; ::_thesis: x |^ n <> 0. L
A2: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume S1[n] ; ::_thesis: S1[n + 1]
then (x |^ n) * x <> 0. L by A1, VECTSP_2:def_1;
hence S1[n + 1] by GROUP_1:def_7; ::_thesis: verum
end;
x |^ 0 = 1_ L by BINOM:8;
then A3: S1[ 0 ] ;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2);
hence x |^ n <> 0. L ; ::_thesis: verum
end;
registration
cluster non empty right_complementable almost_left_invertible associative right-distributive well-unital add-associative right_zeroed -> non empty right_complementable associative right-distributive well-unital add-associative right_zeroed domRing-like for doubleLoopStr ;
coherence
for b1 being non empty right_complementable associative right-distributive well-unital add-associative right_zeroed doubleLoopStr st b1 is almost_left_invertible holds
b1 is domRing-like
proof
let L be non empty right_complementable associative right-distributive well-unital add-associative right_zeroed doubleLoopStr ; ::_thesis: ( L is almost_left_invertible implies L is domRing-like )
assume A1: L is almost_left_invertible ; ::_thesis: L is domRing-like
for x, y being Element of L holds
( not x * y = 0. L or x = 0. L or y = 0. L )
proof
let x, y be Element of L; ::_thesis: ( not x * y = 0. L or x = 0. L or y = 0. L )
assume A2: x * y = 0. L ; ::_thesis: ( x = 0. L or y = 0. L )
now__::_thesis:_(_x_<>_0._L_implies_not_y_<>_0._L_)
assume that
A3: x <> 0. L and
A4: y <> 0. L ; ::_thesis: contradiction
consider xx being Element of L such that
A5: xx * x = 1. L by A1, A3, VECTSP_1:def_9;
y = (1. L) * y by VECTSP_1:def_8
.= xx * (x * y) by A5, GROUP_1:def_3
.= 0. L by A2, VECTSP_1:6 ;
hence contradiction by A4; ::_thesis: verum
end;
hence ( x = 0. L or y = 0. L ) ; ::_thesis: verum
end;
hence L is domRing-like by VECTSP_2:def_1; ::_thesis: verum
end;
end;
theorem Th2: :: POLYNOM8:2
for L being non empty right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for x, y being Element of L st x <> 0. L & y <> 0. L holds
(x * y) " = (x ") * (y ")
proof
let L be non empty right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for x, y being Element of L st x <> 0. L & y <> 0. L holds
(x * y) " = (x ") * (y ")
let x, y be Element of L; ::_thesis: ( x <> 0. L & y <> 0. L implies (x * y) " = (x ") * (y ") )
assume that
A1: x <> 0. L and
A2: y <> 0. L ; ::_thesis: (x * y) " = (x ") * (y ")
A3: ((x ") * (y ")) * (x * y) = (((x ") * (y ")) * y) * x by GROUP_1:def_3
.= ((x ") * ((y ") * y)) * x by GROUP_1:def_3
.= ((x ") * (1. L)) * x by A2, VECTSP_1:def_10
.= (x ") * x by VECTSP_1:def_4
.= 1. L by A1, VECTSP_1:def_10 ;
x * y <> 0. L by A1, A2, VECTSP_1:12;
hence (x * y) " = (x ") * (y ") by A3, VECTSP_1:def_10; ::_thesis: verum
end;
theorem Th3: :: POLYNOM8:3
for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for z, z1 being Element of L st z <> 0. L holds
z1 = (z1 * z) / z
proof
let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for z, z1 being Element of L st z <> 0. L holds
z1 = (z1 * z) / z
let z, z1 be Element of L; ::_thesis: ( z <> 0. L implies z1 = (z1 * z) / z )
assume A1: z <> 0. L ; ::_thesis: z1 = (z1 * z) / z
thus (z1 * z) / z = z1 * (z * (z ")) by GROUP_1:def_3
.= z1 * (1. L) by A1, VECTSP_1:def_10
.= z1 by VECTSP_1:def_8 ; ::_thesis: verum
end;
theorem Th4: :: POLYNOM8:4
for L being non empty right_complementable add-associative right_zeroed left_zeroed doubleLoopStr
for m being Element of NAT
for s being FinSequence of L st len s = m & ( for k being Element of NAT st 1 <= k & k <= m holds
s /. k = 1. L ) holds
Sum s = m * (1. L)
proof
let L be non empty right_complementable add-associative right_zeroed left_zeroed doubleLoopStr ; ::_thesis: for m being Element of NAT
for s being FinSequence of L st len s = m & ( for k being Element of NAT st 1 <= k & k <= m holds
s /. k = 1. L ) holds
Sum s = m * (1. L)
let m be Element of NAT ; ::_thesis: for s being FinSequence of L st len s = m & ( for k being Element of NAT st 1 <= k & k <= m holds
s /. k = 1. L ) holds
Sum s = m * (1. L)
let s be FinSequence of L; ::_thesis: ( len s = m & ( for k being Element of NAT st 1 <= k & k <= m holds
s /. k = 1. L ) implies Sum s = m * (1. L) )
assume A1: ( len s = m & ( for k being Element of NAT st 1 <= k & k <= m holds
s /. k = 1. L ) ) ; ::_thesis: Sum s = m * (1. L)
defpred S1[ Element of NAT ] means for s being FinSequence of L st len s = $1 & ( for k being Element of NAT st 1 <= k & k <= $1 holds
s /. k = 1. L ) holds
Sum s = $1 * (1. L);
A2: for l being Element of NAT st S1[l] holds
S1[l + 1]
proof
let l be Element of NAT ; ::_thesis: ( S1[l] implies S1[l + 1] )
assume A3: for g being FinSequence of L st len g = l & ( for k being Element of NAT st 1 <= k & k <= l holds
g /. k = 1. L ) holds
Sum g = l * (1. L) ; ::_thesis: S1[l + 1]
for s being FinSequence of L st len s = l + 1 & ( for k being Element of NAT st 1 <= k & k <= l + 1 holds
s /. k = 1. L ) holds
Sum s = (l + 1) * (1. L)
proof
ex G being FinSequence of L st
( dom G = Seg l & ( for k being Nat st k in Seg l holds
G . k = 1. L ) )
proof
defpred S2[ Nat, set ] means $2 = 1. L;
A4: for n being Nat st n in Seg l holds
ex x being Element of L st S2[n,x] ;
ex G being FinSequence of L st
( dom G = Seg l & ( for nn being Nat st nn in Seg l holds
S2[nn,G . nn] ) ) from FINSEQ_1:sch_5(A4);
hence ex G being FinSequence of L st
( dom G = Seg l & ( for k being Nat st k in Seg l holds
G . k = 1. L ) ) ; ::_thesis: verum
end;
then consider g being FinSequence of L such that
A5: dom g = Seg l and
A6: for k being Nat st k in Seg l holds
g . k = 1. L ;
A7: len g = l by A5, FINSEQ_1:def_3;
A8: for k being Nat st 1 <= k & k <= l holds
g /. k = 1. L
proof
let k be Nat; ::_thesis: ( 1 <= k & k <= l implies g /. k = 1. L )
assume A9: ( 1 <= k & k <= l ) ; ::_thesis: g /. k = 1. L
then A10: k in dom g by A5, FINSEQ_1:1;
k in Seg l by A9, FINSEQ_1:1;
then 1. L = g . k by A6
.= g /. k by A10, PARTFUN1:def_6 ;
hence g /. k = 1. L ; ::_thesis: verum
end;
then A11: for k being Element of NAT st 1 <= k & k <= l holds
g /. k = 1. L ;
dom <*(1. L)*> = Seg 1 by FINSEQ_1:def_8;
then A12: len <*(1. L)*> = 1 by FINSEQ_1:def_3;
let s be FinSequence of L; ::_thesis: ( len s = l + 1 & ( for k being Element of NAT st 1 <= k & k <= l + 1 holds
s /. k = 1. L ) implies Sum s = (l + 1) * (1. L) )
assume that
A13: len s = l + 1 and
A14: for k being Element of NAT st 1 <= k & k <= l + 1 holds
s /. k = 1. L ; ::_thesis: Sum s = (l + 1) * (1. L)
A15: dom s = Seg (l + 1) by A13, FINSEQ_1:def_3;
A16: for k being Nat st k in dom s holds
s . k = (g ^ <*(1. L)*>) . k
proof
A17: dom s = Seg (l + 1) by A13, FINSEQ_1:def_3;
let k be Nat; ::_thesis: ( k in dom s implies s . k = (g ^ <*(1. L)*>) . k )
A18: k in NAT by ORDINAL1:def_12;
assume A19: k in dom s ; ::_thesis: s . k = (g ^ <*(1. L)*>) . k
percases ( ( 1 <= k & k <= l ) or ( l < k & k <= l + 1 ) ) by A19, A17, FINSEQ_1:1;
supposeA20: ( 1 <= k & k <= l ) ; ::_thesis: s . k = (g ^ <*(1. L)*>) . k
then A21: k <= l + 1 by NAT_1:12;
A22: k in dom g by A5, A18, A20;
then (g ^ <*(1. L)*>) . k = g . k by FINSEQ_1:def_7
.= g /. k by A22, PARTFUN1:def_6
.= 1. L by A8, A20
.= s /. k by A14, A18, A20, A21
.= s . k by A19, PARTFUN1:def_6 ;
hence s . k = (g ^ <*(1. L)*>) . k ; ::_thesis: verum
end;
supposeA23: ( l < k & k <= l + 1 ) ; ::_thesis: s . k = (g ^ <*(1. L)*>) . k
then k - k <= (l + 1) - k by XREAL_1:9;
then reconsider ii = ((l + 1) - k) + 1 as Element of NAT by INT_1:3;
l + 1 <= k by A23, NAT_1:13;
then ( dom <*(1. L)*> = Seg 1 & ii = (k - k) + 1 ) by A23, FINSEQ_1:def_8, XXREAL_0:1;
then A24: ii in dom <*(1. L)*> ;
l + 0 < k + l by A23, XREAL_1:8;
then l + 1 <= k + l by NAT_1:13;
then A25: (l + 1) - l <= (k + l) - l by XREAL_1:9;
l + 1 <= k by A23, NAT_1:13;
then A26: ii = (k - k) + 1 by A23, XXREAL_0:1;
then (g ^ <*(1. L)*>) . k = (g ^ <*(1. L)*>) . ((len g) + ii) by A5, FINSEQ_1:def_3
.= <*(1. L)*> . 1 by A24, A26, FINSEQ_1:def_7
.= 1. L by FINSEQ_1:def_8
.= s /. k by A14, A18, A23, A25
.= s . k by A19, PARTFUN1:def_6 ;
hence s . k = (g ^ <*(1. L)*>) . k ; ::_thesis: verum
end;
end;
end;
dom (g ^ <*(1. L)*>) = Seg ((len g) + (len <*(1. L)*>)) by FINSEQ_1:def_7
.= dom s by A5, A12, A15, FINSEQ_1:def_3 ;
then s = g ^ <*(1. L)*> by A16, FINSEQ_1:13;
then Sum s = (Sum g) + (1. L) by FVSUM_1:71
.= (l * (1. L)) + (1. L) by A3, A7, A11
.= (l * (1. L)) + (1 * (1. L)) by BINOM:13
.= (l + 1) * (1. L) by BINOM:15 ;
hence Sum s = (l + 1) * (1. L) ; ::_thesis: verum
end;
hence S1[l + 1] ; ::_thesis: verum
end;
for s being FinSequence of L st len s = 0 & ( for k being Element of NAT st 1 <= k & k <= 0 holds
s /. k = 1. L ) holds
Sum s = 0 * (1. L)
proof
let s be FinSequence of L; ::_thesis: ( len s = 0 & ( for k being Element of NAT st 1 <= k & k <= 0 holds
s /. k = 1. L ) implies Sum s = 0 * (1. L) )
assume that
A27: len s = 0 and
for k being Element of NAT st 1 <= k & k <= 0 holds
s /. k = 1. L ; ::_thesis: Sum s = 0 * (1. L)
A28: <*> the carrier of L is Element of 0 -tuples_on the carrier of L by FINSEQ_2:131;
s = {} by A27;
then Sum s = Sum (<*> the carrier of L)
.= 0. L by A28, FVSUM_1:74
.= 0 * (1. L) by BINOM:12 ;
hence Sum s = 0 * (1. L) ; ::_thesis: verum
end;
then A29: S1[ 0 ] ;
for l being Element of NAT holds S1[l] from NAT_1:sch_1(A29, A2);
hence Sum s = m * (1. L) by A1; ::_thesis: verum
end;
theorem Th5: :: POLYNOM8:5
for L being non empty right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for s being FinSequence of L
for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds
s . i = q |^ (i -' 1) ) holds
Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q)
proof
let L be non empty right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for s being FinSequence of L
for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds
s . i = q |^ (i -' 1) ) holds
Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q)
let s be FinSequence of L; ::_thesis: for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds
s . i = q |^ (i -' 1) ) holds
Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q)
let q be Element of L; ::_thesis: ( q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds
s . i = q |^ (i -' 1) ) implies Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q) )
assume A1: ( q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds
s . i = q |^ (i -' 1) ) ) ; ::_thesis: Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q)
defpred S1[ Nat] means for s being FinSequence of L st len s = $1 holds
for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds
s . i = q |^ (i -' 1) ) holds
Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q);
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
now__::_thesis:_for_s_being_FinSequence_of_L_st_len_s_=_k_+_1_holds_
for_q_being_Element_of_L_st_q_<>_1._L_&_(_for_i_being_Nat_st_1_<=_i_&_i_<=_len_s_holds_
s_._i_=_q_|^_(i_-'_1)_)_holds_
Sum_s_=_((1._L)_-_(q_|^_(len_s)))_/_((1._L)_-_q)
let s be FinSequence of L; ::_thesis: ( len s = k + 1 implies for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds
s . i = q |^ (i -' 1) ) holds
Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q) )
set f = s | (Seg k);
reconsider f = s | (Seg k) as FinSequence by FINSEQ_1:15;
assume A4: len s = k + 1 ; ::_thesis: for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds
s . i = q |^ (i -' 1) ) holds
Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q)
then A5: 1 <= len s by NAT_1:12;
then len s in dom s by FINSEQ_3:25;
then A6: s /. (len s) = s . (len s) by PARTFUN1:def_6;
A7: k <= len s by A4, NAT_1:13;
then A8: len f = k by FINSEQ_1:17;
now__::_thesis:_for_u_being_set_st_u_in_rng_f_holds_
u_in_the_carrier_of_L
let u be set ; ::_thesis: ( u in rng f implies u in the carrier of L )
assume u in rng f ; ::_thesis: u in the carrier of L
then consider x being set such that
A9: x in dom f and
A10: f . x = u by FUNCT_1:def_3;
reconsider x9 = x as Element of NAT by A9;
x9 <= len f by A9, FINSEQ_3:25;
then A11: x9 <= len s by A4, A8, NAT_1:12;
1 <= x9 by A9, FINSEQ_3:25;
then A12: x in dom s by A11, FINSEQ_3:25;
f . x = s . x by A9, FUNCT_1:47
.= s /. x by A12, PARTFUN1:def_6 ;
hence u in the carrier of L by A10; ::_thesis: verum
end;
then rng f c= the carrier of L by TARSKI:def_3;
then reconsider f = f as FinSequence of L by FINSEQ_1:def_4;
A13: len s = (len f) + 1 by A4, A7, FINSEQ_1:17;
let q be Element of L; ::_thesis: ( q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds
s . i = q |^ (i -' 1) ) implies Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q) )
assume that
A14: q <> 1. L and
A15: for i being Nat st 1 <= i & i <= len s holds
s . i = q |^ (i -' 1) ; ::_thesis: Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q)
A16: now__::_thesis:_not_(1._L)_-_q_=_0._L
assume (1. L) - q = 0. L ; ::_thesis: contradiction
then ((1. L) - q) + q = q by ALGSTR_1:def_2;
then (1. L) + ((- q) + q) = q by RLVECT_1:def_3;
then (1. L) + (0. L) = q by RLVECT_1:5;
hence contradiction by A14, RLVECT_1:def_4; ::_thesis: verum
end;
(len s) - 1 >= 1 - 1 by A5, XREAL_1:9;
then A17: (len s) -' 1 = (len s) - 1 by XREAL_0:def_2
.= ((len f) + 1) - 1 by A4, A7, FINSEQ_1:17 ;
A18: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_f_holds_
f_._i_=_q_|^_(i_-'_1)
let i be Nat; ::_thesis: ( 1 <= i & i <= len f implies f . i = q |^ (i -' 1) )
assume that
A19: 1 <= i and
A20: i <= len f ; ::_thesis: f . i = q |^ (i -' 1)
A21: i <= len s by A4, A8, A20, NAT_1:13;
i in dom f by A19, A20, FINSEQ_3:25;
hence f . i = s . i by FUNCT_1:47
.= q |^ (i -' 1) by A15, A19, A21 ;
::_thesis: verum
end;
f = s | (dom f) by A7, FINSEQ_1:17;
hence Sum s = (Sum f) + (s /. (len s)) by A13, A6, RLVECT_1:38
.= (((1. L) - (q |^ (len f))) / ((1. L) - q)) + (s /. (len s)) by A3, A14, A7, A18, FINSEQ_1:17
.= (((1. L) - (q |^ (len f))) / ((1. L) - q)) + (q |^ (len f)) by A15, A5, A17, A6
.= (((1. L) - (q |^ (len f))) / ((1. L) - q)) + (((q |^ (len f)) * ((1. L) - q)) / ((1. L) - q)) by A16, Th3
.= (((1. L) - (q |^ (len f))) + ((q |^ (len f)) * ((1. L) - q))) / ((1. L) - q) by VECTSP_1:def_3
.= (((1. L) - (q |^ (len f))) + (((q |^ (len f)) * (1. L)) + ((q |^ (len f)) * (- q)))) / ((1. L) - q) by VECTSP_1:def_2
.= (((1. L) - (q |^ (len f))) + ((q |^ (len f)) + ((q |^ (len f)) * (- q)))) / ((1. L) - q) by VECTSP_1:def_4
.= ((1. L) + ((- (q |^ (len f))) + ((q |^ (len f)) + ((q |^ (len f)) * (- q))))) / ((1. L) - q) by RLVECT_1:def_3
.= ((1. L) + (((- (q |^ (len f))) + (q |^ (len f))) + ((q |^ (len f)) * (- q)))) / ((1. L) - q) by RLVECT_1:def_3
.= ((1. L) + ((0. L) + ((q |^ (len f)) * (- q)))) / ((1. L) - q) by RLVECT_1:5
.= ((1. L) + ((q |^ (len f)) * (- q))) / ((1. L) - q) by ALGSTR_1:def_2
.= ((1. L) + (- ((q |^ (len f)) * q))) / ((1. L) - q) by VECTSP_1:8
.= ((1. L) - (q |^ (len s))) / ((1. L) - q) by A13, GROUP_1:def_7 ;
::_thesis: verum
end;
hence S1[k + 1] ; ::_thesis: verum
end;
now__::_thesis:_for_s_being_FinSequence_of_L_st_len_s_=_0_holds_
for_q_being_Element_of_L_st_q_<>_1._L_&_(_for_i_being_Nat_st_1_<=_i_&_i_<=_len_s_holds_
s_._i_=_q_|^_(i_-'_1)_)_holds_
((1._L)_-_(q_|^_0))_/_((1._L)_-_q)_=_Sum_s
let s be FinSequence of L; ::_thesis: ( len s = 0 implies for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds
s . i = q |^ (i -' 1) ) holds
((1. L) - (q |^ 0)) / ((1. L) - q) = Sum s )
assume len s = 0 ; ::_thesis: for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds
s . i = q |^ (i -' 1) ) holds
((1. L) - (q |^ 0)) / ((1. L) - q) = Sum s
then A22: s = <*> the carrier of L ;
let q be Element of L; ::_thesis: ( q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds
s . i = q |^ (i -' 1) ) implies ((1. L) - (q |^ 0)) / ((1. L) - q) = Sum s )
assume that
q <> 1. L and
for i being Nat st 1 <= i & i <= len s holds
s . i = q |^ (i -' 1) ; ::_thesis: ((1. L) - (q |^ 0)) / ((1. L) - q) = Sum s
thus ((1. L) - (q |^ 0)) / ((1. L) - q) = ((1. L) - (1_ L)) / ((1. L) - q) by BINOM:8
.= (0. L) / ((1. L) - q) by RLVECT_1:15
.= 0. L by VECTSP_1:6
.= Sum s by A22, RLVECT_1:43 ; ::_thesis: verum
end;
then A23: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch_2(A23, A2);
hence Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q) by A1; ::_thesis: verum
end;
definition
let L be non empty well-unital doubleLoopStr ;
let m be Element of NAT ;
func emb (m,L) -> Element of L equals :: POLYNOM8:def 1
m * (1. L);
coherence
m * (1. L) is Element of L ;
end;
:: deftheorem defines emb POLYNOM8:def_1_:_
for L being non empty well-unital doubleLoopStr
for m being Element of NAT holds emb (m,L) = m * (1. L);
theorem Th6: :: POLYNOM8:6
for L being Field
for m, n, k being Element of NAT st m > 0 & n > 0 holds
for M1 being Matrix of m,n,L
for M2 being Matrix of n,k,L holds ((emb (m,L)) * M1) * M2 = (emb (m,L)) * (M1 * M2)
proof
let L be Field; ::_thesis: for m, n, k being Element of NAT st m > 0 & n > 0 holds
for M1 being Matrix of m,n,L
for M2 being Matrix of n,k,L holds ((emb (m,L)) * M1) * M2 = (emb (m,L)) * (M1 * M2)
let m, n, k be Element of NAT ; ::_thesis: ( m > 0 & n > 0 implies for M1 being Matrix of m,n,L
for M2 being Matrix of n,k,L holds ((emb (m,L)) * M1) * M2 = (emb (m,L)) * (M1 * M2) )
assume that
A1: m > 0 and
A2: n > 0 ; ::_thesis: for M1 being Matrix of m,n,L
for M2 being Matrix of n,k,L holds ((emb (m,L)) * M1) * M2 = (emb (m,L)) * (M1 * M2)
let M1 be Matrix of m,n,L; ::_thesis: for M2 being Matrix of n,k,L holds ((emb (m,L)) * M1) * M2 = (emb (m,L)) * (M1 * M2)
let M2 be Matrix of n,k,L; ::_thesis: ((emb (m,L)) * M1) * M2 = (emb (m,L)) * (M1 * M2)
A3: width M1 = n by A1, MATRIX_1:23
.= len M2 by A2, MATRIX_1:23 ;
A4: width ((emb (m,L)) * M1) = width M1 by MATRIX_3:def_5
.= n by A1, MATRIX_1:23
.= len M2 by A2, MATRIX_1:23 ;
A5: for i, j being Nat st [i,j] in Indices (((emb (m,L)) * M1) * M2) holds
(((emb (m,L)) * M1) * M2) * (i,j) = ((emb (m,L)) * (M1 * M2)) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (((emb (m,L)) * M1) * M2) implies (((emb (m,L)) * M1) * M2) * (i,j) = ((emb (m,L)) * (M1 * M2)) * (i,j) )
A6: len M1 = len (M1 * M2) by A3, MATRIX_3:def_4;
len (((emb (m,L)) * M1) * M2) = len ((emb (m,L)) * M1) by A4, MATRIX_3:def_4
.= len M1 by MATRIX_3:def_5 ;
then A7: dom (((emb (m,L)) * M1) * M2) = Seg (len M1) by FINSEQ_1:def_3
.= dom (M1 * M2) by A6, FINSEQ_1:def_3 ;
Seg (len ((emb (m,L)) * (Line (M1,i)))) = dom ((emb (m,L)) * (Line (M1,i))) by FINSEQ_1:def_3
.= dom (Line (M1,i)) by POLYNOM1:def_1
.= Seg (len (Line (M1,i))) by FINSEQ_1:def_3 ;
then A8: len ((emb (m,L)) * (Line (M1,i))) = len (Line (M1,i)) by FINSEQ_1:6
.= width M1 by MATRIX_1:def_7 ;
A9: len (Line (M1,i)) = len M2 by A3, MATRIX_1:def_7
.= len (Col (M2,j)) by MATRIX_1:def_8 ;
assume A10: [i,j] in Indices (((emb (m,L)) * M1) * M2) ; ::_thesis: (((emb (m,L)) * M1) * M2) * (i,j) = ((emb (m,L)) * (M1 * M2)) * (i,j)
then A11: (((emb (m,L)) * M1) * M2) * (i,j) = (Line (((emb (m,L)) * M1),i)) "*" (Col (M2,j)) by A4, MATRIX_3:def_4
.= Sum (mlt ((Line (((emb (m,L)) * M1),i)),(Col (M2,j)))) by FVSUM_1:def_9 ;
len (Line (((emb (m,L)) * M1),i)) = width ((emb (m,L)) * M1) by MATRIX_1:def_7
.= width M1 by MATRIX_3:def_5 ;
then dom (Line (((emb (m,L)) * M1),i)) = Seg (width M1) by FINSEQ_1:def_3;
then A12: dom (Line (((emb (m,L)) * M1),i)) = dom ((emb (m,L)) * (Line (M1,i))) by A8, FINSEQ_1:def_3;
for k being Nat st k in dom (Line (((emb (m,L)) * M1),i)) holds
(Line (((emb (m,L)) * M1),i)) . k = ((emb (m,L)) * (Line (M1,i))) . k
proof
len (M1 * M2) = len M1 by A3, MATRIX_3:def_4
.= m by A1, MATRIX_1:23 ;
then A13: dom (M1 * M2) = Seg m by FINSEQ_1:def_3;
A14: ( Indices M1 = [:(Seg m),(Seg n):] & i in dom (M1 * M2) ) by A1, A10, A7, MATRIX_1:23, ZFMISC_1:87;
let k be Nat; ::_thesis: ( k in dom (Line (((emb (m,L)) * M1),i)) implies (Line (((emb (m,L)) * M1),i)) . k = ((emb (m,L)) * (Line (M1,i))) . k )
assume A15: k in dom (Line (((emb (m,L)) * M1),i)) ; ::_thesis: (Line (((emb (m,L)) * M1),i)) . k = ((emb (m,L)) * (Line (M1,i))) . k
A16: len (Line (((emb (m,L)) * M1),i)) = width ((emb (m,L)) * M1) by MATRIX_1:def_7
.= width M1 by MATRIX_3:def_5 ;
then A17: k in Seg (width M1) by A15, FINSEQ_1:def_3;
len (Line (M1,i)) = width M1 by MATRIX_1:def_7;
then k in dom (Line (M1,i)) by A17, FINSEQ_1:def_3;
then (Line (M1,i)) . k = (Line (M1,i)) /. k by PARTFUN1:def_6;
then reconsider a = (Line (M1,i)) . k as Element of L ;
A18: a = M1 * (i,k) by A17, MATRIX_1:def_7;
k in Seg n by A1, A17, MATRIX_1:23;
then [i,k] in Indices M1 by A14, A13, ZFMISC_1:87;
then A19: (emb (m,L)) * a = ((emb (m,L)) * M1) * (i,k) by A18, MATRIX_3:def_5;
dom (Line (((emb (m,L)) * M1),i)) = Seg (width M1) by A16, FINSEQ_1:def_3;
then A20: k in Seg (width ((emb (m,L)) * M1)) by A15, MATRIX_3:def_5;
((emb (m,L)) * (Line (M1,i))) . k = (emb (m,L)) * a by A12, A15, FVSUM_1:50;
hence (Line (((emb (m,L)) * M1),i)) . k = ((emb (m,L)) * (Line (M1,i))) . k by A20, A19, MATRIX_1:def_7; ::_thesis: verum
end;
then A21: Line (((emb (m,L)) * M1),i) = (emb (m,L)) * (Line (M1,i)) by A12, FINSEQ_1:13;
Seg (len ((emb (m,L)) * (Line (M1,i)))) = dom ((emb (m,L)) * (Line (M1,i))) by FINSEQ_1:def_3
.= dom (Line (M1,i)) by POLYNOM1:def_1
.= Seg (len (Line (M1,i))) by FINSEQ_1:def_3 ;
then A22: len ((emb (m,L)) * (Line (M1,i))) = len (Line (M1,i)) by FINSEQ_1:6
.= len M2 by A3, MATRIX_1:def_7
.= len (Col (M2,j)) by MATRIX_1:def_8 ;
A23: dom ((emb (m,L)) * (Line (M1,i))) = Seg (len ((emb (m,L)) * (Line (M1,i)))) by FINSEQ_1:def_3
.= Seg (len (mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j))))) by A22, MATRIX_3:6
.= dom (mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j)))) by FINSEQ_1:def_3 ;
A24: dom ((emb (m,L)) * (Line (M1,i))) = dom (Line (M1,i)) by POLYNOM1:def_1
.= Seg (len (Line (M1,i))) by FINSEQ_1:def_3
.= Seg (len (mlt ((Line (M1,i)),(Col (M2,j))))) by A9, MATRIX_3:6
.= dom (mlt ((Line (M1,i)),(Col (M2,j)))) by FINSEQ_1:def_3 ;
then A25: dom (mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j)))) = dom ((emb (m,L)) * (mlt ((Line (M1,i)),(Col (M2,j))))) by A23, POLYNOM1:def_1;
for k being Nat st k in dom (mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j)))) holds
(mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j)))) . k = ((emb (m,L)) * (mlt ((Line (M1,i)),(Col (M2,j))))) . k
proof
A26: len (Line (M1,i)) = len M2 by A3, MATRIX_1:def_7
.= len (Col (M2,j)) by MATRIX_1:def_8 ;
A27: len (Line (M1,i)) = width M1 by MATRIX_1:def_7;
let k be Nat; ::_thesis: ( k in dom (mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j)))) implies (mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j)))) . k = ((emb (m,L)) * (mlt ((Line (M1,i)),(Col (M2,j))))) . k )
assume A28: k in dom (mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j)))) ; ::_thesis: (mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j)))) . k = ((emb (m,L)) * (mlt ((Line (M1,i)),(Col (M2,j))))) . k
dom (Line (M1,i)) = Seg (len (Line (M1,i))) by FINSEQ_1:def_3
.= Seg (len (mlt ((Line (M1,i)),(Col (M2,j))))) by A26, MATRIX_3:6
.= dom (mlt ((Line (M1,i)),(Col (M2,j)))) by FINSEQ_1:def_3 ;
then A29: k in Seg (width M1) by A23, A24, A28, A27, FINSEQ_1:def_3;
then k in dom M2 by A3, FINSEQ_1:def_3;
then A30: (Col (M2,j)) . k = M2 * (k,j) by MATRIX_1:def_8;
(Line (M1,i)) . k = M1 * (i,k) by A29, MATRIX_1:def_7;
then reconsider c = (Col (M2,j)) . k, d = (Line (M1,i)) . k as Element of L by A30;
(mlt ((Line (M1,i)),(Col (M2,j)))) . k = c * d by A23, A24, A28, FVSUM_1:60;
then reconsider a = (mlt ((Line (M1,i)),(Col (M2,j)))) . k as Element of L ;
A31: ((emb (m,L)) * (mlt ((Line (M1,i)),(Col (M2,j))))) . k = (emb (m,L)) * a by A25, A28, FVSUM_1:50;
((emb (m,L)) * (Line (M1,i))) . k = (emb (m,L)) * d by A23, A28, FVSUM_1:50;
then reconsider b = ((emb (m,L)) * (Line (M1,i))) . k as Element of L ;
b * c = ((emb (m,L)) * d) * c by A23, A28, FVSUM_1:50
.= (emb (m,L)) * (d * c) by GROUP_1:def_3
.= (emb (m,L)) * a by A23, A24, A28, FVSUM_1:60 ;
hence (mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j)))) . k = ((emb (m,L)) * (mlt ((Line (M1,i)),(Col (M2,j))))) . k by A28, A31, FVSUM_1:60; ::_thesis: verum
end;
then A32: (emb (m,L)) * (mlt ((Line (M1,i)),(Col (M2,j)))) = mlt ((Line (((emb (m,L)) * M1),i)),(Col (M2,j))) by A21, A25, FINSEQ_1:13;
Seg (width (((emb (m,L)) * M1) * M2)) = Seg (width M2) by A4, MATRIX_3:def_4
.= Seg (width (M1 * M2)) by A3, MATRIX_3:def_4 ;
then A33: [i,j] in Indices (M1 * M2) by A10, A7;
then ((emb (m,L)) * (M1 * M2)) * (i,j) = (emb (m,L)) * ((M1 * M2) * (i,j)) by MATRIX_3:def_5
.= (emb (m,L)) * ((Line (M1,i)) "*" (Col (M2,j))) by A3, A33, MATRIX_3:def_4
.= (emb (m,L)) * (Sum (mlt ((Line (M1,i)),(Col (M2,j))))) by FVSUM_1:def_9 ;
hence (((emb (m,L)) * M1) * M2) * (i,j) = ((emb (m,L)) * (M1 * M2)) * (i,j) by A11, A32, FVSUM_1:73; ::_thesis: verum
end;
A34: len ((emb (m,L)) * (M1 * M2)) = len (M1 * M2) by MATRIX_3:def_5
.= len M1 by A3, MATRIX_3:def_4 ;
width ((emb (m,L)) * (M1 * M2)) = width (M1 * M2) by MATRIX_3:def_5
.= width M2 by A3, MATRIX_3:def_4 ;
then A35: width (((emb (m,L)) * M1) * M2) = width ((emb (m,L)) * (M1 * M2)) by A4, MATRIX_3:def_4;
len (((emb (m,L)) * M1) * M2) = len ((emb (m,L)) * M1) by A4, MATRIX_3:def_4
.= len M1 by MATRIX_3:def_5 ;
hence ((emb (m,L)) * M1) * M2 = (emb (m,L)) * (M1 * M2) by A34, A35, A5, MATRIX_1:21; ::_thesis: verum
end;
theorem Th7: :: POLYNOM8:7
for L being non empty ZeroStr
for p being AlgSequence of L
for i being Element of NAT st p . i <> 0. L holds
len p >= i + 1
proof
let L be non empty ZeroStr ; ::_thesis: for p being AlgSequence of L
for i being Element of NAT st p . i <> 0. L holds
len p >= i + 1
let p be AlgSequence of L; ::_thesis: for i being Element of NAT st p . i <> 0. L holds
len p >= i + 1
let i be Element of NAT ; ::_thesis: ( p . i <> 0. L implies len p >= i + 1 )
A1: len p is_at_least_length_of p by ALGSEQ_1:def_3;
assume p . i <> 0. L ; ::_thesis: len p >= i + 1
then len p > i by A1, ALGSEQ_1:def_2;
hence len p >= i + 1 by NAT_1:13; ::_thesis: verum
end;
theorem Th8: :: POLYNOM8:8
for L being non empty ZeroStr
for s being AlgSequence of L st len s > 0 holds
s . ((len s) - 1) <> 0. L
proof
let L be non empty ZeroStr ; ::_thesis: for s being AlgSequence of L st len s > 0 holds
s . ((len s) - 1) <> 0. L
let s be AlgSequence of L; ::_thesis: ( len s > 0 implies s . ((len s) - 1) <> 0. L )
assume len s > 0 ; ::_thesis: s . ((len s) - 1) <> 0. L
then len s >= 0 + 1 by NAT_1:13;
then (len s) - 1 >= 1 - 1 by XREAL_1:9;
then reconsider l = (len s) - 1 as Element of NAT by INT_1:3;
assume A1: s . ((len s) - 1) = 0. L ; ::_thesis: contradiction
now__::_thesis:_for_i_being_Nat_st_i_>=_l_holds_
s_._i_=_0._L
let i be Nat; ::_thesis: ( i >= l implies s . b1 = 0. L )
assume A2: i >= l ; ::_thesis: s . b1 = 0. L
percases ( i = l or i > l ) by A2, XXREAL_0:1;
suppose i = l ; ::_thesis: s . b1 = 0. L
hence s . i = 0. L by A1; ::_thesis: verum
end;
suppose i > l ; ::_thesis: s . b1 = 0. L
then i >= l + 1 by NAT_1:13;
hence s . i = 0. L by ALGSEQ_1:8; ::_thesis: verum
end;
end;
end;
then A3: l is_at_least_length_of s by ALGSEQ_1:def_2;
len s < (len s) + 1 by NAT_1:13;
then (len s) - 1 < ((len s) + 1) - 1 by XREAL_1:9;
hence contradiction by A3, ALGSEQ_1:def_3; ::_thesis: verum
end;
theorem Th9: :: POLYNOM8:9
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 len p > 0 & len q > 0 holds
len (p *' q) <= (len p) + (len 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 len p > 0 & len q > 0 holds
len (p *' q) <= (len p) + (len q)
let p, q be Polynomial of L; ::_thesis: ( len p > 0 & len q > 0 implies len (p *' q) <= (len p) + (len q) )
assume that
A1: len p > 0 and
A2: len q > 0 ; ::_thesis: len (p *' q) <= (len p) + (len q)
A3: ((len p) + (len q)) - 1 <= ((len p) + (len q)) - 0 by XREAL_1:13;
(len q) + 1 > 0 + 1 by A2, XREAL_1:6;
then len q >= 1 by NAT_1:13;
then A4: (len q) - 1 >= 1 - 1 by XREAL_1:13;
q . ((len q) - 1) <> 0. L by A2, Th8;
then A5: q . ((len q) -' 1) <> 0. L by A4, XREAL_0:def_2;
(len p) + 1 > 0 + 1 by A1, XREAL_1:6;
then len p >= 1 by NAT_1:13;
then A6: (len p) - 1 >= 1 - 1 by XREAL_1:13;
p . ((len p) - 1) <> 0. L by A1, Th8;
then p . ((len p) -' 1) <> 0. L by A6, XREAL_0:def_2;
then (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. L by A5, VECTSP_2:def_1;
hence len (p *' q) <= (len p) + (len q) by A3, POLYNOM4:10; ::_thesis: verum
end;
theorem Th10: :: POLYNOM8:10
for L being non empty associative doubleLoopStr
for k, l being Element of L
for seq being sequence of L holds k * (l * seq) = (k * l) * seq
proof
let L be non empty associative doubleLoopStr ; ::_thesis: for k, l being Element of L
for seq being sequence of L holds k * (l * seq) = (k * l) * seq
let k, l be Element of L; ::_thesis: for seq being sequence of L holds k * (l * seq) = (k * l) * seq
let seq be sequence of L; ::_thesis: k * (l * seq) = (k * l) * seq
now__::_thesis:_for_i_being_Element_of_NAT_holds_(k_*_(l_*_seq))_._i_=_((k_*_l)_*_seq)_._i
let i be Element of NAT ; ::_thesis: (k * (l * seq)) . i = ((k * l) * seq) . i
thus (k * (l * seq)) . i = k * ((l * seq) . i) by POLYNOM5:def_3
.= k * (l * (seq . i)) by POLYNOM5:def_3
.= (k * l) * (seq . i) by GROUP_1:def_3
.= ((k * l) * seq) . i by POLYNOM5:def_3 ; ::_thesis: verum
end;
hence k * (l * seq) = (k * l) * seq by FUNCT_2:63; ::_thesis: verum
end;
begin
definition
let L be non empty doubleLoopStr ;
let m1, m2 be sequence of L;
funcm1 * m2 -> sequence of L means :Def2: :: POLYNOM8:def 2
for i being Nat holds it . i = (m1 . i) * (m2 . i);
existence
ex b1 being sequence of L st
for i being Nat holds b1 . i = (m1 . i) * (m2 . i)
proof
defpred S1[ set , set ] means $2 = (m1 /. $1) * (m2 /. $1);
A1: for x being set st x in NAT holds
ex y being set st
( y in the carrier of L & S1[x,y] ) ;
consider f being Function of NAT, the carrier of L such that
A2: for x being set st x in NAT holds
S1[x,f . x] from FUNCT_2:sch_1(A1);
reconsider f = f as sequence of L ;
take f ; ::_thesis: for i being Nat holds f . i = (m1 . i) * (m2 . i)
now__::_thesis:_for_i_being_Nat_holds_f_._i_=_(m1_._i)_*_(m2_._i)
let i be Nat; ::_thesis: f . i = (m1 . i) * (m2 . i)
A3: i in NAT by ORDINAL1:def_12;
dom m2 = NAT by FUNCT_2:def_1;
then A4: m2 /. i = m2 . i by A3, PARTFUN1:def_6;
dom m1 = NAT by FUNCT_2:def_1;
then m1 /. i = m1 . i by A3, PARTFUN1:def_6;
hence f . i = (m1 . i) * (m2 . i) by A2, A3, A4; ::_thesis: verum
end;
hence for i being Nat holds f . i = (m1 . i) * (m2 . i) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being sequence of L st ( for i being Nat holds b1 . i = (m1 . i) * (m2 . i) ) & ( for i being Nat holds b2 . i = (m1 . i) * (m2 . i) ) holds
b1 = b2
proof
let z1, z2 be sequence of L; ::_thesis: ( ( for i being Nat holds z1 . i = (m1 . i) * (m2 . i) ) & ( for i being Nat holds z2 . i = (m1 . i) * (m2 . i) ) implies z1 = z2 )
assume A5: for i being Nat holds z1 . i = (m1 . i) * (m2 . i) ; ::_thesis: ( ex i being Nat st not z2 . i = (m1 . i) * (m2 . i) or z1 = z2 )
assume A6: for i being Nat holds z2 . i = (m1 . i) * (m2 . i) ; ::_thesis: z1 = z2
A7: now__::_thesis:_for_x_being_set_st_x_in_dom_z1_holds_
z1_._x_=_z2_._x
let x be set ; ::_thesis: ( x in dom z1 implies z1 . x = z2 . x )
assume x in dom z1 ; ::_thesis: z1 . x = z2 . x
then reconsider x9 = x as Element of NAT by FUNCT_2:def_1;
thus z1 . x = (m1 . x9) * (m2 . x9) by A5
.= z2 . x by A6 ; ::_thesis: verum
end;
dom z1 = NAT by FUNCT_2:def_1
.= dom z2 by FUNCT_2:def_1 ;
hence z1 = z2 by A7, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines * POLYNOM8:def_2_:_
for L being non empty doubleLoopStr
for m1, m2, b4 being sequence of L holds
( b4 = m1 * m2 iff for i being Nat holds b4 . i = (m1 . i) * (m2 . i) );
registration
let L be non empty right_complementable left-distributive add-associative right_zeroed doubleLoopStr ;
let m1, m2 be AlgSequence of L;
clusterm1 * m2 -> finite-Support ;
coherence
m1 * m2 is finite-Support
proof
set f = m1 * m2;
ex n being Nat st
for i being Nat st i >= n holds
(m1 * m2) . i = 0. L
proof
take (len m1) + 1 ; ::_thesis: for i being Nat st i >= (len m1) + 1 holds
(m1 * m2) . i = 0. L
now__::_thesis:_for_i_being_Nat_st_i_>=_(len_m1)_+_1_holds_
0._L_=_(m1_*_m2)_._i
let i be Nat; ::_thesis: ( i >= (len m1) + 1 implies 0. L = (m1 * m2) . i )
assume i >= (len m1) + 1 ; ::_thesis: 0. L = (m1 * m2) . i
then i > len m1 by NAT_1:13;
then m1 . i = 0. L by ALGSEQ_1:8;
hence 0. L = (m1 . i) * (m2 . i) by VECTSP_1:7
.= (m1 * m2) . i by Def2 ;
::_thesis: verum
end;
hence for i being Nat st i >= (len m1) + 1 holds
(m1 * m2) . i = 0. L ; ::_thesis: verum
end;
hence m1 * m2 is finite-Support by ALGSEQ_1:def_1; ::_thesis: verum
end;
end;
theorem Th11: :: POLYNOM8:11
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for m1, m2 being AlgSequence of L holds len (m1 * m2) <= min ((len m1),(len m2))
proof
let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for m1, m2 being AlgSequence of L holds len (m1 * m2) <= min ((len m1),(len m2))
let m1, m2 be AlgSequence of L; ::_thesis: len (m1 * m2) <= min ((len m1),(len m2))
set p = m1 * m2;
set k = min ((len m1),(len m2));
reconsider k = min ((len m1),(len m2)) as Element of NAT ;
now__::_thesis:_for_i_being_Nat_st_i_>=_k_holds_
0._L_=_(m1_*_m2)_._i
let i be Nat; ::_thesis: ( i >= k implies 0. L = (m1 * m2) . b1 )
assume A1: i >= k ; ::_thesis: 0. L = (m1 * m2) . b1
percases ( k = len m1 or k = len m2 ) by XXREAL_0:15;
suppose k = len m1 ; ::_thesis: 0. L = (m1 * m2) . b1
then m1 . i = 0. L by A1, ALGSEQ_1:8;
hence 0. L = (m1 . i) * (m2 . i) by VECTSP_1:7
.= (m1 * m2) . i by Def2 ;
::_thesis: verum
end;
suppose k = len m2 ; ::_thesis: 0. L = (m1 * m2) . b1
then m2 . i = 0. L by A1, ALGSEQ_1:8;
hence 0. L = (m1 . i) * (m2 . i) by VECTSP_1:6
.= (m1 * m2) . i by Def2 ;
::_thesis: verum
end;
end;
end;
then k is_at_least_length_of m1 * m2 by ALGSEQ_1:def_2;
hence len (m1 * m2) <= min ((len m1),(len m2)) by ALGSEQ_1:def_3; ::_thesis: verum
end;
theorem :: POLYNOM8:12
for L being non empty right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr
for m1, m2 being AlgSequence of L st len m1 = len m2 holds
len (m1 * m2) = len m1
proof
let L be non empty right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for m1, m2 being AlgSequence of L st len m1 = len m2 holds
len (m1 * m2) = len m1
let m1, m2 be AlgSequence of L; ::_thesis: ( len m1 = len m2 implies len (m1 * m2) = len m1 )
set p = m1 * m2;
assume A1: len m1 = len m2 ; ::_thesis: len (m1 * m2) = len m1
A2: now__::_thesis:_(_(_len_m1_=_0_&_len_(m1_*_m2)_>=_len_m1_)_or_(_len_m1_<>_0_&_len_(m1_*_m2)_>=_len_m1_)_)
percases ( len m1 = 0 or len m1 <> 0 ) ;
case len m1 = 0 ; ::_thesis: len (m1 * m2) >= len m1
hence len (m1 * m2) >= len m1 ; ::_thesis: verum
end;
case len m1 <> 0 ; ::_thesis: len (m1 * m2) >= len m1
then len m1 >= 0 + 1 by NAT_1:13;
then (len m1) - 1 >= 1 - 1 by XREAL_1:9;
then reconsider l = (len m1) - 1 as Element of NAT by INT_1:3;
A3: l + 1 = (len m1) + 0 ;
then ( m1 . l <> 0. L & m2 . l <> 0. L ) by A1, ALGSEQ_1:10;
then (m1 . l) * (m2 . l) <> 0. L by VECTSP_2:def_1;
then (m1 * m2) . l <> 0. L by Def2;
hence len (m1 * m2) >= len m1 by A3, Th7; ::_thesis: verum
end;
end;
end;
min ((len m1),(len m2)) = len m1 by A1;
then len (m1 * m2) <= len m1 by Th11;
hence len (m1 * m2) = len m1 by A2, XXREAL_0:1; ::_thesis: verum
end;
begin
definition
let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ;
let a be Element of L;
let i be Integer;
func pow (a,i) -> Element of L equals :Def3: :: POLYNOM8:def 3
(power L) . (a,i) if 0 <= i
otherwise ((power L) . (a,(abs i))) " ;
coherence
( ( 0 <= i implies (power L) . (a,i) is Element of L ) & ( not 0 <= i implies ((power L) . (a,(abs i))) " is Element of L ) )
proof
( 0 <= i implies (power L) . (a,i) is Element of L )
proof
assume 0 <= i ; ::_thesis: (power L) . (a,i) is Element of L
then reconsider i9 = i as Element of NAT by INT_1:3;
(power L) . (a,i9) is Element of L ;
hence (power L) . (a,i) is Element of L ; ::_thesis: verum
end;
hence ( ( 0 <= i implies (power L) . (a,i) is Element of L ) & ( not 0 <= i implies ((power L) . (a,(abs i))) " is Element of L ) ) ; ::_thesis: verum
end;
consistency
for b1 being Element of L holds verum ;
end;
:: deftheorem Def3 defines pow POLYNOM8:def_3_:_
for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for a being Element of L
for i being Integer holds
( ( 0 <= i implies pow (a,i) = (power L) . (a,i) ) & ( not 0 <= i implies pow (a,i) = ((power L) . (a,(abs i))) " ) );
theorem Th13: :: POLYNOM8:13
for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for x being Element of L holds pow (x,0) = 1. L
proof
let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for x being Element of L holds pow (x,0) = 1. L
let x be Element of L; ::_thesis: pow (x,0) = 1. L
pow (x,0) = x |^ 0 by Def3
.= 1_ L by BINOM:8 ;
hence pow (x,0) = 1. L ; ::_thesis: verum
end;
Lm3: for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for a being Element of L
for i being Integer st 0 > i holds
pow (a,i) = (pow (a,(abs i))) "
proof
let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for a being Element of L
for i being Integer st 0 > i holds
pow (a,i) = (pow (a,(abs i))) "
let a be Element of L; ::_thesis: for i being Integer st 0 > i holds
pow (a,i) = (pow (a,(abs i))) "
let i be Integer; ::_thesis: ( 0 > i implies pow (a,i) = (pow (a,(abs i))) " )
assume A1: 0 > i ; ::_thesis: pow (a,i) = (pow (a,(abs i))) "
pow (a,(abs i)) = (power L) . (a,(abs i)) by Def3;
hence pow (a,i) = (pow (a,(abs i))) " by A1, Def3; ::_thesis: verum
end;
Lm4: for L being non empty non degenerated almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for i being Integer
for x being Element of L st i <= 0 holds
pow (x,i) = (pow (x,(abs i))) "
proof
let L be non empty non degenerated almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for i being Integer
for x being Element of L st i <= 0 holds
pow (x,i) = (pow (x,(abs i))) "
let i be Integer; ::_thesis: for x being Element of L st i <= 0 holds
pow (x,i) = (pow (x,(abs i))) "
let x be Element of L; ::_thesis: ( i <= 0 implies pow (x,i) = (pow (x,(abs i))) " )
A1: 1. L <> 0. L ;
assume A2: i <= 0 ; ::_thesis: pow (x,i) = (pow (x,(abs i))) "
percases ( i < 0 or i = 0 ) by A2;
suppose i < 0 ; ::_thesis: pow (x,i) = (pow (x,(abs i))) "
hence pow (x,i) = (pow (x,(abs i))) " by Lm3; ::_thesis: verum
end;
supposeA3: i = 0 ; ::_thesis: pow (x,i) = (pow (x,(abs i))) "
hence pow (x,i) = 1. L by Th13
.= (1. L) * ((1. L) ") by A1, VECTSP_1:def_10
.= (1_ L) " by VECTSP_1:def_8
.= (x |^ 0) " by BINOM:8
.= (x |^ (abs i)) " by A3, ABSVALUE:def_1
.= (pow (x,(abs i))) " by Def3 ;
::_thesis: verum
end;
end;
end;
theorem Th14: :: POLYNOM8:14
for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for x being Element of L holds pow (x,1) = x
proof
let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for x being Element of L holds pow (x,1) = x
let x be Element of L; ::_thesis: pow (x,1) = x
thus pow (x,1) = x |^ 1 by Def3
.= x by BINOM:8 ; ::_thesis: verum
end;
theorem Th15: :: POLYNOM8:15
for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for x being Element of L holds pow (x,(- 1)) = x "
proof
let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for x being Element of L holds pow (x,(- 1)) = x "
let x be Element of L; ::_thesis: pow (x,(- 1)) = x "
abs (- 1) = - (- 1) by ABSVALUE:def_1;
hence pow (x,(- 1)) = (pow (x,1)) " by Lm3
.= x " by Th14 ;
::_thesis: verum
end;
Lm5: for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for i being Element of NAT holds pow ((1. L),i) = 1. L
proof
let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for i being Element of NAT holds pow ((1. L),i) = 1. L
let i be Element of NAT ; ::_thesis: pow ((1. L),i) = 1. L
defpred S1[ Element of NAT ] means pow ((1. L),$1) = 1. L;
A1: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
pow ((1. L),(k + 1)) = (power L) . ((1. L),(k + 1)) by Def3
.= ((power L) . ((1. L),k)) * (1. L) by GROUP_1:def_7
.= (1. L) * (1. L) by A2, Def3
.= 1. L by VECTSP_1:def_8 ;
hence S1[k + 1] ; ::_thesis: verum
end;
pow ((1_ L),0) = (power L) . ((1. L),0) by Def3;
then A3: S1[ 0 ] by GROUP_1:def_7;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A3, A1);
hence pow ((1. L),i) = 1. L ; ::_thesis: verum
end;
theorem Th16: :: POLYNOM8:16
for L being non empty non degenerated almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for i being Integer holds pow ((1. L),i) = 1. L
proof
let L be non empty non degenerated almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for i being Integer holds pow ((1. L),i) = 1. L
let i be Integer; ::_thesis: pow ((1. L),i) = 1. L
percases ( 0 <= i or 0 > i ) ;
suppose 0 <= i ; ::_thesis: pow ((1. L),i) = 1. L
then i is Element of NAT by INT_1:3;
hence pow ((1. L),i) = 1. L by Lm5; ::_thesis: verum
end;
supposeA1: 0 > i ; ::_thesis: pow ((1. L),i) = 1. L
A2: ( 1. L <> 0. L & (1. L) * (1. L) = 1. L ) by VECTSP_1:def_4;
A3: pow ((1. L),(abs i)) = 1. L by Lm5;
pow ((1. L),i) = ((power L) . ((1. L),(abs i))) " by A1, Def3
.= (1. L) " by A3, Def3 ;
hence pow ((1. L),i) = 1. L by A2, VECTSP_1:def_10; ::_thesis: verum
end;
end;
end;
theorem Th17: :: POLYNOM8:17
for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for x being Element of L
for n being Element of NAT holds
( pow (x,(n + 1)) = (pow (x,n)) * x & pow (x,(n + 1)) = x * (pow (x,n)) )
proof
let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for x being Element of L
for n being Element of NAT holds
( pow (x,(n + 1)) = (pow (x,n)) * x & pow (x,(n + 1)) = x * (pow (x,n)) )
let x be Element of L; ::_thesis: for n being Element of NAT holds
( pow (x,(n + 1)) = (pow (x,n)) * x & pow (x,(n + 1)) = x * (pow (x,n)) )
let n be Element of NAT ; ::_thesis: ( pow (x,(n + 1)) = (pow (x,n)) * x & pow (x,(n + 1)) = x * (pow (x,n)) )
pow (x,(n + 1)) = x |^ (n + 1) by Def3
.= (x |^ n) * x by GROUP_1:def_7
.= (pow (x,n)) * x by Def3 ;
hence ( pow (x,(n + 1)) = (pow (x,n)) * x & pow (x,(n + 1)) = x * (pow (x,n)) ) ; ::_thesis: verum
end;
Lm6: for L being non empty well-unital doubleLoopStr
for n being Element of NAT holds (1. L) |^ n = 1. L
proof
let L be non empty well-unital doubleLoopStr ; ::_thesis: for n being Element of NAT holds (1. L) |^ n = 1. L
let n be Element of NAT ; ::_thesis: (1. L) |^ n = 1. L
defpred S1[ Element of NAT ] means (1. L) |^ $1 = 1_ L;
A1: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
(1. L) |^ (k + 1) = ((1. L) |^ k) * (1. L) by GROUP_1:def_7
.= 1. L by A2, VECTSP_1:def_8 ;
hence S1[k + 1] ; ::_thesis: verum
end;
A3: S1[ 0 ] by BINOM:8;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A3, A1);
hence (1. L) |^ n = 1. L ; ::_thesis: verum
end;
Lm7: for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for m being Element of NAT
for x being Element of L st x <> 0. L holds
(x |^ m) * ((x ") |^ m) = 1. L
proof
let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for m being Element of NAT
for x being Element of L st x <> 0. L holds
(x |^ m) * ((x ") |^ m) = 1. L
let m be Element of NAT ; ::_thesis: for x being Element of L st x <> 0. L holds
(x |^ m) * ((x ") |^ m) = 1. L
let x be Element of L; ::_thesis: ( x <> 0. L implies (x |^ m) * ((x ") |^ m) = 1. L )
assume A1: x <> 0. L ; ::_thesis: (x |^ m) * ((x ") |^ m) = 1. L
(x |^ m) * ((x ") |^ m) = (x * (x ")) |^ m by BINOM:9
.= (1. L) |^ m by A1, VECTSP_1:def_10
.= 1. L by Lm6 ;
hence (x |^ m) * ((x ") |^ m) = 1. L ; ::_thesis: verum
end;
theorem Th18: :: POLYNOM8:18
for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for i being Integer
for x being Element of L st x <> 0. L holds
(pow (x,i)) " = pow (x,(- i))
proof
let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for i being Integer
for x being Element of L st x <> 0. L holds
(pow (x,i)) " = pow (x,(- i))
let i be Integer; ::_thesis: for x being Element of L st x <> 0. L holds
(pow (x,i)) " = pow (x,(- i))
let x be Element of L; ::_thesis: ( x <> 0. L implies (pow (x,i)) " = pow (x,(- i)) )
assume A1: x <> 0. L ; ::_thesis: (pow (x,i)) " = pow (x,(- i))
A2: 1. L <> 0. L ;
percases ( i >= 0 or i < 0 ) ;
supposeA3: i >= 0 ; ::_thesis: (pow (x,i)) " = pow (x,(- i))
percases ( - i < - 0 or i = 0 ) by A3, XREAL_1:24;
supposeA4: - i < - 0 ; ::_thesis: (pow (x,i)) " = pow (x,(- i))
hence pow (x,(- i)) = (pow (x,(abs (- i)))) " by Lm3
.= (pow (x,(- (- i)))) " by A4, ABSVALUE:def_1
.= (pow (x,i)) " ;
::_thesis: verum
end;
supposeA5: i = 0 ; ::_thesis: (pow (x,i)) " = pow (x,(- i))
hence pow (x,(- i)) = 1. L by Th13
.= (1. L) * ((1. L) ") by A2, VECTSP_1:def_10
.= (1. L) " by VECTSP_1:def_8
.= (pow (x,i)) " by A5, Th13 ;
::_thesis: verum
end;
end;
end;
supposeA6: i < 0 ; ::_thesis: (pow (x,i)) " = pow (x,(- i))
A7: pow (x,(abs i)) = x |^ (abs i) by Def3;
pow (x,i) = (pow (x,(abs i))) " by A6, Lm3;
then (pow (x,i)) " = pow (x,(abs i)) by A1, A7, Th1, VECTSP_1:24;
hence (pow (x,i)) " = pow (x,(- i)) by A6, ABSVALUE:def_1; ::_thesis: verum
end;
end;
end;
theorem Th19: :: POLYNOM8:19
for L being Field
for j being Integer
for x being Element of L st x <> 0. L holds
pow (x,(j + 1)) = (pow (x,j)) * (pow (x,1))
proof
let L be Field; ::_thesis: for j being Integer
for x being Element of L st x <> 0. L holds
pow (x,(j + 1)) = (pow (x,j)) * (pow (x,1))
let j be Integer; ::_thesis: for x being Element of L st x <> 0. L holds
pow (x,(j + 1)) = (pow (x,j)) * (pow (x,1))
let x be Element of L; ::_thesis: ( x <> 0. L implies pow (x,(j + 1)) = (pow (x,j)) * (pow (x,1)) )
A1: pow (x,(- 1)) = (x |^ (abs (- 1))) " by Def3;
assume A2: x <> 0. L ; ::_thesis: pow (x,(j + 1)) = (pow (x,j)) * (pow (x,1))
then x |^ (abs (- 1)) <> 0. L by Th1;
then A3: pow (x,(- 1)) <> 0. L by A1, VECTSP_1:25;
A4: pow (x,(- j)) <> 0. L
proof
percases ( 0 <= - j or - j < 0 ) ;
suppose 0 <= - j ; ::_thesis: pow (x,(- j)) <> 0. L
then reconsider k = - j as Element of NAT by INT_1:3;
pow (x,(- j)) = x |^ k by Def3;
hence pow (x,(- j)) <> 0. L by A2, Th1; ::_thesis: verum
end;
supposeA5: - j < 0 ; ::_thesis: pow (x,(- j)) <> 0. L
A6: x |^ (abs (- j)) <> 0. L by A2, Th1;
pow (x,(- j)) = (x |^ (abs (- j))) " by A5, Def3;
hence pow (x,(- j)) <> 0. L by A6, VECTSP_1:25; ::_thesis: verum
end;
end;
end;
A7: pow (x,(j + 1)) <> 0. L
proof
percases ( 0 <= j + 1 or j + 1 < 0 ) ;
suppose 0 <= j + 1 ; ::_thesis: pow (x,(j + 1)) <> 0. L
then reconsider k = j + 1 as Element of NAT by INT_1:3;
pow (x,(j + 1)) = x |^ k by Def3;
hence pow (x,(j + 1)) <> 0. L by A2, Th1; ::_thesis: verum
end;
supposeA8: j + 1 < 0 ; ::_thesis: pow (x,(j + 1)) <> 0. L
A9: x |^ (abs (j + 1)) <> 0. L by A2, Th1;
pow (x,(j + 1)) = (x |^ (abs (j + 1))) " by A8, Def3;
hence pow (x,(j + 1)) <> 0. L by A9, VECTSP_1:25; ::_thesis: verum
end;
end;
end;
A10: now__::_thesis:_(pow_(x,(j_+_1)))_*_((pow_(x,(-_1)))_*_(pow_(x,(-_j))))_=_1._L
percases ( j >= 0 or j < - 1 or j = - 1 ) by Lm1;
supposeA11: j >= 0 ; ::_thesis: (pow (x,(j + 1))) * ((pow (x,(- 1))) * (pow (x,(- j)))) = 1. L
then reconsider n = j as Element of NAT by INT_1:3;
A12: n + 1 = abs (j + 1) by ABSVALUE:def_1;
pow (x,(abs j)) = x |^ (abs j) by Def3;
then A13: pow (x,(abs j)) <> 0. L by A2, Th1;
pow (x,(abs (j + 1))) = x |^ (abs (j + 1)) by Def3;
then A14: pow (x,(abs (j + 1))) <> 0. L by A2, Th1;
n + 1 >= 0 ;
hence (pow (x,(j + 1))) * ((pow (x,(- 1))) * (pow (x,(- j)))) = (pow (x,(abs (j + 1)))) * ((pow (x,(- 1))) * (pow (x,(- j)))) by ABSVALUE:def_1
.= (pow (x,(abs (j + 1)))) * ((x ") * (pow (x,(- j)))) by Th15
.= (pow (x,(abs (j + 1)))) * ((x ") * ((pow (x,j)) ")) by A2, Th18
.= (pow (x,(abs (j + 1)))) * ((x ") * ((pow (x,(abs j))) ")) by A11, ABSVALUE:def_1
.= (pow (x,(abs (j + 1)))) * ((x * (pow (x,(abs j)))) ") by A2, A13, Th2
.= (pow (x,(abs (j + 1)))) * ((pow (x,((abs j) + 1))) ") by Th17
.= (pow (x,(abs (j + 1)))) * ((pow (x,(abs (j + 1)))) ") by A12, ABSVALUE:def_1
.= 1. L by A14, VECTSP_1:def_10 ;
::_thesis: verum
end;
supposeA15: j < - 1 ; ::_thesis: (pow (x,(j + 1))) * ((pow (x,(- 1))) * (pow (x,(- j)))) = 1. L
A16: pow (x,(- j)) <> 0. L
proof
reconsider k = - j as Element of NAT by A15, INT_1:3;
pow (x,(- j)) = x |^ k by Def3;
hence pow (x,(- j)) <> 0. L by A2, Th1; ::_thesis: verum
end;
pow (x,(abs (j + 1))) = x |^ (abs (j + 1)) by Def3;
then A17: pow (x,(abs (j + 1))) <> 0. L by A2, Th1;
A18: j + 1 < (- 1) + 1 by A15, XREAL_1:6;
hence (pow (x,(j + 1))) * ((pow (x,(- 1))) * (pow (x,(- j)))) = ((pow (x,(abs (j + 1)))) ") * ((pow (x,(- 1))) * (pow (x,(- j)))) by Lm3
.= ((pow (x,(abs (j + 1)))) ") * ((x ") * (pow (x,(- j)))) by Th15
.= (((pow (x,(abs (j + 1)))) ") * (x ")) * (pow (x,(- j))) by GROUP_1:def_3
.= (((pow (x,(abs (j + 1)))) * x) ") * (pow (x,(- j))) by A2, A17, Th2
.= ((pow (x,((abs (j + 1)) + 1))) ") * (pow (x,(- j))) by Th17
.= ((pow (x,((- (j + 1)) + 1))) ") * (pow (x,(- j))) by A18, ABSVALUE:def_1
.= 1. L by A16, VECTSP_1:def_10 ;
::_thesis: verum
end;
supposeA19: j = - 1 ; ::_thesis: (pow (x,(j + 1))) * ((pow (x,(- 1))) * (pow (x,(- j)))) = 1. L
A20: x " <> 0. L by A2, VECTSP_1:25;
thus (pow (x,(j + 1))) * ((pow (x,(- 1))) * (pow (x,(- j)))) = (1. L) * ((pow (x,(- 1))) * (pow (x,(- j)))) by A19, Th13
.= (pow (x,(- 1))) * (pow (x,(- j))) by VECTSP_1:def_8
.= (x ") * (pow (x,(- j))) by Th15
.= (x ") * ((pow (x,j)) ") by A2, Th18
.= (x ") * ((x ") ") by A19, Th15
.= 1. L by A20, VECTSP_1:def_10 ; ::_thesis: verum
end;
end;
end;
A21: pow (x,(j + 1)) <> 0. L
proof
percases ( 0 <= j + 1 or j + 1 < 0 ) ;
suppose 0 <= j + 1 ; ::_thesis: pow (x,(j + 1)) <> 0. L
then reconsider k = j + 1 as Element of NAT by INT_1:3;
pow (x,(j + 1)) = x |^ k by Def3;
hence pow (x,(j + 1)) <> 0. L by A2, Th1; ::_thesis: verum
end;
supposeA22: j + 1 < 0 ; ::_thesis: pow (x,(j + 1)) <> 0. L
A23: x |^ (abs (j + 1)) <> 0. L by A2, Th1;
pow (x,(j + 1)) = (x |^ (abs (j + 1))) " by A22, Def3;
hence pow (x,(j + 1)) <> 0. L by A23, VECTSP_1:25; ::_thesis: verum
end;
end;
end;
(pow (x,(j + 1))) * (pow (x,(- (j + 1)))) = (pow (x,(j + 1))) * ((pow (x,(j + 1))) ") by A2, Th18
.= 1. L by A7, VECTSP_1:def_10 ;
then A24: pow (x,(- (j + 1))) = (pow (x,(- 1))) * (pow (x,(- j))) by A10, A21, VECTSP_1:5;
thus pow (x,(j + 1)) = pow (x,(- (- (j + 1))))
.= ((pow (x,(- 1))) * (pow (x,(- j)))) " by A2, A24, Th18
.= ((pow (x,(- j))) ") * ((pow (x,(- 1))) ") by A4, A3, Th2
.= (pow (x,(- (- j)))) * ((pow (x,(- 1))) ") by A2, Th18
.= (pow (x,j)) * (pow (x,(- (- 1)))) by A2, Th18
.= (pow (x,j)) * (pow (x,1)) ; ::_thesis: verum
end;
theorem Th20: :: POLYNOM8:20
for L being Field
for j being Integer
for x being Element of L st x <> 0. L holds
pow (x,(j - 1)) = (pow (x,j)) * (pow (x,(- 1)))
proof
let L be Field; ::_thesis: for j being Integer
for x being Element of L st x <> 0. L holds
pow (x,(j - 1)) = (pow (x,j)) * (pow (x,(- 1)))
let j be Integer; ::_thesis: for x being Element of L st x <> 0. L holds
pow (x,(j - 1)) = (pow (x,j)) * (pow (x,(- 1)))
let x be Element of L; ::_thesis: ( x <> 0. L implies pow (x,(j - 1)) = (pow (x,j)) * (pow (x,(- 1))) )
assume A1: x <> 0. L ; ::_thesis: pow (x,(j - 1)) = (pow (x,j)) * (pow (x,(- 1)))
A2: pow (x,(j - 1)) <> 0. L
proof
percases ( 0 <= j - 1 or j - 1 < 0 ) ;
suppose 0 <= j - 1 ; ::_thesis: pow (x,(j - 1)) <> 0. L
then reconsider k = j - 1 as Element of NAT by INT_1:3;
pow (x,(j - 1)) = x |^ k by Def3;
hence pow (x,(j - 1)) <> 0. L by A1, Th1; ::_thesis: verum
end;
supposeA3: j - 1 < 0 ; ::_thesis: pow (x,(j - 1)) <> 0. L
A4: x |^ (abs (j - 1)) <> 0. L by A1, Th1;
pow (x,(j - 1)) = (x |^ (abs (j - 1))) " by A3, Def3;
hence pow (x,(j - 1)) <> 0. L by A4, VECTSP_1:25; ::_thesis: verum
end;
end;
end;
A5: now__::_thesis:_(pow_(x,(j_-_1)))_*_(x_*_(pow_(x,(-_j))))_=_1._L
percases ( j >= 1 or j < 0 or j = 0 ) by Lm2;
supposeA6: j >= 1 ; ::_thesis: (pow (x,(j - 1))) * (x * (pow (x,(- j)))) = 1. L
then A7: abs j = j by ABSVALUE:def_1;
pow (x,(abs (- j))) = x |^ (abs (- j)) by Def3;
then A8: pow (x,(abs (- j))) <> 0. L by A1, Th1;
A9: abs j = abs (- j) by COMPLEX1:52;
j >= 1 + 0 by A6;
then A10: j - 1 >= 0 by XREAL_1:19;
then A11: (abs (j - 1)) + 1 = (j - 1) + 1 by ABSVALUE:def_1
.= j ;
thus (pow (x,(j - 1))) * (x * (pow (x,(- j)))) = ((pow (x,(j - 1))) * x) * (pow (x,(- j))) by GROUP_1:def_3
.= ((pow (x,(abs (j - 1)))) * x) * (pow (x,(- j))) by A10, ABSVALUE:def_1
.= ((pow (x,(abs (j - 1)))) * x) * ((pow (x,(abs (- j)))) ") by A6, Lm4
.= (pow (x,((abs (j - 1)) + 1))) * ((pow (x,(abs (- j)))) ") by Th17
.= 1. L by A8, A11, A7, A9, VECTSP_1:def_10 ; ::_thesis: verum
end;
supposeA12: j < 0 ; ::_thesis: (pow (x,(j - 1))) * (x * (pow (x,(- j)))) = 1. L
pow (x,(abs (j - 1))) = x |^ (abs (j - 1)) by Def3;
then A13: pow (x,(abs (j - 1))) <> 0. L by A1, Th1;
A14: 1 - j = - (j - 1) ;
thus (pow (x,(j - 1))) * (x * (pow (x,(- j)))) = ((pow (x,(abs (j - 1)))) ") * (x * (pow (x,(- j)))) by A12, Lm3
.= ((pow (x,(abs (j - 1)))) ") * (x * (pow (x,(abs (- j))))) by A12, ABSVALUE:def_1
.= ((pow (x,(abs (j - 1)))) ") * (pow (x,(1 + (abs (- j))))) by Th17
.= ((pow (x,(abs (j - 1)))) ") * (pow (x,(1 + (- j)))) by A12, ABSVALUE:def_1
.= ((pow (x,(abs (j - 1)))) ") * (pow (x,(abs (j - 1)))) by A12, A14, ABSVALUE:def_1
.= 1. L by A13, VECTSP_1:def_10 ; ::_thesis: verum
end;
supposeA15: j = 0 ; ::_thesis: (pow (x,(j - 1))) * (x * (pow (x,(- j)))) = 1. L
hence (pow (x,(j - 1))) * (x * (pow (x,(- j)))) = (x ") * (x * (pow (x,(- j)))) by Th15
.= ((x ") * x) * (pow (x,(- j))) by GROUP_1:def_3
.= (1. L) * (pow (x,(- j))) by A1, VECTSP_1:def_10
.= pow (x,0) by A15, VECTSP_1:def_8
.= 1. L by Th13 ;
::_thesis: verum
end;
end;
end;
A16: pow (x,(- j)) <> 0. L
proof
percases ( 0 <= - j or - j < 0 ) ;
suppose 0 <= - j ; ::_thesis: pow (x,(- j)) <> 0. L
then reconsider k = - j as Element of NAT by INT_1:3;
pow (x,(- j)) = x |^ k by Def3;
hence pow (x,(- j)) <> 0. L by A1, Th1; ::_thesis: verum
end;
supposeA17: - j < 0 ; ::_thesis: pow (x,(- j)) <> 0. L
A18: x |^ (abs (- j)) <> 0. L by A1, Th1;
pow (x,(- j)) = (x |^ (abs (- j))) " by A17, Def3;
hence pow (x,(- j)) <> 0. L by A18, VECTSP_1:25; ::_thesis: verum
end;
end;
end;
A19: pow (x,(j - 1)) <> 0. L
proof
percases ( 0 <= j - 1 or j - 1 < 0 ) ;
suppose 0 <= j - 1 ; ::_thesis: pow (x,(j - 1)) <> 0. L
then reconsider k = j - 1 as Element of NAT by INT_1:3;
pow (x,(j - 1)) = x |^ k by Def3;
hence pow (x,(j - 1)) <> 0. L by A1, Th1; ::_thesis: verum
end;
supposeA20: j - 1 < 0 ; ::_thesis: pow (x,(j - 1)) <> 0. L
A21: x |^ (abs (j - 1)) <> 0. L by A1, Th1;
pow (x,(j - 1)) = (x |^ (abs (j - 1))) " by A20, Def3;
hence pow (x,(j - 1)) <> 0. L by A21, VECTSP_1:25; ::_thesis: verum
end;
end;
end;
(pow (x,(j - 1))) * (pow (x,(1 - j))) = (pow (x,(j - 1))) * (pow (x,(- (j - 1))))
.= (pow (x,(j - 1))) * ((pow (x,(j - 1))) ") by A1, Th18
.= 1. L by A2, VECTSP_1:def_10 ;
then x * (pow (x,(- j))) = pow (x,(1 - j)) by A5, A19, VECTSP_1:5;
then (pow (x,(1 - j))) " = ((pow (x,(- j))) ") * (x ") by A1, A16, Th2
.= (pow (x,(- (- j)))) * (x ") by A1, Th18
.= (pow (x,j)) * (pow (x,(- 1))) by Th15 ;
then (pow (x,j)) * (pow (x,(- 1))) = pow (x,(- (1 - j))) by A1, Th18;
hence pow (x,(j - 1)) = (pow (x,j)) * (pow (x,(- 1))) ; ::_thesis: verum
end;
theorem Th21: :: POLYNOM8:21
for L being Field
for i, j being Integer
for x being Element of L st x <> 0. L holds
(pow (x,i)) * (pow (x,j)) = pow (x,(i + j))
proof
let L be Field; ::_thesis: for i, j being Integer
for x being Element of L st x <> 0. L holds
(pow (x,i)) * (pow (x,j)) = pow (x,(i + j))
let i, j be Integer; ::_thesis: for x being Element of L st x <> 0. L holds
(pow (x,i)) * (pow (x,j)) = pow (x,(i + j))
let x be Element of L; ::_thesis: ( x <> 0. L implies (pow (x,i)) * (pow (x,j)) = pow (x,(i + j)) )
defpred S1[ Integer] means for i being Integer holds pow (x,(i + $1)) = (pow (x,i)) * (pow (x,$1));
assume A1: x <> 0. L ; ::_thesis: (pow (x,i)) * (pow (x,j)) = pow (x,(i + j))
A2: for j being Integer st S1[j] holds
( S1[j - 1] & S1[j + 1] )
proof
let j be Integer; ::_thesis: ( S1[j] implies ( S1[j - 1] & S1[j + 1] ) )
assume A3: for i being Integer holds pow (x,(i + j)) = (pow (x,i)) * (pow (x,j)) ; ::_thesis: ( S1[j - 1] & S1[j + 1] )
thus for i being Integer holds pow (x,(i + (j - 1))) = (pow (x,i)) * (pow (x,(j - 1))) ::_thesis: S1[j + 1]
proof
let i be Integer; ::_thesis: pow (x,(i + (j - 1))) = (pow (x,i)) * (pow (x,(j - 1)))
thus pow (x,(i + (j - 1))) = pow (x,((i - 1) + j))
.= (pow (x,(i - 1))) * (pow (x,j)) by A3
.= ((pow (x,i)) * (pow (x,(- 1)))) * (pow (x,j)) by A1, Th20
.= (pow (x,i)) * ((pow (x,(- 1))) * (pow (x,j))) by GROUP_1:def_3
.= (pow (x,i)) * (pow (x,(j + (- 1)))) by A3
.= (pow (x,i)) * (pow (x,(j - 1))) ; ::_thesis: verum
end;
let i be Integer; ::_thesis: pow (x,(i + (j + 1))) = (pow (x,i)) * (pow (x,(j + 1)))
thus pow (x,(i + (j + 1))) = pow (x,((i + 1) + j))
.= (pow (x,(i + 1))) * (pow (x,j)) by A3
.= ((pow (x,i)) * (pow (x,1))) * (pow (x,j)) by A1, Th19
.= (pow (x,i)) * ((pow (x,1)) * (pow (x,j))) by GROUP_1:def_3
.= (pow (x,i)) * (pow (x,(j + 1))) by A3 ; ::_thesis: verum
end;
A4: S1[ 0 ]
proof
let i be Integer; ::_thesis: pow (x,(i + 0)) = (pow (x,i)) * (pow (x,0))
thus pow (x,(i + 0)) = (pow (x,i)) * (1. L) by VECTSP_1:def_4
.= (pow (x,i)) * (pow (x,0)) by Th13 ; ::_thesis: verum
end;
for j being Integer holds S1[j] from INT_1:sch_4(A4, A2);
hence (pow (x,i)) * (pow (x,j)) = pow (x,(i + j)) ; ::_thesis: verum
end;
Lm8: for L being non empty non degenerated right_complementable almost_left_invertible associative commutative left-distributive well-unital add-associative right_zeroed doubleLoopStr
for k being Element of NAT
for x being Element of L st x <> 0. L holds
(x ") |^ k = (x |^ k) "
proof
let L be non empty non degenerated right_complementable almost_left_invertible associative commutative left-distributive well-unital add-associative right_zeroed doubleLoopStr ; ::_thesis: for k being Element of NAT
for x being Element of L st x <> 0. L holds
(x ") |^ k = (x |^ k) "
let k be Element of NAT ; ::_thesis: for x being Element of L st x <> 0. L holds
(x ") |^ k = (x |^ k) "
let x be Element of L; ::_thesis: ( x <> 0. L implies (x ") |^ k = (x |^ k) " )
A1: 1. L <> 0. L ;
defpred S1[ Element of NAT ] means (x ") |^ $1 = (x |^ $1) " ;
assume A2: x <> 0. L ; ::_thesis: (x ") |^ k = (x |^ k) "
A3: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; ::_thesis: S1[n + 1]
A5: x |^ n <> 0. L by A2, Th1;
(x ") |^ (n + 1) = ((x ") |^ n) * (x ") by GROUP_1:def_7
.= (x * (x |^ n)) " by A2, A4, A5, Th2
.= ((x |^ 1) * (x |^ n)) " by BINOM:8
.= (x |^ (n + 1)) " by BINOM:10 ;
hence S1[n + 1] ; ::_thesis: verum
end;
(x ") |^ 0 = 1_ L by BINOM:8
.= (1. L) * ((1. L) ") by A1, VECTSP_1:def_10
.= (1_ L) " by VECTSP_1:def_8
.= (x |^ 0) " by BINOM:8 ;
then A6: S1[ 0 ] ;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A3);
hence (x ") |^ k = (x |^ k) " ; ::_thesis: verum
end;
theorem Th22: :: POLYNOM8:22
for L being non empty non degenerated right_complementable almost_left_invertible associative commutative left-distributive well-unital add-associative right_zeroed doubleLoopStr
for k being Element of NAT
for x being Element of L st x <> 0. L holds
pow ((x "),k) = pow (x,(- k))
proof
let L be non empty non degenerated right_complementable almost_left_invertible associative commutative left-distributive well-unital add-associative right_zeroed doubleLoopStr ; ::_thesis: for k being Element of NAT
for x being Element of L st x <> 0. L holds
pow ((x "),k) = pow (x,(- k))
let k be Element of NAT ; ::_thesis: for x being Element of L st x <> 0. L holds
pow ((x "),k) = pow (x,(- k))
let x be Element of L; ::_thesis: ( x <> 0. L implies pow ((x "),k) = pow (x,(- k)) )
assume A1: x <> 0. L ; ::_thesis: pow ((x "),k) = pow (x,(- k))
pow ((x "),k) = (x ") |^ k by Def3
.= (x |^ k) " by A1, Lm8
.= (pow (x,k)) " by Def3
.= pow (x,(- k)) by A1, Th18 ;
hence pow ((x "),k) = pow (x,(- k)) ; ::_thesis: verum
end;
theorem Th23: :: POLYNOM8:23
for L being Field
for x being Element of L st x <> 0. L holds
for i, j, k being Nat holds (pow (x,((i - 1) * (k - 1)))) * (pow (x,(- ((j - 1) * (k - 1))))) = pow (x,((i - j) * (k - 1)))
proof
let L be Field; ::_thesis: for x being Element of L st x <> 0. L holds
for i, j, k being Nat holds (pow (x,((i - 1) * (k - 1)))) * (pow (x,(- ((j - 1) * (k - 1))))) = pow (x,((i - j) * (k - 1)))
let x be Element of L; ::_thesis: ( x <> 0. L implies for i, j, k being Nat holds (pow (x,((i - 1) * (k - 1)))) * (pow (x,(- ((j - 1) * (k - 1))))) = pow (x,((i - j) * (k - 1))) )
assume A1: x <> 0. L ; ::_thesis: for i, j, k being Nat holds (pow (x,((i - 1) * (k - 1)))) * (pow (x,(- ((j - 1) * (k - 1))))) = pow (x,((i - j) * (k - 1)))
let i, j, k be Nat; ::_thesis: (pow (x,((i - 1) * (k - 1)))) * (pow (x,(- ((j - 1) * (k - 1))))) = pow (x,((i - j) * (k - 1)))
(pow (x,((i - 1) * (k - 1)))) * (pow (x,(- ((j - 1) * (k - 1))))) = pow (x,(((i - 1) * (k - 1)) + (- ((j - 1) * (k - 1))))) by A1, Th21
.= pow (x,((i - j) * (k - 1))) ;
hence (pow (x,((i - 1) * (k - 1)))) * (pow (x,(- ((j - 1) * (k - 1))))) = pow (x,((i - j) * (k - 1))) ; ::_thesis: verum
end;
theorem Th24: :: POLYNOM8:24
for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for x being Element of L
for n, m being Element of NAT holds pow (x,(n * m)) = pow ((pow (x,n)),m)
proof
let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for x being Element of L
for n, m being Element of NAT holds pow (x,(n * m)) = pow ((pow (x,n)),m)
let x be Element of L; ::_thesis: for n, m being Element of NAT holds pow (x,(n * m)) = pow ((pow (x,n)),m)
let n, m be Element of NAT ; ::_thesis: pow (x,(n * m)) = pow ((pow (x,n)),m)
pow (x,(n * m)) = x |^ (n * m) by Def3
.= (x |^ n) |^ m by BINOM:11
.= pow ((x |^ n),m) by Def3
.= pow ((pow (x,n)),m) by Def3 ;
hence pow (x,(n * m)) = pow ((pow (x,n)),m) ; ::_thesis: verum
end;
Lm9: for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for x being Element of L st x <> 0. L holds
for n being Element of NAT holds pow ((x "),n) = (pow (x,n)) "
proof
let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for x being Element of L st x <> 0. L holds
for n being Element of NAT holds pow ((x "),n) = (pow (x,n)) "
let x be Element of L; ::_thesis: ( x <> 0. L implies for n being Element of NAT holds pow ((x "),n) = (pow (x,n)) " )
A1: 1. L <> 0. L ;
defpred S1[ Nat] means pow ((x "),$1) = (pow (x,$1)) " ;
assume A2: x <> 0. L ; ::_thesis: for n being Element of NAT holds pow ((x "),n) = (pow (x,n)) "
now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
(_pow_((x_"),(n_+_1))_=_(pow_(x,(n_+_1)))_"_&_S1[n_+_1]_)
let n be Element of NAT ; ::_thesis: ( S1[n] implies ( pow ((x "),(n + 1)) = (pow (x,(n + 1))) " & S1[n + 1] ) )
assume A3: S1[n] ; ::_thesis: ( pow ((x "),(n + 1)) = (pow (x,(n + 1))) " & S1[n + 1] )
A4: x |^ n <> 0. L by A2, Th1;
thus pow ((x "),(n + 1)) = (x ") |^ (n + 1) by Def3
.= ((x ") |^ n) * (x ") by GROUP_1:def_7
.= (pow ((x "),n)) * (x ") by Def3
.= (((power L) . (x,n)) ") * (x ") by A3, Def3
.= (x * (x |^ n)) " by A2, A4, Th2
.= ((x |^ 1) * (x |^ n)) " by BINOM:8
.= (x |^ (n + 1)) " by BINOM:10
.= (pow (x,(n + 1))) " by Def3 ; ::_thesis: S1[n + 1]
hence S1[n + 1] ; ::_thesis: verum
end;
then A5: for n being Element of NAT st S1[n] holds
S1[n + 1] ;
let n be Element of NAT ; ::_thesis: pow ((x "),n) = (pow (x,n)) "
pow ((x "),0) = 1. L by Th13
.= (1. L) * ((1. L) ") by A1, VECTSP_1:def_10
.= (1. L) " by VECTSP_1:def_8
.= (pow (x,0)) " by Th13 ;
then A6: S1[ 0 ] ;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A5);
hence pow ((x "),n) = (pow (x,n)) " ; ::_thesis: verum
end;
theorem Th25: :: POLYNOM8:25
for L being Field
for x being Element of L st x <> 0. L holds
for i being Integer holds pow ((x "),i) = (pow (x,i)) "
proof
let L be Field; ::_thesis: for x being Element of L st x <> 0. L holds
for i being Integer holds pow ((x "),i) = (pow (x,i)) "
let x be Element of L; ::_thesis: ( x <> 0. L implies for i being Integer holds pow ((x "),i) = (pow (x,i)) " )
assume A1: x <> 0. L ; ::_thesis: for i being Integer holds pow ((x "),i) = (pow (x,i)) "
let i be Integer; ::_thesis: pow ((x "),i) = (pow (x,i)) "
percases ( i >= 0 or i < 0 ) ;
suppose i >= 0 ; ::_thesis: pow ((x "),i) = (pow (x,i)) "
then reconsider n = i as Element of NAT by INT_1:3;
thus pow ((x "),i) = (pow (x,n)) " by A1, Lm9
.= (pow (x,i)) " ; ::_thesis: verum
end;
supposeA2: i < 0 ; ::_thesis: pow ((x "),i) = (pow (x,i)) "
A3: pow (x,(abs i)) = x |^ (abs i) by Def3;
thus pow ((x "),i) = (pow ((x "),(abs i))) " by A2, Lm3
.= pow (((x ") "),(abs i)) by A1, Lm9, VECTSP_1:25
.= pow (x,(abs i)) by A1, VECTSP_1:24
.= ((pow (x,(abs i))) ") " by A1, A3, Th1, VECTSP_1:24
.= (pow (x,i)) " by A2, Lm3 ; ::_thesis: verum
end;
end;
end;
theorem Th26: :: POLYNOM8:26
for L being Field
for x being Element of L st x <> 0. L holds
for i, j being Integer holds pow (x,(i * j)) = pow ((pow (x,i)),j)
proof
let L be Field; ::_thesis: for x being Element of L st x <> 0. L holds
for i, j being Integer holds pow (x,(i * j)) = pow ((pow (x,i)),j)
let x be Element of L; ::_thesis: ( x <> 0. L implies for i, j being Integer holds pow (x,(i * j)) = pow ((pow (x,i)),j) )
assume A1: x <> 0. L ; ::_thesis: for i, j being Integer holds pow (x,(i * j)) = pow ((pow (x,i)),j)
let i, j be Integer; ::_thesis: pow (x,(i * j)) = pow ((pow (x,i)),j)
percases ( ( i >= 0 & j >= 0 ) or ( i >= 0 & j < 0 ) or ( i < 0 & j >= 0 ) or ( j < 0 & i < 0 ) ) ;
suppose ( i >= 0 & j >= 0 ) ; ::_thesis: pow (x,(i * j)) = pow ((pow (x,i)),j)
then reconsider m = i, n = j as Element of NAT by INT_1:3;
thus pow (x,(i * j)) = pow ((pow (x,m)),n) by Th24
.= pow ((pow (x,i)),j) ; ::_thesis: verum
end;
supposeA2: ( i >= 0 & j < 0 ) ; ::_thesis: pow (x,(i * j)) = pow ((pow (x,i)),j)
then reconsider m = i, n = - j as Element of NAT by INT_1:3;
A3: pow (x,i) = x |^ m by Def3;
then A4: pow (x,i) <> 0. L by A1, Th1;
A5: pow ((pow (x,i)),j) = ((pow (x,i)) |^ (abs j)) " by A2, Def3;
i * j = - (i * n) ;
hence pow (x,(i * j)) = (pow (x,(i * n))) " by A1, Th18
.= pow ((x "),(i * n)) by A1, Th25
.= pow ((pow ((x "),m)),n) by Th24
.= pow (((pow (x,i)) "),n) by A1, Th25
.= (pow (((pow (x,i)) "),j)) " by A4, Th18, VECTSP_1:25
.= ((pow ((pow (x,i)),j)) ") " by A1, A3, Th1, Th25
.= pow ((pow (x,i)),j) by A4, A5, Th1, VECTSP_1:24 ;
::_thesis: verum
end;
supposeA6: ( i < 0 & j >= 0 ) ; ::_thesis: pow (x,(i * j)) = pow ((pow (x,i)),j)
then reconsider m = - i, n = j as Element of NAT by INT_1:3;
A7: pow (x,i) = (x |^ (abs i)) " by A6, Def3;
i * j = - (m * j) ;
hence pow (x,(i * j)) = (pow (x,(m * j))) " by A1, Th18
.= pow ((x "),(m * j)) by A1, Th25
.= pow ((pow ((x "),m)),n) by Th24
.= pow (((pow ((x "),i)) "),n) by A1, Th18, VECTSP_1:25
.= pow ((((pow (x,i)) ") "),j) by A1, Th25
.= pow ((pow (x,i)),j) by A1, A7, Th1, VECTSP_1:24 ;
::_thesis: verum
end;
supposeA8: ( j < 0 & i < 0 ) ; ::_thesis: pow (x,(i * j)) = pow ((pow (x,i)),j)
then reconsider m = - i, n = - j as Element of NAT by INT_1:3;
A9: pow (x,(- i)) = x |^ m by Def3;
x " <> 0. L by A1, VECTSP_1:25;
then A10: (x ") |^ (abs i) <> 0. L by Th1;
A11: pow ((x "),i) = ((x ") |^ (abs i)) " by A8, Def3;
(i * j) * ((- 1) * (- 1)) = m * n ;
hence pow (x,(i * j)) = pow ((pow (x,m)),n) by Th24
.= (pow ((pow (x,(- i))),j)) " by A1, A9, Th1, Th18
.= (pow (((pow (x,i)) "),j)) " by A1, Th18
.= (pow ((pow ((x "),i)),j)) " by A1, Th25
.= pow (((pow ((x "),i)) "),j) by A11, A10, Th25, VECTSP_1:25
.= pow ((pow (((x ") "),i)),j) by A1, Th25, VECTSP_1:25
.= pow ((pow (x,i)),j) by A1, VECTSP_1:24 ;
::_thesis: verum
end;
end;
end;
theorem Th27: :: POLYNOM8:27
for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for x being Element of L
for i, k being Element of NAT st 1 <= k holds
pow (x,(i * (k - 1))) = pow ((x |^ i),(k - 1))
proof
let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for x being Element of L
for i, k being Element of NAT st 1 <= k holds
pow (x,(i * (k - 1))) = pow ((x |^ i),(k - 1))
let x be Element of L; ::_thesis: for i, k being Element of NAT st 1 <= k holds
pow (x,(i * (k - 1))) = pow ((x |^ i),(k - 1))
let i, k be Element of NAT ; ::_thesis: ( 1 <= k implies pow (x,(i * (k - 1))) = pow ((x |^ i),(k - 1)) )
assume 1 <= k ; ::_thesis: pow (x,(i * (k - 1))) = pow ((x |^ i),(k - 1))
then 0 < k ;
then reconsider m = k - 1 as Element of NAT by NAT_1:20;
pow (x,(i * (k - 1))) = x |^ (i * m) by Def3
.= (x |^ i) |^ m by BINOM:11
.= pow ((x |^ i),m) by Def3 ;
hence pow (x,(i * (k - 1))) = pow ((x |^ i),(k - 1)) ; ::_thesis: verum
end;
Lm10: for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for x being Element of L
for m being Element of NAT st x <> 0. L & x |^ m = 1. L holds
(x ") |^ m = 1. L
proof
let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for x being Element of L
for m being Element of NAT st x <> 0. L & x |^ m = 1. L holds
(x ") |^ m = 1. L
let x be Element of L; ::_thesis: for m being Element of NAT st x <> 0. L & x |^ m = 1. L holds
(x ") |^ m = 1. L
let m be Element of NAT ; ::_thesis: ( x <> 0. L & x |^ m = 1. L implies (x ") |^ m = 1. L )
assume ( x <> 0. L & x |^ m = 1. L ) ; ::_thesis: (x ") |^ m = 1. L
then (1. L) * ((x ") |^ m) = 1. L by Lm7;
hence (x ") |^ m = 1. L by VECTSP_1:def_4; ::_thesis: verum
end;
Lm11: for L being non empty non degenerated almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for x being Element of L
for i being Element of NAT st x <> 0. L & (x ") |^ i = 1. L holds
x |^ i = 1. L
proof
let L be non empty non degenerated almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for x being Element of L
for i being Element of NAT st x <> 0. L & (x ") |^ i = 1. L holds
x |^ i = 1. L
let x be Element of L; ::_thesis: for i being Element of NAT st x <> 0. L & (x ") |^ i = 1. L holds
x |^ i = 1. L
let i be Element of NAT ; ::_thesis: ( x <> 0. L & (x ") |^ i = 1. L implies x |^ i = 1. L )
assume that
A1: x <> 0. L and
A2: (x ") |^ i = 1. L ; ::_thesis: x |^ i = 1. L
A3: 1_ L = x |^ 0 by BINOM:8;
((x ") |^ i) * (1. L) = 1. L by A2, VECTSP_1:def_4;
then ((x ") |^ i) * (x |^ 0) = ((x ") |^ i) * (x |^ i) by A1, A3, Lm7;
hence x |^ i = 1. L by A1, A2, A3, VECTSP_1:5; ::_thesis: verum
end;
begin
definition
let m be Nat;
let L be non empty ZeroStr ;
let p be AlgSequence of L;
func mConv (p,m) -> Matrix of m,1,L means :Def4: :: POLYNOM8:def 4
for i being Nat st 1 <= i & i <= m holds
it * (i,1) = p . (i - 1);
existence
ex b1 being Matrix of m,1,L st
for i being Nat st 1 <= i & i <= m holds
b1 * (i,1) = p . (i - 1)
proof
defpred S1[ Nat, set , set ] means $3 = p . ($1 - 1);
reconsider m9 = m as Element of NAT by ORDINAL1:def_12;
A1: for i, j being Nat st [i,j] in [:(Seg m9),(Seg 1):] holds
ex x being Element of L st S1[i,j,x]
proof
let i, j be Nat; ::_thesis: ( [i,j] in [:(Seg m9),(Seg 1):] implies ex x being Element of L st S1[i,j,x] )
assume A2: [i,j] in [:(Seg m9),(Seg 1):] ; ::_thesis: ex x being Element of L st S1[i,j,x]
take p /. (i - 1) ; ::_thesis: S1[i,j,p /. (i - 1)]
[i,j] `1 in Seg m by A2, MCART_1:10;
then i in Seg m ;
then 1 <= i by FINSEQ_1:1;
then ( dom p = NAT & 1 - 1 <= i - 1 ) by FUNCT_2:def_1, XREAL_1:9;
hence S1[i,j,p /. (i - 1)] by INT_1:3, PARTFUN1:def_6; ::_thesis: verum
end;
consider M being Matrix of m9,1,L such that
A3: for i, j being Nat st [i,j] in Indices M holds
S1[i,j,M * (i,j)] from MATRIX_1:sch_2(A1);
reconsider M = M as Matrix of m,1,L ;
take M ; ::_thesis: for i being Nat st 1 <= i & i <= m holds
M * (i,1) = p . (i - 1)
now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_m_holds_
M_*_(i,1)_=_p_._(i_-_1)
let i be Nat; ::_thesis: ( 1 <= i & i <= m implies M * (i,1) = p . (i - 1) )
assume ( 1 <= i & i <= m ) ; ::_thesis: M * (i,1) = p . (i - 1)
then A4: ( i in Seg m & Indices M = [:(Seg m),(Seg 1):] ) by FINSEQ_1:1, MATRIX_1:23;
1 in Seg 1 ;
then [i,1] in Indices M by A4, ZFMISC_1:def_2;
hence M * (i,1) = p . (i - 1) by A3; ::_thesis: verum
end;
hence for i being Nat st 1 <= i & i <= m holds
M * (i,1) = p . (i - 1) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Matrix of m,1,L st ( for i being Nat st 1 <= i & i <= m holds
b1 * (i,1) = p . (i - 1) ) & ( for i being Nat st 1 <= i & i <= m holds
b2 * (i,1) = p . (i - 1) ) holds
b1 = b2
proof
let M1, M2 be Matrix of m,1,L; ::_thesis: ( ( for i being Nat st 1 <= i & i <= m holds
M1 * (i,1) = p . (i - 1) ) & ( for i being Nat st 1 <= i & i <= m holds
M2 * (i,1) = p . (i - 1) ) implies M1 = M2 )
assume that
A5: for i being Nat st 1 <= i & i <= m holds
M1 * (i,1) = p . (i - 1) and
A6: for i being Nat st 1 <= i & i <= m holds
M2 * (i,1) = p . (i - 1) ; ::_thesis: M1 = M2
percases ( m = 0 or m > 0 ) ;
supposeA7: m = 0 ; ::_thesis: M1 = M2
then A8: for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j) by MATRIX_1:22;
A9: width M1 = 0 by A7, MATRIX_1:22
.= width M2 by A7, MATRIX_1:22 ;
len M1 = 0 by A7, MATRIX_1:22
.= len M2 by A7, MATRIX_1:22 ;
hence M1 = M2 by A9, A8, MATRIX_1:21; ::_thesis: verum
end;
supposeA10: m > 0 ; ::_thesis: M1 = M2
A11: now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_M1_holds_
M1_*_(i,j)_=_M2_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )
assume [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = M2 * (i,j)
then A12: [i,j] in [:(Seg m),(Seg 1):] by A10, MATRIX_1:23;
then [i,j] `2 in Seg 1 by MCART_1:10;
then j in Seg 1 ;
then ( 1 <= j & j <= 1 ) by FINSEQ_1:1;
then A13: j = 1 by XXREAL_0:1;
[i,j] `1 in Seg m by A12, MCART_1:10;
then i in Seg m ;
then A14: ( 1 <= i & i <= m ) by FINSEQ_1:1;
hence M1 * (i,j) = p . (i - 1) by A5, A13
.= M2 * (i,j) by A6, A14, A13 ;
::_thesis: verum
end;
A15: width M1 = 1 by A10, MATRIX_1:23
.= width M2 by A10, MATRIX_1:23 ;
len M1 = m by A10, MATRIX_1:23
.= len M2 by A10, MATRIX_1:23 ;
hence M1 = M2 by A15, A11, MATRIX_1:21; ::_thesis: verum
end;
end;
end;
end;
:: deftheorem Def4 defines mConv POLYNOM8:def_4_:_
for m being Nat
for L being non empty ZeroStr
for p being AlgSequence of L
for b4 being Matrix of m,1,L holds
( b4 = mConv (p,m) iff for i being Nat st 1 <= i & i <= m holds
b4 * (i,1) = p . (i - 1) );
theorem Th28: :: POLYNOM8:28
for m being Nat st m > 0 holds
for L being non empty ZeroStr
for p being AlgSequence of L holds
( len (mConv (p,m)) = m & width (mConv (p,m)) = 1 & ( for i being Nat st i < m holds
(mConv (p,m)) * ((i + 1),1) = p . i ) )
proof
let m be Nat; ::_thesis: ( m > 0 implies for L being non empty ZeroStr
for p being AlgSequence of L holds
( len (mConv (p,m)) = m & width (mConv (p,m)) = 1 & ( for i being Nat st i < m holds
(mConv (p,m)) * ((i + 1),1) = p . i ) ) )
assume A1: m > 0 ; ::_thesis: for L being non empty ZeroStr
for p being AlgSequence of L holds
( len (mConv (p,m)) = m & width (mConv (p,m)) = 1 & ( for i being Nat st i < m holds
(mConv (p,m)) * ((i + 1),1) = p . i ) )
let L be non empty ZeroStr ; ::_thesis: for p being AlgSequence of L holds
( len (mConv (p,m)) = m & width (mConv (p,m)) = 1 & ( for i being Nat st i < m holds
(mConv (p,m)) * ((i + 1),1) = p . i ) )
let p be AlgSequence of L; ::_thesis: ( len (mConv (p,m)) = m & width (mConv (p,m)) = 1 & ( for i being Nat st i < m holds
(mConv (p,m)) * ((i + 1),1) = p . i ) )
set q = mConv (p,m);
thus len (mConv (p,m)) = m by A1, MATRIX_1:23; ::_thesis: ( width (mConv (p,m)) = 1 & ( for i being Nat st i < m holds
(mConv (p,m)) * ((i + 1),1) = p . i ) )
thus width (mConv (p,m)) = 1 by A1, MATRIX_1:23; ::_thesis: for i being Nat st i < m holds
(mConv (p,m)) * ((i + 1),1) = p . i
now__::_thesis:_for_i_being_Nat_st_i_<_m_holds_
(mConv_(p,m))_*_((i_+_1),1)_=_p_._i
let i be Nat; ::_thesis: ( i < m implies (mConv (p,m)) * ((i + 1),1) = p . i )
assume i < m ; ::_thesis: (mConv (p,m)) * ((i + 1),1) = p . i
then ( 0 + 1 <= i + 1 & i + 1 <= m ) by NAT_1:13;
then (mConv (p,m)) * ((i + 1),1) = p . ((i + 1) - 1) by Def4;
hence (mConv (p,m)) * ((i + 1),1) = p . i ; ::_thesis: verum
end;
hence for i being Nat st i < m holds
(mConv (p,m)) * ((i + 1),1) = p . i ; ::_thesis: verum
end;
theorem Th29: :: POLYNOM8:29
for m being Nat st m > 0 holds
for L being non empty ZeroStr
for a being AlgSequence of L
for M being Matrix of m,1,L st ( for i being Nat st i < m holds
M * ((i + 1),1) = a . i ) holds
mConv (a,m) = M
proof
let m be Nat; ::_thesis: ( m > 0 implies for L being non empty ZeroStr
for a being AlgSequence of L
for M being Matrix of m,1,L st ( for i being Nat st i < m holds
M * ((i + 1),1) = a . i ) holds
mConv (a,m) = M )
assume A1: m > 0 ; ::_thesis: for L being non empty ZeroStr
for a being AlgSequence of L
for M being Matrix of m,1,L st ( for i being Nat st i < m holds
M * ((i + 1),1) = a . i ) holds
mConv (a,m) = M
let L be non empty ZeroStr ; ::_thesis: for a being AlgSequence of L
for M being Matrix of m,1,L st ( for i being Nat st i < m holds
M * ((i + 1),1) = a . i ) holds
mConv (a,m) = M
let a be AlgSequence of L; ::_thesis: for M being Matrix of m,1,L st ( for i being Nat st i < m holds
M * ((i + 1),1) = a . i ) holds
mConv (a,m) = M
let M be Matrix of m,1,L; ::_thesis: ( ( for i being Nat st i < m holds
M * ((i + 1),1) = a . i ) implies mConv (a,m) = M )
A2: width (mConv (a,m)) = 1 by A1, Th28
.= width M by A1, MATRIX_1:23 ;
assume A3: for i being Nat st i < m holds
M * ((i + 1),1) = a . i ; ::_thesis: mConv (a,m) = M
A4: for i, j being Nat st [i,j] in Indices (mConv (a,m)) holds
(mConv (a,m)) * (i,j) = M * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (mConv (a,m)) implies (mConv (a,m)) * (i,j) = M * (i,j) )
assume A5: [i,j] in Indices (mConv (a,m)) ; ::_thesis: (mConv (a,m)) * (i,j) = M * (i,j)
then A6: i in dom (mConv (a,m)) by ZFMISC_1:87;
len (mConv (a,m)) = m by A1, Th28;
then A7: i in Seg m by A6, FINSEQ_1:def_3;
then 0 < i by FINSEQ_1:1;
then reconsider k = i - 1 as Nat by NAT_1:20;
A8: j in Seg (width (mConv (a,m))) by A5, ZFMISC_1:87;
then A9: 1 <= j by FINSEQ_1:1;
j in Seg 1 by A1, A8, Th28;
then A10: j <= 1 by FINSEQ_1:1;
k + 1 <= m by A7, FINSEQ_1:1;
then A11: k < m by NAT_1:13;
then M * ((k + 1),1) = a . k by A3
.= (mConv (a,m)) * ((k + 1),1) by A11, Th28
.= (mConv (a,m)) * (i,j) by A9, A10, XXREAL_0:1 ;
hence (mConv (a,m)) * (i,j) = M * (i,j) by A9, A10, XXREAL_0:1; ::_thesis: verum
end;
len (mConv (a,m)) = m by A1, Th28
.= len M by A1, MATRIX_1:23 ;
hence mConv (a,m) = M by A2, A4, MATRIX_1:21; ::_thesis: verum
end;
definition
let L be non empty ZeroStr ;
let M be Matrix of L;
func aConv M -> AlgSequence of L means :Def5: :: POLYNOM8:def 5
( ( for i being Nat st i < len M holds
it . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds
it . i = 0. L ) );
existence
ex b1 being AlgSequence of L st
( ( for i being Nat st i < len M holds
b1 . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds
b1 . i = 0. L ) )
proof
defpred S1[ set , set ] means ex k being Element of NAT st
( k = $1 & ( ( k < len M & $2 = M * ((k + 1),1) ) or ( len M <= k & $2 = 0. L ) ) );
A1: for x being set st x in NAT holds
ex y being set st
( y in the carrier of L & S1[x,y] )
proof
let u be set ; ::_thesis: ( u in NAT implies ex y being set st
( y in the carrier of L & S1[u,y] ) )
assume u in NAT ; ::_thesis: ex y being set st
( y in the carrier of L & S1[u,y] )
then reconsider u9 = u as Element of NAT ;
thus ex y being set st
( y in the carrier of L & S1[u,y] ) ::_thesis: verum
proof
percases ( u9 < len M or u9 >= len M ) ;
supposeA2: u9 < len M ; ::_thesis: ex y being set st
( y in the carrier of L & S1[u,y] )
take M * ((u9 + 1),1) ; ::_thesis: ( M * ((u9 + 1),1) in the carrier of L & S1[u,M * ((u9 + 1),1)] )
thus ( M * ((u9 + 1),1) in the carrier of L & S1[u,M * ((u9 + 1),1)] ) by A2; ::_thesis: verum
end;
supposeA3: u9 >= len M ; ::_thesis: ex y being set st
( y in the carrier of L & S1[u,y] )
take 0. L ; ::_thesis: ( 0. L in the carrier of L & S1[u, 0. L] )
thus ( 0. L in the carrier of L & S1[u, 0. L] ) by A3; ::_thesis: verum
end;
end;
end;
end;
consider f being Function of NAT, the carrier of L such that
A4: for x being set st x in NAT holds
S1[x,f . x] from FUNCT_2:sch_1(A1);
reconsider f = f as sequence of L ;
ex n being Nat st
for i being Nat st i >= n holds
f . i = 0. L
proof
take len M ; ::_thesis: for i being Nat st i >= len M holds
f . i = 0. L
now__::_thesis:_for_i_being_Nat_st_i_>=_len_M_holds_
f_._i_=_0._L
let i be Nat; ::_thesis: ( i >= len M implies f . i = 0. L )
i in NAT by ORDINAL1:def_12;
then A5: ex k being Element of NAT st
( k = i & ( ( k < len M & f . i = M * ((k + 1),1) ) or ( len M <= k & f . i = 0. L ) ) ) by A4;
assume i >= len M ; ::_thesis: f . i = 0. L
hence f . i = 0. L by A5; ::_thesis: verum
end;
hence for i being Nat st i >= len M holds
f . i = 0. L ; ::_thesis: verum
end;
then reconsider q = f as AlgSequence of L by ALGSEQ_1:def_1;
A6: now__::_thesis:_for_i_being_Nat_st_i_>=_len_M_holds_
q_._i_=_0._L
let i be Nat; ::_thesis: ( i >= len M implies q . i = 0. L )
i in NAT by ORDINAL1:def_12;
then A7: ex k being Element of NAT st
( k = i & ( ( k < len M & q . i = M * ((k + 1),1) ) or ( len M <= k & q . i = 0. L ) ) ) by A4;
assume i >= len M ; ::_thesis: q . i = 0. L
hence q . i = 0. L by A7; ::_thesis: verum
end;
take q ; ::_thesis: ( ( for i being Nat st i < len M holds
q . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds
q . i = 0. L ) )
now__::_thesis:_for_i_being_Nat_st_i_<_len_M_holds_
q_._i_=_M_*_((i_+_1),1)
let i be Nat; ::_thesis: ( i < len M implies q . i = M * ((i + 1),1) )
i in NAT by ORDINAL1:def_12;
then A8: ex k being Element of NAT st
( k = i & ( ( k < len M & q . i = M * ((k + 1),1) ) or ( len M <= k & q . i = 0. L ) ) ) by A4;
assume i < len M ; ::_thesis: q . i = M * ((i + 1),1)
hence q . i = M * ((i + 1),1) by A8; ::_thesis: verum
end;
hence ( ( for i being Nat st i < len M holds
q . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds
q . i = 0. L ) ) by A6; ::_thesis: verum
end;
uniqueness
for b1, b2 being AlgSequence of L st ( for i being Nat st i < len M holds
b1 . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds
b1 . i = 0. L ) & ( for i being Nat st i < len M holds
b2 . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds
b2 . i = 0. L ) holds
b1 = b2
proof
let z1, z2 be AlgSequence of L; ::_thesis: ( ( for i being Nat st i < len M holds
z1 . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds
z1 . i = 0. L ) & ( for i being Nat st i < len M holds
z2 . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds
z2 . i = 0. L ) implies z1 = z2 )
assume that
A9: for i being Nat st i < len M holds
z1 . i = M * ((i + 1),1) and
A10: for i being Nat st i >= len M holds
z1 . i = 0. L ; ::_thesis: ( ex i being Nat st
( i < len M & not z2 . i = M * ((i + 1),1) ) or ex i being Nat st
( i >= len M & not z2 . i = 0. L ) or z1 = z2 )
assume that
A11: for i being Nat st i < len M holds
z2 . i = M * ((i + 1),1) and
A12: for i being Nat st i >= len M holds
z2 . i = 0. L ; ::_thesis: z1 = z2
A13: now__::_thesis:_for_u_being_set_st_u_in_dom_z1_holds_
z1_._u_=_z2_._u
let u be set ; ::_thesis: ( u in dom z1 implies z1 . b1 = z2 . b1 )
assume u in dom z1 ; ::_thesis: z1 . b1 = z2 . b1
then reconsider u9 = u as Element of NAT by FUNCT_2:def_1;
percases ( u9 < len M or len M <= u9 ) ;
supposeA14: u9 < len M ; ::_thesis: z1 . b1 = z2 . b1
hence z1 . u = M * ((u9 + 1),1) by A9
.= z2 . u by A11, A14 ;
::_thesis: verum
end;
supposeA15: len M <= u9 ; ::_thesis: z1 . b1 = z2 . b1
hence z1 . u = 0. L by A10
.= z2 . u by A12, A15 ;
::_thesis: verum
end;
end;
end;
dom z1 = NAT by FUNCT_2:def_1
.= dom z2 by FUNCT_2:def_1 ;
hence z1 = z2 by A13, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines aConv POLYNOM8:def_5_:_
for L being non empty ZeroStr
for M being Matrix of L
for b3 being AlgSequence of L holds
( b3 = aConv M iff ( ( for i being Nat st i < len M holds
b3 . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds
b3 . i = 0. L ) ) );
begin
definition
let L be non empty well-unital doubleLoopStr ;
let x be Element of L;
let n be Element of NAT ;
predx is_primitive_root_of_degree n means :Def6: :: POLYNOM8:def 6
( n <> 0 & x |^ n = 1. L & ( for i being Element of NAT st 0 < i & i < n holds
x |^ i <> 1. L ) );
end;
:: deftheorem Def6 defines is_primitive_root_of_degree POLYNOM8:def_6_:_
for L being non empty well-unital doubleLoopStr
for x being Element of L
for n being Element of NAT holds
( x is_primitive_root_of_degree n iff ( n <> 0 & x |^ n = 1. L & ( for i being Element of NAT st 0 < i & i < n holds
x |^ i <> 1. L ) ) );
theorem Th30: :: POLYNOM8:30
for L being non empty non degenerated right_complementable right-distributive well-unital add-associative right_zeroed doubleLoopStr
for n being Element of NAT holds not 0. L is_primitive_root_of_degree n
proof
let L be non empty non degenerated right_complementable right-distributive well-unital add-associative right_zeroed doubleLoopStr ; ::_thesis: for n being Element of NAT holds not 0. L is_primitive_root_of_degree n
let n be Element of NAT ; ::_thesis: not 0. L is_primitive_root_of_degree n
defpred S1[ Nat] means (0. L) |^ $1 = 0. L;
A1: for j being Nat st 1 <= j & S1[j] holds
S1[j + 1]
proof
let j be Nat; ::_thesis: ( 1 <= j & S1[j] implies S1[j + 1] )
assume 1 <= j ; ::_thesis: ( not S1[j] or S1[j + 1] )
assume S1[j] ; ::_thesis: S1[j + 1]
j in NAT by ORDINAL1:def_12;
then (0. L) |^ (j + 1) = ((0. L) |^ j) * (0. L) by GROUP_1:def_7
.= 0. L by VECTSP_1:6 ;
hence S1[j + 1] ; ::_thesis: verum
end;
A2: S1[1] by BINOM:8;
A3: for m being Nat st 1 <= m holds
S1[m] from NAT_1:sch_8(A2, A1);
assume A4: 0. L is_primitive_root_of_degree n ; ::_thesis: contradiction
then n <> 0 by Def6;
then 0 + 1 < n + 1 by XREAL_1:8;
then 1 <= n by NAT_1:13;
then (0. L) |^ n <> 1. L by A3;
hence contradiction by A4, Def6; ::_thesis: verum
end;
theorem Th31: :: POLYNOM8:31
for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for m being Element of NAT
for x being Element of L st x is_primitive_root_of_degree m holds
x " is_primitive_root_of_degree m
proof
let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for m being Element of NAT
for x being Element of L st x is_primitive_root_of_degree m holds
x " is_primitive_root_of_degree m
let m be Element of NAT ; ::_thesis: for x being Element of L st x is_primitive_root_of_degree m holds
x " is_primitive_root_of_degree m
let x be Element of L; ::_thesis: ( x is_primitive_root_of_degree m implies x " is_primitive_root_of_degree m )
assume A1: x is_primitive_root_of_degree m ; ::_thesis: x " is_primitive_root_of_degree m
then A2: x <> 0. L by Th30;
A3: for i being Element of NAT st 0 < i & i < m holds
(x ") |^ i <> 1. L
proof
let i be Element of NAT ; ::_thesis: ( 0 < i & i < m implies (x ") |^ i <> 1. L )
assume ( 0 < i & i < m ) ; ::_thesis: (x ") |^ i <> 1. L
then x |^ i <> 1. L by A1, Def6;
hence (x ") |^ i <> 1. L by A2, Lm11; ::_thesis: verum
end;
x |^ m = 1. L by A1, Def6;
then A4: (x ") |^ m = 1. L by A2, Lm10;
m <> 0 by A1, Def6;
hence x " is_primitive_root_of_degree m by A4, A3, Def6; ::_thesis: verum
end;
theorem Th32: :: POLYNOM8:32
for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for m being Element of NAT
for x being Element of L st x is_primitive_root_of_degree m holds
for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m & i <> j holds
pow (x,(i - j)) <> 1. L
proof
let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for m being Element of NAT
for x being Element of L st x is_primitive_root_of_degree m holds
for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m & i <> j holds
pow (x,(i - j)) <> 1. L
let m be Element of NAT ; ::_thesis: for x being Element of L st x is_primitive_root_of_degree m holds
for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m & i <> j holds
pow (x,(i - j)) <> 1. L
let x be Element of L; ::_thesis: ( x is_primitive_root_of_degree m implies for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m & i <> j holds
pow (x,(i - j)) <> 1. L )
assume A1: x is_primitive_root_of_degree m ; ::_thesis: for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m & i <> j holds
pow (x,(i - j)) <> 1. L
then A2: x <> 0. L by Th30;
let i, j be Nat; ::_thesis: ( 1 <= i & i <= m & 1 <= j & j <= m & i <> j implies pow (x,(i - j)) <> 1. L )
assume that
A3: 1 <= i and
A4: i <= m and
A5: 1 <= j and
A6: j <= m and
A7: i <> j ; ::_thesis: pow (x,(i - j)) <> 1. L
percases ( i > j or i <= j ) ;
supposeA8: i > j ; ::_thesis: pow (x,(i - j)) <> 1. L
then reconsider k = i - j as Element of NAT by INT_1:5;
k <= i - 1 by A5, XREAL_1:13;
then k + 1 <= (i - 1) + 1 by XREAL_1:6;
then k < i by NAT_1:13;
then A9: k < m by A4, XXREAL_0:2;
i - j > j - j by A8, XREAL_1:14;
then x |^ k <> 1. L by A1, A9, Def6;
hence pow (x,(i - j)) <> 1. L by Def3; ::_thesis: verum
end;
suppose i <= j ; ::_thesis: pow (x,(i - j)) <> 1. L
then A10: i < j by A7, XXREAL_0:1;
then A11: j - i > i - i by XREAL_1:14;
A12: i - j < j - j by A10, XREAL_1:14;
then A13: abs (i - j) = - (i - j) by ABSVALUE:def_1;
then reconsider k = - (i - j) as Element of NAT ;
j - i <= j - 1 by A3, XREAL_1:13;
then k + 1 <= (j - 1) + 1 by XREAL_1:6;
then k < j by NAT_1:13;
then A14: k < m by A6, XXREAL_0:2;
A15: x |^ k <> 0. L by A2, Th1;
now__::_thesis:_not_(x_|^_k)_"_=_1._L
assume (x |^ k) " = 1. L ; ::_thesis: contradiction
then 1. L = (x |^ k) * (1. L) by A15, VECTSP_1:def_10
.= x |^ k by VECTSP_1:def_4 ;
hence contradiction by A1, A11, A14, Def6; ::_thesis: verum
end;
hence pow (x,(i - j)) <> 1. L by A12, A13, Def3; ::_thesis: verum
end;
end;
end;
definition
let m be Nat;
let L be non empty well-unital doubleLoopStr ;
let p be Polynomial of L;
let x be Element of L;
func DFT (p,x,m) -> AlgSequence of L means :Def7: :: POLYNOM8:def 7
( ( for i being Nat st i < m holds
it . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds
it . i = 0. L ) );
existence
ex b1 being AlgSequence of L st
( ( for i being Nat st i < m holds
b1 . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds
b1 . i = 0. L ) )
proof
defpred S1[ set , set ] means ex k being Element of NAT st
( k = $1 & ( ( k < m & $2 = eval (p,(x |^ k)) ) or ( m <= k & $2 = 0. L ) ) );
A1: for x being set st x in NAT holds
ex y being set st
( y in the carrier of L & S1[x,y] )
proof
let u be set ; ::_thesis: ( u in NAT implies ex y being set st
( y in the carrier of L & S1[u,y] ) )
assume u in NAT ; ::_thesis: ex y being set st
( y in the carrier of L & S1[u,y] )
then reconsider u9 = u as Element of NAT ;
thus ex y being set st
( y in the carrier of L & S1[u,y] ) ::_thesis: verum
proof
percases ( u9 < m or u9 >= m ) ;
supposeA2: u9 < m ; ::_thesis: ex y being set st
( y in the carrier of L & S1[u,y] )
take eval (p,(x |^ u9)) ; ::_thesis: ( eval (p,(x |^ u9)) in the carrier of L & S1[u, eval (p,(x |^ u9))] )
thus ( eval (p,(x |^ u9)) in the carrier of L & S1[u, eval (p,(x |^ u9))] ) by A2; ::_thesis: verum
end;
supposeA3: u9 >= m ; ::_thesis: ex y being set st
( y in the carrier of L & S1[u,y] )
take 0. L ; ::_thesis: ( 0. L in the carrier of L & S1[u, 0. L] )
thus ( 0. L in the carrier of L & S1[u, 0. L] ) by A3; ::_thesis: verum
end;
end;
end;
end;
consider f being Function of NAT, the carrier of L such that
A4: for x being set st x in NAT holds
S1[x,f . x] from FUNCT_2:sch_1(A1);
reconsider f = f as sequence of L ;
ex n being Nat st
for i being Nat st i >= n holds
f . i = 0. L
proof
reconsider m = m as Element of NAT by ORDINAL1:def_12;
take m ; ::_thesis: for i being Nat st i >= m holds
f . i = 0. L
now__::_thesis:_for_i_being_Nat_st_i_>=_m_holds_
f_._i_=_0._L
let i be Nat; ::_thesis: ( i >= m implies f . i = 0. L )
i in NAT by ORDINAL1:def_12;
then A5: ex k being Element of NAT st
( k = i & ( ( k < m & f . i = eval (p,(x |^ k)) ) or ( m <= k & f . i = 0. L ) ) ) by A4;
assume i >= m ; ::_thesis: f . i = 0. L
hence f . i = 0. L by A5; ::_thesis: verum
end;
hence for i being Nat st i >= m holds
f . i = 0. L ; ::_thesis: verum
end;
then reconsider q = f as AlgSequence of L by ALGSEQ_1:def_1;
A6: now__::_thesis:_for_i_being_Nat_st_i_>=_m_holds_
q_._i_=_0._L
let i be Nat; ::_thesis: ( i >= m implies q . i = 0. L )
i in NAT by ORDINAL1:def_12;
then A7: ex k being Element of NAT st
( k = i & ( ( k < m & q . i = eval (p,(x |^ k)) ) or ( m <= k & q . i = 0. L ) ) ) by A4;
assume i >= m ; ::_thesis: q . i = 0. L
hence q . i = 0. L by A7; ::_thesis: verum
end;
take q ; ::_thesis: ( ( for i being Nat st i < m holds
q . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds
q . i = 0. L ) )
now__::_thesis:_for_i_being_Nat_st_i_<_m_holds_
q_._i_=_eval_(p,(x_|^_i))
let i be Nat; ::_thesis: ( i < m implies q . i = eval (p,(x |^ i)) )
i in NAT by ORDINAL1:def_12;
then A8: ex k being Element of NAT st
( k = i & ( ( k < m & q . i = eval (p,(x |^ k)) ) or ( m <= k & q . i = 0. L ) ) ) by A4;
assume i < m ; ::_thesis: q . i = eval (p,(x |^ i))
hence q . i = eval (p,(x |^ i)) by A8; ::_thesis: verum
end;
hence ( ( for i being Nat st i < m holds
q . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds
q . i = 0. L ) ) by A6; ::_thesis: verum
end;
uniqueness
for b1, b2 being AlgSequence of L st ( for i being Nat st i < m holds
b1 . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds
b1 . i = 0. L ) & ( for i being Nat st i < m holds
b2 . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds
b2 . i = 0. L ) holds
b1 = b2
proof
let z1, z2 be AlgSequence of L; ::_thesis: ( ( for i being Nat st i < m holds
z1 . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds
z1 . i = 0. L ) & ( for i being Nat st i < m holds
z2 . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds
z2 . i = 0. L ) implies z1 = z2 )
assume that
A9: for i being Nat st i < m holds
z1 . i = eval (p,(x |^ i)) and
A10: for i being Nat st i >= m holds
z1 . i = 0. L ; ::_thesis: ( ex i being Nat st
( i < m & not z2 . i = eval (p,(x |^ i)) ) or ex i being Nat st
( i >= m & not z2 . i = 0. L ) or z1 = z2 )
assume that
A11: for i being Nat st i < m holds
z2 . i = eval (p,(x |^ i)) and
A12: for i being Nat st i >= m holds
z2 . i = 0. L ; ::_thesis: z1 = z2
A13: now__::_thesis:_for_u_being_set_st_u_in_dom_z1_holds_
z1_._u_=_z2_._u
let u be set ; ::_thesis: ( u in dom z1 implies z1 . b1 = z2 . b1 )
assume u in dom z1 ; ::_thesis: z1 . b1 = z2 . b1
then reconsider u9 = u as Element of NAT by FUNCT_2:def_1;
percases ( u9 < m or m <= u9 ) ;
supposeA14: u9 < m ; ::_thesis: z1 . b1 = z2 . b1
hence z1 . u = eval (p,(x |^ u9)) by A9
.= z2 . u by A11, A14 ;
::_thesis: verum
end;
supposeA15: m <= u9 ; ::_thesis: z1 . b1 = z2 . b1
hence z1 . u = 0. L by A10
.= z2 . u by A12, A15 ;
::_thesis: verum
end;
end;
end;
dom z1 = NAT by FUNCT_2:def_1
.= dom z2 by FUNCT_2:def_1 ;
hence z1 = z2 by A13, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines DFT POLYNOM8:def_7_:_
for m being Nat
for L being non empty well-unital doubleLoopStr
for p being Polynomial of L
for x being Element of L
for b5 being AlgSequence of L holds
( b5 = DFT (p,x,m) iff ( ( for i being Nat st i < m holds
b5 . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds
b5 . i = 0. L ) ) );
theorem Th33: :: POLYNOM8:33
for m being Nat
for L being non empty well-unital doubleLoopStr
for x being Element of L holds DFT ((0_. L),x,m) = 0_. L
proof
let m be Nat; ::_thesis: for L being non empty well-unital doubleLoopStr
for x being Element of L holds DFT ((0_. L),x,m) = 0_. L
let L be non empty well-unital doubleLoopStr ; ::_thesis: for x being Element of L holds DFT ((0_. L),x,m) = 0_. L
let x be Element of L; ::_thesis: DFT ((0_. L),x,m) = 0_. L
set q = DFT ((0_. L),x,m);
A1: now__::_thesis:_for_u_being_set_st_u_in_dom_(DFT_((0_._L),x,m))_holds_
(DFT_((0_._L),x,m))_._u_=_(0_._L)_._u
let u be set ; ::_thesis: ( u in dom (DFT ((0_. L),x,m)) implies (DFT ((0_. L),x,m)) . b1 = (0_. L) . b1 )
assume u in dom (DFT ((0_. L),x,m)) ; ::_thesis: (DFT ((0_. L),x,m)) . b1 = (0_. L) . b1
then reconsider n = u as Element of NAT by FUNCT_2:def_1;
percases ( n < m or n >= m ) ;
suppose n < m ; ::_thesis: (DFT ((0_. L),x,m)) . b1 = (0_. L) . b1
hence (DFT ((0_. L),x,m)) . u = eval ((0_. L),(x |^ n)) by Def7
.= 0. L by POLYNOM4:17
.= (0_. L) . n by FUNCOP_1:7
.= (0_. L) . u ;
::_thesis: verum
end;
suppose n >= m ; ::_thesis: (DFT ((0_. L),x,m)) . b1 = (0_. L) . b1
hence (DFT ((0_. L),x,m)) . u = 0. L by Def7
.= (0_. L) . n by FUNCOP_1:7
.= (0_. L) . u ;
::_thesis: verum
end;
end;
end;
dom (DFT ((0_. L),x,m)) = NAT by FUNCT_2:def_1
.= dom (0_. L) by FUNCT_2:def_1 ;
hence DFT ((0_. L),x,m) = 0_. L by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem Th34: :: POLYNOM8:34
for m being Nat
for L being Field
for p, q being Polynomial of L
for x being Element of L holds (DFT (p,x,m)) * (DFT (q,x,m)) = DFT ((p *' q),x,m)
proof
let m be Nat; ::_thesis: for L being Field
for p, q being Polynomial of L
for x being Element of L holds (DFT (p,x,m)) * (DFT (q,x,m)) = DFT ((p *' q),x,m)
let L be Field; ::_thesis: for p, q being Polynomial of L
for x being Element of L holds (DFT (p,x,m)) * (DFT (q,x,m)) = DFT ((p *' q),x,m)
let p, q be Polynomial of L; ::_thesis: for x being Element of L holds (DFT (p,x,m)) * (DFT (q,x,m)) = DFT ((p *' q),x,m)
let x be Element of L; ::_thesis: (DFT (p,x,m)) * (DFT (q,x,m)) = DFT ((p *' q),x,m)
set ep = DFT (p,x,m);
set eq = DFT (q,x,m);
set epq = DFT ((p *' q),x,m);
A1: now__::_thesis:_for_u9_being_set_st_u9_in_dom_((DFT_(p,x,m))_*_(DFT_(q,x,m)))_holds_
(DFT_((p_*'_q),x,m))_._u9_=_((DFT_(p,x,m))_*_(DFT_(q,x,m)))_._u9
let u9 be set ; ::_thesis: ( u9 in dom ((DFT (p,x,m)) * (DFT (q,x,m))) implies (DFT ((p *' q),x,m)) . b1 = ((DFT (p,x,m)) * (DFT (q,x,m))) . b1 )
assume u9 in dom ((DFT (p,x,m)) * (DFT (q,x,m))) ; ::_thesis: (DFT ((p *' q),x,m)) . b1 = ((DFT (p,x,m)) * (DFT (q,x,m))) . b1
then reconsider u = u9 as Element of NAT by FUNCT_2:def_1;
percases ( u < m or m <= u ) ;
supposeA2: u < m ; ::_thesis: (DFT ((p *' q),x,m)) . b1 = ((DFT (p,x,m)) * (DFT (q,x,m))) . b1
hence (DFT ((p *' q),x,m)) . u9 = eval ((p *' q),(x |^ u)) by Def7
.= (eval (p,(x |^ u))) * (eval (q,(x |^ u))) by POLYNOM4:24
.= ((DFT (p,x,m)) . u) * (eval (q,(x |^ u))) by A2, Def7
.= ((DFT (p,x,m)) . u) * ((DFT (q,x,m)) . u) by A2, Def7
.= ((DFT (p,x,m)) * (DFT (q,x,m))) . u9 by Def2 ;
::_thesis: verum
end;
supposeA3: m <= u ; ::_thesis: ((DFT (p,x,m)) * (DFT (q,x,m))) . b1 = (DFT ((p *' q),x,m)) . b1
thus ((DFT (p,x,m)) * (DFT (q,x,m))) . u9 = ((DFT (p,x,m)) . u) * ((DFT (q,x,m)) . u) by Def2
.= (0. L) * ((DFT (q,x,m)) . u) by A3, Def7
.= 0. L by VECTSP_1:6
.= (DFT ((p *' q),x,m)) . u9 by A3, Def7 ; ::_thesis: verum
end;
end;
end;
dom ((DFT (p,x,m)) * (DFT (q,x,m))) = NAT by FUNCT_2:def_1
.= dom (DFT ((p *' q),x,m)) by FUNCT_2:def_1 ;
hence (DFT (p,x,m)) * (DFT (q,x,m)) = DFT ((p *' q),x,m) by A1, FUNCT_1:2; ::_thesis: verum
end;
definition
let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ;
let m be Nat;
let x be Element of L;
func Vandermonde (x,m) -> Matrix of m,L means :Def8: :: POLYNOM8:def 8
for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
it * (i,j) = pow (x,((i - 1) * (j - 1)));
existence
ex b1 being Matrix of m,L st
for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
b1 * (i,j) = pow (x,((i - 1) * (j - 1)))
proof
defpred S1[ Nat, Nat, set ] means $3 = pow (x,(($1 - 1) * ($2 - 1)));
reconsider m9 = m as Element of NAT by ORDINAL1:def_12;
A1: for i, j being Nat st [i,j] in [:(Seg m9),(Seg m9):] holds
ex x being Element of L st S1[i,j,x] ;
consider M being Matrix of m9,m9,L such that
A2: for i, j being Nat st [i,j] in Indices M holds
S1[i,j,M * (i,j)] from MATRIX_1:sch_2(A1);
reconsider M = M as Matrix of m,m,L ;
take M ; ::_thesis: for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
M * (i,j) = pow (x,((i - 1) * (j - 1)))
now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_m_holds_
for_j_being_Nat_st_1_<=_j_&_j_<=_m_holds_
M_*_(i,j)_=_pow_(x,((i_-_1)_*_(j_-_1)))
let i be Nat; ::_thesis: ( 1 <= i & i <= m implies for j being Nat st 1 <= j & j <= m holds
M * (i,j) = pow (x,((i - 1) * (j - 1))) )
assume ( 1 <= i & i <= m ) ; ::_thesis: for j being Nat st 1 <= j & j <= m holds
M * (i,j) = pow (x,((i - 1) * (j - 1)))
then A3: ( Indices M = [:(Seg m),(Seg m):] & i in Seg m ) by FINSEQ_1:1, MATRIX_1:24;
let j be Nat; ::_thesis: ( 1 <= j & j <= m implies M * (i,j) = pow (x,((i - 1) * (j - 1))) )
assume ( 1 <= j & j <= m ) ; ::_thesis: M * (i,j) = pow (x,((i - 1) * (j - 1)))
then j in Seg m by FINSEQ_1:1;
then [i,j] in Indices M by A3, ZFMISC_1:def_2;
hence M * (i,j) = pow (x,((i - 1) * (j - 1))) by A2; ::_thesis: verum
end;
hence for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
M * (i,j) = pow (x,((i - 1) * (j - 1))) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Matrix of m,L st ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
b1 * (i,j) = pow (x,((i - 1) * (j - 1))) ) & ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
b2 * (i,j) = pow (x,((i - 1) * (j - 1))) ) holds
b1 = b2
proof
let M1, M2 be Matrix of m,L; ::_thesis: ( ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
M1 * (i,j) = pow (x,((i - 1) * (j - 1))) ) & ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
M2 * (i,j) = pow (x,((i - 1) * (j - 1))) ) implies M1 = M2 )
assume A4: for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
M1 * (i,j) = pow (x,((i - 1) * (j - 1))) ; ::_thesis: ( ex i, j being Nat st
( 1 <= i & i <= m & 1 <= j & j <= m & not M2 * (i,j) = pow (x,((i - 1) * (j - 1))) ) or M1 = M2 )
assume A5: for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
M2 * (i,j) = pow (x,((i - 1) * (j - 1))) ; ::_thesis: M1 = M2
now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_M1_holds_
M1_*_(i,j)_=_M2_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )
A6: Indices M1 = [:(Seg m),(Seg m):] by MATRIX_1:24;
assume [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = M2 * (i,j)
then ex x, y being set st
( x in Seg m & y in Seg m & [x,y] = [i,j] ) by A6, ZFMISC_1:def_2;
then consider z, y being set such that
A7: [i,j] = [z,y] and
A8: z in Seg m and
A9: y in Seg m ;
j = y by A7, XTUPLE_0:1;
then A10: ( 1 <= j & j <= m ) by A9, FINSEQ_1:1;
i = z by A7, XTUPLE_0:1;
then A11: ( 1 <= i & i <= m ) by A8, FINSEQ_1:1;
hence M1 * (i,j) = pow (x,((i - 1) * (j - 1))) by A4, A10
.= M2 * (i,j) by A5, A11, A10 ;
::_thesis: verum
end;
hence M1 = M2 by MATRIX_1:27; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines Vandermonde POLYNOM8:def_8_:_
for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for m being Nat
for x being Element of L
for b4 being Matrix of m,L holds
( b4 = Vandermonde (x,m) iff for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
b4 * (i,j) = pow (x,((i - 1) * (j - 1))) );
notation
let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ;
let m be Nat;
let x be Element of L;
synonym VM (x,m) for Vandermonde (x,m);
end;
theorem Th35: :: POLYNOM8:35
for L being Field
for m, n being Nat st m > 0 holds
for M being Matrix of m,n,L holds (1. (L,m)) * M = M
proof
let L be Field; ::_thesis: for m, n being Nat st m > 0 holds
for M being Matrix of m,n,L holds (1. (L,m)) * M = M
let m, n be Nat; ::_thesis: ( m > 0 implies for M being Matrix of m,n,L holds (1. (L,m)) * M = M )
assume A1: m > 0 ; ::_thesis: for M being Matrix of m,n,L holds (1. (L,m)) * M = M
let M be Matrix of m,n,L; ::_thesis: (1. (L,m)) * M = M
A2: width (1. (L,m)) = m by A1, MATRIX_1:23
.= len M by A1, MATRIX_1:23 ;
set M2 = (1. (L,m)) * M;
A3: len M = m by A1, MATRIX_1:23;
len (1. (L,m)) = m by A1, MATRIX_1:23;
then A4: m = len ((1. (L,m)) * M) by A2, MATRIX_3:def_4;
A5: now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_M_holds_
M_*_(i,j)_=_((1._(L,m))_*_M)_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices M implies M * (i,j) = ((1. (L,m)) * M) * (i,j) )
assume A6: [i,j] in Indices M ; ::_thesis: M * (i,j) = ((1. (L,m)) * M) * (i,j)
then A7: i in dom M by ZFMISC_1:87;
dom M = Seg (len M) by FINSEQ_1:def_3
.= dom ((1. (L,m)) * M) by A3, A4, FINSEQ_1:def_3 ;
then Indices M = Indices ((1. (L,m)) * M) by A2, MATRIX_3:def_4;
then A8: ((1. (L,m)) * M) * (i,j) = (Line ((1. (L,m)),i)) "*" (Col (M,j)) by A2, A6, MATRIX_3:def_4
.= Sum (mlt ((Line ((1. (L,m)),i)),(Col (M,j)))) by FVSUM_1:def_9 ;
len (Line ((1. (L,m)),i)) = width (1. (L,m)) by MATRIX_1:def_7
.= m by MATRIX_1:24 ;
then A9: dom (Line ((1. (L,m)),i)) = Seg m by FINSEQ_1:def_3;
A10: len M = m by A1, MATRIX_1:23;
then A11: i in dom (Line ((1. (L,m)),i)) by A7, A9, FINSEQ_1:def_3;
A12: Indices (1. (L,m)) = [:(Seg m),(Seg m):] by A1, MATRIX_1:23;
then A13: [i,i] in Indices (1. (L,m)) by A9, A11, ZFMISC_1:87;
A14: for k being Nat st k in dom (Line ((1. (L,m)),i)) & k <> i holds
(Line ((1. (L,m)),i)) . k = 0. L
proof
let k be Nat; ::_thesis: ( k in dom (Line ((1. (L,m)),i)) & k <> i implies (Line ((1. (L,m)),i)) . k = 0. L )
assume that
A15: k in dom (Line ((1. (L,m)),i)) and
A16: k <> i ; ::_thesis: (Line ((1. (L,m)),i)) . k = 0. L
A17: [i,k] in Indices (1. (L,m)) by A9, A11, A12, A15, ZFMISC_1:87;
k in Seg (width (1. (L,m))) by A9, A15, MATRIX_1:24;
then (Line ((1. (L,m)),i)) . k = (1. (L,m)) * (i,k) by MATRIX_1:def_7
.= 0. L by A16, A17, MATRIX_1:def_11 ;
hence (Line ((1. (L,m)),i)) . k = 0. L ; ::_thesis: verum
end;
len (Col (M,j)) = len M by MATRIX_1:def_8
.= m by A1, MATRIX_1:23 ;
then dom (Col (M,j)) = Seg m by FINSEQ_1:def_3;
then A18: i in dom (Col (M,j)) by A7, A10, FINSEQ_1:def_3;
i in Seg (width (1. (L,m))) by A9, A11, MATRIX_1:24;
then A19: (Line ((1. (L,m)),i)) . i = (1. (L,m)) * (i,i) by MATRIX_1:def_7
.= 1. L by A13, MATRIX_1:def_11 ;
i in dom (Line ((1. (L,m)),i)) by A7, A10, A9, FINSEQ_1:def_3;
then Sum (mlt ((Line ((1. (L,m)),i)),(Col (M,j)))) = (Col (M,j)) . i by A19, A14, A18, MATRIX_3:17;
hence M * (i,j) = ((1. (L,m)) * M) * (i,j) by A8, A7, MATRIX_1:def_8; ::_thesis: verum
end;
width M = width ((1. (L,m)) * M) by A2, MATRIX_3:def_4;
hence (1. (L,m)) * M = M by A3, A4, A5, MATRIX_1:21; ::_thesis: verum
end;
theorem Th36: :: POLYNOM8:36
for L being Field
for m being Element of NAT st 0 < m holds
for u, v, u1 being Matrix of m,L st ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
(u * v) * (i,j) = (emb (m,L)) * (u1 * (i,j)) ) holds
u * v = (emb (m,L)) * u1
proof
let L be Field; ::_thesis: for m being Element of NAT st 0 < m holds
for u, v, u1 being Matrix of m,L st ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
(u * v) * (i,j) = (emb (m,L)) * (u1 * (i,j)) ) holds
u * v = (emb (m,L)) * u1
let m be Element of NAT ; ::_thesis: ( 0 < m implies for u, v, u1 being Matrix of m,L st ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
(u * v) * (i,j) = (emb (m,L)) * (u1 * (i,j)) ) holds
u * v = (emb (m,L)) * u1 )
assume A1: m > 0 ; ::_thesis: for u, v, u1 being Matrix of m,L st ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
(u * v) * (i,j) = (emb (m,L)) * (u1 * (i,j)) ) holds
u * v = (emb (m,L)) * u1
let u, v, u1 be Matrix of m,L; ::_thesis: ( ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
(u * v) * (i,j) = (emb (m,L)) * (u1 * (i,j)) ) implies u * v = (emb (m,L)) * u1 )
assume A2: for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
(u * v) * (i,j) = (emb (m,L)) * (u1 * (i,j)) ; ::_thesis: u * v = (emb (m,L)) * u1
A3: for i, j being Nat st [i,j] in Indices (u * v) holds
(u * v) * (i,j) = ((emb (m,L)) * u1) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (u * v) implies (u * v) * (i,j) = ((emb (m,L)) * u1) * (i,j) )
A4: ( [i,j] in Indices (u * v) implies ( 1 <= i & i <= m & 1 <= j & j <= m ) )
proof
width u = m by MATRIX_1:24
.= len v by MATRIX_1:24 ;
then A5: width (u * v) = width v by MATRIX_3:def_4
.= m by MATRIX_1:24 ;
assume A6: [i,j] in Indices (u * v) ; ::_thesis: ( 1 <= i & i <= m & 1 <= j & j <= m )
then A7: j in Seg m by A5, ZFMISC_1:87;
width u = m by MATRIX_1:24
.= len v by MATRIX_1:24 ;
then len (u * v) = len u by MATRIX_3:def_4
.= m by MATRIX_1:24 ;
then u * v is Matrix of m,m,L by A1, A5, MATRIX_1:20;
then Indices (u * v) = [:(Seg m),(Seg m):] by A5, MATRIX_1:25;
then i in Seg m by A6, ZFMISC_1:87;
hence ( 1 <= i & i <= m & 1 <= j & j <= m ) by A7, FINSEQ_1:1; ::_thesis: verum
end;
assume A8: [i,j] in Indices (u * v) ; ::_thesis: (u * v) * (i,j) = ((emb (m,L)) * u1) * (i,j)
then ( i in Seg m & j in Seg m ) by A4, FINSEQ_1:1;
then [i,j] in [:(Seg m),(Seg m):] by ZFMISC_1:87;
then [i,j] in Indices u1 by MATRIX_1:24;
then ((emb (m,L)) * u1) * (i,j) = (emb (m,L)) * (u1 * (i,j)) by MATRIX_3:def_5;
hence (u * v) * (i,j) = ((emb (m,L)) * u1) * (i,j) by A2, A8, A4; ::_thesis: verum
end;
A9: width ((emb (m,L)) * u1) = width u1 by MATRIX_3:def_5
.= m by MATRIX_1:24 ;
width u = m by MATRIX_1:24
.= len v by MATRIX_1:24 ;
then A10: width (u * v) = width v by MATRIX_3:def_4
.= m by MATRIX_1:24 ;
width u = m by MATRIX_1:24
.= len v by MATRIX_1:24 ;
then A11: len (u * v) = len u by MATRIX_3:def_4
.= m by MATRIX_1:24 ;
len ((emb (m,L)) * u1) = len u1 by MATRIX_3:def_5
.= m by MATRIX_1:24 ;
hence u * v = (emb (m,L)) * u1 by A11, A9, A10, A3, MATRIX_1:21; ::_thesis: verum
end;
Lm12: for L being Field
for m being Element of NAT st m > 0 holds
for p, q being Polynomial of L holds (emb ((2 * m),L)) * ((1. (L,(2 * m))) * (mConv ((p *' q),(2 * m)))) = (emb ((2 * m),L)) * (mConv ((p *' q),(2 * m)))
proof
let L be Field; ::_thesis: for m being Element of NAT st m > 0 holds
for p, q being Polynomial of L holds (emb ((2 * m),L)) * ((1. (L,(2 * m))) * (mConv ((p *' q),(2 * m)))) = (emb ((2 * m),L)) * (mConv ((p *' q),(2 * m)))
let m be Element of NAT ; ::_thesis: ( m > 0 implies for p, q being Polynomial of L holds (emb ((2 * m),L)) * ((1. (L,(2 * m))) * (mConv ((p *' q),(2 * m)))) = (emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))) )
assume A1: m > 0 ; ::_thesis: for p, q being Polynomial of L holds (emb ((2 * m),L)) * ((1. (L,(2 * m))) * (mConv ((p *' q),(2 * m)))) = (emb ((2 * m),L)) * (mConv ((p *' q),(2 * m)))
let p, q be Polynomial of L; ::_thesis: (emb ((2 * m),L)) * ((1. (L,(2 * m))) * (mConv ((p *' q),(2 * m)))) = (emb ((2 * m),L)) * (mConv ((p *' q),(2 * m)))
2 * m > 2 * 0 by A1, XREAL_1:68;
hence (emb ((2 * m),L)) * ((1. (L,(2 * m))) * (mConv ((p *' q),(2 * m)))) = (emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))) by Th35; ::_thesis: verum
end;
theorem Th37: :: POLYNOM8:37
for L being Field
for x being Element of L
for s being FinSequence of L
for i, j, m being Element of NAT st x is_primitive_root_of_degree m & 1 <= i & i <= m & 1 <= j & j <= m & len s = m & ( for k being Nat st 1 <= k & k <= m holds
s /. k = pow (x,((i - j) * (k - 1))) ) holds
((VM (x,m)) * (VM ((x "),m))) * (i,j) = Sum s
proof
let L be Field; ::_thesis: for x being Element of L
for s being FinSequence of L
for i, j, m being Element of NAT st x is_primitive_root_of_degree m & 1 <= i & i <= m & 1 <= j & j <= m & len s = m & ( for k being Nat st 1 <= k & k <= m holds
s /. k = pow (x,((i - j) * (k - 1))) ) holds
((VM (x,m)) * (VM ((x "),m))) * (i,j) = Sum s
let x be Element of L; ::_thesis: for s being FinSequence of L
for i, j, m being Element of NAT st x is_primitive_root_of_degree m & 1 <= i & i <= m & 1 <= j & j <= m & len s = m & ( for k being Nat st 1 <= k & k <= m holds
s /. k = pow (x,((i - j) * (k - 1))) ) holds
((VM (x,m)) * (VM ((x "),m))) * (i,j) = Sum s
let s be FinSequence of L; ::_thesis: for i, j, m being Element of NAT st x is_primitive_root_of_degree m & 1 <= i & i <= m & 1 <= j & j <= m & len s = m & ( for k being Nat st 1 <= k & k <= m holds
s /. k = pow (x,((i - j) * (k - 1))) ) holds
((VM (x,m)) * (VM ((x "),m))) * (i,j) = Sum s
let i, j, m be Element of NAT ; ::_thesis: ( x is_primitive_root_of_degree m & 1 <= i & i <= m & 1 <= j & j <= m & len s = m & ( for k being Nat st 1 <= k & k <= m holds
s /. k = pow (x,((i - j) * (k - 1))) ) implies ((VM (x,m)) * (VM ((x "),m))) * (i,j) = Sum s )
assume that
A1: x is_primitive_root_of_degree m and
A2: ( 1 <= i & i <= m ) and
A3: 1 <= j and
A4: j <= m and
A5: len s = m and
A6: for k being Nat st 1 <= k & k <= m holds
s /. k = pow (x,((i - j) * (k - 1))) ; ::_thesis: ((VM (x,m)) * (VM ((x "),m))) * (i,j) = Sum s
len (Line ((VM (x,m)),i)) = width (VM (x,m)) by MATRIX_1:def_7
.= m by MATRIX_1:24
.= len (VM ((x "),m)) by MATRIX_1:24
.= len (Col ((VM ((x "),m)),j)) by MATRIX_1:def_8 ;
then A7: len (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) = len (Line ((VM (x,m)),i)) by MATRIX_3:6
.= width (VM (x,m)) by MATRIX_1:def_7
.= m by MATRIX_1:24 ;
A8: x <> 0. L by A1, Th30;
A9: for k being Nat st 1 <= k & k <= m holds
((Line ((VM (x,m)),i)) /. k) * ((Col ((VM ((x "),m)),j)) /. k) = pow (x,((i - j) * (k - 1)))
proof
len (Col ((VM ((x "),m)),j)) = len (VM ((x "),m)) by MATRIX_1:def_8
.= m by MATRIX_1:24 ;
then A10: Seg m = dom (Col ((VM ((x "),m)),j)) by FINSEQ_1:def_3;
len (Line ((VM (x,m)),i)) = width (VM (x,m)) by MATRIX_1:def_7
.= m by MATRIX_1:24 ;
then A11: Seg m = dom (Line ((VM (x,m)),i)) by FINSEQ_1:def_3;
A12: 1 - 1 <= j - 1 by A3, XREAL_1:9;
let k be Nat; ::_thesis: ( 1 <= k & k <= m implies ((Line ((VM (x,m)),i)) /. k) * ((Col ((VM ((x "),m)),j)) /. k) = pow (x,((i - j) * (k - 1))) )
assume that
A13: 1 <= k and
A14: k <= m ; ::_thesis: ((Line ((VM (x,m)),i)) /. k) * ((Col ((VM ((x "),m)),j)) /. k) = pow (x,((i - j) * (k - 1)))
( len (VM ((x "),m)) = m & k in Seg m ) by A13, A14, FINSEQ_1:1, MATRIX_1:24;
then A15: k in dom (VM ((x "),m)) by FINSEQ_1:def_3;
k in Seg m by A13, A14, FINSEQ_1:1;
then A16: (Line ((VM (x,m)),i)) /. k = (Line ((VM (x,m)),i)) . k by A11, PARTFUN1:def_6;
1 - 1 <= k - 1 by A13, XREAL_1:9;
then A17: (j - 1) * (k - 1) in NAT by A12, INT_1:3;
width (VM (x,m)) = m by MATRIX_1:24;
then k in Seg (width (VM (x,m))) by A13, A14, FINSEQ_1:1;
then A18: (Line ((VM (x,m)),i)) . k = (VM (x,m)) * (i,k) by MATRIX_1:def_7;
k in Seg m by A13, A14, FINSEQ_1:1;
then A19: (Col ((VM ((x "),m)),j)) /. k = (Col ((VM ((x "),m)),j)) . k by A10, PARTFUN1:def_6;
(VM ((x "),m)) * (k,j) = pow ((x "),((j - 1) * (k - 1))) by A3, A4, A13, A14, Def8
.= pow (x,(- ((j - 1) * (k - 1)))) by A8, A17, Th22 ;
then (Col ((VM ((x "),m)),j)) . k = pow (x,(- ((j - 1) * (k - 1)))) by A15, MATRIX_1:def_8;
then ((Line ((VM (x,m)),i)) /. k) * ((Col ((VM ((x "),m)),j)) /. k) = (pow (x,((i - 1) * (k - 1)))) * (pow (x,(- ((j - 1) * (k - 1))))) by A2, A13, A14, A16, A18, A19, Def8
.= pow (x,((i - j) * (k - 1))) by A8, Th23 ;
hence ((Line ((VM (x,m)),i)) /. k) * ((Col ((VM ((x "),m)),j)) /. k) = pow (x,((i - j) * (k - 1))) ; ::_thesis: verum
end;
A20: for k being Nat st 1 <= k & k <= m holds
(mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) /. k = s /. k
proof
len (Col ((VM ((x "),m)),j)) = len (VM ((x "),m)) by MATRIX_1:def_8
.= m by MATRIX_1:24 ;
then A21: Seg m = dom (Col ((VM ((x "),m)),j)) by FINSEQ_1:def_3;
let k be Nat; ::_thesis: ( 1 <= k & k <= m implies (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) /. k = s /. k )
len (Line ((VM (x,m)),i)) = width (VM (x,m)) by MATRIX_1:def_7
.= m by MATRIX_1:24 ;
then A22: Seg m = dom (Line ((VM (x,m)),i)) by FINSEQ_1:def_3;
assume A23: ( 1 <= k & k <= m ) ; ::_thesis: (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) /. k = s /. k
then A24: ((Line ((VM (x,m)),i)) /. k) * ((Col ((VM ((x "),m)),j)) /. k) = pow (x,((i - j) * (k - 1))) by A9
.= s /. k by A6, A23 ;
k in Seg m by A23, FINSEQ_1:1;
then A25: (Col ((VM ((x "),m)),j)) . k = (Col ((VM ((x "),m)),j)) /. k by A21, PARTFUN1:def_6;
Seg m = dom (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) by A7, FINSEQ_1:def_3;
then A26: k in dom (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) by A23, FINSEQ_1:1;
k in Seg m by A23, FINSEQ_1:1;
then (Line ((VM (x,m)),i)) . k = (Line ((VM (x,m)),i)) /. k by A22, PARTFUN1:def_6;
then (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) . k = ((Line ((VM (x,m)),i)) /. k) * ((Col ((VM ((x "),m)),j)) /. k) by A26, A25, FVSUM_1:60;
hence (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) /. k = s /. k by A26, A24, PARTFUN1:def_6; ::_thesis: verum
end;
A27: for k being Nat st k in dom (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) holds
(mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) . k = s . k
proof
let k be Nat; ::_thesis: ( k in dom (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) implies (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) . k = s . k )
assume A28: k in dom (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) ; ::_thesis: (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) . k = s . k
A29: Seg m = dom (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) by A7, FINSEQ_1:def_3;
then A30: ( 1 <= k & k <= m ) by A28, FINSEQ_1:1;
A31: k in dom s by A5, A28, A29, FINSEQ_1:def_3;
(mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) . k = (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) /. k by A28, PARTFUN1:def_6
.= s /. k by A20, A30
.= s . k by A31, PARTFUN1:def_6 ;
hence (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) . k = s . k ; ::_thesis: verum
end;
dom (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) = Seg m by A7, FINSEQ_1:def_3
.= dom s by A5, FINSEQ_1:def_3 ;
then A32: Sum (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) = Sum s by A27, FINSEQ_1:13;
width (VM (x,m)) = m by MATRIX_1:24;
then A33: width (VM (x,m)) = len (VM ((x "),m)) by MATRIX_1:24;
A34: ( width (VM (x,m)) = m & len (VM ((x "),m)) = m ) by MATRIX_1:24;
len (VM (x,m)) = m by MATRIX_1:24;
then A35: len ((VM (x,m)) * (VM ((x "),m))) = m by A34, MATRIX_3:def_4;
width (VM ((x "),m)) = m by MATRIX_1:24;
then width ((VM (x,m)) * (VM ((x "),m))) = m by A34, MATRIX_3:def_4;
then (VM (x,m)) * (VM ((x "),m)) is Matrix of m,L by A2, A35, MATRIX_1:20;
then A36: Indices ((VM (x,m)) * (VM ((x "),m))) = [:(Seg m),(Seg m):] by MATRIX_1:24;
( i in Seg m & j in Seg m ) by A2, A3, A4;
then [i,j] in Indices ((VM (x,m)) * (VM ((x "),m))) by A36, ZFMISC_1:def_2;
then ((VM (x,m)) * (VM ((x "),m))) * (i,j) = (Line ((VM (x,m)),i)) "*" (Col ((VM ((x "),m)),j)) by A33, MATRIX_3:def_4;
hence ((VM (x,m)) * (VM ((x "),m))) * (i,j) = Sum s by A32, FVSUM_1:def_9; ::_thesis: verum
end;
theorem Th38: :: POLYNOM8:38
for L being Field
for m, i, j being Element of NAT
for x being Element of L st i <> j & 1 <= i & i <= m & 1 <= j & j <= m & x is_primitive_root_of_degree m holds
((VM (x,m)) * (VM ((x "),m))) * (i,j) = 0. L
proof
let L be Field; ::_thesis: for m, i, j being Element of NAT
for x being Element of L st i <> j & 1 <= i & i <= m & 1 <= j & j <= m & x is_primitive_root_of_degree m holds
((VM (x,m)) * (VM ((x "),m))) * (i,j) = 0. L
let m, i, j be Element of NAT ; ::_thesis: for x being Element of L st i <> j & 1 <= i & i <= m & 1 <= j & j <= m & x is_primitive_root_of_degree m holds
((VM (x,m)) * (VM ((x "),m))) * (i,j) = 0. L
let x be Element of L; ::_thesis: ( i <> j & 1 <= i & i <= m & 1 <= j & j <= m & x is_primitive_root_of_degree m implies ((VM (x,m)) * (VM ((x "),m))) * (i,j) = 0. L )
assume that
A1: i <> j and
A2: ( 1 <= i & i <= m & 1 <= j & j <= m ) and
A3: x is_primitive_root_of_degree m ; ::_thesis: ((VM (x,m)) * (VM ((x "),m))) * (i,j) = 0. L
A4: x <> 0. L by A3, Th30;
then A5: pow (x,(m * (i - j))) = pow ((pow (x,m)),(i - j)) by Th26
.= pow ((x |^ m),(i - j)) by Def3
.= pow ((1. L),(i - j)) by A3, Def6
.= 1. L by Th16 ;
ex G being FinSequence of L st
( dom G = Seg m & ( for k being Nat st k in Seg m holds
G . k = pow (x,((i - j) * (k - 1))) ) )
proof
defpred S1[ Nat, set ] means $2 = pow (x,((i - j) * ($1 - 1)));
A6: for n being Nat st n in Seg m holds
ex x being Element of L st S1[n,x] ;
ex G being FinSequence of L st
( dom G = Seg m & ( for nn being Nat st nn in Seg m holds
S1[nn,G . nn] ) ) from FINSEQ_1:sch_5(A6);
hence ex G being FinSequence of L st
( dom G = Seg m & ( for k being Nat st k in Seg m holds
G . k = pow (x,((i - j) * (k - 1))) ) ) ; ::_thesis: verum
end;
then consider s being FinSequence of L such that
A7: dom s = Seg m and
A8: for k being Nat st k in Seg m holds
s . k = pow (x,((i - j) * (k - 1))) ;
A9: for k being Nat st 1 <= k & k <= m holds
s /. k = pow (x,((i - j) * (k - 1)))
proof
let k be Nat; ::_thesis: ( 1 <= k & k <= m implies s /. k = pow (x,((i - j) * (k - 1))) )
assume A10: ( 1 <= k & k <= m ) ; ::_thesis: s /. k = pow (x,((i - j) * (k - 1)))
then A11: k in dom s by A7, FINSEQ_1:1;
k in Seg m by A10, FINSEQ_1:1;
then pow (x,((i - j) * (k - 1))) = s . k by A8
.= s /. k by A11, PARTFUN1:def_6 ;
hence s /. k = pow (x,((i - j) * (k - 1))) ; ::_thesis: verum
end;
consider r being Element of L such that
A12: r = pow (x,(i - j)) ;
A13: len s = m by A7, FINSEQ_1:def_3;
for k being Nat st 1 <= k & k <= len s holds
s . k = (pow (x,(i - j))) |^ (k -' 1)
proof
let k be Nat; ::_thesis: ( 1 <= k & k <= len s implies s . k = (pow (x,(i - j))) |^ (k -' 1) )
assume that
A14: 1 <= k and
A15: k <= len s ; ::_thesis: s . k = (pow (x,(i - j))) |^ (k -' 1)
A16: 1 - 1 <= k - 1 by A14, XREAL_1:9;
s . k = s /. k by A14, A15, FINSEQ_4:15
.= pow (x,((i - j) * (k - 1))) by A9, A13, A14, A15
.= pow (x,((i - j) * (k -' 1))) by A16, XREAL_0:def_2
.= pow ((pow (x,(i - j))),(k -' 1)) by A4, Th26
.= (pow (x,(i - j))) |^ (k -' 1) by Def3 ;
hence s . k = (pow (x,(i - j))) |^ (k -' 1) ; ::_thesis: verum
end;
then Sum s = ((1. L) - ((pow (x,(i - j))) |^ (len s))) / ((1. L) - (pow (x,(i - j)))) by A1, A2, A3, Th5, Th32
.= ((1. L) - ((pow (x,(i - j))) |^ m)) / ((1. L) - (pow (x,(i - j)))) by A7, FINSEQ_1:def_3
.= ((1. L) - (pow ((pow (x,(i - j))),m))) / ((1. L) - (pow (x,(i - j)))) by Def3
.= ((1. L) - (pow (x,((i - j) * m)))) / ((1. L) - (pow (x,(i - j)))) by A4, Th26
.= (0. L) / ((1. L) - r) by A5, A12, VECTSP_1:19
.= 0. L by VECTSP_1:7 ;
hence ((VM (x,m)) * (VM ((x "),m))) * (i,j) = 0. L by A2, A3, A9, A13, Th37; ::_thesis: verum
end;
theorem Th39: :: POLYNOM8:39
for L being Field
for m being Element of NAT st m > 0 holds
for x being Element of L st x is_primitive_root_of_degree m holds
(VM (x,m)) * (VM ((x "),m)) = (emb (m,L)) * (1. (L,m))
proof
let L be Field; ::_thesis: for m being Element of NAT st m > 0 holds
for x being Element of L st x is_primitive_root_of_degree m holds
(VM (x,m)) * (VM ((x "),m)) = (emb (m,L)) * (1. (L,m))
let m be Element of NAT ; ::_thesis: ( m > 0 implies for x being Element of L st x is_primitive_root_of_degree m holds
(VM (x,m)) * (VM ((x "),m)) = (emb (m,L)) * (1. (L,m)) )
assume A1: m > 0 ; ::_thesis: for x being Element of L st x is_primitive_root_of_degree m holds
(VM (x,m)) * (VM ((x "),m)) = (emb (m,L)) * (1. (L,m))
let x be Element of L; ::_thesis: ( x is_primitive_root_of_degree m implies (VM (x,m)) * (VM ((x "),m)) = (emb (m,L)) * (1. (L,m)) )
assume A2: x is_primitive_root_of_degree m ; ::_thesis: (VM (x,m)) * (VM ((x "),m)) = (emb (m,L)) * (1. (L,m))
for i, j being Nat st i >= 1 & i <= m & j >= 1 & j <= m holds
((VM (x,m)) * (VM ((x "),m))) * (i,j) = (emb (m,L)) * ((1. (L,m)) * (i,j))
proof
let i, j be Nat; ::_thesis: ( i >= 1 & i <= m & j >= 1 & j <= m implies ((VM (x,m)) * (VM ((x "),m))) * (i,j) = (emb (m,L)) * ((1. (L,m)) * (i,j)) )
A3: ( i in NAT & j in NAT ) by ORDINAL1:def_12;
ex G being FinSequence of L st
( dom G = Seg m & ( for k being Nat st k in Seg m holds
G . k = pow (x,((i - j) * (k - 1))) ) )
proof
defpred S1[ Nat, set ] means $2 = pow (x,((i - j) * ($1 - 1)));
A4: for n being Nat st n in Seg m holds
ex x being Element of L st S1[n,x] ;
ex G being FinSequence of L st
( dom G = Seg m & ( for nn being Nat st nn in Seg m holds
S1[nn,G . nn] ) ) from FINSEQ_1:sch_5(A4);
hence ex G being FinSequence of L st
( dom G = Seg m & ( for k being Nat st k in Seg m holds
G . k = pow (x,((i - j) * (k - 1))) ) ) ; ::_thesis: verum
end;
then consider s being FinSequence of L such that
A5: dom s = Seg m and
A6: for k being Nat st k in Seg m holds
s . k = pow (x,((i - j) * (k - 1))) ;
A7: len s = m by A5, FINSEQ_1:def_3;
A8: for k being Nat st 1 <= k & k <= m holds
s /. k = pow (x,((i - j) * (k - 1)))
proof
let k be Nat; ::_thesis: ( 1 <= k & k <= m implies s /. k = pow (x,((i - j) * (k - 1))) )
assume A9: ( 1 <= k & k <= m ) ; ::_thesis: s /. k = pow (x,((i - j) * (k - 1)))
then A10: k in dom s by A5, FINSEQ_1:1;
k in Seg m by A9, FINSEQ_1:1;
then pow (x,((i - j) * (k - 1))) = s . k by A6
.= s /. k by A10, PARTFUN1:def_6 ;
hence s /. k = pow (x,((i - j) * (k - 1))) ; ::_thesis: verum
end;
A11: Indices (1. (L,m)) = [:(Seg m),(Seg m):] by MATRIX_1:24;
assume that
A12: ( 1 <= i & i <= m ) and
A13: ( 1 <= j & j <= m ) ; ::_thesis: ((VM (x,m)) * (VM ((x "),m))) * (i,j) = (emb (m,L)) * ((1. (L,m)) * (i,j))
percases ( i = j or i <> j ) ;
supposeA14: i = j ; ::_thesis: ((VM (x,m)) * (VM ((x "),m))) * (i,j) = (emb (m,L)) * ((1. (L,m)) * (i,j))
A15: for k being Element of NAT st 1 <= k & k <= m holds
s /. k = 1. L
proof
let k be Element of NAT ; ::_thesis: ( 1 <= k & k <= m implies s /. k = 1. L )
assume ( 1 <= k & k <= m ) ; ::_thesis: s /. k = 1. L
then s /. k = pow (x,((i - j) * (k - 1))) by A8
.= 1. L by A14, Th13 ;
hence s /. k = 1. L ; ::_thesis: verum
end;
i in Seg m by A12, FINSEQ_1:1;
then A16: [i,i] in Indices (1. (L,m)) by A11, ZFMISC_1:87;
((VM (x,m)) * (VM ((x "),m))) * (i,j) = Sum s by A2, A3, A12, A13, A7, A8, Th37
.= m * (1. L) by A7, A15, Th4
.= (emb (m,L)) * (1. L) by VECTSP_1:def_8 ;
hence ((VM (x,m)) * (VM ((x "),m))) * (i,j) = (emb (m,L)) * ((1. (L,m)) * (i,j)) by A14, A16, MATRIX_1:def_11; ::_thesis: verum
end;
supposeA17: i <> j ; ::_thesis: ((VM (x,m)) * (VM ((x "),m))) * (i,j) = (emb (m,L)) * ((1. (L,m)) * (i,j))
( i in Seg m & j in Seg m ) by A12, A13, FINSEQ_1:1;
then A18: [i,j] in Indices (1. (L,m)) by A11, ZFMISC_1:87;
((VM (x,m)) * (VM ((x "),m))) * (i,j) = 0. L by A2, A3, A12, A13, A17, Th38
.= (emb (m,L)) * (0. L) by VECTSP_1:6 ;
hence ((VM (x,m)) * (VM ((x "),m))) * (i,j) = (emb (m,L)) * ((1. (L,m)) * (i,j)) by A17, A18, MATRIX_1:def_11; ::_thesis: verum
end;
end;
end;
hence (VM (x,m)) * (VM ((x "),m)) = (emb (m,L)) * (1. (L,m)) by A1, Th36; ::_thesis: verum
end;
theorem Th40: :: POLYNOM8:40
for L being Field
for m being Element of NAT
for x being Element of L st m > 0 & x is_primitive_root_of_degree m holds
(VM (x,m)) * (VM ((x "),m)) = (VM ((x "),m)) * (VM (x,m))
proof
let L be Field; ::_thesis: for m being Element of NAT
for x being Element of L st m > 0 & x is_primitive_root_of_degree m holds
(VM (x,m)) * (VM ((x "),m)) = (VM ((x "),m)) * (VM (x,m))
let m be Element of NAT ; ::_thesis: for x being Element of L st m > 0 & x is_primitive_root_of_degree m holds
(VM (x,m)) * (VM ((x "),m)) = (VM ((x "),m)) * (VM (x,m))
let x be Element of L; ::_thesis: ( m > 0 & x is_primitive_root_of_degree m implies (VM (x,m)) * (VM ((x "),m)) = (VM ((x "),m)) * (VM (x,m)) )
assume that
A1: 0 < m and
A2: x is_primitive_root_of_degree m ; ::_thesis: (VM (x,m)) * (VM ((x "),m)) = (VM ((x "),m)) * (VM (x,m))
x <> 0. L by A2, Th30;
then (VM ((x "),m)) * (VM (x,m)) = (VM ((x "),m)) * (VM (((x ") "),m)) by VECTSP_1:24
.= (emb (m,L)) * (1. (L,m)) by A1, A2, Th31, Th39 ;
hence (VM (x,m)) * (VM ((x "),m)) = (VM ((x "),m)) * (VM (x,m)) by A1, A2, Th39; ::_thesis: verum
end;
begin
theorem Th41: :: POLYNOM8:41
for L being Field
for p being Polynomial of L
for m being Element of NAT st m > 0 & len p <= m holds
for x being Element of L
for i being Element of NAT st i < m holds
(DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1)
proof
let L be Field; ::_thesis: for p being Polynomial of L
for m being Element of NAT st m > 0 & len p <= m holds
for x being Element of L
for i being Element of NAT st i < m holds
(DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1)
let p be Polynomial of L; ::_thesis: for m being Element of NAT st m > 0 & len p <= m holds
for x being Element of L
for i being Element of NAT st i < m holds
(DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1)
let m be Element of NAT ; ::_thesis: ( m > 0 & len p <= m implies for x being Element of L
for i being Element of NAT st i < m holds
(DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1) )
assume that
A1: m > 0 and
A2: len p <= m ; ::_thesis: for x being Element of L
for i being Element of NAT st i < m holds
(DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1)
let x be Element of L; ::_thesis: for i being Element of NAT st i < m holds
(DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1)
set v = VM (x,m);
for i being Element of NAT st i < m holds
(DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1)
proof
A3: for k being Nat st k < m holds
(Col ((mConv (p,m)),1)) . (k + 1) = p . k
proof
let k be Nat; ::_thesis: ( k < m implies (Col ((mConv (p,m)),1)) . (k + 1) = p . k )
assume A4: k < m ; ::_thesis: (Col ((mConv (p,m)),1)) . (k + 1) = p . k
then ( 1 <= k + 1 & k + 1 <= m ) by NAT_1:11, NAT_1:13;
then A5: k + 1 in Seg m ;
len (mConv (p,m)) = m by A1, Th28;
then k + 1 in dom (mConv (p,m)) by A5, FINSEQ_1:def_3;
then (Col ((mConv (p,m)),1)) . (k + 1) = (mConv (p,m)) * ((k + 1),1) by MATRIX_1:def_8;
hence (Col ((mConv (p,m)),1)) . (k + 1) = p . k by A4, Th28; ::_thesis: verum
end;
A6: width (VM (x,m)) = m by MATRIX_1:24
.= len (mConv (p,m)) by A1, Th28 ;
then A7: len ((VM (x,m)) * (mConv (p,m))) = len (VM (x,m)) by MATRIX_3:def_4
.= m by MATRIX_1:24 ;
width ((VM (x,m)) * (mConv (p,m))) = width (mConv (p,m)) by A6, MATRIX_3:def_4
.= 1 by A1, Th28 ;
then (VM (x,m)) * (mConv (p,m)) is Matrix of m,1,L by A1, A7, MATRIX_1:20;
then A8: Indices ((VM (x,m)) * (mConv (p,m))) = [:(Seg m),(Seg (width ((VM (x,m)) * (mConv (p,m))))):] by MATRIX_1:25;
A9: len (mConv (p,m)) = m by A1, Th28
.= width (VM (x,m)) by MATRIX_1:24 ;
width ((VM (x,m)) * (mConv (p,m))) = width (mConv (p,m)) by A6, MATRIX_3:def_4
.= 1 by A1, Th28 ;
then A10: 1 in Seg (width ((VM (x,m)) * (mConv (p,m)))) ;
let i be Element of NAT ; ::_thesis: ( i < m implies (DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1) )
assume A11: i < m ; ::_thesis: (DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1)
A12: for k being Nat st k < m holds
(Line ((VM (x,m)),(i + 1))) . (k + 1) = (VM (x,m)) * ((i + 1),(k + 1))
proof
let k be Nat; ::_thesis: ( k < m implies (Line ((VM (x,m)),(i + 1))) . (k + 1) = (VM (x,m)) * ((i + 1),(k + 1)) )
assume k < m ; ::_thesis: (Line ((VM (x,m)),(i + 1))) . (k + 1) = (VM (x,m)) * ((i + 1),(k + 1))
then ( 1 <= k + 1 & k + 1 <= m ) by NAT_1:11, NAT_1:13;
then k + 1 in Seg m ;
then k + 1 in Seg (width (VM (x,m))) by MATRIX_1:24;
hence (Line ((VM (x,m)),(i + 1))) . (k + 1) = (VM (x,m)) * ((i + 1),(k + 1)) by MATRIX_1:def_7; ::_thesis: verum
end;
A13: for k being Nat st k < m holds
(Line ((VM (x,m)),(i + 1))) . (k + 1) = pow (x,(i * k))
proof
let k be Nat; ::_thesis: ( k < m implies (Line ((VM (x,m)),(i + 1))) . (k + 1) = pow (x,(i * k)) )
assume A14: k < m ; ::_thesis: (Line ((VM (x,m)),(i + 1))) . (k + 1) = pow (x,(i * k))
then A15: ( 1 <= k + 1 & k + 1 <= m ) by NAT_1:11, NAT_1:13;
A16: ( 1 <= i + 1 & i + 1 <= m ) by A11, NAT_1:11, NAT_1:13;
(Line ((VM (x,m)),(i + 1))) . (k + 1) = (VM (x,m)) * ((i + 1),(k + 1)) by A12, A14
.= pow (x,(((i + 1) - 1) * ((k + 1) - 1))) by A16, A15, Def8
.= pow (x,(i * k)) ;
hence (Line ((VM (x,m)),(i + 1))) . (k + 1) = pow (x,(i * k)) ; ::_thesis: verum
end;
A17: for k being Nat
for a, b, c being Element of L st a = (Line ((VM (x,m)),(i + 1))) . (k + 1) & b = (Col ((mConv (p,m)),1)) . (k + 1) & c = p . k & k < m holds
a * b = (pow (x,(i * k))) * c
proof
let k be Nat; ::_thesis: for a, b, c being Element of L st a = (Line ((VM (x,m)),(i + 1))) . (k + 1) & b = (Col ((mConv (p,m)),1)) . (k + 1) & c = p . k & k < m holds
a * b = (pow (x,(i * k))) * c
let a, b, c be Element of L; ::_thesis: ( a = (Line ((VM (x,m)),(i + 1))) . (k + 1) & b = (Col ((mConv (p,m)),1)) . (k + 1) & c = p . k & k < m implies a * b = (pow (x,(i * k))) * c )
assume that
A18: a = (Line ((VM (x,m)),(i + 1))) . (k + 1) and
A19: ( b = (Col ((mConv (p,m)),1)) . (k + 1) & c = p . k ) and
A20: k < m ; ::_thesis: a * b = (pow (x,(i * k))) * c
a = pow (x,(i * k)) by A13, A18, A20;
hence a * b = (pow (x,(i * k))) * c by A3, A19, A20; ::_thesis: verum
end;
A21: for k being Element of NAT st 1 <= k & k <= m holds
(mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (p . (k -' 1)) * ((power L) . ((x |^ i),(k -' 1)))
proof
A22: len (mConv (p,m)) = m by A1, Th28;
let k be Element of NAT ; ::_thesis: ( 1 <= k & k <= m implies (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (p . (k -' 1)) * ((power L) . ((x |^ i),(k -' 1))) )
assume that
A23: 1 <= k and
A24: k <= m ; ::_thesis: (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (p . (k -' 1)) * ((power L) . ((x |^ i),(k -' 1)))
k in Seg m by A23, A24;
then k in dom (mConv (p,m)) by A22, FINSEQ_1:def_3;
then A25: (Col ((mConv (p,m)),1)) . k = (mConv (p,m)) * (k,1) by MATRIX_1:def_8;
0 < k by A23;
then ( dom p = NAT & k - 1 is Element of NAT ) by FUNCT_2:def_1, NAT_1:20;
then A26: p . (k - 1) = p /. (k - 1) by PARTFUN1:def_6;
Seg (width (VM (x,m))) = Seg m by MATRIX_1:24;
then k in Seg (width (VM (x,m))) by A23, A24;
then (Line ((VM (x,m)),(i + 1))) . k = (VM (x,m)) * ((i + 1),k) by MATRIX_1:def_7;
then reconsider a = (Line ((VM (x,m)),(i + 1))) . k, b = (Col ((mConv (p,m)),1)) . k, c = p . (k - 1) as Element of L by A25, A26;
len (Line ((VM (x,m)),(i + 1))) = width (VM (x,m)) by MATRIX_1:def_7
.= m by MATRIX_1:24
.= len (mConv (p,m)) by A1, Th28
.= len (Col ((mConv (p,m)),1)) by MATRIX_1:def_8 ;
then len (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) = len (Line ((VM (x,m)),(i + 1))) by MATRIX_3:6
.= width (VM (x,m)) by MATRIX_1:def_7
.= m by MATRIX_1:24 ;
then dom (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) = Seg m by FINSEQ_1:def_3;
then k in dom (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) by A23, A24;
then A27: (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = a * b by FVSUM_1:60;
A28: a * b = (pow (x,(i * (k - 1)))) * c
proof
A29: 0 < k by A23;
then A30: k - 1 is Nat by NAT_1:20;
( k - 1 <= m - 1 & m - 1 is Nat ) by A1, A24, NAT_1:20, XREAL_1:9;
then A31: k - 1 < (m - 1) + 1 by A30, NAT_1:13;
reconsider l = k - 1 as Nat by A29, NAT_1:20;
a = (Line ((VM (x,m)),(i + 1))) . (l + 1) ;
hence a * b = (pow (x,(i * (k - 1)))) * c by A17, A31; ::_thesis: verum
end;
reconsider d = pow (x,(i * (k - 1))) as Element of L ;
A32: k - 1 >= 0 by A23, NAT_1:20;
d = pow ((x |^ i),(k - 1)) by A23, Th27
.= (power L) . ((x |^ i),(k - 1)) by A32, Def3
.= (power L) . ((x |^ i),(k -' 1)) by A32, XREAL_0:def_2 ;
hence (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (p . (k -' 1)) * ((power L) . ((x |^ i),(k -' 1))) by A28, A27, A32, XREAL_0:def_2; ::_thesis: verum
end;
A33: Sum (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) = eval (p,(x |^ i))
proof
A34: for k being Nat st len p < k & k <= m holds
(mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = 0. L
proof
A35: 1 <= 1 + (len p) by NAT_1:11;
let k be Nat; ::_thesis: ( len p < k & k <= m implies (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = 0. L )
assume that
A36: len p < k and
A37: k <= m ; ::_thesis: (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = 0. L
A38: len p < (k - 1) + 1 by A36;
(len p) + 1 <= k by A36, NAT_1:13;
then A39: 1 <= k by A35, XXREAL_0:2;
then 1 - 1 <= k - 1 by XREAL_1:9;
then k -' 1 = k - 1 by XREAL_0:def_2;
then A40: k -' 1 >= len p by A38, NAT_1:13;
k in NAT by ORDINAL1:def_12;
then (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (p . (k -' 1)) * ((power L) . ((x |^ i),(k -' 1))) by A21, A37, A39
.= (0. L) * ((power L) . ((x |^ i),(k -' 1))) by A40, ALGSEQ_1:8
.= 0. L by VECTSP_1:7 ;
hence (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = 0. L ; ::_thesis: verum
end;
len (Line ((VM (x,m)),(i + 1))) = width (VM (x,m)) by MATRIX_1:def_7
.= m by MATRIX_1:24
.= len (mConv (p,m)) by A1, Th28
.= len (Col ((mConv (p,m)),1)) by MATRIX_1:def_8 ;
then A41: len (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) = len (Line ((VM (x,m)),(i + 1))) by MATRIX_3:6
.= width (VM (x,m)) by MATRIX_1:def_7
.= m by MATRIX_1:24 ;
(len p) - (len p) <= m - (len p) by A2, XREAL_1:9;
then reconsider lengthG = m - (len p) as Element of NAT by INT_1:3;
consider F being FinSequence of L such that
A42: eval (p,(x |^ i)) = Sum F and
A43: len F = len p and
A44: for k being Element of NAT st k in dom F holds
F . k = (p . (k -' 1)) * ((power L) . ((x |^ i),(k -' 1))) by POLYNOM4:def_2;
ex G being FinSequence of L st
( dom G = Seg lengthG & ( for k being Nat st k in Seg lengthG holds
G . k = 0. L ) )
proof
defpred S1[ set , set ] means $2 = 0. L;
A45: for n being Nat st n in Seg lengthG holds
ex x being Element of L st S1[n,x] ;
ex G being FinSequence of L st
( dom G = Seg lengthG & ( for nn being Nat st nn in Seg lengthG holds
S1[nn,G . nn] ) ) from FINSEQ_1:sch_5(A45);
hence ex G being FinSequence of L st
( dom G = Seg lengthG & ( for k being Nat st k in Seg lengthG holds
G . k = 0. L ) ) ; ::_thesis: verum
end;
then consider G being FinSequence of L such that
A46: dom G = Seg lengthG and
A47: for k being Nat st k in Seg lengthG holds
G . k = 0. L ;
A48: for k being Element of NAT st k in Seg lengthG holds
G . k = 0. L by A47;
A49: len G = m - (len p) by A46, FINSEQ_1:def_3;
then (len F) + (len G) = m by A43;
then dom (F ^ G) = Seg m by FINSEQ_1:def_7;
then A50: dom (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) = dom (F ^ G) by A41, FINSEQ_1:def_3;
A51: for k being Element of NAT st 1 <= k & k <= len p holds
F . k = (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k
proof
let k be Element of NAT ; ::_thesis: ( 1 <= k & k <= len p implies F . k = (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k )
assume that
A52: 1 <= k and
A53: k <= len p ; ::_thesis: F . k = (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k
A54: k <= m by A2, A53, XXREAL_0:2;
dom F = Seg (len p) by A43, FINSEQ_1:def_3;
then k in dom F by A52, A53;
then F . k = (p . (k -' 1)) * ((power L) . ((x |^ i),(k -' 1))) by A44
.= (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k by A21, A52, A54 ;
hence F . k = (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k ; ::_thesis: verum
end;
for k being Nat st k in dom (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) holds
(mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (F ^ G) . k
proof
let k be Nat; ::_thesis: ( k in dom (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) implies (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (F ^ G) . k )
(len F) + (len G) = m by A43, A49;
then A55: dom (F ^ G) = Seg m by FINSEQ_1:def_7;
assume A56: k in dom (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) ; ::_thesis: (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (F ^ G) . k
percases ( ( 1 <= k & k <= len F ) or ( len F < k & k <= m ) ) by A50, A56, A55, FINSEQ_1:1;
supposeA57: ( 1 <= k & k <= len F ) ; ::_thesis: (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (F ^ G) . k
then k in dom F by FINSEQ_3:25;
then (F ^ G) . k = F . k by FINSEQ_1:def_7
.= (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k by A43, A51, A56, A57 ;
hence (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (F ^ G) . k ; ::_thesis: verum
end;
supposeA58: ( len F < k & k <= m ) ; ::_thesis: (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (F ^ G) . k
then (len F) + 1 <= k by NAT_1:13;
then ((len F) + 1) - (len F) <= k - (len F) by XREAL_1:9;
then reconsider l = k - (len F) as Element of NAT by INT_1:3;
(len p) - m <= m - m by A2, XREAL_1:9;
then - ((len p) - m) >= 0 ;
then reconsider lengthG = m - (len p) as Element of NAT by INT_1:3;
(len F) + 1 <= k by A58, NAT_1:13;
then A59: ((len F) + 1) - (len F) <= k - (len F) by XREAL_1:9;
l <= lengthG by A43, A58, XREAL_1:9;
then A60: l in dom G by A46, A59;
(len F) + (len G) = m by A43, A49;
then dom (F ^ G) = Seg m by FINSEQ_1:def_7;
then len (F ^ G) = m by FINSEQ_1:def_3;
then (F ^ G) . k = G . (k - (len F)) by A58, FINSEQ_1:24
.= 0. L by A46, A47, A60
.= (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k by A43, A34, A58 ;
hence (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (F ^ G) . k ; ::_thesis: verum
end;
end;
end;
then mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1))) = F ^ G by A50, FINSEQ_1:13;
then Sum (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) = (Sum F) + (Sum G) by RLVECT_1:41
.= (Sum F) + (0. L) by A46, A48, POLYNOM3:1
.= eval (p,(x |^ i)) by A42, RLVECT_1:def_4 ;
hence Sum (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) = eval (p,(x |^ i)) ; ::_thesis: verum
end;
A61: (Line ((VM (x,m)),(i + 1))) "*" (Col ((mConv (p,m)),1)) = Sum (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) by FVSUM_1:def_9;
( 1 <= i + 1 & i + 1 <= m ) by A11, NAT_1:11, NAT_1:13;
then i + 1 in Seg m ;
then [(i + 1),1] in Indices ((VM (x,m)) * (mConv (p,m))) by A8, A10, ZFMISC_1:def_2;
then ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1) = eval (p,(x |^ i)) by A9, A61, A33, MATRIX_3:def_4;
hence (DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1) by A11, Def7; ::_thesis: verum
end;
hence for i being Element of NAT st i < m holds
(DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1) ; ::_thesis: verum
end;
theorem Th42: :: POLYNOM8:42
for L being Field
for p being Polynomial of L
for m being Nat st 0 < m & len p <= m holds
for x being Element of L holds DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m)))
proof
let L be Field; ::_thesis: for p being Polynomial of L
for m being Nat st 0 < m & len p <= m holds
for x being Element of L holds DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m)))
let p be Polynomial of L; ::_thesis: for m being Nat st 0 < m & len p <= m holds
for x being Element of L holds DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m)))
let m be Nat; ::_thesis: ( 0 < m & len p <= m implies for x being Element of L holds DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m))) )
assume that
A1: 0 < m and
A2: len p <= m ; ::_thesis: for x being Element of L holds DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m)))
let x be Element of L; ::_thesis: DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m)))
A3: m in NAT by ORDINAL1:def_12;
A4: now__::_thesis:_for_u9_being_set_st_u9_in_dom_(DFT_(p,x,m))_holds_
(DFT_(p,x,m))_._u9_=_(aConv_((VM_(x,m))_*_(mConv_(p,m))))_._u9
let u9 be set ; ::_thesis: ( u9 in dom (DFT (p,x,m)) implies (DFT (p,x,m)) . b1 = (aConv ((VM (x,m)) * (mConv (p,m)))) . b1 )
assume u9 in dom (DFT (p,x,m)) ; ::_thesis: (DFT (p,x,m)) . b1 = (aConv ((VM (x,m)) * (mConv (p,m)))) . b1
then reconsider u = u9 as Element of NAT by FUNCT_2:def_1;
percases ( u < m or m <= u ) ;
supposeA5: u < m ; ::_thesis: (DFT (p,x,m)) . b1 = (aConv ((VM (x,m)) * (mConv (p,m)))) . b1
width (VM (x,m)) = m by MATRIX_1:24
.= len (mConv (p,m)) by A1, Th28 ;
then A6: len ((VM (x,m)) * (mConv (p,m))) = len (VM (x,m)) by MATRIX_3:def_4
.= m by MATRIX_1:24 ;
thus (DFT (p,x,m)) . u9 = ((VM (x,m)) * (mConv (p,m))) * ((u + 1),1) by A3, A2, A5, Th41
.= (aConv ((VM (x,m)) * (mConv (p,m)))) . u9 by A5, A6, Def5 ; ::_thesis: verum
end;
supposeA7: m <= u ; ::_thesis: (DFT (p,x,m)) . b1 = (aConv ((VM (x,m)) * (mConv (p,m)))) . b1
width (VM (x,m)) = m by MATRIX_1:24
.= len (mConv (p,m)) by A1, Th28 ;
then A8: len ((VM (x,m)) * (mConv (p,m))) = len (VM (x,m)) by MATRIX_3:def_4
.= m by MATRIX_1:24 ;
thus (DFT (p,x,m)) . u9 = 0. L by A7, Def7
.= (aConv ((VM (x,m)) * (mConv (p,m)))) . u9 by A7, A8, Def5 ; ::_thesis: verum
end;
end;
end;
dom (DFT (p,x,m)) = NAT by FUNCT_2:def_1
.= dom (aConv ((VM (x,m)) * (mConv (p,m)))) by FUNCT_2:def_1 ;
hence DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m))) by A4, FUNCT_1:2; ::_thesis: verum
end;
theorem Th43: :: POLYNOM8:43
for L being Field
for p, q being Polynomial of L
for m being Element of NAT st m > 0 & len p <= m & len q <= m holds
for x being Element of L st x is_primitive_root_of_degree 2 * m holds
DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q)
proof
let L be Field; ::_thesis: for p, q being Polynomial of L
for m being Element of NAT st m > 0 & len p <= m & len q <= m holds
for x being Element of L st x is_primitive_root_of_degree 2 * m holds
DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q)
let p, q be Polynomial of L; ::_thesis: for m being Element of NAT st m > 0 & len p <= m & len q <= m holds
for x being Element of L st x is_primitive_root_of_degree 2 * m holds
DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q)
let m be Element of NAT ; ::_thesis: ( m > 0 & len p <= m & len q <= m implies for x being Element of L st x is_primitive_root_of_degree 2 * m holds
DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q) )
assume that
A1: m > 0 and
A2: ( len p <= m & len q <= m ) ; ::_thesis: for x being Element of L st x is_primitive_root_of_degree 2 * m holds
DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q)
let x be Element of L; ::_thesis: ( x is_primitive_root_of_degree 2 * m implies DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q) )
assume A3: x is_primitive_root_of_degree 2 * m ; ::_thesis: DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q)
percases ( len p = 0 or len q = 0 or ( len p <> 0 & len q <> 0 ) ) ;
supposeA4: ( len p = 0 or len q = 0 ) ; ::_thesis: DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q)
percases ( len p = 0 or len q = 0 ) by A4;
suppose len p = 0 ; ::_thesis: DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q)
then p = 0_. L by POLYNOM4:5;
then p *' q = 0_. L by POLYNOM3:34;
then ( (emb ((2 * m),L)) * (p *' q) = 0_. L & DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = DFT ((0_. L),(x "),(2 * m)) ) by Th33, POLYNOM5:28;
hence DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q) by Th33; ::_thesis: verum
end;
suppose len q = 0 ; ::_thesis: DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q)
then q = 0_. L by POLYNOM4:5;
then p *' q = 0_. L by POLYNOM3:34;
then ( (emb ((2 * m),L)) * (p *' q) = 0_. L & DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = DFT ((0_. L),(x "),(2 * m)) ) by Th33, POLYNOM5:28;
hence DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q) by Th33; ::_thesis: verum
end;
end;
end;
supposeA5: ( len p <> 0 & len q <> 0 ) ; ::_thesis: DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q)
set v1 = VM (x,(2 * m));
set v2 = VM ((x "),(2 * m));
A6: (len p) + (len q) <= m + m by A2, XREAL_1:7;
len (p *' q) <= (len p) + (len q) by A5, Th9;
then A7: len (p *' q) <= 2 * m by A6, XXREAL_0:2;
A8: for i being Nat st i < 2 * m holds
((VM (x,(2 * m))) * (mConv ((p *' q),(2 * m)))) * ((i + 1),1) = (DFT ((p *' q),x,(2 * m))) . i
proof
let i be Nat; ::_thesis: ( i < 2 * m implies ((VM (x,(2 * m))) * (mConv ((p *' q),(2 * m)))) * ((i + 1),1) = (DFT ((p *' q),x,(2 * m))) . i )
i in NAT by ORDINAL1:def_12;
hence ( i < 2 * m implies ((VM (x,(2 * m))) * (mConv ((p *' q),(2 * m)))) * ((i + 1),1) = (DFT ((p *' q),x,(2 * m))) . i ) by A7, Th41; ::_thesis: verum
end;
for i being Nat st i >= 2 * m holds
(DFT ((p *' q),x,(2 * m))) . i = 0. L by Def7;
then 2 * m is_at_least_length_of DFT ((p *' q),x,(2 * m)) by ALGSEQ_1:def_2;
then A9: len (DFT ((p *' q),x,(2 * m))) <= 2 * m by ALGSEQ_1:def_3;
A10: width (VM ((x "),(2 * m))) = 2 * m by MATRIX_1:24
.= len (VM (x,(2 * m))) by MATRIX_1:24 ;
A11: m + m <> 0 by A1;
then A12: (VM ((x "),(2 * m))) * (VM (x,(2 * m))) = (VM (x,(2 * m))) * (VM ((x "),(2 * m))) by A3, Th40
.= (emb ((2 * m),L)) * (1. (L,(2 * m))) by A3, A11, Th39 ;
A13: now__::_thesis:_for_u9_being_set_st_u9_in_dom_(aConv_((emb_((2_*_m),L))_*_(mConv_((p_*'_q),(2_*_m)))))_holds_
(aConv_((emb_((2_*_m),L))_*_(mConv_((p_*'_q),(2_*_m)))))_._u9_=_((emb_((2_*_m),L))_*_(p_*'_q))_._u9
let u9 be set ; ::_thesis: ( u9 in dom (aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))))) implies (aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))))) . b1 = ((emb ((2 * m),L)) * (p *' q)) . b1 )
assume u9 in dom (aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))))) ; ::_thesis: (aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))))) . b1 = ((emb ((2 * m),L)) * (p *' q)) . b1
then reconsider u = u9 as Element of NAT by FUNCT_2:def_1;
percases ( u < 2 * m or 2 * m <= u ) ;
supposeA14: u < 2 * m ; ::_thesis: (aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))))) . b1 = ((emb ((2 * m),L)) * (p *' q)) . b1
then ( 0 + 1 <= u + 1 & u + 1 <= 2 * m ) by NAT_1:13;
then A15: u + 1 in Seg (2 * m) ;
len (mConv ((p *' q),(2 * m))) = 2 * m by A11, Th28;
then A16: dom (mConv ((p *' q),(2 * m))) = Seg (2 * m) by FINSEQ_1:def_3;
( Seg (width (mConv ((p *' q),(2 * m)))) = Seg 1 & 1 in Seg 1 ) by A11, Th28;
then A17: [(u + 1),1] in Indices (mConv ((p *' q),(2 * m))) by A16, A15, ZFMISC_1:87;
len ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m)))) = len (mConv ((p *' q),(2 * m))) by MATRIX_3:def_5
.= 2 * m by A11, Th28 ;
hence (aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))))) . u9 = ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m)))) * ((u + 1),1) by A14, Def5
.= (emb ((2 * m),L)) * ((mConv ((p *' q),(2 * m))) * ((u + 1),1)) by A17, MATRIX_3:def_5
.= (emb ((2 * m),L)) * ((p *' q) . u) by A14, Th28
.= ((emb ((2 * m),L)) * (p *' q)) . u9 by POLYNOM5:def_3 ;
::_thesis: verum
end;
supposeA18: 2 * m <= u ; ::_thesis: (aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))))) . b1 = ((emb ((2 * m),L)) * (p *' q)) . b1
len ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m)))) = len (mConv ((p *' q),(2 * m))) by MATRIX_3:def_5
.= 2 * m by A11, Th28 ;
hence (aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))))) . u9 = 0. L by A18, Def5
.= (emb ((2 * m),L)) * (0. L) by VECTSP_1:6
.= (emb ((2 * m),L)) * ((p *' q) . u) by A7, A18, ALGSEQ_1:8, XXREAL_0:2
.= ((emb ((2 * m),L)) * (p *' q)) . u9 by POLYNOM5:def_3 ;
::_thesis: verum
end;
end;
end;
dom (aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))))) = NAT by FUNCT_2:def_1
.= dom ((emb ((2 * m),L)) * (p *' q)) by FUNCT_2:def_1 ;
then A19: aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m)))) = (emb ((2 * m),L)) * (p *' q) by A13, FUNCT_1:2;
A20: len (mConv ((p *' q),(2 * m))) = 2 * m by A11, Th28
.= width (VM (x,(2 * m))) by MATRIX_1:24 ;
then A21: len ((VM (x,(2 * m))) * (mConv ((p *' q),(2 * m)))) = len (VM (x,(2 * m))) by MATRIX_3:def_4
.= 2 * m by MATRIX_1:24 ;
width ((VM (x,(2 * m))) * (mConv ((p *' q),(2 * m)))) = width (mConv ((p *' q),(2 * m))) by A20, MATRIX_3:def_4
.= 1 by A11, Th28 ;
then (VM (x,(2 * m))) * (mConv ((p *' q),(2 * m))) is Matrix of 2 * m,1,L by A11, A21, MATRIX_1:20;
then aConv ((VM ((x "),(2 * m))) * (mConv ((DFT ((p *' q),x,(2 * m))),(2 * m)))) = aConv ((VM ((x "),(2 * m))) * ((VM (x,(2 * m))) * (mConv ((p *' q),(2 * m))))) by A11, A8, Th29
.= aConv (((VM ((x "),(2 * m))) * (VM (x,(2 * m)))) * (mConv ((p *' q),(2 * m)))) by A10, A20, MATRIX_3:33
.= aConv ((emb ((2 * m),L)) * ((1. (L,(2 * m))) * (mConv ((p *' q),(2 * m))))) by A11, A12, Th6
.= aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m)))) by A1, Lm12 ;
hence DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q) by A11, A9, A19, Th42; ::_thesis: verum
end;
end;
end;
theorem :: POLYNOM8:44
for L being Field
for p, q being Polynomial of L
for m being Element of NAT st m > 0 & len p <= m & len q <= m holds
for x being Element of L st x is_primitive_root_of_degree 2 * m & emb ((2 * m),L) <> 0. L holds
((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = p *' q
proof
let L be Field; ::_thesis: for p, q being Polynomial of L
for m being Element of NAT st m > 0 & len p <= m & len q <= m holds
for x being Element of L st x is_primitive_root_of_degree 2 * m & emb ((2 * m),L) <> 0. L holds
((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = p *' q
let p, q be Polynomial of L; ::_thesis: for m being Element of NAT st m > 0 & len p <= m & len q <= m holds
for x being Element of L st x is_primitive_root_of_degree 2 * m & emb ((2 * m),L) <> 0. L holds
((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = p *' q
let m be Element of NAT ; ::_thesis: ( m > 0 & len p <= m & len q <= m implies for x being Element of L st x is_primitive_root_of_degree 2 * m & emb ((2 * m),L) <> 0. L holds
((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = p *' q )
assume A1: ( m > 0 & len p <= m & len q <= m ) ; ::_thesis: for x being Element of L st x is_primitive_root_of_degree 2 * m & emb ((2 * m),L) <> 0. L holds
((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = p *' q
let x be Element of L; ::_thesis: ( x is_primitive_root_of_degree 2 * m & emb ((2 * m),L) <> 0. L implies ((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = p *' q )
assume A2: x is_primitive_root_of_degree 2 * m ; ::_thesis: ( not emb ((2 * m),L) <> 0. L or ((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = p *' q )
assume A3: emb ((2 * m),L) <> 0. L ; ::_thesis: ((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = p *' q
((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = ((emb ((2 * m),L)) ") * (DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m))) by Th34
.= ((emb ((2 * m),L)) ") * ((emb ((2 * m),L)) * (p *' q)) by A1, A2, Th43
.= (((emb ((2 * m),L)) ") * (emb ((2 * m),L))) * (p *' q) by Th10
.= (1. L) * (p *' q) by A3, VECTSP_1:def_10
.= p *' q by POLYNOM5:27 ;
hence ((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = p *' q ; ::_thesis: verum
end;