let r, x, y, z be Element of REAL ; r * |[x,y,z]| = (((r * x) * <e1> ) + ((r * y) * <e2> )) + ((r * z) * <e3> )
A2:
( <e1> . 1 = 1 & <e1> . 2 = 0 & <e1> . 3 = 0 )
by FINSEQ_1:62;
A3:
( <e2> . 1 = 0 & <e2> . 2 = 1 & <e2> . 3 = 0 )
by FINSEQ_1:62;
A4:
( <e3> . 1 = 0 & <e3> . 2 = 0 & <e3> . 3 = 1 )
by FINSEQ_1:62;
set p = |[x,y,z]|;
A6: (((r * x) * <e1> ) + ((r * y) * <e2> )) + ((r * z) * <e3> ) =
(|[((r * x) * 1),((r * x) * 0 ),((r * x) * 0 )]| + ((r * y) * <e2> )) + ((r * z) * <e3> )
by A2, Lm3
.=
(|[(r * x),0 ,0 ]| + |[((r * y) * 0 ),((r * y) * 1),((r * y) * 0 )]|) + ((r * z) * <e3> )
by A3, Lm3
.=
(|[(r * x),0 ,0 ]| + |[0 ,(r * y),0 ]|) + |[((r * z) * 0 ),((r * z) * 0 ),((r * z) * 1)]|
by A4, Lm3
.=
(|[(r * x),0 ,0 ]| + |[0 ,(r * y),0 ]|) + |[0 ,0 ,(r * z)]|
;
A7:
( |[(r * x),0 ,0 ]| . 1 = r * x & |[(r * x),0 ,0 ]| . 2 = 0 & |[(r * x),0 ,0 ]| . 3 = 0 )
by FINSEQ_1:62;
A8:
( |[0 ,(r * y),0 ]| . 1 = 0 & |[0 ,(r * y),0 ]| . 2 = r * y & |[0 ,(r * y),0 ]| . 3 = 0 )
by FINSEQ_1:62;
A9:
( |[0 ,0 ,(r * z)]| . 1 = 0 & |[0 ,0 ,(r * z)]| . 2 = 0 & |[0 ,0 ,(r * z)]| . 3 = r * z )
by FINSEQ_1:62;
A10: (((r * x) * <e1> ) + ((r * y) * <e2> )) + ((r * z) * <e3> ) =
|[((r * x) + 0 ),((r * y) + 0 ),(0 + 0 )]| + |[0 ,0 ,(r * z)]|
by A6, A7, A8, Lm4
.=
|[(r * x),(r * y),0 ]| + |[0 ,0 ,(r * z)]|
;
( |[(r * x),(r * y),0 ]| . 1 = r * x & |[(r * x),(r * y),0 ]| . 2 = r * y & |[(r * x),(r * y),0 ]| . 3 = 0 )
by FINSEQ_1:62;
then (((r * x) * <e1> ) + ((r * y) * <e2> )) + ((r * z) * <e3> ) =
|[((r * x) + 0 ),((r * y) + 0 ),(0 + (r * z))]|
by A9, A10, Lm4
.=
|[(r * x),(r * y),(r * z)]|
;
hence
r * |[x,y,z]| = (((r * x) * <e1> ) + ((r * y) * <e2> )) + ((r * z) * <e3> )
by LmA8; verum