let K be Field; :: thesis: for A being Matrix of K holds (0. K,(len A),(len A)) * A = 0. K,(len A),(width A)
let A be Matrix of K; :: thesis: (0. K,(len A),(len A)) * A = 0. K,(len A),(width A)
per cases
( len A > 0 or len A = 0 )
by NAT_1:3;
suppose A1:
len A > 0
;
:: thesis: (0. K,(len A),(len A)) * A = 0. K,(len A),(width A)A2:
(
len (0. K,(len A),(len A)) = len A &
len (0. K,(len A),(width A)) = len A )
by MATRIX_1:def 3;
then A3:
(
width (0. K,(len A),(len A)) = len A &
width (0. K,(len A),(width A)) = width A )
by A1, MATRIX_1:20;
then A4:
(
len ((0. K,(len A),(len A)) * A) = len A &
len ((0. K,(len A),(len A)) * A) = len (0. K,(len A),(width A)) )
by A2, MATRIX_3:def 4;
A5:
width ((0. K,(len A),(len A)) * A) = width A
by A3, MATRIX_3:def 4;
A6:
len (- ((0. K,(len A),(len A)) * A)) = len ((0. K,(len A),(len A)) * A)
by MATRIX_3:def 2;
A7:
width (- ((0. K,(len A),(len A)) * A)) = width ((0. K,(len A),(len A)) * A)
by MATRIX_3:def 2;
A8:
(0. K,(len A),(len A)) * A =
((0. K,(len A),(len A)) + (0. K,(len A),(len A))) * A
by MATRIX_3:6
.=
((0. K,(len A),(len A)) * A) + ((0. K,(len A),(len A)) * A)
by A1, A2, A3, MATRIX_4:63
;
set B =
(0. K,(len A),(len A)) * A;
0. K,
(len A),
(width A) = (((0. K,(len A),(len A)) * A) + ((0. K,(len A),(len A)) * A)) + (- ((0. K,(len A),(len A)) * A))
by A4, A5, A8, MATRIX_4:2;
then 0. K,
(len A),
(width A) =
((0. K,(len A),(len A)) * A) + (((0. K,(len A),(len A)) * A) - ((0. K,(len A),(len A)) * A))
by A6, A7, MATRIX_3:5
.=
(0. K,(len A),(len A)) * A
by A4, A7, MATRIX_4:20
;
hence
(0. K,(len A),(len A)) * A = 0. K,
(len A),
(width A)
;
:: thesis: verum end; suppose A9:
len A = 0
;
:: thesis: (0. K,(len A),(len A)) * A = 0. K,(len A),(width A)then
len (0. K,(len A),(len A)) = 0
by MATRIX_1:def 3;
then
width (0. K,(len A),(len A)) = len A
by A9, MATRIX_1:def 4;
then A10:
len ((0. K,(len A),(len A)) * A) = len (0. K,(len A),(len A))
by MATRIX_3:def 4;
A11:
len (0. K,(len A),(len A)) = len A
by MATRIX_1:def 3;
len (0. K,(len A),(width A)) = len A
by MATRIX_1:def 3;
hence
(0. K,(len A),(len A)) * A = 0. K,
(len A),
(width A)
by A9, A10, A11, CARD_2:83;
:: thesis: verum end;