Theorem hdmapf1oN

Description: Part 12 in Baer p. 49. The map from vectors to functionals with closed kernels maps one-to-one onto. Combined with hdmapadd , this shows the map is an automorphism from the additive group of vectors to the additive group of functionals with closed kernels. (Contributed by NM, 30-May-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hdmapf1o.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hdmapf1o.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hdmapf1o.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	hdmapf1o.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	hdmapf1o.d	⊢ 𝐷 = ( Base ‘ 𝐶 )
	hdmapf1o.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmapf1o.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion	hdmapf1oN	⊢ ( 𝜑 → 𝑆 : 𝑉 –1-1-onto→ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		hdmapf1o.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hdmapf1o.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		hdmapf1o.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
4		hdmapf1o.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
5		hdmapf1o.d	⊢ 𝐷 = ( Base ‘ 𝐶 )
6		hdmapf1o.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
7		hdmapf1o.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8	1 2 3 6 7	hdmapfnN	⊢ ( 𝜑 → 𝑆 Fn 𝑉 )
9	1 4 5 6 7	hdmaprnN	⊢ ( 𝜑 → ran 𝑆 = 𝐷 )
10	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
11		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝑥 ∈ 𝑉 )
12		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝑦 ∈ 𝑉 )
13	1 2 3 6 10 11 12	hdmap11	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑦 ) ↔ 𝑥 = 𝑦 ) )
14	13	biimpd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
15	14	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
16		dff1o6	⊢ ( 𝑆 : 𝑉 –1-1-onto→ 𝐷 ↔ ( 𝑆 Fn 𝑉 ∧ ran 𝑆 = 𝐷 ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
17	8 9 15 16	syl3anbrc	⊢ ( 𝜑 → 𝑆 : 𝑉 –1-1-onto→ 𝐷 )