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 ⊢ 𝑉 = ( Base ‘ 𝑊 )
baerlem3.m ⊢ − = ( -g ‘ 𝑊 )
baerlem3.o ⊢ 0 = ( 0g ‘ 𝑊 )
baerlem3.s ⊢ ⊕ = ( LSSum ‘ 𝑊 )
baerlem3.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
baerlem3.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
baerlem3.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
baerlem3.c ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
baerlem3.d ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ≠ ( 𝑁 ‘ { 𝑍 } ) )
baerlem3.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
baerlem3.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑉 ∖ { 0 } ) )
baerlem5a.p ⊢ + = ( +g ‘ 𝑊 )
Assertion baerlem5abmN ( 𝜑 → ( ( 𝑁 ‘ { ( 𝑋 − ( 𝑌 − 𝑍 ) ) } ) = ( ( ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ⊕ ( 𝑁 ‘ { 𝑍 } ) ) ∩ ( ( 𝑁 ‘ { ( 𝑋 + 𝑍 ) } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ ( 𝑁 ‘ { ( 𝑌 − 𝑍 ) } ) = ( ( ( 𝑁 ‘ { 𝑌 } ) ⊕ ( 𝑁 ‘ { 𝑍 } ) ) ∩ ( ( 𝑁 ‘ { ( 𝑋 − ( 𝑌 − 𝑍 ) ) } ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ) )

Proof

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