let n, m, k, i be Nat; :: thesis: for K being Field
for a being Element of K
for X being Matrix of K
for A' being Matrix of m,n,K
for B' being Matrix of m,k,K st X in Solutions_of A',B' holds
X in Solutions_of (RLine A',i,(a * (Line A',i))),(RLine B',i,(a * (Line B',i)))
let K be Field; :: thesis: for a being Element of K
for X being Matrix of K
for A' being Matrix of m,n,K
for B' being Matrix of m,k,K st X in Solutions_of A',B' holds
X in Solutions_of (RLine A',i,(a * (Line A',i))),(RLine B',i,(a * (Line B',i)))
let a be Element of K; :: thesis: for X being Matrix of K
for A' being Matrix of m,n,K
for B' being Matrix of m,k,K st X in Solutions_of A',B' holds
X in Solutions_of (RLine A',i,(a * (Line A',i))),(RLine B',i,(a * (Line B',i)))
let X be Matrix of K; :: thesis: for A' being Matrix of m,n,K
for B' being Matrix of m,k,K st X in Solutions_of A',B' holds
X in Solutions_of (RLine A',i,(a * (Line A',i))),(RLine B',i,(a * (Line B',i)))
let A' be Matrix of m,n,K; :: thesis: for B' being Matrix of m,k,K st X in Solutions_of A',B' holds
X in Solutions_of (RLine A',i,(a * (Line A',i))),(RLine B',i,(a * (Line B',i)))
let B' be Matrix of m,k,K; :: thesis: ( X in Solutions_of A',B' implies X in Solutions_of (RLine A',i,(a * (Line A',i))),(RLine B',i,(a * (Line B',i))) )
assume A1:
X in Solutions_of A',B'
; :: thesis: X in Solutions_of (RLine A',i,(a * (Line A',i))),(RLine B',i,(a * (Line B',i)))
then consider X1 being Matrix of K such that
A2:
( X = X1 & len X1 = width A' & width X1 = width B' )
and
A3:
A' * X1 = B'
;
set LA = Line A',i;
set LB = Line B',i;
set RA = RLine A',i,(a * (Line A',i));
set RB = RLine B',i,(a * (Line B',i));
set RX = (RLine A',i,(a * (Line A',i))) * X1;
A4:
( len (a * (Line A',i)) = len (Line A',i) & len (Line A',i) = width A' & len (a * (Line B',i)) = len (Line B',i) & len (Line B',i) = width B' & len A' = len B' )
by A1, Th33, FINSEQ_1:def 18, MATRIXR1:16;
then A5:
( len (RLine A',i,(a * (Line A',i))) = len A' & width (RLine A',i,(a * (Line A',i))) = width A' & len (RLine B',i,(a * (Line B',i))) = len B' & width (RLine B',i,(a * (Line B',i))) = width B' )
by MATRIX11:def 3;
then A6:
( len ((RLine A',i,(a * (Line A',i))) * X1) = len (RLine A',i,(a * (Line A',i))) & width ((RLine A',i,(a * (Line A',i))) * X1) = width X1 )
by A2, MATRIX_3:def 4;
dom B' = Seg (len (RLine A',i,(a * (Line A',i))))
by A4, A5, FINSEQ_1:def 3;
then A7:
( Indices ((RLine A',i,(a * (Line A',i))) * X1) = Indices B' & Indices (RLine B',i,(a * (Line B',i))) = Indices B' )
by A2, A6, FINSEQ_1:def 3, MATRIX_1:27;
now let j,
k be
Nat;
:: thesis: ( [j,k] in Indices (RLine B',i,(a * (Line B',i))) implies (RLine B',i,(a * (Line B',i))) * j,k = ((RLine A',i,(a * (Line A',i))) * X1) * j,k )assume A8:
[j,k] in Indices (RLine B',i,(a * (Line B',i)))
;
:: thesis: (RLine B',i,(a * (Line B',i))) * j,k = ((RLine A',i,(a * (Line A',i))) * X1) * j,k
len B' = m
by MATRIX_1:def 3;
then A9:
(
j in dom B' &
dom B' = Seg m &
k in Seg (width B') &
len (Line B',i) = width B' )
by A7, A8, FINSEQ_1:def 3, MATRIX_1:def 8, ZFMISC_1:106;
then
B' * i,
k = (Line B',i) . k
by MATRIX_1:def 8;
then reconsider LBk =
(Line B',i) . k as
Element of
K ;
A10:
B' * j,
k = (Line A',j) "*" (Col X1,k)
by A2, A3, A7, A8, MATRIX_3:def 4;
now per cases
( j = i or j <> i )
;
suppose A11:
j = i
;
:: thesis: ((RLine A',i,(a * (Line A',i))) * X1) * j,k = (RLine B',i,(a * (Line B',i))) * j,kthen
Line (RLine A',i,(a * (Line A',i))),
i = a * (Line A',i)
by A4, A9, MATRIX11:28;
hence ((RLine A',i,(a * (Line A',i))) * X1) * j,
k =
(a * (Line A',i)) "*" (Col X1,k)
by A2, A5, A7, A8, A11, MATRIX_3:def 4
.=
Sum (a * (mlt (Line A',i),(Col X1,k)))
by A2, FVSUM_1:82
.=
a * (Sum (mlt (Line A',i),(Col X1,k)))
by FVSUM_1:92
.=
a * LBk
by A9, A10, A11, MATRIX_1:def 8
.=
(a * (Line B',i)) . k
by A9, FVSUM_1:63
.=
(RLine B',i,(a * (Line B',i))) * j,
k
by A11, A4, A7, A8, MATRIX11:def 3
;
:: thesis: verum end; suppose A12:
j <> i
;
:: thesis: ((RLine A',i,(a * (Line A',i))) * X1) * j,k = (RLine B',i,(a * (Line B',i))) * j,kthen
Line (RLine A',i,(a * (Line A',i))),
j = Line A',
j
by A9, MATRIX11:28;
hence ((RLine A',i,(a * (Line A',i))) * X1) * j,
k =
(Line A',j) "*" (Col X1,k)
by A2, A5, A7, A8, MATRIX_3:def 4
.=
B' * j,
k
by A2, A3, A7, A8, MATRIX_3:def 4
.=
(RLine B',i,(a * (Line B',i))) * j,
k
by A12, A4, A7, A8, MATRIX11:def 3
;
:: thesis: verum end; hence
(RLine B',i,(a * (Line B',i))) * j,
k = ((RLine A',i,(a * (Line A',i))) * X1) * j,
k
;
:: thesis: verum end;
then
(RLine A',i,(a * (Line A',i))) * X1 = RLine B',i,(a * (Line B',i))
by A2, A4, A5, A6, MATRIX_1:21;
hence
X in Solutions_of (RLine A',i,(a * (Line A',i))),(RLine B',i,(a * (Line B',i)))
by A2, A5; :: thesis: verum