Metamath Proof Explorer


Theorem baerlem5bmN

Description: An equality that holds when X , Y , Z are independent (non-colinear) vectors. Subtraction version of second equation of part (5) in Baer p. 46. TODO: This is the subtraction version, may not be needed. TODO: delete if baerlem5abmN is used. (Contributed by NM, 24-May-2015) (New usage is discouraged.)

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 baerlem5bmN φNY-˙Z=NY˙NZNX-˙Y-˙Z˙NX

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 10 eldifad φYV
14 11 eldifad φZV
15 eqid invgW=invgW
16 1 12 15 2 grpsubval YVZVY-˙Z=Y+˙invgWZ
17 13 14 16 syl2anc φY-˙Z=Y+˙invgWZ
18 17 sneqd φY-˙Z=Y+˙invgWZ
19 18 fveq2d φNY-˙Z=NY+˙invgWZ
20 lveclmod WLVecWLMod
21 6 20 syl φWLMod
22 1 15 lmodvnegcl WLModZVinvgWZV
23 21 14 22 syl2anc φinvgWZV
24 eqid LSubSpW=LSubSpW
25 1 24 5 21 13 14 lspprcl φNYZLSubSpW
26 3 24 21 25 7 8 lssneln0 φXV0˙
27 1 5 6 7 13 14 8 lspindpi φNXNYNXNZ
28 27 simpld φNXNY
29 1 3 5 6 26 13 28 lspsnne1 φ¬XNY
30 9 necomd φNZNY
31 1 3 5 6 11 13 30 lspsnne1 φ¬ZNY
32 1 5 6 7 14 13 31 8 lspexchn2 φ¬ZNYX
33 lmodgrp WLModWGrp
34 21 33 syl φWGrp
35 34 adantr φinvgWZNYXWGrp
36 14 adantr φinvgWZNYXZV
37 1 15 grpinvinv WGrpZVinvgWinvgWZ=Z
38 35 36 37 syl2anc φinvgWZNYXinvgWinvgWZ=Z
39 21 adantr φinvgWZNYXWLMod
40 1 24 5 21 13 7 lspprcl φNYXLSubSpW
41 40 adantr φinvgWZNYXNYXLSubSpW
42 simpr φinvgWZNYXinvgWZNYX
43 24 15 lssvnegcl WLModNYXLSubSpWinvgWZNYXinvgWinvgWZNYX
44 39 41 42 43 syl3anc φinvgWZNYXinvgWinvgWZNYX
45 38 44 eqeltrrd φinvgWZNYXZNYX
46 32 45 mtand φ¬invgWZNYX
47 1 5 6 23 7 13 29 46 lspexchn2 φ¬XNYinvgWZ
48 1 15 5 lspsnneg WLModZVNinvgWZ=NZ
49 21 14 48 syl2anc φNinvgWZ=NZ
50 9 49 neeqtrrd φNYNinvgWZ
51 1 3 15 grpinvnzcl WGrpZV0˙invgWZV0˙
52 34 11 51 syl2anc φinvgWZV0˙
53 1 2 3 4 5 6 7 47 50 10 52 12 baerlem5b φNY+˙invgWZ=NY˙NinvgWZNX-˙Y+˙invgWZ˙NX
54 49 oveq2d φNY˙NinvgWZ=NY˙NZ
55 17 eqcomd φY+˙invgWZ=Y-˙Z
56 55 oveq2d φX-˙Y+˙invgWZ=X-˙Y-˙Z
57 56 sneqd φX-˙Y+˙invgWZ=X-˙Y-˙Z
58 57 fveq2d φNX-˙Y+˙invgWZ=NX-˙Y-˙Z
59 58 oveq1d φNX-˙Y+˙invgWZ˙NX=NX-˙Y-˙Z˙NX
60 54 59 ineq12d φNY˙NinvgWZNX-˙Y+˙invgWZ˙NX=NY˙NZNX-˙Y-˙Z˙NX
61 19 53 60 3eqtrd φNY-˙Z=NY˙NZNX-˙Y-˙Z˙NX