Theorem hdmapnzcl

Description: Nonzero vector closure of map from vectors to functionals with closed kernels. (Contributed by NM, 27-May-2015)

	Ref	Expression
Hypotheses	hdmapnzcl.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hdmapnzcl.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hdmapnzcl.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	hdmapnzcl.o	⊢ 0 = ( 0g ‘ 𝑈 )
	hdmapnzcl.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	hdmapnzcl.q	⊢ 𝑄 = ( 0g ‘ 𝐶 )
	hdmapnzcl.d	⊢ 𝐷 = ( Base ‘ 𝐶 )
	hdmapnzcl.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmapnzcl.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	hdmapnzcl.t	⊢ ( 𝜑 → 𝑇 ∈ ( 𝑉 ∖ { 0 } ) )
Assertion	hdmapnzcl	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑇 ) ∈ ( 𝐷 ∖ { 𝑄 } ) )

Proof

Step	Hyp	Ref	Expression
1		hdmapnzcl.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hdmapnzcl.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		hdmapnzcl.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
4		hdmapnzcl.o	⊢ 0 = ( 0g ‘ 𝑈 )
5		hdmapnzcl.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
6		hdmapnzcl.q	⊢ 𝑄 = ( 0g ‘ 𝐶 )
7		hdmapnzcl.d	⊢ 𝐷 = ( Base ‘ 𝐶 )
8		hdmapnzcl.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
9		hdmapnzcl.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10		hdmapnzcl.t	⊢ ( 𝜑 → 𝑇 ∈ ( 𝑉 ∖ { 0 } ) )
11	10	eldifad	⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
12	1 2 3 5 7 8 9 11	hdmapcl	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑇 ) ∈ 𝐷 )
13		eldifsni	⊢ ( 𝑇 ∈ ( 𝑉 ∖ { 0 } ) → 𝑇 ≠ 0 )
14	10 13	syl	⊢ ( 𝜑 → 𝑇 ≠ 0 )
15	1 2 3 4 5 6 8 9 11	hdmapeq0	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑇 ) = 𝑄 ↔ 𝑇 = 0 ) )
16	15	necon3bid	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑇 ) ≠ 𝑄 ↔ 𝑇 ≠ 0 ) )
17	14 16	mpbird	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑇 ) ≠ 𝑄 )
18		eldifsn	⊢ ( ( 𝑆 ‘ 𝑇 ) ∈ ( 𝐷 ∖ { 𝑄 } ) ↔ ( ( 𝑆 ‘ 𝑇 ) ∈ 𝐷 ∧ ( 𝑆 ‘ 𝑇 ) ≠ 𝑄 ) )
19	12 17 18	sylanbrc	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑇 ) ∈ ( 𝐷 ∖ { 𝑄 } ) )