Metamath Proof Explorer

Theorem hvmapffval

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

Ref Expression
Hypothesis hvmapval.h ⊢H=LHyp⁡K
Assertion hvmapffval ⊢K∈X→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

Proof

Step Hyp Ref Expression
1 hvmapval.h ⊢H=LHyp⁡K
2 elex ⊢K∈X→K∈V
3 fveq2 ⊢k=K→LHyp⁡k=LHyp⁡K
4 3 1 eqtr4di ⊢k=K→LHyp⁡k=H
5 fveq2 ⊢k=K→DVecH⁡k=DVecH⁡K
6 5 fveq1d ⊢k=K→DVecH⁡k⁡w=DVecH⁡K⁡w
7 6 fveq2d ⊢k=K→BaseDVecH⁡k⁡w=BaseDVecH⁡K⁡w
8 6 fveq2d ⊢k=K→0DVecH⁡k⁡w=0DVecH⁡K⁡w
9 8 sneqd ⊢k=K→0DVecH⁡k⁡w=0DVecH⁡K⁡w
10 7 9 difeq12d ⊢k=K→BaseDVecH⁡k⁡w∖0DVecH⁡k⁡w=BaseDVecH⁡K⁡w∖0DVecH⁡K⁡w
11 6 fveq2d ⊢k=K→Scalar⁡DVecH⁡k⁡w=Scalar⁡DVecH⁡K⁡w
12 11 fveq2d ⊢k=K→BaseScalar⁡DVecH⁡k⁡w=BaseScalar⁡DVecH⁡K⁡w
13 fveq2 ⊢k=K→ocH⁡k=ocH⁡K
14 13 fveq1d ⊢k=K→ocH⁡k⁡w=ocH⁡K⁡w
15 14 fveq1d ⊢k=K→ocH⁡k⁡w⁡x=ocH⁡K⁡w⁡x
16 6 fveq2d ⊢k=K→+DVecH⁡k⁡w=+DVecH⁡K⁡w
17 eqidd ⊢k=K→t=t
18 6 fveq2d ⊢k=K→⋅DVecH⁡k⁡w=⋅DVecH⁡K⁡w
19 18 oveqd ⊢k=K→j⋅DVecH⁡k⁡wx=j⋅DVecH⁡K⁡wx
20 16 17 19 oveq123d ⊢k=K→t+DVecH⁡k⁡wj⋅DVecH⁡k⁡wx=t+DVecH⁡K⁡wj⋅DVecH⁡K⁡wx
21 20 eqeq2d ⊢k=K→v=t+DVecH⁡k⁡wj⋅DVecH⁡k⁡wx↔v=t+DVecH⁡K⁡wj⋅DVecH⁡K⁡wx
22 15 21 rexeqbidv ⊢k=K→∃t∈ocH⁡k⁡w⁡xv=t+DVecH⁡k⁡wj⋅DVecH⁡k⁡wx↔∃t∈ocH⁡K⁡w⁡xv=t+DVecH⁡K⁡wj⋅DVecH⁡K⁡wx
23 12 22 riotaeqbidv ⊢k=K→ιj∈BaseScalar⁡DVecH⁡k⁡w|∃t∈ocH⁡k⁡w⁡xv=t+DVecH⁡k⁡wj⋅DVecH⁡k⁡wx=ιj∈BaseScalar⁡DVecH⁡K⁡w|∃t∈ocH⁡K⁡w⁡xv=t+DVecH⁡K⁡wj⋅DVecH⁡K⁡wx
24 7 23 mpteq12dv ⊢k=K→v∈BaseDVecH⁡k⁡w⟼ιj∈BaseScalar⁡DVecH⁡k⁡w|∃t∈ocH⁡k⁡w⁡xv=t+DVecH⁡k⁡wj⋅DVecH⁡k⁡wx=v∈BaseDVecH⁡K⁡w⟼ιj∈BaseScalar⁡DVecH⁡K⁡w|∃t∈ocH⁡K⁡w⁡xv=t+DVecH⁡K⁡wj⋅DVecH⁡K⁡wx
25 10 24 mpteq12dv ⊢k=K→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∈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
26 4 25 mpteq12dv ⊢k=K→w∈LHyp⁡k⟼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
27 df-hvmap ⊢HVMap=k∈V⟼w∈LHyp⁡k⟼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
28 26 27 1 mptfvmpt ⊢K∈V→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
29 2 28 syl ⊢K∈X→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