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 ( 𝜑 → ( 𝑆𝑇 ) ∈ 𝐷 )