let n, m, k be Nat; for f being n -element real-valued FinSequence
for A being Matrix of n,k,F_Real
for B being Matrix of n,m,F_Real st ( n = 0 implies k + m = 0 ) holds
(Mx2Tran (A ^^ B)) . f = ((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)
let f be n -element real-valued FinSequence; for A being Matrix of n,k,F_Real
for B being Matrix of n,m,F_Real st ( n = 0 implies k + m = 0 ) holds
(Mx2Tran (A ^^ B)) . f = ((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)
let A be Matrix of n,k,F_Real; for B being Matrix of n,m,F_Real st ( n = 0 implies k + m = 0 ) holds
(Mx2Tran (A ^^ B)) . f = ((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)
let B be Matrix of n,m,F_Real; ( ( n = 0 implies k + m = 0 ) implies (Mx2Tran (A ^^ B)) . f = ((Mx2Tran A) . f) ^ ((Mx2Tran B) . f) )
set L = LineVec2Mx (@ f);
set MAB = (Mx2Tran (A ^^ B)) . f;
set MA = (Mx2Tran A) . f;
set MB = (Mx2Tran B) . f;
A1:
len ((Mx2Tran A) . f) = k
by CARD_1:def 7;
assume A2:
( n = 0 implies k + m = 0 )
; (Mx2Tran (A ^^ B)) . f = ((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)
then
( n = 0 implies k = 0 )
;
then A3:
width A = k
by MATRIX13:1;
( n = 0 implies m = 0 )
by A2;
then A4:
width B = m
by MATRIX13:1;
A5:
len ((Mx2Tran B) . f) = m
by CARD_1:def 7;
then A6:
len (((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) = k + m
by A1, FINSEQ_1:22;
A7:
for i being Nat st 1 <= i & i <= k + m holds
(((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) . i = ((Mx2Tran (A ^^ B)) . f) . i
proof
let i be
Nat;
( 1 <= i & i <= k + m implies (((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) . i = ((Mx2Tran (A ^^ B)) . f) . i )
assume that A8:
1
<= i
and A9:
i <= k + m
;
(((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) . i = ((Mx2Tran (A ^^ B)) . f) . i
A10:
i in dom (((Mx2Tran A) . f) ^ ((Mx2Tran B) . f))
by A6, A8, A9, FINSEQ_3:25;
A11:
((Mx2Tran (A ^^ B)) . f) . i = (@ f) "*" (Col ((A ^^ B),i))
by A2, A3, A4, A8, A9, Th18;
per cases
( i in dom ((Mx2Tran A) . f) or ex j being Nat st
( j in dom ((Mx2Tran B) . f) & i = (len ((Mx2Tran A) . f)) + j ) )
by A10, FINSEQ_1:25;
suppose A12:
i in dom ((Mx2Tran A) . f)
;
(((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) . i = ((Mx2Tran (A ^^ B)) . f) . ithen
i <= k
by A1, FINSEQ_3:25;
then A13:
((Mx2Tran A) . f) . i = (@ f) "*" (Col (A,i))
by A2, A8, Th18;
(
i in Seg (width A) &
(((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) . i = ((Mx2Tran A) . f) . i )
by A3, A1, A12, FINSEQ_1:def 3, FINSEQ_1:def 7;
hence
(((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) . i = ((Mx2Tran (A ^^ B)) . f) . i
by A11, A13, MATRIX15:16;
verum end; suppose
ex
j being
Nat st
(
j in dom ((Mx2Tran B) . f) &
i = (len ((Mx2Tran A) . f)) + j )
;
(((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) . i = ((Mx2Tran (A ^^ B)) . f) . ithen consider j being
Nat such that A14:
j in dom ((Mx2Tran B) . f)
and A15:
i = (len ((Mx2Tran A) . f)) + j
;
( 1
<= j &
j <= m )
by A5, A14, FINSEQ_3:25;
then A16:
((Mx2Tran B) . f) . j = (@ f) "*" (Col (B,j))
by A2, Th18;
(
j in Seg (width B) &
(((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) . i = ((Mx2Tran B) . f) . j )
by A4, A5, A14, A15, FINSEQ_1:def 3, FINSEQ_1:def 7;
hence
(((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) . i = ((Mx2Tran (A ^^ B)) . f) . i
by A3, A1, A11, A15, A16, MATRIX15:17;
verum end;
end;
len ((Mx2Tran (A ^^ B)) . f) = k + m
by A3, A4, CARD_1:def 7;
hence
(Mx2Tran (A ^^ B)) . f = ((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)
by A6, A7; verum