let n, m, k be Nat; :: thesis: for f being n -element real-valued FinSequence
for A being Matrix of n,m,F_Real
for B being Matrix of k,m,F_Real holds
( (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f & (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f )
let f be n -element real-valued FinSequence; :: thesis: for A being Matrix of n,m,F_Real
for B being Matrix of k,m,F_Real holds
( (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f & (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f )
let A be Matrix of n,m,F_Real; :: thesis: for B being Matrix of k,m,F_Real holds
( (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f & (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f )
let B be Matrix of k,m,F_Real; :: thesis: ( (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f & (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f )
reconsider k0 = k |-> 0 as k -element FinSequence of REAL ;
A1: len B = k by MATRIX_1:def 2;
set kf = k0 ^ f;
per cases ( n <> 0 or n = 0 ) ;
suppose A2: n <> 0 ; :: thesis: ( (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f & (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f )
then A3: width A = m by MATRIX13:1;
A4: ( len f = n & len k0 = k ) by CARD_1:def 7;
then len (k0 ^ f) = n + k by FINSEQ_1:22;
then A5: k0 ^ f is n + k -element by CARD_1:def 7;
A6: len A = n by A2, MATRIX13:1;
thus (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f :: thesis: (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f
proof
set fk = f ^ k0;
len (f ^ k0) = n + k by A4, FINSEQ_1:22;
then A7: f ^ k0 is n + k -element by CARD_1:def 7;
per cases ( k = 0 or k <> 0 ) ;
suppose A8: k = 0 ; :: thesis: (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f
then B is empty by A1;
then A9: Mx2Tran (A ^ B) = Mx2Tran A by A8, FINSEQ_1:34;
k0 is empty by A8;
hence (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f by A9, FINSEQ_1:34; :: thesis: verum
end;
suppose A10: k <> 0 ; :: thesis: (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f
set Mab = Mx2Tran (A ^ B);
set Ma = Mx2Tran A;
A11: width B = m by A10, MATRIX_1:23;
A12: now
let i be Nat; :: thesis: ( 1 <= i & i <= m implies ((Mx2Tran A) . f) . i = ((Mx2Tran (A ^ B)) . (f ^ k0)) . i )
reconsider S1 = Sum (mlt ((@ k0),(Col (B,i)))), S2 = Sum (mlt ((@ f),(Col (A,i)))) as Element of F_Real ;
assume A13: ( 1 <= i & i <= m ) ; :: thesis: ((Mx2Tran A) . f) . i = ((Mx2Tran (A ^ B)) . (f ^ k0)) . i
then A14: i in Seg m by FINSEQ_1:1;
mlt ((@ k0),(Col (B,i))) = (0. F_Real) * (Col (B,i)) by A1, FVSUM_1:66
.= k |-> (0. F_Real) by A1, FVSUM_1:58 ;
then A15: Sum (mlt ((@ k0),(Col (B,i)))) = Sum (k |-> 0) by MATRPROB:36
.= 0. F_Real by RVSUM_1:81 ;
A16: ( len (Col (A,i)) = n & len (Col (B,i)) = k ) by A6, A1, MATRIX_1:def 8;
mlt ((@ (f ^ k0)),(Col ((A ^ B),i))) = mlt (((@ f) ^ (@ k0)),((Col (A,i)) ^ (Col (B,i)))) by A3, A11, A14, MATRLIN:26
.= (mlt ((@ f),(Col (A,i)))) ^ (mlt ((@ k0),(Col (B,i)))) by A4, A16, MATRIX14:7 ;
then Sum (mlt ((@ (f ^ k0)),(Col ((A ^ B),i)))) = addreal . ((Sum (mlt ((@ f),(Col (A,i))))),(Sum (mlt ((@ k0),(Col (B,i)))))) by FINSOP_1:5
.= (Sum (mlt ((@ f),(Col (A,i))))) + (Sum (mlt ((@ k0),(Col (B,i))))) by BINOP_2:def 9
.= (@ f) "*" (Col (A,i)) by A15 ;
hence ((Mx2Tran A) . f) . i = (@ (f ^ k0)) "*" (Col ((A ^ B),i)) by A2, A13, Th18
.= ((Mx2Tran (A ^ B)) . (f ^ k0)) . i by A2, A7, A13, Th18 ;
:: thesis: verum
end;
( len ((Mx2Tran (A ^ B)) . (f ^ k0)) = m & len ((Mx2Tran A) . f) = m ) by A7, CARD_1:def 7;
hence (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f by A12, FINSEQ_1:14; :: thesis: verum
end;
end;
end;
per cases ( k = 0 or k <> 0 ) ;
suppose A19: k <> 0 ; :: thesis: (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f
set Mba = Mx2Tran (B ^ A);
set Ma = Mx2Tran A;
A20: width B = m by A19, MATRIX_1:23;
A21: now
let i be Nat; :: thesis: ( 1 <= i & i <= m implies ((Mx2Tran A) . f) . i = ((Mx2Tran (B ^ A)) . (k0 ^ f)) . i )
reconsider S1 = Sum (mlt ((@ k0),(Col (B,i)))), S2 = Sum (mlt ((@ f),(Col (A,i)))) as Element of F_Real ;
assume A22: ( 1 <= i & i <= m ) ; :: thesis: ((Mx2Tran A) . f) . i = ((Mx2Tran (B ^ A)) . (k0 ^ f)) . i
then A23: i in Seg m by FINSEQ_1:1;
mlt ((@ k0),(Col (B,i))) = (0. F_Real) * (Col (B,i)) by A1, FVSUM_1:66
.= k |-> (0. F_Real) by A1, FVSUM_1:58 ;
then A24: Sum (mlt ((@ k0),(Col (B,i)))) = Sum (k |-> 0) by MATRPROB:36
.= 0. F_Real by RVSUM_1:81 ;
A25: ( len (Col (A,i)) = n & len (Col (B,i)) = k ) by A6, A1, MATRIX_1:def 8;
mlt ((@ (k0 ^ f)),(Col ((B ^ A),i))) = mlt (((@ k0) ^ (@ f)),((Col (B,i)) ^ (Col (A,i)))) by A3, A20, A23, MATRLIN:26
.= (mlt ((@ k0),(Col (B,i)))) ^ (mlt ((@ f),(Col (A,i)))) by A4, A25, MATRIX14:7 ;
then Sum (mlt ((@ (k0 ^ f)),(Col ((B ^ A),i)))) = addreal . ((Sum (mlt ((@ k0),(Col (B,i))))),(Sum (mlt ((@ f),(Col (A,i)))))) by FINSOP_1:5
.= (Sum (mlt ((@ f),(Col (A,i))))) + (0. F_Real) by A24, BINOP_2:def 9
.= (@ f) "*" (Col (A,i)) ;
hence ((Mx2Tran A) . f) . i = (@ (k0 ^ f)) "*" (Col ((B ^ A),i)) by A2, A22, Th18
.= ((Mx2Tran (B ^ A)) . (k0 ^ f)) . i by A2, A5, A22, Th18 ;
:: thesis: verum
end;
( len ((Mx2Tran (B ^ A)) . (k0 ^ f)) = m & len ((Mx2Tran A) . f) = m ) by A5, CARD_1:def 7;
hence (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f by A21, FINSEQ_1:14; :: thesis: verum
end;
end;
end;
suppose A26: n = 0 ; :: thesis: ( (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f & (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f )
A27: 0. (TOP-REAL k) = 0* k by EUCLID:70
.= k |-> 0 ;
f = {} by A26;
then A28: ( f ^ (k |-> 0) = k |-> 0 & (k |-> 0) ^ f = k |-> 0 ) by FINSEQ_1:34;
thus (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = 0. (TOP-REAL m) by A27, A28, Th29, A26
.= (Mx2Tran A) . f by A26, Def3 ; :: thesis: (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f
thus (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = 0. (TOP-REAL m) by A27, A28, Th29, A26
.= (Mx2Tran A) . f by A26, Def3 ; :: thesis: verum
end;
end;