let r, x, y, z be Real; r * |[x,y,z]| = (((r * x) * <e1>) + ((r * y) * <e2>)) + ((r * z) * <e3>)
A1:
( <e1> . 1 = 1 & <e1> . 2 = 0 & <e1> . 3 = 0 )
;
A2:
( <e2> . 1 = 0 & <e2> . 2 = 1 & <e2> . 3 = 0 )
;
A3:
( <e3> . 1 = 0 & <e3> . 2 = 0 & <e3> . 3 = 1 )
;
set p = |[x,y,z]|;
A4: (((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 A1, Lm1
.=
(|[(r * x),0,0]| + |[((r * y) * 0),((r * y) * 1),((r * y) * 0)]|) + ((r * z) * <e3>)
by A2, Lm1
.=
(|[(r * x),0,0]| + |[0,(r * y),0]|) + |[((r * z) * 0),((r * z) * 0),((r * z) * 1)]|
by A3, Lm1
.=
(|[(r * x),0,0]| + |[0,(r * y),0]|) + |[0,0,(r * z)]|
;
A5:
( |[(r * x),0,0]| . 1 = r * x & |[(r * x),0,0]| . 2 = 0 & |[(r * x),0,0]| . 3 = 0 )
;
A6:
( |[0,(r * y),0]| . 1 = 0 & |[0,(r * y),0]| . 2 = r * y & |[0,(r * y),0]| . 3 = 0 )
;
A7:
( |[0,0,(r * z)]| . 1 = 0 & |[0,0,(r * z)]| . 2 = 0 & |[0,0,(r * z)]| . 3 = r * z )
;
A8: (((r * x) * <e1>) + ((r * y) * <e2>)) + ((r * z) * <e3>) =
|[((r * x) + 0),((r * y) + 0),(0 + 0)]| + |[0,0,(r * z)]|
by A4, A5, A6, Lm2
.=
|[(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 )
;
then (((r * x) * <e1>) + ((r * y) * <e2>)) + ((r * z) * <e3>) =
|[((r * x) + 0),((r * y) + 0),(0 + (r * z))]|
by A7, A8, Lm2
.=
|[(r * x),(r * y),(r * z)]|
;
hence
r * |[x,y,z]| = (((r * x) * <e1>) + ((r * y) * <e2>)) + ((r * z) * <e3>)
by Lm6; verum