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>) )
A1:
for r1, r2 being Real
for R being Element of 3 -tuples_on REAL holds (r1 * R) - (r2 * R) = (r1 - r2) * R
A2:
( <e1> . 1 = 1 & <e1> . 2 = 0 & <e1> . 3 = 0 )
by FINSEQ_1:45;
A3:
( <e2> . 1 = 0 & <e2> . 2 = 1 & <e2> . 3 = 0 )
by FINSEQ_1:45;
A4:
( <e3> . 1 = 0 & <e3> . 2 = 0 & <e3> . 3 = 1 )
by FINSEQ_1:45;
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>) )
now ( (((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>) )assume A5:
(((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>) )
((((((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
A6:
((p2 . 1) * <e1>) . 1 =
(p2 . 1) * 1
by A2, RVSUM_1:44
.=
p2 . 1
;
A7:
((p2 . 1) * <e1>) . 2 =
(p2 . 1) * 0
by A2, RVSUM_1:44
.=
0
;
A8:
((p2 . 1) * <e1>) . 3 =
(p2 . 1) * 0
by A2, RVSUM_1:44
.=
0
;
A9:
((p2 . 2) * <e2>) . 1 =
(p2 . 2) * (<e2> . 1)
by RVSUM_1:44
.=
0
by A3
;
A10:
((p2 . 2) * <e2>) . 2 =
(p2 . 2) * 1
by A3, RVSUM_1:44
.=
p2 . 2
;
A11:
((p2 . 2) * <e2>) . 3 =
(p2 . 2) * 0
by A3, RVSUM_1:44
.=
0
;
A12:
((p2 . 3) * <e3>) . 1 =
(p2 . 3) * 0
by A4, RVSUM_1:44
.=
0
;
A13:
((p2 . 3) * <e3>) . 2 =
(p2 . 3) * 0
by A4, RVSUM_1:44
.=
0
;
A14:
((p2 . 3) * <e3>) . 3 =
(p2 . 3) * 1
by A4, RVSUM_1:44
.=
p2 . 3
;
A15:
((p3 . 1) * <e1>) . 1 =
(p3 . 1) * 1
by A2, RVSUM_1:44
.=
p3 . 1
;
A16:
((p3 . 1) * <e1>) . 2 =
(p3 . 1) * 0
by A2, RVSUM_1:44
.=
0
;
A17:
((p3 . 1) * <e1>) . 3 =
(p3 . 1) * 0
by A2, RVSUM_1:44
.=
0
;
A18:
((p3 . 2) * <e2>) . 1 =
(p3 . 2) * (<e2> . 1)
by RVSUM_1:44
.=
0
by A3
;
A19:
((p3 . 2) * <e2>) . 2 =
(p3 . 2) * 1
by A3, RVSUM_1:44
.=
p3 . 2
;
A20:
((p3 . 2) * <e2>) . 3 =
(p3 . 2) * 0
by A3, RVSUM_1:44
.=
0
;
A21:
((p3 . 3) * <e3>) . 1 =
(p3 . 3) * 0
by A4, RVSUM_1:44
.=
0
;
A22:
((p3 . 3) * <e3>) . 2 =
(p3 . 3) * 0
by A4, RVSUM_1:44
.=
0
;
A23:
((p3 . 3) * <e3>) . 3 =
(p3 . 3) * 1
by A4, RVSUM_1:44
.=
p3 . 3
;
A24:
(((p2 . 1) * <e1>) + ((p2 . 2) * <e2>)) + ((p2 . 3) * <e3>) =
((p2 . 1) * <e1>) + (((p2 . 2) * <e2>) + ((p2 . 3) * <e3>))
by RVSUM_1:15
.=
((p2 . 1) * <e1>) + |[(0 + 0),((p2 . 2) + 0),(0 + (p2 . 3))]|
by A9, A10, A11, A12, A13, A14, Lm2
.=
|[(p2 . 1),0,0]| + |[0,(p2 . 2),(p2 . 3)]|
by A6, A7, A8, Th1
.=
|[((p2 . 1) + 0),(0 + (p2 . 2)),(0 + (p2 . 3))]|
by Lm8
.=
|[(p2 . 1),(p2 . 2),(p2 . 3)]|
;
A25:
(((p3 . 1) * <e1>) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>) =
((p3 . 1) * <e1>) + (((p3 . 2) * <e2>) + ((p3 . 3) * <e3>))
by RVSUM_1:15
.=
((p3 . 1) * <e1>) + |[(0 + 0),((p3 . 2) + 0),(0 + (p3 . 3))]|
by A18, A19, A20, A21, A22, A23, Lm2
.=
|[(p3 . 1),0,0]| + |[0,(p3 . 2),(p3 . 3)]|
by A15, A16, A17, Th1
.=
|[((p3 . 1) + 0),(0 + (p3 . 2)),(0 + (p3 . 3))]|
by Lm8
.=
|[(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:15
.=
(((((p2 . 1) * <e1>) + |[(0 + 0),((p2 . 2) + 0),(0 + (p2 . 3))]|) + ((p3 . 1) * <e1>)) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>)
by A9, A10, A11, A12, A13, A14, Lm2
.=
(((|[(p2 . 1),0,0]| + |[0,(p2 . 2),(p2 . 3)]|) + ((p3 . 1) * <e1>)) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>)
by A6, A7, A8, Th1
.=
((|[((p2 . 1) + 0),(0 + (p2 . 2)),(0 + (p2 . 3))]| + ((p3 . 1) * <e1>)) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>)
by Lm8
.=
((|[(p2 . 1),(p2 . 2),(p2 . 3)]| + |[(p3 . 1),0,0]|) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>)
by A15, A16, A17, Th1
.=
(|[((p2 . 1) + (p3 . 1)),((p2 . 2) + 0),((p2 . 3) + 0)]| + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>)
by Lm8
.=
(|[((p2 . 1) + (p3 . 1)),(p2 . 2),(p2 . 3)]| + |[0,(p3 . 2),0]|) + ((p3 . 3) * <e3>)
by A18, A19, A20, Th1
.=
|[(((p2 . 1) + (p3 . 1)) + 0),((p2 . 2) + (p3 . 2)),((p2 . 3) + 0)]| + ((p3 . 3) * <e3>)
by Lm8
.=
|[((p2 . 1) + (p3 . 1)),((p2 . 2) + (p3 . 2)),(p2 . 3)]| + |[0,0,(p3 . 3)]|
by A21, A22, A23, Th1
.=
|[(((p2 . 1) + (p3 . 1)) + 0),(((p2 . 2) + (p3 . 2)) + 0),((p2 . 3) + (p3 . 3))]|
by Lm8
;
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 A24, A25, Lm8;
verum
end; then
((((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 A5, EUCLIDLP:24;
then
((((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 RVSUM_1:15;
then
((((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 A1;
then
((((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 RVSUM_1:15;
then
((((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 RVSUM_1:15;
then
((((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 RVSUM_1:37;
then
((((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 EUCLID_4:1;
then
((((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 RVSUM_1:15;
then
((((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 A1;
then
((((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 RVSUM_1:15;
then
((((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 RVSUM_1:15;
then
((((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 RVSUM_1:15;
then
((((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 RVSUM_1:37;
then
((((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 EUCLID_4:1;
then
((((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 RVSUM_1:15;
then
((((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 A1;
then
((((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 RVSUM_1:15;
then
((((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 RVSUM_1:15;
then
((((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 RVSUM_1:15;
then
((((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 RVSUM_1:15;
then
((((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 RVSUM_1:37;
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