let L be 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
let x be 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 s be 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 i, j, m be Element of NAT ; ( 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)))
; ((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
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;
( 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
;
((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)))
;
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_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;
( 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 )
;
(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;
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;
( 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))))
;
(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
;
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_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; verum