let k, l, n be Nat; for K being comRing
for a being Element of K
for A being Matrix of n,K st l in dom (1. (K,n)) & k in dom (1. (K,n)) holds
(RLineXS ((1. (K,n)),l,k,a)) * A = RLineXS (A,l,k,a)
let K be comRing; for a being Element of K
for A being Matrix of n,K st l in dom (1. (K,n)) & k in dom (1. (K,n)) holds
(RLineXS ((1. (K,n)),l,k,a)) * A = RLineXS (A,l,k,a)
let a be Element of K; for A being Matrix of n,K st l in dom (1. (K,n)) & k in dom (1. (K,n)) holds
(RLineXS ((1. (K,n)),l,k,a)) * A = RLineXS (A,l,k,a)
let A be Matrix of n,K; ( l in dom (1. (K,n)) & k in dom (1. (K,n)) implies (RLineXS ((1. (K,n)),l,k,a)) * A = RLineXS (A,l,k,a) )
assume that
A1:
l in dom (1. (K,n))
and
A2:
k in dom (1. (K,n))
; (RLineXS ((1. (K,n)),l,k,a)) * A = RLineXS (A,l,k,a)
set B = RLineXS ((1. (K,n)),l,k,a);
A3:
len (RLineXS ((1. (K,n)),l,k,a)) = n
by MATRIX_0:24;
A4:
len A = n
by MATRIX_0:24;
dom (1. (K,n)) =
Seg (len (1. (K,n)))
by FINSEQ_1:def 3
.=
Seg (len A)
by A4, MATRIX_0:24
.=
dom A
by FINSEQ_1:def 3
;
then A5:
len (RLineXS (A,l,k,a)) = len A
by A2, Def3;
A6:
( len ((RLineXS ((1. (K,n)),l,k,a)) * A) = n & width ((RLineXS ((1. (K,n)),l,k,a)) * A) = n )
by MATRIX_0:24;
A7:
width A = n
by MATRIX_0:24;
A8:
len (RLineXS ((1. (K,n)),l,k,a)) = len (1. (K,n))
by A2, Def3;
then A9:
l in Seg n
by A1, A3, FINSEQ_1:def 3;
A10:
width (RLineXS ((1. (K,n)),l,k,a)) = n
by MATRIX_0:24;
A11:
width (RLineXS ((1. (K,n)),l,k,a)) = width (1. (K,n))
by Th1;
then A12:
l in Seg (width (1. (K,n)))
by A1, A8, A3, A10, FINSEQ_1:def 3;
then A13:
[l,l] in Indices (1. (K,n))
by A1, ZFMISC_1:87;
A14:
Indices ((RLineXS ((1. (K,n)),l,k,a)) * A) = [:(Seg n),(Seg n):]
by MATRIX_0:24;
A15:
k in Seg (width (1. (K,n)))
by A2, A8, A11, A3, A10, FINSEQ_1:def 3;
then A16:
[k,k] in Indices (1. (K,n))
by A2, ZFMISC_1:87;
A17:
for i, j being Nat st j in Seg n & i in dom (1. (K,n)) & i = l holds
((RLineXS ((1. (K,n)),l,k,a)) * A) * (i,j) = (RLineXS (A,l,k,a)) * (i,j)
proof
let i,
j be
Nat;
( j in Seg n & i in dom (1. (K,n)) & i = l implies ((RLineXS ((1. (K,n)),l,k,a)) * A) * (i,j) = (RLineXS (A,l,k,a)) * (i,j) )
assume that A18:
j in Seg n
and
i in dom (1. (K,n))
;
( not i = l or ((RLineXS ((1. (K,n)),l,k,a)) * A) * (i,j) = (RLineXS (A,l,k,a)) * (i,j) )
thus
(
i = l implies
((RLineXS ((1. (K,n)),l,k,a)) * A) * (
i,
j)
= (RLineXS (A,l,k,a)) * (
i,
j) )
verumproof
A19:
(
(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 A13, 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 A20:
t in dom (Line ((1. (K,n)),l))
and A21:
t <> l
;
(Line ((1. (K,n)),l)) . t = 0. K
t in Seg (len (Line ((1. (K,n)),l)))
by A20, 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 A21, MATRIX_3:15;
verum
end;
reconsider q =
Col (
A,
j) as
Element of
(width A) -tuples_on the
carrier of
K by A4, MATRIX_0:24;
A22:
len (Col (A,j)) = len A
by MATRIX_0:def 8;
k in Seg n
by A2, A8, A3, FINSEQ_1:def 3;
then A23:
k in dom (Col (A,j))
by A4, A22, FINSEQ_1:def 3;
len (Line ((1. (K,n)),k)) = width (1. (K,n))
by MATRIX_0:def 7;
then A24:
k in dom (Line ((1. (K,n)),k))
by A15, FINSEQ_1:def 3;
l in Seg n
by A1, A8, A3, FINSEQ_1:def 3;
then A25:
l in dom (Col (A,j))
by A4, A22, FINSEQ_1:def 3;
len (Line ((1. (K,n)),l)) = width (1. (K,n))
by MATRIX_0:def 7;
then A26:
l in dom (Line ((1. (K,n)),l))
by A12, FINSEQ_1:def 3;
reconsider p2 =
Line (
(1. (K,n)),
l) as
Element of
(width A) -tuples_on the
carrier of
K by Th1;
A27:
len q = width A
by CARD_1:def 7;
reconsider p1 =
Line (
(1. (K,n)),
k) as
Element of
(width A) -tuples_on the
carrier of
K by Th1;
A28:
(
len (a * p1) = width A &
len p2 = width A )
by CARD_1:def 7;
A29:
(
(Line ((1. (K,n)),k)) . k = 1_ K & ( for
t being
Nat st
t in dom (Line ((1. (K,n)),k)) &
t <> k holds
(Line ((1. (K,n)),k)) . t = 0. K ) )
proof
thus
(Line ((1. (K,n)),k)) . k = 1_ K
by A16, MATRIX_3:15;
for t being Nat st t in dom (Line ((1. (K,n)),k)) & t <> k holds
(Line ((1. (K,n)),k)) . t = 0. K
let t be
Nat;
( t in dom (Line ((1. (K,n)),k)) & t <> k implies (Line ((1. (K,n)),k)) . t = 0. K )
assume that A30:
t in dom (Line ((1. (K,n)),k))
and A31:
t <> k
;
(Line ((1. (K,n)),k)) . t = 0. K
t in Seg (len (Line ((1. (K,n)),k)))
by A30, FINSEQ_1:def 3;
then
t in Seg (width (1. (K,n)))
by MATRIX_0:def 7;
then
[k,t] in Indices (1. (K,n))
by A2, ZFMISC_1:87;
hence
(Line ((1. (K,n)),k)) . t = 0. K
by A31, MATRIX_3:15;
verum
end;
A32:
dom (1. (K,n)) =
Seg (len (1. (K,n)))
by FINSEQ_1:def 3
.=
Seg (len A)
by A4, MATRIX_0:24
.=
dom A
by FINSEQ_1:def 3
;
then
(Col (A,j)) . k = A * (
k,
j)
by A2, MATRIX_0:def 8;
then consider a1 being
Element of
K such that A33:
a1 = (Col (A,j)) . k
;
A34:
(Col (A,j)) . l = A * (
l,
j)
by A1, A32, MATRIX_0:def 8;
then consider a2 being
Element of
K such that A35:
a2 = (Col (A,j)) . l
;
assume A36:
i = l
;
((RLineXS ((1. (K,n)),l,k,a)) * A) * (i,j) = (RLineXS (A,l,k,a)) * (i,j)
then
[i,j] in Indices ((RLineXS ((1. (K,n)),l,k,a)) * A)
by A9, A14, A18, ZFMISC_1:87;
then ((RLineXS ((1. (K,n)),l,k,a)) * A) * (
i,
j) =
(Line ((RLineXS ((1. (K,n)),l,k,a)),i)) "*" (Col (A,j))
by A10, A4, MATRIX_3:def 4
.=
Sum (mlt (((a * p1) + p2),q))
by A1, A2, A36, Th5
.=
Sum ((mlt ((a * p1),q)) + (mlt (p2,q)))
by A28, A27, MATRIX_4:56
.=
Sum ((a * (mlt (p1,q))) + (mlt (p2,q)))
by FVSUM_1:69
.=
(Sum (a * (mlt (p1,q)))) + (Sum (mlt (p2,q)))
by FVSUM_1:76
.=
(a * (Sum (mlt ((Line ((1. (K,n)),k)),(Col (A,j)))))) + (Sum (mlt ((Line ((1. (K,n)),l)),(Col (A,j)))))
by FVSUM_1:73
.=
(a * a1) + (Sum (mlt ((Line ((1. (K,n)),l)),(Col (A,j)))))
by A24, A23, A29, A33, MATRIX_3:17
.=
(a * a1) + a2
by A26, A25, A19, A35, MATRIX_3:17
.=
(a * (A * (k,j))) + (A * (l,j))
by A2, A32, A33, A34, A35, MATRIX_0:def 8
.=
(RLineXS (A,l,k,a)) * (
i,
j)
by A1, A2, A7, A18, A36, A32, Def3
;
hence
((RLineXS ((1. (K,n)),l,k,a)) * A) * (
i,
j)
= (RLineXS (A,l,k,a)) * (
i,
j)
;
verum
end;
end;
A37:
for i, j being Nat st j in Seg n & i in dom (1. (K,n)) & i <> l holds
((RLineXS ((1. (K,n)),l,k,a)) * A) * (i,j) = (RLineXS (A,l,k,a)) * (i,j)
proof
let i,
j be
Nat;
( j in Seg n & i in dom (1. (K,n)) & i <> l implies ((RLineXS ((1. (K,n)),l,k,a)) * A) * (i,j) = (RLineXS (A,l,k,a)) * (i,j) )
assume that A38:
j in Seg n
and A39:
i in dom (1. (K,n))
;
( not i <> l or ((RLineXS ((1. (K,n)),l,k,a)) * A) * (i,j) = (RLineXS (A,l,k,a)) * (i,j) )
A40:
i in Seg n
by A8, A3, A39, FINSEQ_1:def 3;
then A41:
[i,i] in Indices (1. (K,n))
by A11, A10, A39, ZFMISC_1:87;
thus
(
i <> l implies
((RLineXS ((1. (K,n)),l,k,a)) * A) * (
i,
j)
= (RLineXS (A,l,k,a)) * (
i,
j) )
verumproof
A42:
(
(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 A41, 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 A43:
t in dom (Line ((1. (K,n)),i))
and A44:
t <> i
;
(Line ((1. (K,n)),i)) . t = 0. K
t in Seg (len (Line ((1. (K,n)),i)))
by A43, 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 A39, ZFMISC_1:87;
hence
(Line ((1. (K,n)),i)) . t = 0. K
by A44, MATRIX_3:15;
verum
end;
len (Col (A,j)) = len A
by MATRIX_0:def 8;
then A45:
i in dom (Col (A,j))
by A4, A40, FINSEQ_1:def 3;
A46:
dom (1. (K,n)) =
Seg (len (1. (K,n)))
by FINSEQ_1:def 3
.=
Seg (len A)
by A4, 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 A47:
i in dom (Line ((1. (K,n)),i))
by A11, A10, A40, FINSEQ_1:def 3;
assume A48:
i <> l
;
((RLineXS ((1. (K,n)),l,k,a)) * A) * (i,j) = (RLineXS (A,l,k,a)) * (i,j)
[i,j] in Indices ((RLineXS ((1. (K,n)),l,k,a)) * A)
by A14, A38, A40, ZFMISC_1:87;
then ((RLineXS ((1. (K,n)),l,k,a)) * A) * (
i,
j) =
(Line ((RLineXS ((1. (K,n)),l,k,a)),i)) "*" (Col (A,j))
by A10, A4, MATRIX_3:def 4
.=
Sum (mlt ((Line ((1. (K,n)),i)),(Col (A,j))))
by A1, A2, A39, A48, Th5
.=
(Col (A,j)) . i
by A47, A45, A42, MATRIX_3:17
.=
A * (
i,
j)
by A39, A46, MATRIX_0:def 8
.=
(RLineXS (A,l,k,a)) * (
i,
j)
by A2, A7, A38, A39, A48, A46, Def3
;
hence
((RLineXS ((1. (K,n)),l,k,a)) * A) * (
i,
j)
= (RLineXS (A,l,k,a)) * (
i,
j)
;
verum
end;
end;
A49:
for i, j being Nat st [i,j] in Indices ((RLineXS ((1. (K,n)),l,k,a)) * A) holds
((RLineXS ((1. (K,n)),l,k,a)) * A) * (i,j) = (RLineXS (A,l,k,a)) * (i,j)
proof
let i,
j be
Nat;
( [i,j] in Indices ((RLineXS ((1. (K,n)),l,k,a)) * A) implies ((RLineXS ((1. (K,n)),l,k,a)) * A) * (i,j) = (RLineXS (A,l,k,a)) * (i,j) )
assume
[i,j] in Indices ((RLineXS ((1. (K,n)),l,k,a)) * A)
;
((RLineXS ((1. (K,n)),l,k,a)) * A) * (i,j) = (RLineXS (A,l,k,a)) * (i,j)
then A50:
(
i in Seg n &
j in Seg n )
by A14, ZFMISC_1:87;
dom (1. (K,n)) =
Seg (len (1. (K,n)))
by FINSEQ_1:def 3
.=
Seg n
by MATRIX_0:24
;
hence
((RLineXS ((1. (K,n)),l,k,a)) * A) * (
i,
j)
= (RLineXS (A,l,k,a)) * (
i,
j)
by A17, A37, A50;
verum
end;
width (RLineXS (A,l,k,a)) = width A
by Th1;
hence
(RLineXS ((1. (K,n)),l,k,a)) * A = RLineXS (A,l,k,a)
by A4, A7, A6, A5, A49, MATRIX_0:21; verum