set Mx = Mx2Tran (M,b1,B2);
per cases ( len b1 = 0 or len b1 > 0 ) ;
suppose A1: len b1 = 0 ; :: thesis: ( Mx2Tran (M,b1,B2) is homogeneous & Mx2Tran (M,b1,B2) is additive )
A2: now :: thesis: for a being Scalar of K
for v1 being Vector of V1 holds (Mx2Tran (M,b1,B2)) . (a * v1) = a * ((Mx2Tran (M,b1,B2)) . v1)
let a be Scalar of K; :: thesis: for v1 being Vector of V1 holds (Mx2Tran (M,b1,B2)) . (a * v1) = a * ((Mx2Tran (M,b1,B2)) . v1)
let v1 be Vector of V1; :: thesis: (Mx2Tran (M,b1,B2)) . (a * v1) = a * ((Mx2Tran (M,b1,B2)) . v1)
thus (Mx2Tran (M,b1,B2)) . (a * v1) = 0. V2 by A1, Th33
.= a * (0. V2) by VECTSP_1:14
.= a * ((Mx2Tran (M,b1,B2)) . v1) by A1, Th33 ; :: thesis: verum
end;
now :: thesis: for v1, w1 being Vector of V1 holds (Mx2Tran (M,b1,B2)) . (v1 + w1) = ((Mx2Tran (M,b1,B2)) . v1) + ((Mx2Tran (M,b1,B2)) . w1)
let v1, w1 be Vector of V1; :: thesis: (Mx2Tran (M,b1,B2)) . (v1 + w1) = ((Mx2Tran (M,b1,B2)) . v1) + ((Mx2Tran (M,b1,B2)) . w1)
thus (Mx2Tran (M,b1,B2)) . (v1 + w1) = 0. V2 by A1, Th33
.= (0. V2) + (0. V2) by RLVECT_1:def 4
.= ((Mx2Tran (M,b1,B2)) . v1) + (0. V2) by A1, Th33
.= ((Mx2Tran (M,b1,B2)) . v1) + ((Mx2Tran (M,b1,B2)) . w1) by A1, Th33 ; :: thesis: verum
end;
then ( Mx2Tran (M,b1,B2) is additive & Mx2Tran (M,b1,B2) is homogeneous ) by A2, MOD_2:def 2;
hence ( Mx2Tran (M,b1,B2) is homogeneous & Mx2Tran (M,b1,B2) is additive ) ; :: thesis: verum
end;
suppose A3: len b1 > 0 ; :: thesis: ( Mx2Tran (M,b1,B2) is homogeneous & Mx2Tran (M,b1,B2) is additive )
A4: now :: thesis: for v1, w1 being Vector of V1 holds (Mx2Tran (M,b1,B2)) . (v1 + w1) = ((Mx2Tran (M,b1,B2)) . v1) + ((Mx2Tran (M,b1,B2)) . w1)
let v1, w1 be Vector of V1; :: thesis: (Mx2Tran (M,b1,B2)) . (v1 + w1) = ((Mx2Tran (M,b1,B2)) . v1) + ((Mx2Tran (M,b1,B2)) . w1)
set vb = v1 |-- b1;
set wb = w1 |-- b1;
set vwb = (v1 + w1) |-- b1;
set Lvw = LineVec2Mx ((v1 + w1) |-- b1);
set Lv = LineVec2Mx (v1 |-- b1);
set Lw = LineVec2Mx (w1 |-- b1);
set LLvw = Line (((LineVec2Mx ((v1 + w1) |-- b1)) * M),1);
set LLv = Line (((LineVec2Mx (v1 |-- b1)) * M),1);
set LLw = Line (((LineVec2Mx (w1 |-- b1)) * M),1);
A5: len (LineVec2Mx (w1 |-- b1)) = 1 by MATRIX_0:23;
A6: len b1 = len (v1 |-- b1) by MATRLIN:def 7;
A7: len M = len b1 by A3, MATRIX_0:23;
A8: width (LineVec2Mx (v1 |-- b1)) = len (v1 |-- b1) by MATRIX_0:23;
then A9: width ((LineVec2Mx (v1 |-- b1)) * M) = width M by A7, A6, MATRIX_3:def 4;
then A10: len (Line (((LineVec2Mx (v1 |-- b1)) * M),1)) = width M by CARD_1:def 7;
A11: len (LineVec2Mx (v1 |-- b1)) = 1 by MATRIX_0:23;
then A12: len ((LineVec2Mx (v1 |-- b1)) * M) = 1 by A8, A7, A6, MATRIX_3:def 4;
A13: len b1 = len (w1 |-- b1) by MATRLIN:def 7;
( width (LineVec2Mx ((v1 + w1) |-- b1)) = len ((v1 + w1) |-- b1) & len b1 = len ((v1 + w1) |-- b1) ) by MATRIX_0:23, MATRLIN:def 7;
then width ((LineVec2Mx ((v1 + w1) |-- b1)) * M) = width M by A7, MATRIX_3:def 4;
then A14: len (Line (((LineVec2Mx ((v1 + w1) |-- b1)) * M),1)) = width M by CARD_1:def 7;
A15: dom (lmlt ((Line (((LineVec2Mx ((v1 + w1) |-- b1)) * M),1)),B2)) = (dom (Line (((LineVec2Mx ((v1 + w1) |-- b1)) * M),1))) /\ (dom B2) by Lm1
.= (dom (Line (((LineVec2Mx (v1 |-- b1)) * M),1))) /\ (dom B2) by A14, A10, FINSEQ_3:29
.= dom (lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2)) by Lm1 ;
A16: width (LineVec2Mx (w1 |-- b1)) = len (w1 |-- b1) by MATRIX_0:23;
then A17: width ((LineVec2Mx (w1 |-- b1)) * M) = width M by A7, A13, MATRIX_3:def 4;
then A18: len (Line (((LineVec2Mx (w1 |-- b1)) * M),1)) = width M by CARD_1:def 7;
A19: dom (lmlt ((Line (((LineVec2Mx ((v1 + w1) |-- b1)) * M),1)),B2)) = (dom (Line (((LineVec2Mx ((v1 + w1) |-- b1)) * M),1))) /\ (dom B2) by Lm1
.= (dom (Line (((LineVec2Mx (w1 |-- b1)) * M),1))) /\ (dom B2) by A14, A18, FINSEQ_3:29
.= dom (lmlt ((Line (((LineVec2Mx (w1 |-- b1)) * M),1)),B2)) by Lm1 ;
then A20: len (lmlt ((Line (((LineVec2Mx ((v1 + w1) |-- b1)) * M),1)),B2)) = len (lmlt ((Line (((LineVec2Mx (w1 |-- b1)) * M),1)),B2)) by FINSEQ_3:29;
LineVec2Mx ((v1 + w1) |-- b1) = LineVec2Mx ((v1 |-- b1) + (w1 |-- b1)) by Th17
.= (LineVec2Mx (v1 |-- b1)) + (LineVec2Mx (w1 |-- b1)) by A6, A13, MATRIX15:27 ;
then (LineVec2Mx ((v1 + w1) |-- b1)) * M = ((LineVec2Mx (v1 |-- b1)) * M) + ((LineVec2Mx (w1 |-- b1)) * M) by A3, A11, A8, A5, A16, A7, A6, A13, MATRIX_4:63;
then Line (((LineVec2Mx ((v1 + w1) |-- b1)) * M),1) = (Line (((LineVec2Mx (v1 |-- b1)) * M),1)) + (Line (((LineVec2Mx (w1 |-- b1)) * M),1)) by A12, A9, A17, Lm5;
then A21: lmlt ((Line (((LineVec2Mx ((v1 + w1) |-- b1)) * M),1)),B2) = (lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2)) + (lmlt ((Line (((LineVec2Mx (w1 |-- b1)) * M),1)),B2)) by Th7;
A22: now :: thesis: for i being Nat st i in dom (lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2)) holds
(lmlt ((Line (((LineVec2Mx ((v1 + w1) |-- b1)) * M),1)),B2)) . i = ((lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2)) /. i) + ((lmlt ((Line (((LineVec2Mx (w1 |-- b1)) * M),1)),B2)) /. i)
let i be Nat; :: thesis: ( i in dom (lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2)) implies (lmlt ((Line (((LineVec2Mx ((v1 + w1) |-- b1)) * M),1)),B2)) . i = ((lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2)) /. i) + ((lmlt ((Line (((LineVec2Mx (w1 |-- b1)) * M),1)),B2)) /. i) )
assume A23: i in dom (lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2)) ; :: thesis: (lmlt ((Line (((LineVec2Mx ((v1 + w1) |-- b1)) * M),1)),B2)) . i = ((lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2)) /. i) + ((lmlt ((Line (((LineVec2Mx (w1 |-- b1)) * M),1)),B2)) /. i)
( (lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2)) /. i = (lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2)) . i & (lmlt ((Line (((LineVec2Mx (w1 |-- b1)) * M),1)),B2)) /. i = (lmlt ((Line (((LineVec2Mx (w1 |-- b1)) * M),1)),B2)) . i ) by A15, A19, A23, PARTFUN1:def 6;
hence (lmlt ((Line (((LineVec2Mx ((v1 + w1) |-- b1)) * M),1)),B2)) . i = ((lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2)) /. i) + ((lmlt ((Line (((LineVec2Mx (w1 |-- b1)) * M),1)),B2)) /. i) by A21, A15, A23, FVSUM_1:17; :: thesis: verum
end;
len (lmlt ((Line (((LineVec2Mx ((v1 + w1) |-- b1)) * M),1)),B2)) = len (lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2)) by A15, FINSEQ_3:29;
then Sum (lmlt ((Line (((LineVec2Mx ((v1 + w1) |-- b1)) * M),1)),B2)) = (Sum (lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2))) + (Sum (lmlt ((Line (((LineVec2Mx (w1 |-- b1)) * M),1)),B2))) by A20, A22, RLVECT_2:2;
hence (Mx2Tran (M,b1,B2)) . (v1 + w1) = (Sum (lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2))) + (Sum (lmlt ((Line (((LineVec2Mx (w1 |-- b1)) * M),1)),B2))) by Def3
.= ((Mx2Tran (M,b1,B2)) . v1) + (Sum (lmlt ((Line (((LineVec2Mx (w1 |-- b1)) * M),1)),B2))) by Def3
.= ((Mx2Tran (M,b1,B2)) . v1) + ((Mx2Tran (M,b1,B2)) . w1) by Def3 ;
:: thesis: verum
end;
now :: thesis: for a being Scalar of K
for v1 being Vector of V1 holds (Mx2Tran (M,b1,B2)) . (a * v1) = a * ((Mx2Tran (M,b1,B2)) . v1)
let a be Scalar of K; :: thesis: for v1 being Vector of V1 holds (Mx2Tran (M,b1,B2)) . (a * v1) = a * ((Mx2Tran (M,b1,B2)) . v1)
let v1 be Vector of V1; :: thesis: (Mx2Tran (M,b1,B2)) . (a * v1) = a * ((Mx2Tran (M,b1,B2)) . v1)
set vb = v1 |-- b1;
set avb = (a * v1) |-- b1;
set Lav = LineVec2Mx ((a * v1) |-- b1);
set Lv = LineVec2Mx (v1 |-- b1);
set LLav = Line (((LineVec2Mx ((a * v1) |-- b1)) * M),1);
set LLv = Line (((LineVec2Mx (v1 |-- b1)) * M),1);
A24: len M = len b1 by A3, MATRIX_0:23;
( width (LineVec2Mx ((a * v1) |-- b1)) = len ((a * v1) |-- b1) & len b1 = len ((a * v1) |-- b1) ) by MATRIX_0:23, MATRLIN:def 7;
then width ((LineVec2Mx ((a * v1) |-- b1)) * M) = width M by A24, MATRIX_3:def 4;
then A25: len (Line (((LineVec2Mx ((a * v1) |-- b1)) * M),1)) = width M by CARD_1:def 7;
A26: ( width (LineVec2Mx (v1 |-- b1)) = len (v1 |-- b1) & len b1 = len (v1 |-- b1) ) by MATRIX_0:23, MATRLIN:def 7;
then width ((LineVec2Mx (v1 |-- b1)) * M) = width M by A24, MATRIX_3:def 4;
then len (Line (((LineVec2Mx (v1 |-- b1)) * M),1)) = width M by CARD_1:def 7;
then A27: dom (Line (((LineVec2Mx ((a * v1) |-- b1)) * M),1)) = dom (Line (((LineVec2Mx (v1 |-- b1)) * M),1)) by A25, FINSEQ_3:29;
LineVec2Mx ((a * v1) |-- b1) = LineVec2Mx (a * (v1 |-- b1)) by Th18
.= a * (LineVec2Mx (v1 |-- b1)) by MATRIX15:29 ;
then A28: (LineVec2Mx ((a * v1) |-- b1)) * M = a * ((LineVec2Mx (v1 |-- b1)) * M) by A24, A26, MATRIX15:1;
A29: dom (lmlt ((Line (((LineVec2Mx ((a * v1) |-- b1)) * M),1)),B2)) = (dom (Line (((LineVec2Mx ((a * v1) |-- b1)) * M),1))) /\ (dom B2) by Lm1;
A30: (dom (Line (((LineVec2Mx (v1 |-- b1)) * M),1))) /\ (dom B2) = dom (lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2)) by Lm1;
len (LineVec2Mx (v1 |-- b1)) = 1 by MATRIX_0:23;
then len ((LineVec2Mx (v1 |-- b1)) * M) = 1 by A24, A26, MATRIX_3:def 4;
then A31: Line (((LineVec2Mx ((a * v1) |-- b1)) * M),1) = a * (Line (((LineVec2Mx (v1 |-- b1)) * M),1)) by A28, MATRIXR1:20;
A32: now :: thesis: for i being Nat st i in dom (lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2)) holds
(lmlt ((Line (((LineVec2Mx ((a * v1) |-- b1)) * M),1)),B2)) . i = a * ((lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2)) /. i)
let i be Nat; :: thesis: ( i in dom (lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2)) implies (lmlt ((Line (((LineVec2Mx ((a * v1) |-- b1)) * M),1)),B2)) . i = a * ((lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2)) /. i) )
assume A33: i in dom (lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2)) ; :: thesis: (lmlt ((Line (((LineVec2Mx ((a * v1) |-- b1)) * M),1)),B2)) . i = a * ((lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2)) /. i)
A34: (lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2)) . i = (lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2)) /. i by A33, PARTFUN1:def 6;
i in dom (Line (((LineVec2Mx (v1 |-- b1)) * M),1)) by A30, A33, XBOOLE_0:def 4;
then A35: (Line (((LineVec2Mx (v1 |-- b1)) * M),1)) . i = (Line (((LineVec2Mx (v1 |-- b1)) * M),1)) /. i by PARTFUN1:def 6;
i in dom B2 by A30, A33, XBOOLE_0:def 4;
then A36: B2 . i = B2 /. i by PARTFUN1:def 6;
A37: i in dom (Line (((LineVec2Mx ((a * v1) |-- b1)) * M),1)) by A27, A30, A33, XBOOLE_0:def 4;
then A38: (Line (((LineVec2Mx ((a * v1) |-- b1)) * M),1)) . i = (Line (((LineVec2Mx ((a * v1) |-- b1)) * M),1)) /. i by PARTFUN1:def 6;
hence (lmlt ((Line (((LineVec2Mx ((a * v1) |-- b1)) * M),1)),B2)) . i = the lmult of V2 . (((Line (((LineVec2Mx ((a * v1) |-- b1)) * M),1)) /. i),(B2 /. i)) by A29, A27, A30, A33, A36, FUNCOP_1:22
.= (a * ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)) /. i)) * (B2 /. i) by A31, A37, A35, A38, FVSUM_1:50
.= a * (((Line (((LineVec2Mx (v1 |-- b1)) * M),1)) /. i) * (B2 /. i)) by VECTSP_1:def 16
.= a * ((lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2)) /. i) by A33, A35, A36, A34, FUNCOP_1:22 ;
:: thesis: verum
end;
len (lmlt ((Line (((LineVec2Mx ((a * v1) |-- b1)) * M),1)),B2)) = len (lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2)) by A29, A27, A30, FINSEQ_3:29;
then Sum (lmlt ((Line (((LineVec2Mx ((a * v1) |-- b1)) * M),1)),B2)) = a * (Sum (lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2))) by A32, RLVECT_2:67;
hence (Mx2Tran (M,b1,B2)) . (a * v1) = a * (Sum (lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2))) by Def3
.= a * ((Mx2Tran (M,b1,B2)) . v1) by Def3 ;
:: thesis: verum
end;
then ( Mx2Tran (M,b1,B2) is additive & Mx2Tran (M,b1,B2) is homogeneous ) by A4, MOD_2:def 2;
hence ( Mx2Tran (M,b1,B2) is homogeneous & Mx2Tran (M,b1,B2) is additive ) ; :: thesis: verum
end;
end;