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 ⊢ H = LHyp ⁡ K
hdmapevec.e ⊢ E = I ↾ Base K I ↾ LTrn ⁡ K ⁡ W
hdmapevec.j ⊢ J = HVMap ⁡ K ⁡ W
hdmapevec.s ⊢ S = HDMap ⁡ K ⁡ W
hdmapevec.k ⊢ φ → K ∈ HL ∧ W ∈ H
Assertion hdmapevec ⊢ φ → S ⁡ E = J ⁡ E

Proof

Step Hyp Ref Expression
1 hdmapevec.h ⊢ H = LHyp ⁡ K
2 hdmapevec.e ⊢ E = I ↾ Base K I ↾ LTrn ⁡ K ⁡ W
3 hdmapevec.j ⊢ J = HVMap ⁡ K ⁡ W
4 hdmapevec.s ⊢ S = HDMap ⁡ K ⁡ W
5 hdmapevec.k ⊢ φ → K ∈ HL ∧ W ∈ H
6 eqid ⊢ DVecH ⁡ K ⁡ W = DVecH ⁡ K ⁡ W
7 eqid ⊢ Base DVecH ⁡ K ⁡ W = Base DVecH ⁡ K ⁡ W
8 eqid ⊢ LSpan ⁡ DVecH ⁡ K ⁡ W = LSpan ⁡ DVecH ⁡ K ⁡ W
9 eqid ⊢ Base K = Base K
10 eqid ⊢ LTrn ⁡ K ⁡ W = LTrn ⁡ K ⁡ W
11 eqid ⊢ 0 DVecH ⁡ K ⁡ W = 0 DVecH ⁡ K ⁡ W
12 1 9 10 6 7 11 2 5 dvheveccl ⊢ φ → E ∈ Base DVecH ⁡ K ⁡ W ∖ 0 DVecH ⁡ K ⁡ W
13 12 eldifad ⊢ φ → E ∈ Base DVecH ⁡ K ⁡ W
14 1 6 7 8 5 13 dvh2dim ⊢ φ → ∃ z ∈ Base DVecH ⁡ K ⁡ W ¬ z ∈ LSpan ⁡ DVecH ⁡ K ⁡ W ⁡ E
15 5 3ad2ant1 ⊢ φ ∧ z ∈ Base DVecH ⁡ K ⁡ W ∧ ¬ z ∈ LSpan ⁡ DVecH ⁡ K ⁡ W ⁡ E → K ∈ HL ∧ W ∈ H
16 eqid ⊢ LCDual ⁡ K ⁡ W = LCDual ⁡ K ⁡ W
17 eqid ⊢ Base LCDual ⁡ K ⁡ W = Base LCDual ⁡ K ⁡ W
18 eqid ⊢ HDMap1 ⁡ K ⁡ W = HDMap1 ⁡ K ⁡ W
19 simp2 ⊢ φ ∧ z ∈ Base DVecH ⁡ K ⁡ W ∧ ¬ z ∈ LSpan ⁡ DVecH ⁡ K ⁡ W ⁡ E → z ∈ Base DVecH ⁡ K ⁡ W
20 ssid ⊢ LSpan ⁡ DVecH ⁡ K ⁡ W ⁡ E ⊆ LSpan ⁡ DVecH ⁡ K ⁡ W ⁡ E
21 20 20 unssi ⊢ LSpan ⁡ DVecH ⁡ K ⁡ W ⁡ E ∪ LSpan ⁡ DVecH ⁡ K ⁡ W ⁡ E ⊆ LSpan ⁡ DVecH ⁡ K ⁡ W ⁡ E
22 21 sseli ⊢ z ∈ LSpan ⁡ DVecH ⁡ K ⁡ W ⁡ E ∪ LSpan ⁡ DVecH ⁡ K ⁡ W ⁡ E → z ∈ LSpan ⁡ DVecH ⁡ K ⁡ W ⁡ E
23 22 con3i ⊢ ¬ z ∈ LSpan ⁡ DVecH ⁡ K ⁡ W ⁡ E → ¬ z ∈ LSpan ⁡ DVecH ⁡ K ⁡ W ⁡ E ∪ LSpan ⁡ DVecH ⁡ K ⁡ W ⁡ E
24 23 3ad2ant3 ⊢ φ ∧ z ∈ Base DVecH ⁡ K ⁡ W ∧ ¬ z ∈ LSpan ⁡ DVecH ⁡ K ⁡ W ⁡ E → ¬ z ∈ LSpan ⁡ DVecH ⁡ K ⁡ W ⁡ E ∪ LSpan ⁡ DVecH ⁡ K ⁡ W ⁡ E
25 1 2 3 4 15 6 7 8 16 17 18 19 24 hdmapeveclem ⊢ φ ∧ z ∈ Base DVecH ⁡ K ⁡ W ∧ ¬ z ∈ LSpan ⁡ DVecH ⁡ K ⁡ W ⁡ E → S ⁡ E = J ⁡ E
26 25 rexlimdv3a ⊢ φ → ∃ z ∈ Base DVecH ⁡ K ⁡ W ¬ z ∈ LSpan ⁡ DVecH ⁡ K ⁡ W ⁡ E → S ⁡ E = J ⁡ E
27 14 26 mpd ⊢ φ → S ⁡ E = J ⁡ E