let p1, p2, p3 be Element of REAL 3; p1 <X> (p2 + p3) = (p1 <X> p2) + (p1 <X> p3)
A1:
p2 + p3 = |[((p2 . 1) + (p3 . 1)),((p2 . 2) + (p3 . 2)),((p2 . 3) + (p3 . 3))]|
by Lm2;
then A2:
(p2 + p3) . 1 = (p2 . 1) + (p3 . 1)
by FINSEQ_1:45;
A3:
(p2 + p3) . 2 = (p2 . 2) + (p3 . 2)
by A1, FINSEQ_1:45;
A4:
(p2 + p3) . 3 = (p2 . 3) + (p3 . 3)
by A1, FINSEQ_1:45;
(p1 <X> p2) + (p1 <X> p3) =
|[((((p1 . 2) * (p2 . 3)) - ((p1 . 3) * (p2 . 2))) + (((p1 . 2) * (p3 . 3)) - ((p1 . 3) * (p3 . 2)))),((((p1 . 3) * (p2 . 1)) - ((p1 . 1) * (p2 . 3))) + (((p1 . 3) * (p3 . 1)) - ((p1 . 1) * (p3 . 3)))),((((p1 . 1) * (p2 . 2)) - ((p1 . 2) * (p2 . 1))) + (((p1 . 1) * (p3 . 2)) - ((p1 . 2) * (p3 . 1))))]|
by Lm8
.=
|[(((((p1 . 2) * (p2 . 3)) - ((p1 . 3) * (p2 . 2))) + ((p1 . 2) * (p3 . 3))) - ((p1 . 3) * (p3 . 2))),(((((p1 . 3) * (p2 . 1)) - ((p1 . 1) * (p2 . 3))) + ((p1 . 3) * (p3 . 1))) - ((p1 . 1) * (p3 . 3))),(((((p1 . 1) * (p2 . 2)) - ((p1 . 2) * (p2 . 1))) + ((p1 . 1) * (p3 . 2))) - ((p1 . 2) * (p3 . 1)))]|
;
hence
p1 <X> (p2 + p3) = (p1 <X> p2) + (p1 <X> p3)
by A2, A3, A4; verum