let n be Nat; for K being comRing
for l being Nat
for a being Element of K
for A being Matrix of n,K st l in dom (1. (K,n)) holds
(SXLine ((1. (K,n)),l,a)) * A = SXLine (A,l,a)
let K be comRing; for l being Nat
for a being Element of K
for A being Matrix of n,K st l in dom (1. (K,n)) holds
(SXLine ((1. (K,n)),l,a)) * A = SXLine (A,l,a)
let l be Nat; for a being Element of K
for A being Matrix of n,K st l in dom (1. (K,n)) holds
(SXLine ((1. (K,n)),l,a)) * A = SXLine (A,l,a)
let a be Element of K; for A being Matrix of n,K st l in dom (1. (K,n)) holds
(SXLine ((1. (K,n)),l,a)) * A = SXLine (A,l,a)
let A be Matrix of n,K; ( l in dom (1. (K,n)) implies (SXLine ((1. (K,n)),l,a)) * A = SXLine (A,l,a) )
assume A1:
l in dom (1. (K,n))
; (SXLine ((1. (K,n)),l,a)) * A = SXLine (A,l,a)
set B = SXLine ((1. (K,n)),l,a);
A2:
( len (SXLine ((1. (K,n)),l,a)) = len (1. (K,n)) & len (SXLine ((1. (K,n)),l,a)) = n )
by Def2, MATRIX_0:24;
then A3:
l in Seg n
by A1, FINSEQ_1:def 3;
A4:
width (SXLine ((1. (K,n)),l,a)) = n
by MATRIX_0:24;
A5:
width A = n
by MATRIX_0:24;
A6:
len A = n
by MATRIX_0:24;
A7:
Indices ((SXLine ((1. (K,n)),l,a)) * A) = [:(Seg n),(Seg n):]
by MATRIX_0:24;
A8:
width (SXLine ((1. (K,n)),l,a)) = width (1. (K,n))
by Th1;
then A9:
l in Seg (width (1. (K,n)))
by A1, A2, A4, FINSEQ_1:def 3;
then A10:
[l,l] in Indices (1. (K,n))
by A1, ZFMISC_1:87;
A11:
for i, j being Nat st j in Seg n & i in dom (1. (K,n)) & i = l holds
((SXLine ((1. (K,n)),l,a)) * A) * (i,j) = (SXLine (A,l,a)) * (i,j)
proof
let i,
j be
Nat;
( j in Seg n & i in dom (1. (K,n)) & i = l implies ((SXLine ((1. (K,n)),l,a)) * A) * (i,j) = (SXLine (A,l,a)) * (i,j) )
assume that A12:
j in Seg n
and A13:
i in dom (1. (K,n))
;
( not i = l or ((SXLine ((1. (K,n)),l,a)) * A) * (i,j) = (SXLine (A,l,a)) * (i,j) )
thus
(
i = l implies
((SXLine ((1. (K,n)),l,a)) * A) * (
i,
j)
= (SXLine (A,l,a)) * (
i,
j) )
verumproof
reconsider p =
Line (
(1. (K,n)),
l) as
Element of
(width A) -tuples_on the
carrier of
K by Th1;
reconsider q =
Col (
A,
j) as
Element of
(width A) -tuples_on the
carrier of
K by A6, MATRIX_0:24;
len (Line ((1. (K,n)),l)) = width (1. (K,n))
by MATRIX_0:def 7;
then A14:
l in dom (Line ((1. (K,n)),l))
by A9, FINSEQ_1:def 3;
(
len (Col (A,j)) = len A &
l in Seg n )
by A1, A2, FINSEQ_1:def 3, MATRIX_0:def 8;
then A15:
l in dom (Col (A,j))
by A6, FINSEQ_1:def 3;
A16:
(
(Line ((1. (K,n)),l)) . l = 1_ K & ( for
t being
Nat st
t in dom (Line ((1. (K,n)),l)) &
t <> l holds
(Line ((1. (K,n)),l)) . t = 0. K ) )
proof
thus
(Line ((1. (K,n)),l)) . l = 1_ K
by A10, MATRIX_3:15;
for t being Nat st t in dom (Line ((1. (K,n)),l)) & t <> l holds
(Line ((1. (K,n)),l)) . t = 0. K
let t be
Nat;
( t in dom (Line ((1. (K,n)),l)) & t <> l implies (Line ((1. (K,n)),l)) . t = 0. K )
assume that A17:
t in dom (Line ((1. (K,n)),l))
and A18:
t <> l
;
(Line ((1. (K,n)),l)) . t = 0. K
t in Seg (len (Line ((1. (K,n)),l)))
by A17, FINSEQ_1:def 3;
then
t in Seg (width (1. (K,n)))
by MATRIX_0:def 7;
then
[l,t] in Indices (1. (K,n))
by A1, ZFMISC_1:87;
hence
(Line ((1. (K,n)),l)) . t = 0. K
by A18, MATRIX_3:15;
verum
end;
A19:
dom (1. (K,n)) =
Seg (len (1. (K,n)))
by FINSEQ_1:def 3
.=
Seg (len A)
by A6, MATRIX_0:24
.=
dom A
by FINSEQ_1:def 3
;
then
(Col (A,j)) . l = A * (
l,
j)
by A1, MATRIX_0:def 8;
then consider a1 being
Element of
K such that A20:
a1 = (Col (A,j)) . l
;
assume A21:
i = l
;
((SXLine ((1. (K,n)),l,a)) * A) * (i,j) = (SXLine (A,l,a)) * (i,j)
then
[i,j] in Indices ((SXLine ((1. (K,n)),l,a)) * A)
by A3, A7, A12, ZFMISC_1:87;
then ((SXLine ((1. (K,n)),l,a)) * A) * (
i,
j) =
(Line ((SXLine ((1. (K,n)),l,a)),i)) "*" (Col (A,j))
by A4, A6, MATRIX_3:def 4
.=
Sum (mlt ((a * p),q))
by A1, A21, Th4
.=
Sum (a * (mlt (p,q)))
by FVSUM_1:69
.=
a * (Sum (mlt ((Line ((1. (K,n)),l)),(Col (A,j)))))
by FVSUM_1:73
.=
a * a1
by A14, A15, A16, A20, MATRIX_3:17
.=
a * (A * (l,j))
by A1, A19, A20, MATRIX_0:def 8
.=
(SXLine (A,l,a)) * (
i,
j)
by A5, A12, A13, A21, A19, Def2
;
hence
((SXLine ((1. (K,n)),l,a)) * A) * (
i,
j)
= (SXLine (A,l,a)) * (
i,
j)
;
verum
end;
end;
A22:
for i, j being Nat st j in Seg n & i in dom (1. (K,n)) & i <> l holds
((SXLine ((1. (K,n)),l,a)) * A) * (i,j) = (SXLine (A,l,a)) * (i,j)
proof
let i,
j be
Nat;
( j in Seg n & i in dom (1. (K,n)) & i <> l implies ((SXLine ((1. (K,n)),l,a)) * A) * (i,j) = (SXLine (A,l,a)) * (i,j) )
assume that A23:
j in Seg n
and A24:
i in dom (1. (K,n))
;
( not i <> l or ((SXLine ((1. (K,n)),l,a)) * A) * (i,j) = (SXLine (A,l,a)) * (i,j) )
A25:
i in Seg n
by A2, A24, FINSEQ_1:def 3;
then A26:
[i,i] in Indices (1. (K,n))
by A8, A4, A24, ZFMISC_1:87;
thus
(
i <> l implies
((SXLine ((1. (K,n)),l,a)) * A) * (
i,
j)
= (SXLine (A,l,a)) * (
i,
j) )
verumproof
A27:
(
(Line ((1. (K,n)),i)) . i = 1_ K & ( for
t being
Nat st
t in dom (Line ((1. (K,n)),i)) &
t <> i holds
(Line ((1. (K,n)),i)) . t = 0. K ) )
proof
thus
(Line ((1. (K,n)),i)) . i = 1_ K
by A26, MATRIX_3:15;
for t being Nat st t in dom (Line ((1. (K,n)),i)) & t <> i holds
(Line ((1. (K,n)),i)) . t = 0. K
let t be
Nat;
( t in dom (Line ((1. (K,n)),i)) & t <> i implies (Line ((1. (K,n)),i)) . t = 0. K )
assume that A28:
t in dom (Line ((1. (K,n)),i))
and A29:
t <> i
;
(Line ((1. (K,n)),i)) . t = 0. K
t in Seg (len (Line ((1. (K,n)),i)))
by A28, FINSEQ_1:def 3;
then
t in Seg (width (1. (K,n)))
by MATRIX_0:def 7;
then
[i,t] in Indices (1. (K,n))
by A24, ZFMISC_1:87;
hence
(Line ((1. (K,n)),i)) . t = 0. K
by A29, MATRIX_3:15;
verum
end;
len (Col (A,j)) = len A
by MATRIX_0:def 8;
then A30:
i in dom (Col (A,j))
by A6, A25, FINSEQ_1:def 3;
A31:
dom (1. (K,n)) =
Seg (len (1. (K,n)))
by FINSEQ_1:def 3
.=
Seg (len A)
by A6, MATRIX_0:24
.=
dom A
by FINSEQ_1:def 3
;
len (Line ((1. (K,n)),i)) = width (1. (K,n))
by MATRIX_0:def 7;
then A32:
i in dom (Line ((1. (K,n)),i))
by A8, A4, A25, FINSEQ_1:def 3;
assume A33:
i <> l
;
((SXLine ((1. (K,n)),l,a)) * A) * (i,j) = (SXLine (A,l,a)) * (i,j)
[i,j] in Indices ((SXLine ((1. (K,n)),l,a)) * A)
by A7, A23, A25, ZFMISC_1:87;
then ((SXLine ((1. (K,n)),l,a)) * A) * (
i,
j) =
(Line ((SXLine ((1. (K,n)),l,a)),i)) "*" (Col (A,j))
by A4, A6, MATRIX_3:def 4
.=
Sum (mlt ((Line ((1. (K,n)),i)),(Col (A,j))))
by A1, A24, A33, Th4
.=
(Col (A,j)) . i
by A32, A30, A27, MATRIX_3:17
.=
A * (
i,
j)
by A24, A31, MATRIX_0:def 8
.=
(SXLine (A,l,a)) * (
i,
j)
by A5, A23, A24, A33, A31, Def2
;
hence
((SXLine ((1. (K,n)),l,a)) * A) * (
i,
j)
= (SXLine (A,l,a)) * (
i,
j)
;
verum
end;
end;
A34:
for i, j being Nat st [i,j] in Indices ((SXLine ((1. (K,n)),l,a)) * A) holds
((SXLine ((1. (K,n)),l,a)) * A) * (i,j) = (SXLine (A,l,a)) * (i,j)
proof
let i,
j be
Nat;
( [i,j] in Indices ((SXLine ((1. (K,n)),l,a)) * A) implies ((SXLine ((1. (K,n)),l,a)) * A) * (i,j) = (SXLine (A,l,a)) * (i,j) )
assume
[i,j] in Indices ((SXLine ((1. (K,n)),l,a)) * A)
;
((SXLine ((1. (K,n)),l,a)) * A) * (i,j) = (SXLine (A,l,a)) * (i,j)
then A35:
(
i in Seg n &
j in Seg n )
by A7, ZFMISC_1:87;
dom (1. (K,n)) =
Seg (len (1. (K,n)))
by FINSEQ_1:def 3
.=
Seg n
by MATRIX_0:24
;
hence
((SXLine ((1. (K,n)),l,a)) * A) * (
i,
j)
= (SXLine (A,l,a)) * (
i,
j)
by A11, A22, A35;
verum
end;
A36:
( len ((SXLine ((1. (K,n)),l,a)) * A) = n & width ((SXLine ((1. (K,n)),l,a)) * A) = n )
by MATRIX_0:24;
( len (SXLine (A,l,a)) = len A & width (SXLine (A,l,a)) = width A )
by Def2, Th1;
hence
(SXLine ((1. (K,n)),l,a)) * A = SXLine (A,l,a)
by A6, A5, A36, A34, MATRIX_0:21; verum