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

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

hence
(VM (x,m)) * (VM ((x "),m)) = (emb (m,L)) * (1. (L,m))
by A1, Th36; :: thesis: verum
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))) ) )

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

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

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

then consider s being FinSequence of L such that
defpred S_{1}[ 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 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(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;A4: 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

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

A11:
Indices (1. (L,m)) = [:(Seg m),(Seg m):]
by MATRIX_0:24;
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;

k in Seg m by A9;

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

then A10: k in dom s by A5;

k in Seg m by A9;

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

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

per cases
( i = j or i <> j )
;

end;

suppose A14:
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

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

hence ((VM (x,m)) * (VM ((x "),m))) * (i,j) = (emb (m,L)) * ((1. (L,m)) * (i,j)) by A14, A16, MATRIX_1:def 3; :: thesis: verum

end;s /. k = 1. L

proof

i in Seg m
by A12;
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;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

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

hence ((VM (x,m)) * (VM ((x "),m))) * (i,j) = (emb (m,L)) * ((1. (L,m)) * (i,j)) by A14, A16, MATRIX_1:def 3; :: thesis: verum

suppose A17:
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;

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

hence ((VM (x,m)) * (VM ((x "),m))) * (i,j) = (emb (m,L)) * ((1. (L,m)) * (i,j)) by A17, A18, MATRIX_1:def 3; :: thesis: verum

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

hence ((VM (x,m)) * (VM ((x "),m))) * (i,j) = (emb (m,L)) * ((1. (L,m)) * (i,j)) by A17, A18, MATRIX_1:def 3; :: thesis: verum