Metamath Proof Explorer


Theorem baerlem5a

Description: An equality that holds when X , Y , Z are independent (non-colinear) vectors. First equation of part (5) in Baer p. 46. (Contributed by NM, 10-Apr-2015)

Ref Expression
Hypotheses baerlem3.v V=BaseW
baerlem3.m -˙=-W
baerlem3.o 0˙=0W
baerlem3.s ˙=LSSumW
baerlem3.n N=LSpanW
baerlem3.w φWLVec
baerlem3.x φXV
baerlem3.c φ¬XNYZ
baerlem3.d φNYNZ
baerlem3.y φYV0˙
baerlem3.z φZV0˙
baerlem5a.p +˙=+W
Assertion baerlem5a φNX-˙Y+˙Z=NX-˙Y˙NZNX-˙Z˙NY

Proof

Step Hyp Ref Expression
1 baerlem3.v V=BaseW
2 baerlem3.m -˙=-W
3 baerlem3.o 0˙=0W
4 baerlem3.s ˙=LSSumW
5 baerlem3.n N=LSpanW
6 baerlem3.w φWLVec
7 baerlem3.x φXV
8 baerlem3.c φ¬XNYZ
9 baerlem3.d φNYNZ
10 baerlem3.y φYV0˙
11 baerlem3.z φZV0˙
12 baerlem5a.p +˙=+W
13 eqid W=W
14 eqid ScalarW=ScalarW
15 eqid BaseScalarW=BaseScalarW
16 eqid +ScalarW=+ScalarW
17 eqid -ScalarW=-ScalarW
18 eqid 0ScalarW=0ScalarW
19 eqid invgScalarW=invgScalarW
20 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 baerlem5alem2 φNX-˙Y+˙Z=NX-˙Y˙NZNX-˙Z˙NY