Metamath Proof Explorer

Theorem hdmapevec

Description: Value of map from vectors to functionals at the reference vector E . (Contributed by NM, 16-May-2015)

Ref Expression
Hypotheses hdmapevec.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hdmapevec.e ⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
hdmapevec.j ⊢ 𝐽 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
hdmapevec.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hdmapevec.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion hdmapevec ( 𝜑 → ( 𝑆 ‘ 𝐸 ) = ( 𝐽 ‘ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 hdmapevec.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmapevec.e ⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
3 hdmapevec.j ⊢ 𝐽 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
4 hdmapevec.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
5 hdmapevec.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6 eqid ⊢ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
7 eqid ⊢ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
8 eqid ⊢ ( LSpan ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( LSpan ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
9 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
10 eqid ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
11 eqid ⊢ ( 0g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( 0g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
12 1 9 10 6 7 11 2 5 dvheveccl ⊢ ( 𝜑 → 𝐸 ∈ ( ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) } ) )
13 12 eldifad ⊢ ( 𝜑 → 𝐸 ∈ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
14 1 6 7 8 5 13 dvh2dim ⊢ ( 𝜑 → ∃ 𝑧 ∈ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ¬ 𝑧 ∈ ( ( LSpan ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ { 𝐸 } ) )
15 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ¬ 𝑧 ∈ ( ( LSpan ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ { 𝐸 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
16 eqid ⊢ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
17 eqid ⊢ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
18 eqid ⊢ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
19 simp2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ¬ 𝑧 ∈ ( ( LSpan ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ { 𝐸 } ) ) → 𝑧 ∈ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
20 ssid ⊢ ( ( LSpan ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ { 𝐸 } ) ⊆ ( ( LSpan ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ { 𝐸 } )
21 20 20 unssi ⊢ ( ( ( LSpan ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ { 𝐸 } ) ∪ ( ( LSpan ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ { 𝐸 } ) ) ⊆ ( ( LSpan ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ { 𝐸 } )
22 21 sseli ⊢ ( 𝑧 ∈ ( ( ( LSpan ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ { 𝐸 } ) ∪ ( ( LSpan ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ { 𝐸 } ) ) → 𝑧 ∈ ( ( LSpan ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ { 𝐸 } ) )
23 22 con3i ⊢ ( ¬ 𝑧 ∈ ( ( LSpan ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ { 𝐸 } ) → ¬ 𝑧 ∈ ( ( ( LSpan ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ { 𝐸 } ) ∪ ( ( LSpan ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ { 𝐸 } ) ) )
24 23 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ¬ 𝑧 ∈ ( ( LSpan ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ { 𝐸 } ) ) → ¬ 𝑧 ∈ ( ( ( LSpan ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ { 𝐸 } ) ∪ ( ( LSpan ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ { 𝐸 } ) ) )
25 1 2 3 4 15 6 7 8 16 17 18 19 24 hdmapeveclem ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ¬ 𝑧 ∈ ( ( LSpan ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ { 𝐸 } ) ) → ( 𝑆 ‘ 𝐸 ) = ( 𝐽 ‘ 𝐸 ) )
26 25 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ¬ 𝑧 ∈ ( ( LSpan ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ { 𝐸 } ) → ( 𝑆 ‘ 𝐸 ) = ( 𝐽 ‘ 𝐸 ) ) )
27 14 26 mpd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐸 ) = ( 𝐽 ‘ 𝐸 ) )