Theorem mapdn0

Description: Transfer nonzero property from domain to range of projectivity mapd . (Contributed by NM, 12-Apr-2015)

	Ref	Expression
Hypotheses	mapdindp.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	mapdindp.m	⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
	mapdindp.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	mapdindp.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	mapdindp.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
	mapdindp.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	mapdindp.d	⊢ 𝐷 = ( Base ‘ 𝐶 )
	mapdindp.j	⊢ 𝐽 = ( LSpan ‘ 𝐶 )
	mapdindp.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	mapdindp.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐷 )
	mapdindp.mx	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝐽 ‘ { 𝐹 } ) )
	mapdn0.o	⊢ 0 = ( 0g ‘ 𝑈 )
	mapdn0.z	⊢ 𝑍 = ( 0g ‘ 𝐶 )
	mapdn0.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
Assertion	mapdn0	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 ∖ { 𝑍 } ) )

Proof

Step	Hyp	Ref	Expression
1		mapdindp.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		mapdindp.m	⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
3		mapdindp.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		mapdindp.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		mapdindp.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
6		mapdindp.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
7		mapdindp.d	⊢ 𝐷 = ( Base ‘ 𝐶 )
8		mapdindp.j	⊢ 𝐽 = ( LSpan ‘ 𝐶 )
9		mapdindp.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10		mapdindp.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐷 )
11		mapdindp.mx	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝐽 ‘ { 𝐹 } ) )
12		mapdn0.o	⊢ 0 = ( 0g ‘ 𝑈 )
13		mapdn0.z	⊢ 𝑍 = ( 0g ‘ 𝐶 )
14		mapdn0.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
15		eldifsni	⊢ ( 𝑋 ∈ ( 𝑉 ∖ { 0 } ) → 𝑋 ≠ 0 )
16	14 15	syl	⊢ ( 𝜑 → 𝑋 ≠ 0 )
17		sneq	⊢ ( 𝐹 = 𝑍 → { 𝐹 } = { 𝑍 } )
18	17	fveq2d	⊢ ( 𝐹 = 𝑍 → ( 𝐽 ‘ { 𝐹 } ) = ( 𝐽 ‘ { 𝑍 } ) )
19	11 18	sylan9eq	⊢ ( ( 𝜑 ∧ 𝐹 = 𝑍 ) → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝐽 ‘ { 𝑍 } ) )
20	1 2 3 12 6 13 9	mapd0	⊢ ( 𝜑 → ( 𝑀 ‘ { 0 } ) = { 𝑍 } )
21	1 6 9	lcdlmod	⊢ ( 𝜑 → 𝐶 ∈ LMod )
22	13 8	lspsn0	⊢ ( 𝐶 ∈ LMod → ( 𝐽 ‘ { 𝑍 } ) = { 𝑍 } )
23	21 22	syl	⊢ ( 𝜑 → ( 𝐽 ‘ { 𝑍 } ) = { 𝑍 } )
24	20 23	eqtr4d	⊢ ( 𝜑 → ( 𝑀 ‘ { 0 } ) = ( 𝐽 ‘ { 𝑍 } ) )
25	24	adantr	⊢ ( ( 𝜑 ∧ 𝐹 = 𝑍 ) → ( 𝑀 ‘ { 0 } ) = ( 𝐽 ‘ { 𝑍 } ) )
26	19 25	eqtr4d	⊢ ( ( 𝜑 ∧ 𝐹 = 𝑍 ) → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝑀 ‘ { 0 } ) )
27	26	ex	⊢ ( 𝜑 → ( 𝐹 = 𝑍 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝑀 ‘ { 0 } ) ) )
28		eqid	⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
29	1 3 9	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
30	14	eldifad	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
31	4 28 5	lspsncl	⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) )
32	29 30 31	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) )
33	12 28	lsssn0	⊢ ( 𝑈 ∈ LMod → { 0 } ∈ ( LSubSp ‘ 𝑈 ) )
34	29 33	syl	⊢ ( 𝜑 → { 0 } ∈ ( LSubSp ‘ 𝑈 ) )
35	1 3 28 2 9 32 34	mapd11	⊢ ( 𝜑 → ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝑀 ‘ { 0 } ) ↔ ( 𝑁 ‘ { 𝑋 } ) = { 0 } ) )
36	4 12 5	lspsneq0	⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑁 ‘ { 𝑋 } ) = { 0 } ↔ 𝑋 = 0 ) )
37	29 30 36	syl2anc	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = { 0 } ↔ 𝑋 = 0 ) )
38	35 37	bitrd	⊢ ( 𝜑 → ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝑀 ‘ { 0 } ) ↔ 𝑋 = 0 ) )
39	27 38	sylibd	⊢ ( 𝜑 → ( 𝐹 = 𝑍 → 𝑋 = 0 ) )
40	39	necon3d	⊢ ( 𝜑 → ( 𝑋 ≠ 0 → 𝐹 ≠ 𝑍 ) )
41	16 40	mpd	⊢ ( 𝜑 → 𝐹 ≠ 𝑍 )
42		eldifsn	⊢ ( 𝐹 ∈ ( 𝐷 ∖ { 𝑍 } ) ↔ ( 𝐹 ∈ 𝐷 ∧ 𝐹 ≠ 𝑍 ) )
43	10 41 42	sylanbrc	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 ∖ { 𝑍 } ) )