baerlem5amN

Description: An equality that holds when X , Y , Z are independent (non-colinear) vectors. Subtraction version of first 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	baerlem5amN	\|- ( ph -> ( N ` { ( X .- ( Y .- Z ) ) } ) = ( ( ( N ` { ( X .- Y ) } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .+ Z ) } ) .(+) ( N ` { Y } ) ) ) )

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 } ) ) ) )

Metamath Proof Explorer

Theorem baerlem5amN

Proof