let p1, p2, p3 be Element of REAL 3; ( (((p1 . 1) * <e1> ) + ((p1 . 2) * <e2> )) + ((p1 . 3) * <e3> ) = ((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> ) iff (((p2 . 1) * <e1> ) + ((p2 . 2) * <e2> )) + ((p2 . 3) * <e3> ) = ((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) - (p3 . 3)) * <e3> ) )
F1:
for R1, R2, R3 being Element of 3 -tuples_on REAL holds (R1 + R2) - R3 = (R1 - R3) + R2
by RVSUM_1:32;
F2:
for r1, r2 being Element of REAL
for R being Element of 3 -tuples_on REAL holds (r1 * R) - (r2 * R) = (r1 - r2) * R
A1:
( <e1> . 1 = 1 & <e1> . 2 = 0 & <e1> . 3 = 0 )
by FINSEQ_1:62;
A2:
( <e2> . 1 = 0 & <e2> . 2 = 1 & <e2> . 3 = 0 )
by FINSEQ_1:62;
A3:
( <e3> . 1 = 0 & <e3> . 2 = 0 & <e3> . 3 = 1 )
by FINSEQ_1:62;
thus
( (((p1 . 1) * <e1> ) + ((p1 . 2) * <e2> )) + ((p1 . 3) * <e3> ) = ((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> ) implies (((p2 . 1) * <e1> ) + ((p2 . 2) * <e2> )) + ((p2 . 3) * <e3> ) = ((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) - (p3 . 3)) * <e3> ) )
( (((p2 . 1) * <e1> ) + ((p2 . 2) * <e2> )) + ((p2 . 3) * <e3> ) = ((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) - (p3 . 3)) * <e3> ) implies (((p1 . 1) * <e1> ) + ((p1 . 2) * <e2> )) + ((p1 . 3) * <e3> ) = ((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> ) )proof
assume A4:
(((p1 . 1) * <e1> ) + ((p1 . 2) * <e2> )) + ((p1 . 3) * <e3> ) = ((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> )
;
(((p2 . 1) * <e1> ) + ((p2 . 2) * <e2> )) + ((p2 . 3) * <e3> ) = ((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) - (p3 . 3)) * <e3> )
A8:
(((((p1 . 1) * <e1> ) + (((p1 . 2) * <e2> ) + ((p1 . 3) * <e3> ))) - ((p3 . 1) * <e1> )) - ((p3 . 2) * <e2> )) - ((p3 . 3) * <e3> ) = (((((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> )) - ((p3 . 1) * <e1> )) - ((p3 . 2) * <e2> )) - ((p3 . 3) * <e3> )
by A4, RVSUM_1:32;
B1:
(((((p1 . 1) * <e1> ) - ((p3 . 1) * <e1> )) + (((p1 . 2) * <e2> ) + ((p1 . 3) * <e3> ))) - ((p3 . 2) * <e2> )) - ((p3 . 3) * <e3> ) = (((((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> )) - ((p3 . 1) * <e1> )) - ((p3 . 2) * <e2> )) - ((p3 . 3) * <e3> )
by A8, RVSUM_1:32;
B2:
(((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) * <e2> ) + ((p1 . 3) * <e3> ))) - ((p3 . 2) * <e2> )) - ((p3 . 3) * <e3> ) = (((((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> )) - ((p3 . 1) * <e1> )) - ((p3 . 2) * <e2> )) - ((p3 . 3) * <e3> )
by B1, F2;
B3:
((((((p1 . 1) - (p3 . 1)) * <e1> ) + ((p1 . 2) * <e2> )) + ((p1 . 3) * <e3> )) - ((p3 . 2) * <e2> )) - ((p3 . 3) * <e3> ) = (((((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> )) - ((p3 . 1) * <e1> )) - ((p3 . 2) * <e2> )) - ((p3 . 3) * <e3> )
by B2, RVSUM_1:32;
B4:
((((((p1 . 1) - (p3 . 1)) * <e1> ) + ((p1 . 2) * <e2> )) - ((p3 . 2) * <e2> )) + ((p1 . 3) * <e3> )) - ((p3 . 3) * <e3> ) = (((((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> )) - ((p3 . 1) * <e1> )) - ((p3 . 2) * <e2> )) - ((p3 . 3) * <e3> )
by B3, RVSUM_1:32;
B7:
(((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) * <e2> ) + (- ((p3 . 2) * <e2> )))) + ((p1 . 3) * <e3> )) + (- ((p3 . 3) * <e3> )) = (((((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> )) - ((p3 . 1) * <e1> )) - ((p3 . 2) * <e2> )) - ((p3 . 3) * <e3> )
by B4, RVSUM_1:32;
B9:
((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) * <e2> ) - ((p3 . 2) * <e2> ))) + (((p1 . 3) * <e3> ) - ((p3 . 3) * <e3> )) = (((((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> )) - ((p3 . 1) * <e1> )) - ((p3 . 2) * <e2> )) - ((p3 . 3) * <e3> )
by B7, RVSUM_1:32;
B10:
((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) * <e3> ) - ((p3 . 3) * <e3> )) = (((((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> )) - ((p3 . 1) * <e1> )) - ((p3 . 2) * <e2> )) - ((p3 . 3) * <e3> )
by B9, F2;
B11:
((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) - (p3 . 3)) * <e3> ) = (((((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> )) - ((p3 . 1) * <e1> )) - ((p3 . 2) * <e2> )) - ((p3 . 3) * <e3> )
by B10, F2;
B12:
((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) - (p3 . 3)) * <e3> ) = (((((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) - ((p3 . 1) * <e1> )) + (((p2 . 3) + (p3 . 3)) * <e3> )) - ((p3 . 2) * <e2> )) - ((p3 . 3) * <e3> )
by B11, RVSUM_1:32;
B13:
((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) - (p3 . 3)) * <e3> ) = (((((((p2 . 1) + (p3 . 1)) * <e1> ) - ((p3 . 1) * <e1> )) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> )) - ((p3 . 2) * <e2> )) - ((p3 . 3) * <e3> )
by B12, RVSUM_1:32;
B14:
((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) - (p3 . 3)) * <e3> ) = (((((((p2 . 1) + (p3 . 1)) * <e1> ) - ((p3 . 1) * <e1> )) + (((p2 . 2) + (p3 . 2)) * <e2> )) - ((p3 . 2) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> )) - ((p3 . 3) * <e3> )
by B13, RVSUM_1:32;
B16:
((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) - (p3 . 3)) * <e3> ) = (((((((p2 . 1) * <e1> ) + ((p3 . 1) * <e1> )) + (- ((p3 . 1) * <e1> ))) + (((p2 . 2) + (p3 . 2)) * <e2> )) - ((p3 . 2) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> )) - ((p3 . 3) * <e3> )
by B14, RVSUM_1:72;
B18:
((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) - (p3 . 3)) * <e3> ) = ((((((p2 . 1) * <e1> ) + (((p3 . 1) * <e1> ) - ((p3 . 1) * <e1> ))) + (((p2 . 2) + (p3 . 2)) * <e2> )) - ((p3 . 2) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> )) - ((p3 . 3) * <e3> )
by B16, RVSUM_1:32;
B19:
((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) - (p3 . 3)) * <e3> ) = ((((((p2 . 1) * <e1> ) + (0.REAL 3)) + (((p2 . 2) + (p3 . 2)) * <e2> )) - ((p3 . 2) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> )) - ((p3 . 3) * <e3> )
by B18, EUCLIDLP:7;
B20:
((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) - (p3 . 3)) * <e3> ) = (((((p2 . 1) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) - ((p3 . 2) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> )) - ((p3 . 3) * <e3> )
by B19, EUCLID_4:1;
B21:
((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) - (p3 . 3)) * <e3> ) = (((((p2 . 1) * <e1> ) + (((p2 . 2) * <e2> ) + ((p3 . 2) * <e2> ))) - ((p3 . 2) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> )) - ((p3 . 3) * <e3> )
by B20, RVSUM_1:72;
E1:
((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) - (p3 . 3)) * <e3> ) = ((((((p2 . 1) * <e1> ) + ((p2 . 2) * <e2> )) + ((p3 . 2) * <e2> )) + (- ((p3 . 2) * <e2> ))) + (((p2 . 3) + (p3 . 3)) * <e3> )) - ((p3 . 3) * <e3> )
by B21, RVSUM_1:32;
E2:
((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) - (p3 . 3)) * <e3> ) = (((((p2 . 1) * <e1> ) + ((p2 . 2) * <e2> )) + (((p3 . 2) * <e2> ) + (- ((p3 . 2) * <e2> )))) + (((p2 . 3) + (p3 . 3)) * <e3> )) - ((p3 . 3) * <e3> )
by E1, RVSUM_1:32;
B24:
((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) - (p3 . 3)) * <e3> ) = (((((p2 . 1) * <e1> ) + ((p2 . 2) * <e2> )) + (0.REAL 3)) + (((p2 . 3) + (p3 . 3)) * <e3> )) - ((p3 . 3) * <e3> )
by E2, EUCLIDLP:7;
B25:
((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) - (p3 . 3)) * <e3> ) = ((((p2 . 1) * <e1> ) + ((p2 . 2) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> )) - ((p3 . 3) * <e3> )
by B24, EUCLID_4:1;
B26:
((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) - (p3 . 3)) * <e3> ) = ((((p2 . 1) * <e1> ) + ((p2 . 2) * <e2> )) + (((p2 . 3) * <e3> ) + ((p3 . 3) * <e3> ))) - ((p3 . 3) * <e3> )
by B25, RVSUM_1:72;
B27:
((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) - (p3 . 3)) * <e3> ) = (((((p2 . 1) * <e1> ) + ((p2 . 2) * <e2> )) + ((p2 . 3) * <e3> )) + ((p3 . 3) * <e3> )) - ((p3 . 3) * <e3> )
by B26, RVSUM_1:32;
B28:
((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) - (p3 . 3)) * <e3> ) = ((((p2 . 1) * <e1> ) + ((p2 . 2) * <e2> )) + ((p2 . 3) * <e3> )) + (((p3 . 3) * <e3> ) + (- ((p3 . 3) * <e3> )))
by B27, RVSUM_1:32;
((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) - (p3 . 3)) * <e3> ) = ((((p2 . 1) * <e1> ) + ((p2 . 2) * <e2> )) + ((p2 . 3) * <e3> )) + (0.REAL 3)
by B28, EUCLIDLP:7;
hence
(((p2 . 1) * <e1> ) + ((p2 . 2) * <e2> )) + ((p2 . 3) * <e3> ) = ((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) - (p3 . 3)) * <e3> )
by EUCLID_4:1;
verum
end;
now assume C1:
(((p2 . 1) * <e1> ) + ((p2 . 2) * <e2> )) + ((p2 . 3) * <e3> ) = ((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) - (p3 . 3)) * <e3> )
;
( (((p2 . 1) * <e1> ) + ((p2 . 2) * <e2> )) + ((p2 . 3) * <e3> ) = ((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) - (p3 . 3)) * <e3> ) implies (((p1 . 1) * <e1> ) + ((p1 . 2) * <e2> )) + ((p1 . 3) * <e3> ) = ((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> ) )C3:
((((((p2 . 1) * <e1> ) + ((p2 . 2) * <e2> )) + ((p2 . 3) * <e3> )) + ((p3 . 1) * <e1> )) + ((p3 . 2) * <e2> )) + ((p3 . 3) * <e3> ) = ((((p2 . 1) * <e1> ) + ((p2 . 2) * <e2> )) + ((p2 . 3) * <e3> )) + ((((p3 . 1) * <e1> ) + ((p3 . 2) * <e2> )) + ((p3 . 3) * <e3> ))
proof
D1:
((p2 . 1) * <e1> ) . 1 =
(p2 . 1) * 1
by A1, RVSUM_1:66
.=
p2 . 1
;
D2:
((p2 . 1) * <e1> ) . 2 =
(p2 . 1) * 0
by A1, RVSUM_1:66
.=
0
;
D3:
((p2 . 1) * <e1> ) . 3 =
(p2 . 1) * 0
by A1, RVSUM_1:66
.=
0
;
D4:
((p2 . 2) * <e2> ) . 1 =
(p2 . 2) * (<e2> . 1)
by RVSUM_1:66
.=
0
by A2
;
D5:
((p2 . 2) * <e2> ) . 2 =
(p2 . 2) * 1
by A2, RVSUM_1:66
.=
p2 . 2
;
D6:
((p2 . 2) * <e2> ) . 3 =
(p2 . 2) * 0
by A2, RVSUM_1:66
.=
0
;
D7:
((p2 . 3) * <e3> ) . 1 =
(p2 . 3) * 0
by A3, RVSUM_1:66
.=
0
;
D8:
((p2 . 3) * <e3> ) . 2 =
(p2 . 3) * 0
by A3, RVSUM_1:66
.=
0
;
D9:
((p2 . 3) * <e3> ) . 3 =
(p2 . 3) * 1
by A3, RVSUM_1:66
.=
p2 . 3
;
D10:
((p3 . 1) * <e1> ) . 1 =
(p3 . 1) * 1
by A1, RVSUM_1:66
.=
p3 . 1
;
D11:
((p3 . 1) * <e1> ) . 2 =
(p3 . 1) * 0
by A1, RVSUM_1:66
.=
0
;
D12:
((p3 . 1) * <e1> ) . 3 =
(p3 . 1) * 0
by A1, RVSUM_1:66
.=
0
;
D13:
((p3 . 2) * <e2> ) . 1 =
(p3 . 2) * (<e2> . 1)
by RVSUM_1:66
.=
0
by A2
;
D14:
((p3 . 2) * <e2> ) . 2 =
(p3 . 2) * 1
by A2, RVSUM_1:66
.=
p3 . 2
;
D15:
((p3 . 2) * <e2> ) . 3 =
(p3 . 2) * 0
by A2, RVSUM_1:66
.=
0
;
D16:
((p3 . 3) * <e3> ) . 1 =
(p3 . 3) * 0
by A3, RVSUM_1:66
.=
0
;
D17:
((p3 . 3) * <e3> ) . 2 =
(p3 . 3) * 0
by A3, RVSUM_1:66
.=
0
;
D18:
((p3 . 3) * <e3> ) . 3 =
(p3 . 3) * 1
by A3, RVSUM_1:66
.=
p3 . 3
;
D19:
(((p2 . 1) * <e1> ) + ((p2 . 2) * <e2> )) + ((p2 . 3) * <e3> ) =
((p2 . 1) * <e1> ) + (((p2 . 2) * <e2> ) + ((p2 . 3) * <e3> ))
by RVSUM_1:32
.=
((p2 . 1) * <e1> ) + |[(0 + 0 ),((p2 . 2) + 0 ),(0 + (p2 . 3))]|
by D4, D5, D6, D7, D8, D9, Lm4
.=
|[(p2 . 1),0 ,0 ]| + |[0 ,(p2 . 2),(p2 . 3)]|
by D1, D2, D3, Lm1
.=
|[((p2 . 1) + 0 ),(0 + (p2 . 2)),(0 + (p2 . 3))]|
by LmA31
.=
|[(p2 . 1),(p2 . 2),(p2 . 3)]|
;
D20:
(((p3 . 1) * <e1> ) + ((p3 . 2) * <e2> )) + ((p3 . 3) * <e3> ) =
((p3 . 1) * <e1> ) + (((p3 . 2) * <e2> ) + ((p3 . 3) * <e3> ))
by RVSUM_1:32
.=
((p3 . 1) * <e1> ) + |[(0 + 0 ),((p3 . 2) + 0 ),(0 + (p3 . 3))]|
by D13, D14, D15, D16, D17, D18, Lm4
.=
|[(p3 . 1),0 ,0 ]| + |[0 ,(p3 . 2),(p3 . 3)]|
by D10, D11, D12, Lm1
.=
|[((p3 . 1) + 0 ),(0 + (p3 . 2)),(0 + (p3 . 3))]|
by LmA31
.=
|[(p3 . 1),(p3 . 2),(p3 . 3)]|
;
((((((p2 . 1) * <e1> ) + ((p2 . 2) * <e2> )) + ((p2 . 3) * <e3> )) + ((p3 . 1) * <e1> )) + ((p3 . 2) * <e2> )) + ((p3 . 3) * <e3> ) =
(((((p2 . 1) * <e1> ) + (((p2 . 2) * <e2> ) + ((p2 . 3) * <e3> ))) + ((p3 . 1) * <e1> )) + ((p3 . 2) * <e2> )) + ((p3 . 3) * <e3> )
by RVSUM_1:32
.=
(((((p2 . 1) * <e1> ) + |[(0 + 0 ),((p2 . 2) + 0 ),(0 + (p2 . 3))]|) + ((p3 . 1) * <e1> )) + ((p3 . 2) * <e2> )) + ((p3 . 3) * <e3> )
by D4, D5, D6, D7, D8, D9, Lm4
.=
(((|[(p2 . 1),0 ,0 ]| + |[0 ,(p2 . 2),(p2 . 3)]|) + ((p3 . 1) * <e1> )) + ((p3 . 2) * <e2> )) + ((p3 . 3) * <e3> )
by D1, D2, D3, Lm1
.=
((|[((p2 . 1) + 0 ),(0 + (p2 . 2)),(0 + (p2 . 3))]| + ((p3 . 1) * <e1> )) + ((p3 . 2) * <e2> )) + ((p3 . 3) * <e3> )
by LmA31
.=
((|[(p2 . 1),(p2 . 2),(p2 . 3)]| + |[(p3 . 1),0 ,0 ]|) + ((p3 . 2) * <e2> )) + ((p3 . 3) * <e3> )
by D10, D11, D12, Lm1
.=
(|[((p2 . 1) + (p3 . 1)),((p2 . 2) + 0 ),((p2 . 3) + 0 )]| + ((p3 . 2) * <e2> )) + ((p3 . 3) * <e3> )
by LmA31
.=
(|[((p2 . 1) + (p3 . 1)),(p2 . 2),(p2 . 3)]| + |[0 ,(p3 . 2),0 ]|) + ((p3 . 3) * <e3> )
by D13, D14, D15, Lm1
.=
|[(((p2 . 1) + (p3 . 1)) + 0 ),((p2 . 2) + (p3 . 2)),((p2 . 3) + 0 )]| + ((p3 . 3) * <e3> )
by LmA31
.=
|[((p2 . 1) + (p3 . 1)),((p2 . 2) + (p3 . 2)),(p2 . 3)]| + |[0 ,0 ,(p3 . 3)]|
by D16, D17, D18, Lm1
.=
|[(((p2 . 1) + (p3 . 1)) + 0 ),(((p2 . 2) + (p3 . 2)) + 0 ),((p2 . 3) + (p3 . 3))]|
by LmA31
;
hence
((((((p2 . 1) * <e1> ) + ((p2 . 2) * <e2> )) + ((p2 . 3) * <e3> )) + ((p3 . 1) * <e1> )) + ((p3 . 2) * <e2> )) + ((p3 . 3) * <e3> ) = ((((p2 . 1) * <e1> ) + ((p2 . 2) * <e2> )) + ((p2 . 3) * <e3> )) + ((((p3 . 1) * <e1> ) + ((p3 . 2) * <e2> )) + ((p3 . 3) * <e3> ))
by D19, D20, LmA31;
verum
end; C6:
((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> ) = (((((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) - (p3 . 3)) * <e3> )) + ((p3 . 1) * <e1> )) + ((p3 . 2) * <e2> )) + ((p3 . 3) * <e3> )
by EUCLIDLP:29, C1, C3;
C7:
((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> ) = ((((((p1 . 1) - (p3 . 1)) * <e1> ) + ((((p1 . 2) - (p3 . 2)) * <e2> ) + (((p1 . 3) - (p3 . 3)) * <e3> ))) + ((p3 . 1) * <e1> )) + ((p3 . 2) * <e2> )) + ((p3 . 3) * <e3> )
by C6, RVSUM_1:32;
C8:
((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> ) = ((((((p1 . 1) * <e1> ) - ((p3 . 1) * <e1> )) + ((((p1 . 2) - (p3 . 2)) * <e2> ) + (((p1 . 3) - (p3 . 3)) * <e3> ))) + ((p3 . 1) * <e1> )) + ((p3 . 2) * <e2> )) + ((p3 . 3) * <e3> )
by C7, F2;
C9:
((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> ) = ((((((p1 . 1) * <e1> ) + ((((p1 . 2) - (p3 . 2)) * <e2> ) + (((p1 . 3) - (p3 . 3)) * <e3> ))) - ((p3 . 1) * <e1> )) + ((p3 . 1) * <e1> )) + ((p3 . 2) * <e2> )) + ((p3 . 3) * <e3> )
by C8, RVSUM_1:32;
C13:
((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> ) = (((((p1 . 1) * <e1> ) + ((((p1 . 2) - (p3 . 2)) * <e2> ) + (((p1 . 3) - (p3 . 3)) * <e3> ))) + (((p3 . 1) * <e1> ) - ((p3 . 1) * <e1> ))) + ((p3 . 2) * <e2> )) + ((p3 . 3) * <e3> )
by C9, RVSUM_1:32;
C14:
((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> ) = (((((p1 . 1) * <e1> ) + ((((p1 . 2) - (p3 . 2)) * <e2> ) + (((p1 . 3) - (p3 . 3)) * <e3> ))) + (0.REAL 3)) + ((p3 . 2) * <e2> )) + ((p3 . 3) * <e3> )
by C13, RVSUM_1:58;
C15:
((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> ) = ((((p1 . 1) * <e1> ) + ((((p1 . 2) - (p3 . 2)) * <e2> ) + (((p1 . 3) - (p3 . 3)) * <e3> ))) + ((p3 . 2) * <e2> )) + ((p3 . 3) * <e3> )
by C14, EUCLID_4:1;
C16:
((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> ) = (((((p1 . 1) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) - (p3 . 3)) * <e3> )) + ((p3 . 2) * <e2> )) + ((p3 . 3) * <e3> )
by C15, RVSUM_1:32;
C17:
((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> ) = (((((p1 . 1) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) * <e3> ) - ((p3 . 3) * <e3> ))) + ((p3 . 2) * <e2> )) + ((p3 . 3) * <e3> )
by C16, F2;
C20:
((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> ) = ((((((p1 . 1) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + ((p1 . 3) * <e3> )) - ((p3 . 3) * <e3> )) + ((p3 . 2) * <e2> )) + ((p3 . 3) * <e3> )
by C17, RVSUM_1:32;
C21:
((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> ) = ((((((p1 . 1) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + ((p1 . 3) * <e3> )) + ((p3 . 2) * <e2> )) - ((p3 . 3) * <e3> )) + ((p3 . 3) * <e3> )
by C20, RVSUM_1:32;
C25:
((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> ) = (((((p1 . 1) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + ((p1 . 3) * <e3> )) + ((p3 . 2) * <e2> )) + (((p3 . 3) * <e3> ) - ((p3 . 3) * <e3> ))
by C21, RVSUM_1:32;
C26:
((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> ) = (((((p1 . 1) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + ((p1 . 3) * <e3> )) + ((p3 . 2) * <e2> )) + (0.REAL 3)
by C25, RVSUM_1:58;
C27:
((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> ) = ((((p1 . 1) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + ((p1 . 3) * <e3> )) + ((p3 . 2) * <e2> )
by C26, EUCLID_4:1;
C28:
((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> ) = (((p1 . 1) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) * <e3> ) + ((p3 . 2) * <e2> ))
by C27, RVSUM_1:32;
C29:
((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> ) = (((p1 . 1) * <e1> ) + (((p1 . 2) * <e2> ) - ((p3 . 2) * <e2> ))) + (((p1 . 3) * <e3> ) + ((p3 . 2) * <e2> ))
by C28, F2;
C31:
((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> ) = ((((p1 . 1) * <e1> ) + ((p1 . 2) * <e2> )) + (- ((p3 . 2) * <e2> ))) + (((p1 . 3) * <e3> ) + ((p3 . 2) * <e2> ))
by C29, RVSUM_1:32;
C33:
((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> ) = (((((p1 . 1) * <e1> ) + ((p1 . 2) * <e2> )) - ((p3 . 2) * <e2> )) + ((p1 . 3) * <e3> )) + ((p3 . 2) * <e2> )
by C31, RVSUM_1:32;
C34:
((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> ) = (((((p1 . 1) * <e1> ) + ((p1 . 2) * <e2> )) + ((p1 . 3) * <e3> )) - ((p3 . 2) * <e2> )) + ((p3 . 2) * <e2> )
by C33, RVSUM_1:32;
C38:
((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> ) = ((((p1 . 1) * <e1> ) + ((p1 . 2) * <e2> )) + ((p1 . 3) * <e3> )) + (((p3 . 2) * <e2> ) - ((p3 . 2) * <e2> ))
by C34, RVSUM_1:32;
((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> ) = ((((p1 . 1) * <e1> ) + ((p1 . 2) * <e2> )) + ((p1 . 3) * <e3> )) + (0.REAL 3)
by C38, RVSUM_1:58;
hence
(
(((p2 . 1) * <e1> ) + ((p2 . 2) * <e2> )) + ((p2 . 3) * <e3> ) = ((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) - (p3 . 3)) * <e3> ) implies
(((p1 . 1) * <e1> ) + ((p1 . 2) * <e2> )) + ((p1 . 3) * <e3> ) = ((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> ) )
by EUCLID_4:1;
verum end;
hence
( (((p2 . 1) * <e1> ) + ((p2 . 2) * <e2> )) + ((p2 . 3) * <e3> ) = ((((p1 . 1) - (p3 . 1)) * <e1> ) + (((p1 . 2) - (p3 . 2)) * <e2> )) + (((p1 . 3) - (p3 . 3)) * <e3> ) implies (((p1 . 1) * <e1> ) + ((p1 . 2) * <e2> )) + ((p1 . 3) * <e3> ) = ((((p2 . 1) + (p3 . 1)) * <e1> ) + (((p2 . 2) + (p3 . 2)) * <e2> )) + (((p2 . 3) + (p3 . 3)) * <e3> ) )
; verum