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_0:def 7

.= m by MATRIX_0:24

.= len (VM ((x "),m)) by MATRIX_0:24

.= len (Col ((VM ((x "),m)),j)) by MATRIX_0: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_0:def 7

.= m by MATRIX_0: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)))

(mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) /. k = s /. k

(mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) . k = s . k

.= 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_0:24;

then A33: width (VM (x,m)) = len (VM ((x "),m)) by MATRIX_0:24;

A34: ( width (VM (x,m)) = m & len (VM ((x "),m)) = m ) by MATRIX_0:24;

len (VM (x,m)) = m by MATRIX_0:24;

then A35: len ((VM (x,m)) * (VM ((x "),m))) = m by A34, MATRIX_3:def 4;

width (VM ((x "),m)) = m by MATRIX_0: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_0:20;

then A36: Indices ((VM (x,m)) * (VM ((x "),m))) = [:(Seg m),(Seg m):] by MATRIX_0: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

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_0:def 7

.= m by MATRIX_0:24

.= len (VM ((x "),m)) by MATRIX_0:24

.= len (Col ((VM ((x "),m)),j)) by MATRIX_0: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_0:def 7

.= m by MATRIX_0: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

A20:
for k being Nat st 1 <= k & k <= m holds
len (Col ((VM ((x "),m)),j)) =
len (VM ((x "),m))
by MATRIX_0:def 8

.= m by MATRIX_0: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_0:def 7

.= m by MATRIX_0: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, MATRIX_0:24;

then A15: k in dom (VM ((x "),m)) by FINSEQ_1:def 3;

k in Seg m by A13, A14;

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_0:24;

then k in Seg (width (VM (x,m))) by A13, A14;

then A18: (Line ((VM (x,m)),i)) . k = (VM (x,m)) * (i,k) by MATRIX_0:def 7;

k in Seg m by A13, A14;

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, Def7

.= 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_0: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, Def7

.= 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;.= m by MATRIX_0: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_0:def 7

.= m by MATRIX_0: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, MATRIX_0:24;

then A15: k in dom (VM ((x "),m)) by FINSEQ_1:def 3;

k in Seg m by A13, A14;

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_0:24;

then k in Seg (width (VM (x,m))) by A13, A14;

then A18: (Line ((VM (x,m)),i)) . k = (VM (x,m)) * (i,k) by MATRIX_0:def 7;

k in Seg m by A13, A14;

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, Def7

.= 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_0: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, Def7

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

(mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) /. k = s /. k

proof

A27:
for k being Nat st k in dom (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) holds
len (Col ((VM ((x "),m)),j)) =
len (VM ((x "),m))
by MATRIX_0:def 8

.= m by MATRIX_0: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_0:def 7

.= m by MATRIX_0: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;

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;

k in Seg m by A23;

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;.= m by MATRIX_0: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_0:def 7

.= m by MATRIX_0: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;

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;

k in Seg m by A23;

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

(mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) . k = s . k

proof

dom (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) =
Seg m
by A7, FINSEQ_1:def 3
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;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

.= 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_0:24;

then A33: width (VM (x,m)) = len (VM ((x "),m)) by MATRIX_0:24;

A34: ( width (VM (x,m)) = m & len (VM ((x "),m)) = m ) by MATRIX_0:24;

len (VM (x,m)) = m by MATRIX_0:24;

then A35: len ((VM (x,m)) * (VM ((x "),m))) = m by A34, MATRIX_3:def 4;

width (VM ((x "),m)) = m by MATRIX_0: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_0:20;

then A36: Indices ((VM (x,m)) * (VM ((x "),m))) = [:(Seg m),(Seg m):] by MATRIX_0: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