let M be Matrix of 3,F_Real; for N being Matrix of 3,1,F_Real st N = <*<*0*>,<*0*>,<*0*>*> holds
M * N = <*<*0*>,<*0*>,<*0*>*>
let N be Matrix of 3,1,F_Real; ( N = <*<*0*>,<*0*>,<*0*>*> implies M * N = <*<*0*>,<*0*>,<*0*>*> )
assume A1:
N = <*<*0*>,<*0*>,<*0*>*>
; M * N = <*<*0*>,<*0*>,<*0*>*>
A2:
( len M = 3 & width M = 3 )
by MATRIX_0:23;
A3:
( len N = 3 & width N = 1 )
by MATRIX_0:23;
width M = len N
by A3, MATRIX_0:23;
then A4A:
( len (M * N) = len M & width (M * N) = width N )
by MATRIX_3:def 4;
then A4:
( len (M * N) = 3 & width (M * N) = 1 )
by MATRIX_0:23;
then A5:
M * N is Matrix of 3,1,F_Real
by MATRIX_0:20;
now ( len (Line (M,1)) = 3 & (Line (M,1)) . 1 = M * (1,1) & (Line (M,1)) . 2 = M * (1,2) & (Line (M,1)) . 3 = M * (1,3) )thus len (Line (M,1)) =
width M
by MATRIX_0:def 7
.=
3
by MATRIX_0:23
;
( (Line (M,1)) . 1 = M * (1,1) & (Line (M,1)) . 2 = M * (1,2) & (Line (M,1)) . 3 = M * (1,3) )
( 1
in Seg (width M) & 2
in Seg (width M) & 3
in Seg (width M) )
by A2, FINSEQ_1:1;
hence
(
(Line (M,1)) . 1
= M * (1,1) &
(Line (M,1)) . 2
= M * (1,2) &
(Line (M,1)) . 3
= M * (1,3) )
by MATRIX_0:def 7;
verum end;
then A6:
Line (M,1) = <*(M * (1,1)),(M * (1,2)),(M * (1,3))*>
by FINSEQ_1:45;
reconsider ze = 0 as Element of F_Real ;
<*(M * (1,1)),(M * (1,2)),(M * (1,3))*> "*" <*ze,ze,ze*> = (((M * (1,1)) * ze) + ((M * (1,2)) * ze)) + ((M * (1,3)) * ze)
by Th6;
then A7:
(Line (M,1)) "*" (Col (N,1)) = 0
by A1, Th4, A6;
now ( (M * N) . 1 = <*0*> & (M * N) . 2 = <*0*> & (M * N) . 3 = <*0*> )A8:
1
in Seg 3
by FINSEQ_1:1;
len (Line ((M * N),1)) =
width (M * N)
by MATRIX_0:def 7
.=
1
by A4A, MATRIX_0:23
;
then A9:
Line (
(M * N),1)
= <*((Line ((M * N),1)) . 1)*>
by FINSEQ_1:40;
2
in Seg 3
by FINSEQ_1:1;
then A10:
(M * N) . 2
= Line (
(M * N),2)
by A5, MATRIX_0:52;
A11:
len (Line ((M * N),2)) =
width (M * N)
by MATRIX_0:def 7
.=
1
by A4A, MATRIX_0:23
;
3
in Seg 3
by FINSEQ_1:1;
then A12:
(M * N) . 3
= Line (
(M * N),3)
by A5, MATRIX_0:52;
A13:
len (Line ((M * N),3)) =
width (M * N)
by MATRIX_0:def 7
.=
1
by A4A, MATRIX_0:23
;
(Line ((M * N),1)) . 1
= 0
proof
A14:
[1,1] in Indices (M * N)
by A5, MATRIX_0:23, Th2;
1
in Seg (width (M * N))
by A4, FINSEQ_1:1;
then (Line ((M * N),1)) . 1 =
(M * N) * (1,1)
by MATRIX_0:def 7
.=
0
by A7, A14, A2, A3, MATRIX_3:def 4
;
hence
(Line ((M * N),1)) . 1
= 0
;
verum
end; hence
(M * N) . 1
= <*0*>
by A9, A8, A5, MATRIX_0:52;
( (M * N) . 2 = <*0*> & (M * N) . 3 = <*0*> )now ( len (Line (M,2)) = 3 & (Line (M,2)) . 1 = M * (2,1) & (Line (M,2)) . 2 = M * (2,2) & (Line (M,2)) . 3 = M * (2,3) )thus len (Line (M,2)) =
width M
by MATRIX_0:def 7
.=
3
by MATRIX_0:23
;
( (Line (M,2)) . 1 = M * (2,1) & (Line (M,2)) . 2 = M * (2,2) & (Line (M,2)) . 3 = M * (2,3) )
( 1
in Seg (width M) & 2
in Seg (width M) & 3
in Seg (width M) )
by A2, FINSEQ_1:1;
hence
(
(Line (M,2)) . 1
= M * (2,1) &
(Line (M,2)) . 2
= M * (2,2) &
(Line (M,2)) . 3
= M * (2,3) )
by MATRIX_0:def 7;
verum end; then A15:
Line (
M,2)
= <*(M * (2,1)),(M * (2,2)),(M * (2,3))*>
by FINSEQ_1:45;
reconsider ze =
0 as
Element of
F_Real ;
<*(M * (2,1)),(M * (2,2)),(M * (2,3))*> "*" <*ze,ze,ze*> = (((M * (2,1)) * ze) + ((M * (2,2)) * ze)) + ((M * (2,3)) * ze)
by Th6;
then A16:
(Line (M,2)) "*" (Col (N,1)) = 0
by A1, Th4, A15;
(Line ((M * N),2)) . 1
= 0
proof
A17:
[2,1] in Indices (M * N)
by A5, MATRIX_0:23, Th2;
1
in Seg (width (M * N))
by A4, FINSEQ_1:1;
then (Line ((M * N),2)) . 1 =
(M * N) * (2,1)
by MATRIX_0:def 7
.=
0
by A16, A17, A2, A3, MATRIX_3:def 4
;
hence
(Line ((M * N),2)) . 1
= 0
;
verum
end; hence
(M * N) . 2
= <*0*>
by FINSEQ_1:40, A10, A11;
(M * N) . 3 = <*0*>now ( len (Line (M,3)) = 3 & (Line (M,3)) . 1 = M * (3,1) & (Line (M,3)) . 2 = M * (3,2) & (Line (M,3)) . 3 = M * (3,3) )thus len (Line (M,3)) =
width M
by MATRIX_0:def 7
.=
3
by MATRIX_0:23
;
( (Line (M,3)) . 1 = M * (3,1) & (Line (M,3)) . 2 = M * (3,2) & (Line (M,3)) . 3 = M * (3,3) )
( 1
in Seg (width M) & 2
in Seg (width M) & 3
in Seg (width M) )
by A2, FINSEQ_1:1;
hence
(
(Line (M,3)) . 1
= M * (3,1) &
(Line (M,3)) . 2
= M * (3,2) &
(Line (M,3)) . 3
= M * (3,3) )
by MATRIX_0:def 7;
verum end; then A18:
Line (
M,3)
= <*(M * (3,1)),(M * (3,2)),(M * (3,3))*>
by FINSEQ_1:45;
reconsider ze =
0 as
Element of
F_Real ;
<*(M * (3,1)),(M * (3,2)),(M * (3,3))*> "*" <*ze,ze,ze*> = (((M * (3,1)) * ze) + ((M * (3,2)) * ze)) + ((M * (3,3)) * ze)
by Th6;
then A19:
(Line (M,3)) "*" (Col (N,1)) = 0
by A1, Th4, A18;
(Line ((M * N),3)) . 1
= 0
proof
A20:
[3,1] in Indices (M * N)
by A5, MATRIX_0:23, Th2;
1
in Seg (width (M * N))
by A4, FINSEQ_1:1;
then (Line ((M * N),3)) . 1 =
(M * N) * (3,1)
by MATRIX_0:def 7
.=
0
by A20, A2, A3, MATRIX_3:def 4, A19
;
hence
(Line ((M * N),3)) . 1
= 0
;
verum
end; hence
(M * N) . 3
= <*0*>
by A13, FINSEQ_1:40, A12;
verum end;
hence
M * N = <*<*0*>,<*0*>,<*0*>*>
by A4A, MATRIX_0:23, FINSEQ_1:45; verum