let r be Element of REAL ; for p being Element of REAL 3 holds r * p = (((r * (p . 1)) * <e1>) + ((r * (p . 2)) * <e2>)) + ((r * (p . 3)) * <e3>)
let p be Element of REAL 3; r * p = (((r * (p . 1)) * <e1>) + ((r * (p . 2)) * <e2>)) + ((r * (p . 3)) * <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;
A5: (((r * (p . 1)) * <e1>) + ((r * (p . 2)) * <e2>)) + ((r * (p . 3)) * <e3>) =
(|[((r * (p . 1)) * 1),((r * (p . 1)) * 0),((r * (p . 1)) * 0)]| + ((r * (p . 2)) * <e2>)) + ((r * (p . 3)) * <e3>)
by A2, Lm3
.=
(|[(r * (p . 1)),0,0]| + |[((r * (p . 2)) * 0),((r * (p . 2)) * 1),((r * (p . 2)) * 0)]|) + ((r * (p . 3)) * <e3>)
by A3, Lm3
.=
(|[(r * (p . 1)),0,0]| + |[0,(r * (p . 2)),0]|) + |[((r * (p . 3)) * 0),((r * (p . 3)) * 0),((r * (p . 3)) * 1)]|
by A4, Lm3
.=
(|[(r * (p . 1)),0,0]| + |[0,(r * (p . 2)),0]|) + |[0,0,(r * (p . 3))]|
;
A6:
( |[(r * (p . 1)),0,0]| . 1 = r * (p . 1) & |[(r * (p . 1)),0,0]| . 2 = 0 & |[(r * (p . 1)),0,0]| . 3 = 0 )
by FINSEQ_1:62;
A7:
( |[0,(r * (p . 2)),0]| . 1 = 0 & |[0,(r * (p . 2)),0]| . 2 = r * (p . 2) & |[0,(r * (p . 2)),0]| . 3 = 0 )
by FINSEQ_1:62;
A8:
( |[0,0,(r * (p . 3))]| . 1 = 0 & |[0,0,(r * (p . 3))]| . 2 = 0 & |[0,0,(r * (p . 3))]| . 3 = r * (p . 3) )
by FINSEQ_1:62;
A9: (((r * (p . 1)) * <e1>) + ((r * (p . 2)) * <e2>)) + ((r * (p . 3)) * <e3>) =
|[((r * (p . 1)) + 0),(0 + (r * (p . 2))),(0 + 0)]| + |[0,0,(r * (p . 3))]|
by A5, A6, A7, Lm4
.=
|[(r * (p . 1)),(r * (p . 2)),0]| + |[0,0,(r * (p . 3))]|
;
( |[(r * (p . 1)),(r * (p . 2)),0]| . 1 = r * (p . 1) & |[(r * (p . 1)),(r * (p . 2)),0]| . 2 = r * (p . 2) & |[(r * (p . 1)),(r * (p . 2)),0]| . 3 = 0 )
by FINSEQ_1:62;
then (((r * (p . 1)) * <e1>) + ((r * (p . 2)) * <e2>)) + ((r * (p . 3)) * <e3>) =
|[((r * (p . 1)) + 0),((r * (p . 2)) + 0),(0 + (r * (p . 3)))]|
by A8, A9, Lm4
.=
|[(r * (p . 1)),(r * (p . 2)),(r * (p . 3))]|
;
hence
r * p = (((r * (p . 1)) * <e1>) + ((r * (p . 2)) * <e2>)) + ((r * (p . 3)) * <e3>)
by Lm3; verum