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 
|- .- = ( -g ` W )
baerlem3.o 
|- .0. = ( 0g ` W )
baerlem3.s 
|- .(+) = ( LSSum ` W )
baerlem3.n 
|- N = ( LSpan ` W )
baerlem3.w 
|- ( ph -> W e. LVec )
baerlem3.x 
|- ( ph -> X e. V )
baerlem3.c 
|- ( ph -> -. X e. ( N ` { Y , Z } ) )
baerlem3.d 
|- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )
baerlem3.y 
|- ( ph -> Y e. ( V \ { .0. } ) )
baerlem3.z 
|- ( ph -> Z e. ( V \ { .0. } ) )
baerlem5a.p 
|- .+ = ( +g ` W )
Assertion baerlem5abmN 
|- ( ph -> ( ( N ` { ( X .- ( Y .- Z ) ) } ) = ( ( ( N ` { ( X .- Y ) } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .+ Z ) } ) .(+) ( N ` { Y } ) ) ) /\ ( N ` { ( Y .- Z ) } ) = ( ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- ( Y .- Z ) ) } ) .(+) ( N ` { X } ) ) ) ) )

Proof

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