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 𝑉 = ( 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 baerlem5bmN ( 𝜑 → ( 𝑁 ‘ { ( 𝑌 𝑍 ) } ) = ( ( ( 𝑁 ‘ { 𝑌 } ) ( 𝑁 ‘ { 𝑍 } ) ) ∩ ( ( 𝑁 ‘ { ( 𝑋 ( 𝑌 𝑍 ) ) } ) ( 𝑁 ‘ { 𝑋 } ) ) ) )

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 sneqd ( 𝜑 → { ( 𝑌 𝑍 ) } = { ( 𝑌 + ( ( invg𝑊 ) ‘ 𝑍 ) ) } )
19 18 fveq2d ( 𝜑 → ( 𝑁 ‘ { ( 𝑌 𝑍 ) } ) = ( 𝑁 ‘ { ( 𝑌 + ( ( invg𝑊 ) ‘ 𝑍 ) ) } ) )
20 lveclmod ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
21 6 20 syl ( 𝜑𝑊 ∈ LMod )
22 1 15 lmodvnegcl ( ( 𝑊 ∈ LMod ∧ 𝑍𝑉 ) → ( ( invg𝑊 ) ‘ 𝑍 ) ∈ 𝑉 )
23 21 14 22 syl2anc ( 𝜑 → ( ( invg𝑊 ) ‘ 𝑍 ) ∈ 𝑉 )
24 eqid ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
25 1 24 5 21 13 14 lspprcl ( 𝜑 → ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ∈ ( LSubSp ‘ 𝑊 ) )
26 3 24 21 25 7 8 lssneln0 ( 𝜑𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
27 1 5 6 7 13 14 8 lspindpi ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) ∧ ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑍 } ) ) )
28 27 simpld ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
29 1 3 5 6 26 13 28 lspsnne1 ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) )
30 9 necomd ( 𝜑 → ( 𝑁 ‘ { 𝑍 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
31 1 3 5 6 11 13 30 lspsnne1 ( 𝜑 → ¬ 𝑍 ∈ ( 𝑁 ‘ { 𝑌 } ) )
32 1 5 6 7 14 13 31 8 lspexchn2 ( 𝜑 → ¬ 𝑍 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) )
33 lmodgrp ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
34 21 33 syl ( 𝜑𝑊 ∈ Grp )
35 34 adantr ( ( 𝜑 ∧ ( ( invg𝑊 ) ‘ 𝑍 ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ) → 𝑊 ∈ Grp )
36 14 adantr ( ( 𝜑 ∧ ( ( invg𝑊 ) ‘ 𝑍 ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ) → 𝑍𝑉 )
37 1 15 grpinvinv ( ( 𝑊 ∈ Grp ∧ 𝑍𝑉 ) → ( ( invg𝑊 ) ‘ ( ( invg𝑊 ) ‘ 𝑍 ) ) = 𝑍 )
38 35 36 37 syl2anc ( ( 𝜑 ∧ ( ( invg𝑊 ) ‘ 𝑍 ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ) → ( ( invg𝑊 ) ‘ ( ( invg𝑊 ) ‘ 𝑍 ) ) = 𝑍 )
39 21 adantr ( ( 𝜑 ∧ ( ( invg𝑊 ) ‘ 𝑍 ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ) → 𝑊 ∈ LMod )
40 1 24 5 21 13 7 lspprcl ( 𝜑 → ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
41 40 adantr ( ( 𝜑 ∧ ( ( invg𝑊 ) ‘ 𝑍 ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ) → ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
42 simpr ( ( 𝜑 ∧ ( ( invg𝑊 ) ‘ 𝑍 ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ) → ( ( invg𝑊 ) ‘ 𝑍 ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) )
43 24 15 lssvnegcl ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) ∧ ( ( invg𝑊 ) ‘ 𝑍 ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ) → ( ( invg𝑊 ) ‘ ( ( invg𝑊 ) ‘ 𝑍 ) ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) )
44 39 41 42 43 syl3anc ( ( 𝜑 ∧ ( ( invg𝑊 ) ‘ 𝑍 ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ) → ( ( invg𝑊 ) ‘ ( ( invg𝑊 ) ‘ 𝑍 ) ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) )
45 38 44 eqeltrrd ( ( 𝜑 ∧ ( ( invg𝑊 ) ‘ 𝑍 ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ) → 𝑍 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) )
46 32 45 mtand ( 𝜑 → ¬ ( ( invg𝑊 ) ‘ 𝑍 ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) )
47 1 5 6 23 7 13 29 46 lspexchn2 ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , ( ( invg𝑊 ) ‘ 𝑍 ) } ) )
48 1 15 5 lspsnneg ( ( 𝑊 ∈ LMod ∧ 𝑍𝑉 ) → ( 𝑁 ‘ { ( ( invg𝑊 ) ‘ 𝑍 ) } ) = ( 𝑁 ‘ { 𝑍 } ) )
49 21 14 48 syl2anc ( 𝜑 → ( 𝑁 ‘ { ( ( invg𝑊 ) ‘ 𝑍 ) } ) = ( 𝑁 ‘ { 𝑍 } ) )
50 9 49 neeqtrrd ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ≠ ( 𝑁 ‘ { ( ( invg𝑊 ) ‘ 𝑍 ) } ) )
51 1 3 15 grpinvnzcl ( ( 𝑊 ∈ Grp ∧ 𝑍 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ( invg𝑊 ) ‘ 𝑍 ) ∈ ( 𝑉 ∖ { 0 } ) )
52 34 11 51 syl2anc ( 𝜑 → ( ( invg𝑊 ) ‘ 𝑍 ) ∈ ( 𝑉 ∖ { 0 } ) )
53 1 2 3 4 5 6 7 47 50 10 52 12 baerlem5b ( 𝜑 → ( 𝑁 ‘ { ( 𝑌 + ( ( invg𝑊 ) ‘ 𝑍 ) ) } ) = ( ( ( 𝑁 ‘ { 𝑌 } ) ( 𝑁 ‘ { ( ( invg𝑊 ) ‘ 𝑍 ) } ) ) ∩ ( ( 𝑁 ‘ { ( 𝑋 ( 𝑌 + ( ( invg𝑊 ) ‘ 𝑍 ) ) ) } ) ( 𝑁 ‘ { 𝑋 } ) ) ) )
54 49 oveq2d ( 𝜑 → ( ( 𝑁 ‘ { 𝑌 } ) ( 𝑁 ‘ { ( ( invg𝑊 ) ‘ 𝑍 ) } ) ) = ( ( 𝑁 ‘ { 𝑌 } ) ( 𝑁 ‘ { 𝑍 } ) ) )
55 17 eqcomd ( 𝜑 → ( 𝑌 + ( ( invg𝑊 ) ‘ 𝑍 ) ) = ( 𝑌 𝑍 ) )
56 55 oveq2d ( 𝜑 → ( 𝑋 ( 𝑌 + ( ( invg𝑊 ) ‘ 𝑍 ) ) ) = ( 𝑋 ( 𝑌 𝑍 ) ) )
57 56 sneqd ( 𝜑 → { ( 𝑋 ( 𝑌 + ( ( invg𝑊 ) ‘ 𝑍 ) ) ) } = { ( 𝑋 ( 𝑌 𝑍 ) ) } )
58 57 fveq2d ( 𝜑 → ( 𝑁 ‘ { ( 𝑋 ( 𝑌 + ( ( invg𝑊 ) ‘ 𝑍 ) ) ) } ) = ( 𝑁 ‘ { ( 𝑋 ( 𝑌 𝑍 ) ) } ) )
59 58 oveq1d ( 𝜑 → ( ( 𝑁 ‘ { ( 𝑋 ( 𝑌 + ( ( invg𝑊 ) ‘ 𝑍 ) ) ) } ) ( 𝑁 ‘ { 𝑋 } ) ) = ( ( 𝑁 ‘ { ( 𝑋 ( 𝑌 𝑍 ) ) } ) ( 𝑁 ‘ { 𝑋 } ) ) )
60 54 59 ineq12d ( 𝜑 → ( ( ( 𝑁 ‘ { 𝑌 } ) ( 𝑁 ‘ { ( ( invg𝑊 ) ‘ 𝑍 ) } ) ) ∩ ( ( 𝑁 ‘ { ( 𝑋 ( 𝑌 + ( ( invg𝑊 ) ‘ 𝑍 ) ) ) } ) ( 𝑁 ‘ { 𝑋 } ) ) ) = ( ( ( 𝑁 ‘ { 𝑌 } ) ( 𝑁 ‘ { 𝑍 } ) ) ∩ ( ( 𝑁 ‘ { ( 𝑋 ( 𝑌 𝑍 ) ) } ) ( 𝑁 ‘ { 𝑋 } ) ) ) )
61 19 53 60 3eqtrd ( 𝜑 → ( 𝑁 ‘ { ( 𝑌 𝑍 ) } ) = ( ( ( 𝑁 ‘ { 𝑌 } ) ( 𝑁 ‘ { 𝑍 } ) ) ∩ ( ( 𝑁 ‘ { ( 𝑋 ( 𝑌 𝑍 ) ) } ) ( 𝑁 ‘ { 𝑋 } ) ) ) )