Metamath Proof Explorer

Theorem hvmapfval

Description: Map from nonzero vectors to nonzero functionals in the closed kernel dual space. (Contributed by NM, 23-Mar-2015)

Ref Expression
Hypotheses hvmapval.h ⊢H=LHyp⁡K
hvmapval.u ⊢U=DVecH⁡K⁡W
hvmapval.o ⊢O=ocH⁡K⁡W
hvmapval.v ⊢V=BaseU
hvmapval.p ⊢+˙=+U
hvmapval.t ⊢·˙=⋅U
hvmapval.z ⊢0˙=0U
hvmapval.s ⊢S=Scalar⁡U
hvmapval.r ⊢R=BaseS
hvmapval.m ⊢M=HVMap⁡K⁡W
hvmapval.k ⊢φ→K∈A∧W∈H
Assertion hvmapfval ⊢φ→M=x∈V∖0˙⟼v∈V⟼ιj∈R|∃t∈O⁡xv=t+˙j·˙x

Proof

Step Hyp Ref Expression
1 hvmapval.h ⊢H=LHyp⁡K
2 hvmapval.u ⊢U=DVecH⁡K⁡W
3 hvmapval.o ⊢O=ocH⁡K⁡W
4 hvmapval.v ⊢V=BaseU
5 hvmapval.p ⊢+˙=+U
6 hvmapval.t ⊢·˙=⋅U
7 hvmapval.z ⊢0˙=0U
8 hvmapval.s ⊢S=Scalar⁡U
9 hvmapval.r ⊢R=BaseS
10 hvmapval.m ⊢M=HVMap⁡K⁡W
11 hvmapval.k ⊢φ→K∈A∧W∈H
12 1 hvmapffval ⊢K∈A→HVMap⁡K=w∈H⟼x∈BaseDVecH⁡K⁡w∖0DVecH⁡K⁡w⟼v∈BaseDVecH⁡K⁡w⟼ιj∈BaseScalar⁡DVecH⁡K⁡w|∃t∈ocH⁡K⁡w⁡xv=t+DVecH⁡K⁡wj⋅DVecH⁡K⁡wx
13 12 fveq1d ⊢K∈A→HVMap⁡K⁡W=w∈H⟼x∈BaseDVecH⁡K⁡w∖0DVecH⁡K⁡w⟼v∈BaseDVecH⁡K⁡w⟼ιj∈BaseScalar⁡DVecH⁡K⁡w|∃t∈ocH⁡K⁡w⁡xv=t+DVecH⁡K⁡wj⋅DVecH⁡K⁡wx⁡W
14 10 13 eqtrid ⊢K∈A→M=w∈H⟼x∈BaseDVecH⁡K⁡w∖0DVecH⁡K⁡w⟼v∈BaseDVecH⁡K⁡w⟼ιj∈BaseScalar⁡DVecH⁡K⁡w|∃t∈ocH⁡K⁡w⁡xv=t+DVecH⁡K⁡wj⋅DVecH⁡K⁡wx⁡W
15 fveq2 ⊢w=W→DVecH⁡K⁡w=DVecH⁡K⁡W
16 15 2 eqtr4di ⊢w=W→DVecH⁡K⁡w=U
17 16 fveq2d ⊢w=W→BaseDVecH⁡K⁡w=BaseU
18 17 4 eqtr4di ⊢w=W→BaseDVecH⁡K⁡w=V
19 16 fveq2d ⊢w=W→0DVecH⁡K⁡w=0U
20 19 7 eqtr4di ⊢w=W→0DVecH⁡K⁡w=0˙
21 20 sneqd ⊢w=W→0DVecH⁡K⁡w=0˙
22 18 21 difeq12d ⊢w=W→BaseDVecH⁡K⁡w∖0DVecH⁡K⁡w=V∖0˙
23 16 fveq2d ⊢w=W→Scalar⁡DVecH⁡K⁡w=Scalar⁡U
24 23 8 eqtr4di ⊢w=W→Scalar⁡DVecH⁡K⁡w=S
25 24 fveq2d ⊢w=W→BaseScalar⁡DVecH⁡K⁡w=BaseS
26 25 9 eqtr4di ⊢w=W→BaseScalar⁡DVecH⁡K⁡w=R
27 fveq2 ⊢w=W→ocH⁡K⁡w=ocH⁡K⁡W
28 27 3 eqtr4di ⊢w=W→ocH⁡K⁡w=O
29 28 fveq1d ⊢w=W→ocH⁡K⁡w⁡x=O⁡x
30 16 fveq2d ⊢w=W→+DVecH⁡K⁡w=+U
31 30 5 eqtr4di ⊢w=W→+DVecH⁡K⁡w=+˙
32 eqidd ⊢w=W→t=t
33 16 fveq2d ⊢w=W→⋅DVecH⁡K⁡w=⋅U
34 33 6 eqtr4di ⊢w=W→⋅DVecH⁡K⁡w=·˙
35 34 oveqd ⊢w=W→j⋅DVecH⁡K⁡wx=j·˙x
36 31 32 35 oveq123d ⊢w=W→t+DVecH⁡K⁡wj⋅DVecH⁡K⁡wx=t+˙j·˙x
37 36 eqeq2d ⊢w=W→v=t+DVecH⁡K⁡wj⋅DVecH⁡K⁡wx↔v=t+˙j·˙x
38 29 37 rexeqbidv ⊢w=W→∃t∈ocH⁡K⁡w⁡xv=t+DVecH⁡K⁡wj⋅DVecH⁡K⁡wx↔∃t∈O⁡xv=t+˙j·˙x
39 26 38 riotaeqbidv ⊢w=W→ιj∈BaseScalar⁡DVecH⁡K⁡w|∃t∈ocH⁡K⁡w⁡xv=t+DVecH⁡K⁡wj⋅DVecH⁡K⁡wx=ιj∈R|∃t∈O⁡xv=t+˙j·˙x
40 18 39 mpteq12dv ⊢w=W→v∈BaseDVecH⁡K⁡w⟼ιj∈BaseScalar⁡DVecH⁡K⁡w|∃t∈ocH⁡K⁡w⁡xv=t+DVecH⁡K⁡wj⋅DVecH⁡K⁡wx=v∈V⟼ιj∈R|∃t∈O⁡xv=t+˙j·˙x
41 22 40 mpteq12dv ⊢w=W→x∈BaseDVecH⁡K⁡w∖0DVecH⁡K⁡w⟼v∈BaseDVecH⁡K⁡w⟼ιj∈BaseScalar⁡DVecH⁡K⁡w|∃t∈ocH⁡K⁡w⁡xv=t+DVecH⁡K⁡wj⋅DVecH⁡K⁡wx=x∈V∖0˙⟼v∈V⟼ιj∈R|∃t∈O⁡xv=t+˙j·˙x
42 eqid ⊢w∈H⟼x∈BaseDVecH⁡K⁡w∖0DVecH⁡K⁡w⟼v∈BaseDVecH⁡K⁡w⟼ιj∈BaseScalar⁡DVecH⁡K⁡w|∃t∈ocH⁡K⁡w⁡xv=t+DVecH⁡K⁡wj⋅DVecH⁡K⁡wx=w∈H⟼x∈BaseDVecH⁡K⁡w∖0DVecH⁡K⁡w⟼v∈BaseDVecH⁡K⁡w⟼ιj∈BaseScalar⁡DVecH⁡K⁡w|∃t∈ocH⁡K⁡w⁡xv=t+DVecH⁡K⁡wj⋅DVecH⁡K⁡wx
43 4 fvexi ⊢V∈V
44 43 difexi ⊢V∖0˙∈V
45 44 mptex ⊢x∈V∖0˙⟼v∈V⟼ιj∈R|∃t∈O⁡xv=t+˙j·˙x∈V
46 41 42 45 fvmpt ⊢W∈H→w∈H⟼x∈BaseDVecH⁡K⁡w∖0DVecH⁡K⁡w⟼v∈BaseDVecH⁡K⁡w⟼ιj∈BaseScalar⁡DVecH⁡K⁡w|∃t∈ocH⁡K⁡w⁡xv=t+DVecH⁡K⁡wj⋅DVecH⁡K⁡wx⁡W=x∈V∖0˙⟼v∈V⟼ιj∈R|∃t∈O⁡xv=t+˙j·˙x
47 14 46 sylan9eq ⊢K∈A∧W∈H→M=x∈V∖0˙⟼v∈V⟼ιj∈R|∃t∈O⁡xv=t+˙j·˙x
48 11 47 syl ⊢φ→M=x∈V∖0˙⟼v∈V⟼ιj∈R|∃t∈O⁡xv=t+˙j·˙x