let l, n, k be Nat; for K being Field
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 Field; 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_1:25;
A4:
len A = n
by MATRIX_1:25;
dom (1. K,n) =
Seg (len (1. K,n))
by FINSEQ_1:def 3
.=
Seg (len A)
by A4, MATRIX_1:25
.=
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_1:25;
A7:
width A = n
by MATRIX_1:25;
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_1:25;
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:106;
A14:
Indices ((RLineXS (1. K,n),l,k,a) * A) = [:(Seg n),(Seg n):]
by MATRIX_1:25;
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:106;
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:17;
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_1:def 8;
then
[l,t] in Indices (1. K,n)
by A1, ZFMISC_1:106;
hence
(Line (1. K,n),l) . t = 0. K
by A21, MATRIX_3:17;
verum
end;
reconsider q =
Col A,
j as
Element of
(width A) -tuples_on the
carrier of
K by A4, MATRIX_1:25;
A22:
len (Col A,j) = len A
by MATRIX_1:def 9;
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_1:def 8;
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_1:def 8;
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 FINSEQ_1:def 18;
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 FINSEQ_1:def 18;
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:17;
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_1:def 8;
then
[k,t] in Indices (1. K,n)
by A2, ZFMISC_1:106;
hence
(Line (1. K,n),k) . t = 0. K
by A31, MATRIX_3:17;
verum
end;
A32:
dom (1. K,n) =
Seg (len (1. K,n))
by FINSEQ_1:def 3
.=
Seg (len A)
by A4, MATRIX_1:25
.=
dom A
by FINSEQ_1:def 3
;
then
(Col A,j) . k = A * k,
j
by A2, MATRIX_1:def 9;
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_1:def 9;
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:106;
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:83
.=
(Sum (a * (mlt p1,q))) + (Sum (mlt p2,q))
by FVSUM_1:95
.=
(a * (Sum (mlt (Line (1. K,n),k),(Col A,j)))) + (Sum (mlt (Line (1. K,n),l),(Col A,j)))
by FVSUM_1:92
.=
(a * a1) + (Sum (mlt (Line (1. K,n),l),(Col A,j)))
by A24, A23, A29, A33, MATRIX_3:19
.=
(a * a1) + a2
by A26, A25, A19, A35, MATRIX_3:19
.=
(a * (A * k,j)) + (A * l,j)
by A2, A32, A33, A34, A35, MATRIX_1:def 9
.=
(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:106;
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:17;
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_1:def 8;
then
[i,t] in Indices (1. K,n)
by A39, ZFMISC_1:106;
hence
(Line (1. K,n),i) . t = 0. K
by A44, MATRIX_3:17;
verum
end;
len (Col A,j) = len A
by MATRIX_1:def 9;
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_1:25
.=
dom A
by FINSEQ_1:def 3
;
len (Line (1. K,n),i) = width (1. K,n)
by MATRIX_1:def 8;
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:106;
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:19
.=
A * i,
j
by A39, A46, MATRIX_1:def 9
.=
(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:106;
dom (1. K,n) =
Seg (len (1. K,n))
by FINSEQ_1:def 3
.=
Seg n
by MATRIX_1:25
;
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_1:21; verum