mapdpglem5N

Description: Lemma for mapdpg . (Contributed by NM, 20-Mar-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mapdpglem.h	\|- H = ( LHyp ` K )
	mapdpglem.m	\|- M = ( ( mapd ` K ) ` W )
	mapdpglem.u	\|- U = ( ( DVecH ` K ) ` W )
	mapdpglem.v	\|- V = ( Base ` U )
	mapdpglem.s	\|- .- = ( -g ` U )
	mapdpglem.n	\|- N = ( LSpan ` U )
	mapdpglem.c	\|- C = ( ( LCDual ` K ) ` W )
	mapdpglem.k	\|- ( ph -> ( K e. HL /\ W e. H ) )
	mapdpglem.x	\|- ( ph -> X e. V )
	mapdpglem.y	\|- ( ph -> Y e. V )
	mapdpglem1.p	\|- .(+) = ( LSSum ` C )
	mapdpglem2.j	\|- J = ( LSpan ` C )
	mapdpglem3.f	\|- F = ( Base ` C )
	mapdpglem3.te	\|- ( ph -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) )
	mapdpglem3.a	\|- A = ( Scalar ` U )
	mapdpglem3.b	\|- B = ( Base ` A )
	mapdpglem3.t	\|- .x. = ( .s ` C )
	mapdpglem3.r	\|- R = ( -g ` C )
	mapdpglem3.g	\|- ( ph -> G e. F )
	mapdpglem3.e	\|- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )
	mapdpglem4.q	\|- Q = ( 0g ` U )
	mapdpglem.ne	\|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
	mapdpglem4.jt	\|- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) )
Assertion	mapdpglem5N	\|- ( ph -> t =/= ( 0g ` C ) )

Proof

Step	Hyp	Ref	Expression
1		mapdpglem.h	\|- H = ( LHyp ` K )
2		mapdpglem.m	\|- M = ( ( mapd ` K ) ` W )
3		mapdpglem.u	\|- U = ( ( DVecH ` K ) ` W )
4		mapdpglem.v	\|- V = ( Base ` U )
5		mapdpglem.s	\|- .- = ( -g ` U )
6		mapdpglem.n	\|- N = ( LSpan ` U )
7		mapdpglem.c	\|- C = ( ( LCDual ` K ) ` W )
8		mapdpglem.k	\|- ( ph -> ( K e. HL /\ W e. H ) )
9		mapdpglem.x	\|- ( ph -> X e. V )
10		mapdpglem.y	\|- ( ph -> Y e. V )
11		mapdpglem1.p	\|- .(+) = ( LSSum ` C )
12		mapdpglem2.j	\|- J = ( LSpan ` C )
13		mapdpglem3.f	\|- F = ( Base ` C )
14		mapdpglem3.te	\|- ( ph -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) )
15		mapdpglem3.a	\|- A = ( Scalar ` U )
16		mapdpglem3.b	\|- B = ( Base ` A )
17		mapdpglem3.t	\|- .x. = ( .s ` C )
18		mapdpglem3.r	\|- R = ( -g ` C )
19		mapdpglem3.g	\|- ( ph -> G e. F )
20		mapdpglem3.e	\|- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )
21		mapdpglem4.q	\|- Q = ( 0g ` U )
22		mapdpglem.ne	\|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
23		mapdpglem4.jt	\|- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) )
24		eqid	\|- ( LSAtoms ` U ) = ( LSAtoms ` U )
25		eqid	\|- ( LSAtoms ` C ) = ( LSAtoms ` C )
26	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22	mapdpglem4N	\|- ( ph -> ( X .- Y ) =/= Q )
27	1 3 8	dvhlmod	\|- ( ph -> U e. LMod )
28	4 5	lmodvsubcl	\|- ( ( U e. LMod /\ X e. V /\ Y e. V ) -> ( X .- Y ) e. V )
29	27 9 10 28	syl3anc	\|- ( ph -> ( X .- Y ) e. V )
30	4 6 21 24 27 29	lsatspn0	\|- ( ph -> ( ( N ` { ( X .- Y ) } ) e. ( LSAtoms ` U ) <-> ( X .- Y ) =/= Q ) )
31	26 30	mpbird	\|- ( ph -> ( N ` { ( X .- Y ) } ) e. ( LSAtoms ` U ) )
32	1 2 3 24 7 25 8 31	mapdat	\|- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) e. ( LSAtoms ` C ) )
33	23 32	eqeltrrd	\|- ( ph -> ( J ` { t } ) e. ( LSAtoms ` C ) )
34		eqid	\|- ( 0g ` C ) = ( 0g ` C )
35	1 7 8	lcdlmod	\|- ( ph -> C e. LMod )
36	1 2 3 4 5 6 7 8 9 10 11 12 13 14	mapdpglem2a	\|- ( ph -> t e. F )
37	13 12 34 25 35 36	lsatspn0	\|- ( ph -> ( ( J ` { t } ) e. ( LSAtoms ` C ) <-> t =/= ( 0g ` C ) ) )
38	33 37	mpbid	\|- ( ph -> t =/= ( 0g ` C ) )

Metamath Proof Explorer

Theorem mapdpglem5N

Proof