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 Def2

.= pow ((1. L),(i - j)) by A3

.= 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))) ) )

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)))

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)

.= ((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 Def2

.= ((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 ;

hence ((VM (x,m)) * (VM ((x "),m))) * (i,j) = 0. L by A2, A3, A9, A13, Th37; :: thesis: verum

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 Def2

.= pow ((1. L),(i - j)) by A3

.= 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

then consider s being FinSequence of L such that
defpred S_{1}[ 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 S_{1}[n,x]
;

ex G being FinSequence of L st

( dom G = Seg m & ( for nn being Nat st nn in Seg m holds

S_{1}[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;A6: for n being Nat st n in Seg m holds

ex x being Element of L st S

ex G being FinSequence of L st

( dom G = Seg m & ( for nn being Nat st nn in Seg m holds

S

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

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

consider r being Element of L such that
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;

k in Seg m by A10;

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;assume A10: ( 1 <= k & k <= m ) ; :: thesis: s /. k = pow (x,((i - j) * (k - 1)))

then A11: k in dom s by A7;

k in Seg m by A10;

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

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

then Sum s =
((1. L) - ((pow (x,(i - j))) |^ (len s))) / ((1. L) - (pow (x,(i - j))))
by A1, A2, A3, Th5, Th32
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 Def2 ;

hence s . k = (pow (x,(i - j))) |^ (k -' 1) ; :: thesis: verum

end;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 Def2 ;

hence s . k = (pow (x,(i - j))) |^ (k -' 1) ; :: thesis: verum

.= ((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 Def2

.= ((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 ;

hence ((VM (x,m)) * (VM ((x "),m))) * (i,j) = 0. L by A2, A3, A9, A13, Th37; :: thesis: verum