Theorem mapdpglem30a

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

	Ref	Expression
Hypotheses	mapdpg.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	mapdpg.m	⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
	mapdpg.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	mapdpg.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	mapdpg.s	⊢ − = ( -g ‘ 𝑈 )
	mapdpg.z	⊢ 0 = ( 0g ‘ 𝑈 )
	mapdpg.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
	mapdpg.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	mapdpg.f	⊢ 𝐹 = ( Base ‘ 𝐶 )
	mapdpg.r	⊢ 𝑅 = ( -g ‘ 𝐶 )
	mapdpg.j	⊢ 𝐽 = ( LSpan ‘ 𝐶 )
	mapdpg.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	mapdpg.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
	mapdpg.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
	mapdpg.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
	mapdpg.ne	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
	mapdpg.e	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝐽 ‘ { 𝐺 } ) )
Assertion	mapdpglem30a	⊢ ( 𝜑 → 𝐺 ≠ ( 0g ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		mapdpg.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		mapdpg.m	⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
3		mapdpg.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		mapdpg.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		mapdpg.s	⊢ − = ( -g ‘ 𝑈 )
6		mapdpg.z	⊢ 0 = ( 0g ‘ 𝑈 )
7		mapdpg.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
8		mapdpg.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
9		mapdpg.f	⊢ 𝐹 = ( Base ‘ 𝐶 )
10		mapdpg.r	⊢ 𝑅 = ( -g ‘ 𝐶 )
11		mapdpg.j	⊢ 𝐽 = ( LSpan ‘ 𝐶 )
12		mapdpg.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13		mapdpg.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
14		mapdpg.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
15		mapdpg.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
16		mapdpg.ne	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
17		mapdpg.e	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝐽 ‘ { 𝐺 } ) )
18		eqid	⊢ ( LSAtoms ‘ 𝑈 ) = ( LSAtoms ‘ 𝑈 )
19		eqid	⊢ ( LSAtoms ‘ 𝐶 ) = ( LSAtoms ‘ 𝐶 )
20	1 3 12	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
21	4 7 6 18 20 13	lsatlspsn	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSAtoms ‘ 𝑈 ) )
22	1 2 3 18 8 19 12 21	mapdat	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ∈ ( LSAtoms ‘ 𝐶 ) )
23	17 22	eqeltrrd	⊢ ( 𝜑 → ( 𝐽 ‘ { 𝐺 } ) ∈ ( LSAtoms ‘ 𝐶 ) )
24		eqid	⊢ ( 0g ‘ 𝐶 ) = ( 0g ‘ 𝐶 )
25	1 8 12	lcdlmod	⊢ ( 𝜑 → 𝐶 ∈ LMod )
26	9 11 24 19 25 15	lsatspn0	⊢ ( 𝜑 → ( ( 𝐽 ‘ { 𝐺 } ) ∈ ( LSAtoms ‘ 𝐶 ) ↔ 𝐺 ≠ ( 0g ‘ 𝐶 ) ) )
27	23 26	mpbid	⊢ ( 𝜑 → 𝐺 ≠ ( 0g ‘ 𝐶 ) )