Theorem mapdpglem30b

Description: Lemma for mapdpg . (Contributed by NM, 22-Mar-2015)

	Ref	Expression
Hypotheses	mapdpg.h	|- H = ( LHyp ` K )
	mapdpg.m	|- M = ( ( mapd ` K ) ` W )
	mapdpg.u	|- U = ( ( DVecH ` K ) ` W )
	mapdpg.v	|- V = ( Base ` U )
	mapdpg.s	|- .- = ( -g ` U )
	mapdpg.z	|- .0. = ( 0g ` U )
	mapdpg.n	|- N = ( LSpan ` U )
	mapdpg.c	|- C = ( ( LCDual ` K ) ` W )
	mapdpg.f	|- F = ( Base ` C )
	mapdpg.r	|- R = ( -g ` C )
	mapdpg.j	|- J = ( LSpan ` C )
	mapdpg.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	mapdpg.x	|- ( ph -> X e. ( V \ { .0. } ) )
	mapdpg.y	|- ( ph -> Y e. ( V \ { .0. } ) )
	mapdpg.g	|- ( ph -> G e. F )
	mapdpg.ne	|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
	mapdpg.e	|- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )
	mapdpgem25.h1	|- ( ph -> ( h e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) ) )
	mapdpgem25.i1	|- ( ph -> ( i e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) )
Assertion	mapdpglem30b	|- ( ph -> i =/= ( 0g ` C ) )

Proof

Step	Hyp	Ref	Expression
1		mapdpg.h	|- H = ( LHyp ` K )
2		mapdpg.m	|- M = ( ( mapd ` K ) ` W )
3		mapdpg.u	|- U = ( ( DVecH ` K ) ` W )
4		mapdpg.v	|- V = ( Base ` U )
5		mapdpg.s	|- .- = ( -g ` U )
6		mapdpg.z	|- .0. = ( 0g ` U )
7		mapdpg.n	|- N = ( LSpan ` U )
8		mapdpg.c	|- C = ( ( LCDual ` K ) ` W )
9		mapdpg.f	|- F = ( Base ` C )
10		mapdpg.r	|- R = ( -g ` C )
11		mapdpg.j	|- J = ( LSpan ` C )
12		mapdpg.k	|- ( ph -> ( K e. HL /\ W e. H ) )
13		mapdpg.x	|- ( ph -> X e. ( V \ { .0. } ) )
14		mapdpg.y	|- ( ph -> Y e. ( V \ { .0. } ) )
15		mapdpg.g	|- ( ph -> G e. F )
16		mapdpg.ne	|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
17		mapdpg.e	|- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )
18		mapdpgem25.h1	|- ( ph -> ( h e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) ) )
19		mapdpgem25.i1	|- ( ph -> ( i e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) )
20	19	simprd	|- ( ph -> ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) )
21	20	simpld	|- ( ph -> ( M ` ( N ` { Y } ) ) = ( J ` { i } ) )
22		eqid	|- ( LSAtoms ` U ) = ( LSAtoms ` U )
23		eqid	|- ( LSAtoms ` C ) = ( LSAtoms ` C )
24	1 3 12	dvhlmod	|- ( ph -> U e. LMod )
25	4 7 6 22 24 14	lsatlspsn	|- ( ph -> ( N ` { Y } ) e. ( LSAtoms ` U ) )
26	1 2 3 22 8 23 12 25	mapdat	|- ( ph -> ( M ` ( N ` { Y } ) ) e. ( LSAtoms ` C ) )
27	21 26	eqeltrrd	|- ( ph -> ( J ` { i } ) e. ( LSAtoms ` C ) )
28		eqid	|- ( 0g ` C ) = ( 0g ` C )
29	1 8 12	lcdlmod	|- ( ph -> C e. LMod )
30	19	simpld	|- ( ph -> i e. F )
31	9 11 28 23 29 30	lsatspn0	|- ( ph -> ( ( J ` { i } ) e. ( LSAtoms ` C ) <-> i =/= ( 0g ` C ) ) )
32	27 31	mpbid	|- ( ph -> i =/= ( 0g ` C ) )