let r be Real; for p1, p2 being Element of REAL 3 holds
( (r * p1) <X> p2 = r * (p1 <X> p2) & (r * p1) <X> p2 = p1 <X> (r * p2) )
let p1, p2 be Element of REAL 3; ( (r * p1) <X> p2 = r * (p1 <X> p2) & (r * p1) <X> p2 = p1 <X> (r * p2) )
A1:
( (p1 <X> p2) . 1 = ((p1 . 2) * (p2 . 3)) - ((p1 . 3) * (p2 . 2)) & (p1 <X> p2) . 2 = ((p1 . 3) * (p2 . 1)) - ((p1 . 1) * (p2 . 3)) & (p1 <X> p2) . 3 = ((p1 . 1) * (p2 . 2)) - ((p1 . 2) * (p2 . 1)) )
by FINSEQ_1:45;
A2: (r * p1) <X> p2 =
|[(r * (p1 . 1)),(r * (p1 . 2)),(r * (p1 . 3))]| <X> p2
by Lm1
.=
|[(r * (p1 . 1)),(r * (p1 . 2)),(r * (p1 . 3))]| <X> |[(p2 . 1),(p2 . 2),(p2 . 3)]|
by Th1
.=
|[(((r * (p1 . 2)) * (p2 . 3)) - ((r * (p1 . 3)) * (p2 . 2))),(((r * (p1 . 3)) * (p2 . 1)) - ((r * (p1 . 1)) * (p2 . 3))),(((r * (p1 . 1)) * (p2 . 2)) - ((r * (p1 . 2)) * (p2 . 1)))]|
by Lm13
;
then A3: (r * p1) <X> p2 =
|[(r * ((p1 <X> p2) . 1)),(r * ((p1 <X> p2) . 2)),(r * ((p1 <X> p2) . 3))]|
by A1
.=
r * (p1 <X> p2)
by Lm1
;
(r * p1) <X> p2 =
|[(((p1 . 2) * (r * (p2 . 3))) - ((p1 . 3) * (r * (p2 . 2)))),(((p1 . 3) * (r * (p2 . 1))) - ((p1 . 1) * (r * (p2 . 3)))),(((p1 . 1) * (r * (p2 . 2))) - ((p1 . 2) * (r * (p2 . 1))))]|
by A2
.=
|[(p1 . 1),(p1 . 2),(p1 . 3)]| <X> |[(r * (p2 . 1)),(r * (p2 . 2)),(r * (p2 . 3))]|
by Lm13
.=
p1 <X> |[(r * (p2 . 1)),(r * (p2 . 2)),(r * (p2 . 3))]|
by Th1
.=
p1 <X> (r * p2)
by Lm1
;
hence
( (r * p1) <X> p2 = r * (p1 <X> p2) & (r * p1) <X> p2 = p1 <X> (r * p2) )
by A3; verum