Metamath Proof Explorer

Theorem hdmapcl

Description: Closure of map from vectors to functionals with closed kernels. (Contributed by NM, 15-May-2015)

Ref Expression
Hypotheses hdmapcl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hdmapcl.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmapcl.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
hdmapcl.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
hdmapcl.d ⊢ 𝐷 = ( Base ‘ 𝐶 )
hdmapcl.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hdmapcl.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
hdmapcl.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
Assertion hdmapcl ( 𝜑 → ( 𝑆 ‘ 𝑇 ) ∈ 𝐷 )

Proof

Step Hyp Ref Expression
1 hdmapcl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmapcl.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hdmapcl.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 hdmapcl.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
5 hdmapcl.d ⊢ 𝐷 = ( Base ‘ 𝐶 )
6 hdmapcl.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
7 hdmapcl.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8 hdmapcl.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
9 eqid ⊢ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
10 eqid ⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
11 eqid ⊢ ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
12 eqid ⊢ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
13 1 9 2 3 10 4 5 11 12 6 7 8 hdmapval ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑇 ) = ( ℩ ℎ ∈ 𝐷 ∀ 𝑦 ∈ 𝑉 ( ¬ 𝑦 ∈ ( ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) ∪ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑇 } ) ) → ℎ = ( ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ 𝑦 , ( ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ) , 𝑦 ⟩ ) , 𝑇 ⟩ ) ) ) )
14 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
15 eqid ⊢ ( LSpan ‘ 𝐶 ) = ( LSpan ‘ 𝐶 )
16 eqid ⊢ ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
17 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
18 eqid ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
19 1 17 18 2 3 14 9 7 dvheveccl ⊢ ( 𝜑 → ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) )
20 1 2 3 14 10 4 15 16 11 7 19 mapdhvmap ⊢ ( 𝜑 → ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) ) = ( ( LSpan ‘ 𝐶 ) ‘ { ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ) } ) )
21 eqid ⊢ ( 0g ‘ 𝐶 ) = ( 0g ‘ 𝐶 )
22 1 2 3 14 4 5 21 11 7 19 hvmapcl2 ⊢ ( 𝜑 → ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ) ∈ ( 𝐷 ∖ { ( 0g ‘ 𝐶 ) } ) )
23 22 eldifad ⊢ ( 𝜑 → ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ) ∈ 𝐷 )
24 1 2 3 14 10 4 5 15 16 12 7 20 19 23 8 hdmap1eu ⊢ ( 𝜑 → ∃! ℎ ∈ 𝐷 ∀ 𝑦 ∈ 𝑉 ( ¬ 𝑦 ∈ ( ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) ∪ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑇 } ) ) → ℎ = ( ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ 𝑦 , ( ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ) , 𝑦 ⟩ ) , 𝑇 ⟩ ) ) )
25 riotacl ⊢ ( ∃! ℎ ∈ 𝐷 ∀ 𝑦 ∈ 𝑉 ( ¬ 𝑦 ∈ ( ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) ∪ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑇 } ) ) → ℎ = ( ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ 𝑦 , ( ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ) , 𝑦 ⟩ ) , 𝑇 ⟩ ) ) → ( ℩ ℎ ∈ 𝐷 ∀ 𝑦 ∈ 𝑉 ( ¬ 𝑦 ∈ ( ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) ∪ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑇 } ) ) → ℎ = ( ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ 𝑦 , ( ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ) , 𝑦 ⟩ ) , 𝑇 ⟩ ) ) ) ∈ 𝐷 )
26 24 25 syl ⊢ ( 𝜑 → ( ℩ ℎ ∈ 𝐷 ∀ 𝑦 ∈ 𝑉 ( ¬ 𝑦 ∈ ( ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) ∪ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑇 } ) ) → ℎ = ( ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ 𝑦 , ( ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ) , 𝑦 ⟩ ) , 𝑇 ⟩ ) ) ) ∈ 𝐷 )
27 13 26 eqeltrd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑇 ) ∈ 𝐷 )