Metamath Proof Explorer


Theorem baerlem5abmN

Description: An equality that holds when X , Y , Z are independent (non-colinear) vectors. Subtraction versions of first and second equations of part (5) in Baer p. 46, conjoined to share commonality in their proofs. TODO: Delete if not needed. (Contributed by NM, 24-May-2015) (New usage is discouraged.)

Ref Expression
Hypotheses baerlem3.v V = Base W
baerlem3.m - ˙ = - W
baerlem3.o 0 ˙ = 0 W
baerlem3.s ˙ = LSSum W
baerlem3.n N = LSpan W
baerlem3.w φ W LVec
baerlem3.x φ X V
baerlem3.c φ ¬ X N Y Z
baerlem3.d φ N Y N Z
baerlem3.y φ Y V 0 ˙
baerlem3.z φ Z V 0 ˙
baerlem5a.p + ˙ = + W
Assertion baerlem5abmN φ N X - ˙ Y - ˙ Z = N X - ˙ Y ˙ N Z N X + ˙ Z ˙ N Y N Y - ˙ Z = N Y ˙ N Z N X - ˙ Y - ˙ Z ˙ N X

Proof

Step Hyp Ref Expression
1 baerlem3.v V = Base W
2 baerlem3.m - ˙ = - W
3 baerlem3.o 0 ˙ = 0 W
4 baerlem3.s ˙ = LSSum W
5 baerlem3.n N = LSpan W
6 baerlem3.w φ W LVec
7 baerlem3.x φ X V
8 baerlem3.c φ ¬ X N Y Z
9 baerlem3.d φ N Y N Z
10 baerlem3.y φ Y V 0 ˙
11 baerlem3.z φ Z V 0 ˙
12 baerlem5a.p + ˙ = + W
13 10 eldifad φ Y V
14 11 eldifad φ Z V
15 eqid inv g W = inv g W
16 1 12 15 2 grpsubval Y V Z V Y - ˙ Z = Y + ˙ inv g W Z
17 13 14 16 syl2anc φ Y - ˙ Z = Y + ˙ inv g W Z
18 17 oveq2d φ X - ˙ Y - ˙ Z = X - ˙ Y + ˙ inv g W Z
19 18 sneqd φ X - ˙ Y - ˙ Z = X - ˙ Y + ˙ inv g W Z
20 19 fveq2d φ N X - ˙ Y - ˙ Z = N X - ˙ Y + ˙ inv g W Z
21 lveclmod W LVec W LMod
22 6 21 syl φ W LMod
23 1 15 lmodvnegcl W LMod Z V inv g W Z V
24 22 14 23 syl2anc φ inv g W Z V
25 eqid LSubSp W = LSubSp W
26 1 25 5 22 13 14 lspprcl φ N Y Z LSubSp W
27 3 25 22 26 7 8 lssneln0 φ X V 0 ˙
28 1 5 6 7 13 14 8 lspindpi φ N X N Y N X N Z
29 28 simpld φ N X N Y
30 1 3 5 6 27 13 29 lspsnne1 φ ¬ X N Y
31 9 necomd φ N Z N Y
32 1 3 5 6 11 13 31 lspsnne1 φ ¬ Z N Y
33 1 5 6 7 14 13 32 8 lspexchn2 φ ¬ Z N Y X
34 lmodgrp W LMod W Grp
35 6 21 34 3syl φ W Grp
36 35 adantr φ inv g W Z N Y X W Grp
37 14 adantr φ inv g W Z N Y X Z V
38 1 15 grpinvinv W Grp Z V inv g W inv g W Z = Z
39 36 37 38 syl2anc φ inv g W Z N Y X inv g W inv g W Z = Z
40 22 adantr φ inv g W Z N Y X W LMod
41 1 25 5 22 13 7 lspprcl φ N Y X LSubSp W
42 41 adantr φ inv g W Z N Y X N Y X LSubSp W
43 simpr φ inv g W Z N Y X inv g W Z N Y X
44 25 15 lssvnegcl W LMod N Y X LSubSp W inv g W Z N Y X inv g W inv g W Z N Y X
45 40 42 43 44 syl3anc φ inv g W Z N Y X inv g W inv g W Z N Y X
46 39 45 eqeltrrd φ inv g W Z N Y X Z N Y X
47 33 46 mtand φ ¬ inv g W Z N Y X
48 1 5 6 24 7 13 30 47 lspexchn2 φ ¬ X N Y inv g W Z
49 1 15 5 lspsnneg W LMod Z V N inv g W Z = N Z
50 22 14 49 syl2anc φ N inv g W Z = N Z
51 9 50 neeqtrrd φ N Y N inv g W Z
52 1 3 15 grpinvnzcl W Grp Z V 0 ˙ inv g W Z V 0 ˙
53 35 11 52 syl2anc φ inv g W Z V 0 ˙
54 1 2 3 4 5 6 7 48 51 10 53 12 baerlem5a φ N X - ˙ Y + ˙ inv g W Z = N X - ˙ Y ˙ N inv g W Z N X - ˙ inv g W Z ˙ N Y
55 50 oveq2d φ N X - ˙ Y ˙ N inv g W Z = N X - ˙ Y ˙ N Z
56 1 12 2 15 35 7 14 grpsubinv φ X - ˙ inv g W Z = X + ˙ Z
57 56 sneqd φ X - ˙ inv g W Z = X + ˙ Z
58 57 fveq2d φ N X - ˙ inv g W Z = N X + ˙ Z
59 58 oveq1d φ N X - ˙ inv g W Z ˙ N Y = N X + ˙ Z ˙ N Y
60 55 59 ineq12d φ N X - ˙ Y ˙ N inv g W Z N X - ˙ inv g W Z ˙ N Y = N X - ˙ Y ˙ N Z N X + ˙ Z ˙ N Y
61 20 54 60 3eqtrd φ N X - ˙ Y - ˙ Z = N X - ˙ Y ˙ N Z N X + ˙ Z ˙ N Y
62 17 sneqd φ Y - ˙ Z = Y + ˙ inv g W Z
63 62 fveq2d φ N Y - ˙ Z = N Y + ˙ inv g W Z
64 1 2 3 4 5 6 7 48 51 10 53 12 baerlem5b φ N Y + ˙ inv g W Z = N Y ˙ N inv g W Z N X - ˙ Y + ˙ inv g W Z ˙ N X
65 50 oveq2d φ N Y ˙ N inv g W Z = N Y ˙ N Z
66 17 eqcomd φ Y + ˙ inv g W Z = Y - ˙ Z
67 66 oveq2d φ X - ˙ Y + ˙ inv g W Z = X - ˙ Y - ˙ Z
68 67 sneqd φ X - ˙ Y + ˙ inv g W Z = X - ˙ Y - ˙ Z
69 68 fveq2d φ N X - ˙ Y + ˙ inv g W Z = N X - ˙ Y - ˙ Z
70 69 oveq1d φ N X - ˙ Y + ˙ inv g W Z ˙ N X = N X - ˙ Y - ˙ Z ˙ N X
71 65 70 ineq12d φ N Y ˙ N inv g W Z N X - ˙ Y + ˙ inv g W Z ˙ N X = N Y ˙ N Z N X - ˙ Y - ˙ Z ˙ N X
72 63 64 71 3eqtrd φ N Y - ˙ Z = N Y ˙ N Z N X - ˙ Y - ˙ Z ˙ N X
73 61 72 jca φ N X - ˙ Y - ˙ Z = N X - ˙ Y ˙ N Z N X + ˙ Z ˙ N Y N Y - ˙ Z = N Y ˙ N Z N X - ˙ Y - ˙ Z ˙ N X