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 = ( 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 baerlem5bmN
|- ( ph -> ( 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 sneqd
 |-  ( ph -> { ( Y .- Z ) } = { ( Y .+ ( ( invg ` W ) ` Z ) ) } )
19 18 fveq2d
 |-  ( ph -> ( N ` { ( Y .- Z ) } ) = ( N ` { ( Y .+ ( ( invg ` W ) ` Z ) ) } ) )
20 lveclmod
 |-  ( W e. LVec -> W e. LMod )
21 6 20 syl
 |-  ( ph -> W e. LMod )
22 1 15 lmodvnegcl
 |-  ( ( W e. LMod /\ Z e. V ) -> ( ( invg ` W ) ` Z ) e. V )
23 21 14 22 syl2anc
 |-  ( ph -> ( ( invg ` W ) ` Z ) e. V )
24 eqid
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
25 1 24 5 21 13 14 lspprcl
 |-  ( ph -> ( N ` { Y , Z } ) e. ( LSubSp ` W ) )
26 3 24 21 25 7 8 lssneln0
 |-  ( ph -> X e. ( V \ { .0. } ) )
27 1 5 6 7 13 14 8 lspindpi
 |-  ( ph -> ( ( N ` { X } ) =/= ( N ` { Y } ) /\ ( N ` { X } ) =/= ( N ` { Z } ) ) )
28 27 simpld
 |-  ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
29 1 3 5 6 26 13 28 lspsnne1
 |-  ( ph -> -. X e. ( N ` { Y } ) )
30 9 necomd
 |-  ( ph -> ( N ` { Z } ) =/= ( N ` { Y } ) )
31 1 3 5 6 11 13 30 lspsnne1
 |-  ( ph -> -. Z e. ( N ` { Y } ) )
32 1 5 6 7 14 13 31 8 lspexchn2
 |-  ( ph -> -. Z e. ( N ` { Y , X } ) )
33 lmodgrp
 |-  ( W e. LMod -> W e. Grp )
34 21 33 syl
 |-  ( ph -> W e. Grp )
35 34 adantr
 |-  ( ( ph /\ ( ( invg ` W ) ` Z ) e. ( N ` { Y , X } ) ) -> W e. Grp )
36 14 adantr
 |-  ( ( ph /\ ( ( invg ` W ) ` Z ) e. ( N ` { Y , X } ) ) -> Z e. V )
37 1 15 grpinvinv
 |-  ( ( W e. Grp /\ Z e. V ) -> ( ( invg ` W ) ` ( ( invg ` W ) ` Z ) ) = Z )
38 35 36 37 syl2anc
 |-  ( ( ph /\ ( ( invg ` W ) ` Z ) e. ( N ` { Y , X } ) ) -> ( ( invg ` W ) ` ( ( invg ` W ) ` Z ) ) = Z )
39 21 adantr
 |-  ( ( ph /\ ( ( invg ` W ) ` Z ) e. ( N ` { Y , X } ) ) -> W e. LMod )
40 1 24 5 21 13 7 lspprcl
 |-  ( ph -> ( N ` { Y , X } ) e. ( LSubSp ` W ) )
41 40 adantr
 |-  ( ( ph /\ ( ( invg ` W ) ` Z ) e. ( N ` { Y , X } ) ) -> ( N ` { Y , X } ) e. ( LSubSp ` W ) )
42 simpr
 |-  ( ( ph /\ ( ( invg ` W ) ` Z ) e. ( N ` { Y , X } ) ) -> ( ( invg ` W ) ` Z ) e. ( N ` { Y , X } ) )
43 24 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 } ) )
44 39 41 42 43 syl3anc
 |-  ( ( ph /\ ( ( invg ` W ) ` Z ) e. ( N ` { Y , X } ) ) -> ( ( invg ` W ) ` ( ( invg ` W ) ` Z ) ) e. ( N ` { Y , X } ) )
45 38 44 eqeltrrd
 |-  ( ( ph /\ ( ( invg ` W ) ` Z ) e. ( N ` { Y , X } ) ) -> Z e. ( N ` { Y , X } ) )
46 32 45 mtand
 |-  ( ph -> -. ( ( invg ` W ) ` Z ) e. ( N ` { Y , X } ) )
47 1 5 6 23 7 13 29 46 lspexchn2
 |-  ( ph -> -. X e. ( N ` { Y , ( ( invg ` W ) ` Z ) } ) )
48 1 15 5 lspsnneg
 |-  ( ( W e. LMod /\ Z e. V ) -> ( N ` { ( ( invg ` W ) ` Z ) } ) = ( N ` { Z } ) )
49 21 14 48 syl2anc
 |-  ( ph -> ( N ` { ( ( invg ` W ) ` Z ) } ) = ( N ` { Z } ) )
50 9 49 neeqtrrd
 |-  ( ph -> ( N ` { Y } ) =/= ( N ` { ( ( invg ` W ) ` Z ) } ) )
51 1 3 15 grpinvnzcl
 |-  ( ( W e. Grp /\ Z e. ( V \ { .0. } ) ) -> ( ( invg ` W ) ` Z ) e. ( V \ { .0. } ) )
52 34 11 51 syl2anc
 |-  ( ph -> ( ( invg ` W ) ` Z ) e. ( V \ { .0. } ) )
53 1 2 3 4 5 6 7 47 50 10 52 12 baerlem5b
 |-  ( ph -> ( N ` { ( Y .+ ( ( invg ` W ) ` Z ) ) } ) = ( ( ( N ` { Y } ) .(+) ( N ` { ( ( invg ` W ) ` Z ) } ) ) i^i ( ( N ` { ( X .- ( Y .+ ( ( invg ` W ) ` Z ) ) ) } ) .(+) ( N ` { X } ) ) ) )
54 49 oveq2d
 |-  ( ph -> ( ( N ` { Y } ) .(+) ( N ` { ( ( invg ` W ) ` Z ) } ) ) = ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) )
55 17 eqcomd
 |-  ( ph -> ( Y .+ ( ( invg ` W ) ` Z ) ) = ( Y .- Z ) )
56 55 oveq2d
 |-  ( ph -> ( X .- ( Y .+ ( ( invg ` W ) ` Z ) ) ) = ( X .- ( Y .- Z ) ) )
57 56 sneqd
 |-  ( ph -> { ( X .- ( Y .+ ( ( invg ` W ) ` Z ) ) ) } = { ( X .- ( Y .- Z ) ) } )
58 57 fveq2d
 |-  ( ph -> ( N ` { ( X .- ( Y .+ ( ( invg ` W ) ` Z ) ) ) } ) = ( N ` { ( X .- ( Y .- Z ) ) } ) )
59 58 oveq1d
 |-  ( ph -> ( ( N ` { ( X .- ( Y .+ ( ( invg ` W ) ` Z ) ) ) } ) .(+) ( N ` { X } ) ) = ( ( N ` { ( X .- ( Y .- Z ) ) } ) .(+) ( N ` { X } ) ) )
60 54 59 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 } ) ) ) )
61 19 53 60 3eqtrd
 |-  ( ph -> ( N ` { ( Y .- Z ) } ) = ( ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- ( Y .- Z ) ) } ) .(+) ( N ` { X } ) ) ) )