let n, m, k be Nat; :: thesis: for A being Matrix of n,m,F_Real
for B being Matrix of width A,k,F_Real st ( n = 0 implies m = 0 ) & ( m = 0 implies k = 0 ) holds
(Mx2Tran B) * (Mx2Tran A) = Mx2Tran (A * B)
let A be Matrix of n,m,F_Real; :: thesis: for B being Matrix of width A,k,F_Real st ( n = 0 implies m = 0 ) & ( m = 0 implies k = 0 ) holds
(Mx2Tran B) * (Mx2Tran A) = Mx2Tran (A * B)
let B be Matrix of width A,k,F_Real; :: thesis: ( ( n = 0 implies m = 0 ) & ( m = 0 implies k = 0 ) implies (Mx2Tran B) * (Mx2Tran A) = Mx2Tran (A * B) )
assume that
A1: ( n = 0 implies m = 0 ) and
A2: ( m = 0 implies k = 0 ) ; :: thesis: (Mx2Tran B) * (Mx2Tran A) = Mx2Tran (A * B)
reconsider Bk = MX2FinS (1. (F_Real,k)) as OrdBasis of k -VectSp_over F_Real by MATRLIN2:45;
reconsider Bm = MX2FinS (1. (F_Real,m)) as OrdBasis of m -VectSp_over F_Real by MATRLIN2:45;
reconsider Bn = MX2FinS (1. (F_Real,n)) as OrdBasis of n -VectSp_over F_Real by MATRLIN2:45;
A3: len A = n by A1, MATRIX13:1;
A4: len Bk = k by Th19;
A5: len Bm = m by Th19;
A6: len Bn = n by Th19;
then reconsider A1 = A as Matrix of len Bn, len Bm,F_Real by A5;
A7: Mx2Tran A = Mx2Tran (A1,Bn,Bm) by Th20;
A8: width A = m by A1, MATRIX13:1;
then A9: width B = k by A2, MATRIX13:1;
then reconsider AB = A * B as Matrix of len Bn, len Bk,F_Real by A3, A6, A4;
len Bm = m by Th19;
then reconsider B1 = B as Matrix of len Bm, len Bk,F_Real by A8, A4;
A10: len B1 = m by A2, A8, MATRIX13:1;
Mx2Tran (A * B) = Mx2Tran (AB,Bn,Bk) by A3, A9, Th20;
then Mx2Tran (A * B) = (Mx2Tran (B1,Bm,Bk)) * (Mx2Tran (A1,Bn,Bm)) by A8, A10, MATRLIN2:40;
hence (Mx2Tran B) * (Mx2Tran A) = Mx2Tran (A * B) by A8, A7, Th20; :: thesis: verum