Theorem hdmapfnN

Description: Functionality of map from vectors to functionals with closed kernels. (Contributed by NM, 30-May-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hdmapfn.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hdmapfn.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hdmapfn.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	hdmapfn.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmapfn.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion	hdmapfnN	⊢ ( 𝜑 → 𝑆 Fn 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		hdmapfn.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hdmapfn.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		hdmapfn.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
4		hdmapfn.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
5		hdmapfn.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6		riotaex	⊢ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) ∪ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑡 } ) ) → 𝑦 = ( ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ 𝑧 , ( ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ∈ V
7		eqid	⊢ ( 𝑡 ∈ 𝑉 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) ∪ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑡 } ) ) → 𝑦 = ( ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ 𝑧 , ( ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) = ( 𝑡 ∈ 𝑉 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) ∪ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑡 } ) ) → 𝑦 = ( ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ 𝑧 , ( ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) )
8	6 7	fnmpti	⊢ ( 𝑡 ∈ 𝑉 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) ∪ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑡 } ) ) → 𝑦 = ( ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ 𝑧 , ( ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) Fn 𝑉
9		eqid	⊢ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
10		eqid	⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
11		eqid	⊢ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
12		eqid	⊢ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
13		eqid	⊢ ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
14		eqid	⊢ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
15	1 9 2 3 10 11 12 13 14 4 5	hdmapfval	⊢ ( 𝜑 → 𝑆 = ( 𝑡 ∈ 𝑉 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) ∪ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑡 } ) ) → 𝑦 = ( ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ 𝑧 , ( ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) )
16	15	fneq1d	⊢ ( 𝜑 → ( 𝑆 Fn 𝑉 ↔ ( 𝑡 ∈ 𝑉 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) ∪ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑡 } ) ) → 𝑦 = ( ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ 𝑧 , ( ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) Fn 𝑉 ) )
17	8 16	mpbiri	⊢ ( 𝜑 → 𝑆 Fn 𝑉 )