Theorem hvmap1o

Description: The vector to functional map provides a bijection from nonzero vectors V to nonzero functionals with closed kernels C . (Contributed by NM, 27-Mar-2015)

	Ref	Expression
Hypotheses	hvmap1o.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hvmap1o.o	⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	hvmap1o.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hvmap1o.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	hvmap1o.z	⊢ 0 = ( 0g ‘ 𝑈 )
	hvmap1o.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	hvmap1o.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	hvmap1o.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
	hvmap1o.q	⊢ 𝑄 = ( 0g ‘ 𝐷 )
	hvmap1o.c	⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
	hvmap1o.m	⊢ 𝑀 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
	hvmap1o.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion	hvmap1o	⊢ ( 𝜑 → 𝑀 : ( 𝑉 ∖ { 0 } ) –1-1-onto→ ( 𝐶 ∖ { 𝑄 } ) )

Proof

Step	Hyp	Ref	Expression
1		hvmap1o.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hvmap1o.o	⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		hvmap1o.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		hvmap1o.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		hvmap1o.z	⊢ 0 = ( 0g ‘ 𝑈 )
6		hvmap1o.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
7		hvmap1o.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
8		hvmap1o.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
9		hvmap1o.q	⊢ 𝑄 = ( 0g ‘ 𝐷 )
10		hvmap1o.c	⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
11		hvmap1o.m	⊢ 𝑀 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
12		hvmap1o.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13		eqid	⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
14		eqid	⊢ ( ·𝑠 ‘ 𝑈 ) = ( ·𝑠 ‘ 𝑈 )
15		eqid	⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
16		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( Base ‘ ( Scalar ‘ 𝑈 ) )
17		eqid	⊢ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∃ 𝑤 ∈ ( 𝑂 ‘ { 𝑥 } ) 𝑣 = ( 𝑤 ( +g ‘ 𝑈 ) ( 𝑘 ( ·𝑠 ‘ 𝑈 ) 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∃ 𝑤 ∈ ( 𝑂 ‘ { 𝑥 } ) 𝑣 = ( 𝑤 ( +g ‘ 𝑈 ) ( 𝑘 ( ·𝑠 ‘ 𝑈 ) 𝑥 ) ) ) ) )
18	1 2 3 4 13 14 15 16 5 6 7 8 9 10 17 12	lcf1o	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∃ 𝑤 ∈ ( 𝑂 ‘ { 𝑥 } ) 𝑣 = ( 𝑤 ( +g ‘ 𝑈 ) ( 𝑘 ( ·𝑠 ‘ 𝑈 ) 𝑥 ) ) ) ) ) : ( 𝑉 ∖ { 0 } ) –1-1-onto→ ( 𝐶 ∖ { 𝑄 } ) )
19	1 3 2 4 13 14 5 15 16 11 12	hvmapfval	⊢ ( 𝜑 → 𝑀 = ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∃ 𝑤 ∈ ( 𝑂 ‘ { 𝑥 } ) 𝑣 = ( 𝑤 ( +g ‘ 𝑈 ) ( 𝑘 ( ·𝑠 ‘ 𝑈 ) 𝑥 ) ) ) ) ) )
20	19	f1oeq1d	⊢ ( 𝜑 → ( 𝑀 : ( 𝑉 ∖ { 0 } ) –1-1-onto→ ( 𝐶 ∖ { 𝑄 } ) ↔ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∃ 𝑤 ∈ ( 𝑂 ‘ { 𝑥 } ) 𝑣 = ( 𝑤 ( +g ‘ 𝑈 ) ( 𝑘 ( ·𝑠 ‘ 𝑈 ) 𝑥 ) ) ) ) ) : ( 𝑉 ∖ { 0 } ) –1-1-onto→ ( 𝐶 ∖ { 𝑄 } ) ) )
21	18 20	mpbird	⊢ ( 𝜑 → 𝑀 : ( 𝑉 ∖ { 0 } ) –1-1-onto→ ( 𝐶 ∖ { 𝑄 } ) )