Theorem hdmaprnlem17N

Description: Lemma for hdmaprnN . Include zero. (Contributed by NM, 30-May-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hdmaprnlem15.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hdmaprnlem15.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hdmaprnlem15.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	hdmaprnlem15.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
	hdmaprnlem15.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	hdmaprnlem15.d	⊢ 𝐷 = ( Base ‘ 𝐶 )
	hdmaprnlem15.q	⊢ 0 = ( 0g ‘ 𝐶 )
	hdmaprnlem15.l	⊢ 𝐿 = ( LSpan ‘ 𝐶 )
	hdmaprnlem15.m	⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
	hdmaprnlem15.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmaprnlem15.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	hdmaprnlem17.se	⊢ ( 𝜑 → 𝑠 ∈ 𝐷 )
Assertion	hdmaprnlem17N	⊢ ( 𝜑 → 𝑠 ∈ ran 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		hdmaprnlem15.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hdmaprnlem15.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		hdmaprnlem15.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
4		hdmaprnlem15.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
5		hdmaprnlem15.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
6		hdmaprnlem15.d	⊢ 𝐷 = ( Base ‘ 𝐶 )
7		hdmaprnlem15.q	⊢ 0 = ( 0g ‘ 𝐶 )
8		hdmaprnlem15.l	⊢ 𝐿 = ( LSpan ‘ 𝐶 )
9		hdmaprnlem15.m	⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
10		hdmaprnlem15.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
11		hdmaprnlem15.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12		hdmaprnlem17.se	⊢ ( 𝜑 → 𝑠 ∈ 𝐷 )
13		eleq1	⊢ ( 𝑠 = 0 → ( 𝑠 ∈ ran 𝑆 ↔ 0 ∈ ran 𝑆 ) )
14	11	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ≠ 0 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
15	12	anim1i	⊢ ( ( 𝜑 ∧ 𝑠 ≠ 0 ) → ( 𝑠 ∈ 𝐷 ∧ 𝑠 ≠ 0 ) )
16		eldifsn	⊢ ( 𝑠 ∈ ( 𝐷 ∖ { 0 } ) ↔ ( 𝑠 ∈ 𝐷 ∧ 𝑠 ≠ 0 ) )
17	15 16	sylibr	⊢ ( ( 𝜑 ∧ 𝑠 ≠ 0 ) → 𝑠 ∈ ( 𝐷 ∖ { 0 } ) )
18	1 2 3 4 5 6 7 8 9 10 14 17	hdmaprnlem16N	⊢ ( ( 𝜑 ∧ 𝑠 ≠ 0 ) → 𝑠 ∈ ran 𝑆 )
19		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
20	1 2 19 5 7 10 11	hdmapval0	⊢ ( 𝜑 → ( 𝑆 ‘ ( 0g ‘ 𝑈 ) ) = 0 )
21	1 2 3 10 11	hdmapfnN	⊢ ( 𝜑 → 𝑆 Fn 𝑉 )
22	1 2 11	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
23	3 19	lmod0vcl	⊢ ( 𝑈 ∈ LMod → ( 0g ‘ 𝑈 ) ∈ 𝑉 )
24	22 23	syl	⊢ ( 𝜑 → ( 0g ‘ 𝑈 ) ∈ 𝑉 )
25		fnfvelrn	⊢ ( ( 𝑆 Fn 𝑉 ∧ ( 0g ‘ 𝑈 ) ∈ 𝑉 ) → ( 𝑆 ‘ ( 0g ‘ 𝑈 ) ) ∈ ran 𝑆 )
26	21 24 25	syl2anc	⊢ ( 𝜑 → ( 𝑆 ‘ ( 0g ‘ 𝑈 ) ) ∈ ran 𝑆 )
27	20 26	eqeltrrd	⊢ ( 𝜑 → 0 ∈ ran 𝑆 )
28	13 18 27	pm2.61ne	⊢ ( 𝜑 → 𝑠 ∈ ran 𝑆 )