Theorem hgmapf1oN

Description: The scalar sigma map is a one-to-one onto function. (Contributed by NM, 7-Jun-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hgmapf1o.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hgmapf1o.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hgmapf1o.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
	hgmapf1o.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	hgmapf1o.g	⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
	hgmapf1o.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion	hgmapf1oN	⊢ ( 𝜑 → 𝐺 : 𝐵 –1-1-onto→ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		hgmapf1o.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hgmapf1o.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		hgmapf1o.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
4		hgmapf1o.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
5		hgmapf1o.g	⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
6		hgmapf1o.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7	1 2 3 4 5 6	hgmapfnN	⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
8	1 2 3 4 5 6	hgmaprnN	⊢ ( 𝜑 → ran 𝐺 = 𝐵 )
9	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
11		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
12	1 2 3 4 5 9 10 11	hgmap11	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ↔ 𝑥 = 𝑦 ) )
13	12	biimpd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
14	13	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
15		dff1o6	⊢ ( 𝐺 : 𝐵 –1-1-onto→ 𝐵 ↔ ( 𝐺 Fn 𝐵 ∧ ran 𝐺 = 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
16	7 8 14 15	syl3anbrc	⊢ ( 𝜑 → 𝐺 : 𝐵 –1-1-onto→ 𝐵 )