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↾BaseKI↾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↾BaseKI↾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 ⊢BaseDVecH⁡K⁡W=BaseDVecH⁡K⁡W
8 eqid ⊢LSpan⁡DVecH⁡K⁡W=LSpan⁡DVecH⁡K⁡W
9 eqid ⊢BaseK=BaseK
10 eqid ⊢LTrn⁡K⁡W=LTrn⁡K⁡W
11 eqid ⊢0DVecH⁡K⁡W=0DVecH⁡K⁡W
12 1 9 10 6 7 11 2 5 dvheveccl ⊢φ→E∈BaseDVecH⁡K⁡W∖0DVecH⁡K⁡W
13 12 eldifad ⊢φ→E∈BaseDVecH⁡K⁡W
14 1 6 7 8 5 13 dvh2dim ⊢φ→∃z∈BaseDVecH⁡K⁡W¬z∈LSpan⁡DVecH⁡K⁡W⁡E
15 5 3ad2ant1 ⊢φ∧z∈BaseDVecH⁡K⁡W∧¬z∈LSpan⁡DVecH⁡K⁡W⁡E→K∈HL∧W∈H
16 eqid ⊢LCDual⁡K⁡W=LCDual⁡K⁡W
17 eqid ⊢BaseLCDual⁡K⁡W=BaseLCDual⁡K⁡W
18 eqid ⊢HDMap1⁡K⁡W=HDMap1⁡K⁡W
19 simp2 ⊢φ∧z∈BaseDVecH⁡K⁡W∧¬z∈LSpan⁡DVecH⁡K⁡W⁡E→z∈BaseDVecH⁡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∈BaseDVecH⁡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∈BaseDVecH⁡K⁡W∧¬z∈LSpan⁡DVecH⁡K⁡W⁡E→S⁡E=J⁡E
26 25 rexlimdv3a ⊢φ→∃z∈BaseDVecH⁡K⁡W¬z∈LSpan⁡DVecH⁡K⁡W⁡E→S⁡E=J⁡E
27 14 26 mpd ⊢φ→S⁡E=J⁡E