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 ∈ Base DVecH ⁡ K ⁡ w ∖ 0 DVecH ⁡ K ⁡ w ⟼ v ∈ Base DVecH ⁡ K ⁡ w ⟼ ι j ∈ Base Scalar ⁡ DVecH ⁡ K ⁡ w | ∃ t ∈ ocH ⁡ K ⁡ w ⁡ x v = t + DVecH ⁡ K ⁡ w j ⋅ DVecH ⁡ K ⁡ w x

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 → Base DVecH ⁡ k ⁡ w = Base DVecH ⁡ K ⁡ w
8 6 fveq2d ⊢ k = K → 0 DVecH ⁡ k ⁡ w = 0 DVecH ⁡ K ⁡ w
9 8 sneqd ⊢ k = K → 0 DVecH ⁡ k ⁡ w = 0 DVecH ⁡ K ⁡ w
10 7 9 difeq12d ⊢ k = K → Base DVecH ⁡ k ⁡ w ∖ 0 DVecH ⁡ k ⁡ w = Base DVecH ⁡ K ⁡ w ∖ 0 DVecH ⁡ K ⁡ w
11 6 fveq2d ⊢ k = K → Scalar ⁡ DVecH ⁡ k ⁡ w = Scalar ⁡ DVecH ⁡ K ⁡ w
12 11 fveq2d ⊢ k = K → Base Scalar ⁡ DVecH ⁡ k ⁡ w = Base Scalar ⁡ 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 ⁡ w x = j ⋅ DVecH ⁡ K ⁡ w x
20 16 17 19 oveq123d ⊢ k = K → t + DVecH ⁡ k ⁡ w j ⋅ DVecH ⁡ k ⁡ w x = t + DVecH ⁡ K ⁡ w j ⋅ DVecH ⁡ K ⁡ w x
21 20 eqeq2d ⊢ k = K → v = t + DVecH ⁡ k ⁡ w j ⋅ DVecH ⁡ k ⁡ w x ↔ v = t + DVecH ⁡ K ⁡ w j ⋅ DVecH ⁡ K ⁡ w x
22 15 21 rexeqbidv ⊢ k = K → ∃ t ∈ ocH ⁡ k ⁡ w ⁡ x v = t + DVecH ⁡ k ⁡ w j ⋅ DVecH ⁡ k ⁡ w x ↔ ∃ t ∈ ocH ⁡ K ⁡ w ⁡ x v = t + DVecH ⁡ K ⁡ w j ⋅ DVecH ⁡ K ⁡ w x
23 12 22 riotaeqbidv ⊢ k = K → ι j ∈ Base Scalar ⁡ DVecH ⁡ k ⁡ w | ∃ t ∈ ocH ⁡ k ⁡ w ⁡ x v = t + DVecH ⁡ k ⁡ w j ⋅ DVecH ⁡ k ⁡ w x = ι j ∈ Base Scalar ⁡ DVecH ⁡ K ⁡ w | ∃ t ∈ ocH ⁡ K ⁡ w ⁡ x v = t + DVecH ⁡ K ⁡ w j ⋅ DVecH ⁡ K ⁡ w x
24 7 23 mpteq12dv ⊢ k = K → v ∈ Base DVecH ⁡ k ⁡ w ⟼ ι j ∈ Base Scalar ⁡ DVecH ⁡ k ⁡ w | ∃ t ∈ ocH ⁡ k ⁡ w ⁡ x v = t + DVecH ⁡ k ⁡ w j ⋅ DVecH ⁡ k ⁡ w x = v ∈ Base DVecH ⁡ K ⁡ w ⟼ ι j ∈ Base Scalar ⁡ DVecH ⁡ K ⁡ w | ∃ t ∈ ocH ⁡ K ⁡ w ⁡ x v = t + DVecH ⁡ K ⁡ w j ⋅ DVecH ⁡ K ⁡ w x
25 10 24 mpteq12dv ⊢ k = K → x ∈ Base DVecH ⁡ k ⁡ w ∖ 0 DVecH ⁡ k ⁡ w ⟼ v ∈ Base DVecH ⁡ k ⁡ w ⟼ ι j ∈ Base Scalar ⁡ DVecH ⁡ k ⁡ w | ∃ t ∈ ocH ⁡ k ⁡ w ⁡ x v = t + DVecH ⁡ k ⁡ w j ⋅ DVecH ⁡ k ⁡ w x = x ∈ Base DVecH ⁡ K ⁡ w ∖ 0 DVecH ⁡ K ⁡ w ⟼ v ∈ Base DVecH ⁡ K ⁡ w ⟼ ι j ∈ Base Scalar ⁡ DVecH ⁡ K ⁡ w | ∃ t ∈ ocH ⁡ K ⁡ w ⁡ x v = t + DVecH ⁡ K ⁡ w j ⋅ DVecH ⁡ K ⁡ w x
26 4 25 mpteq12dv ⊢ k = K → w ∈ LHyp ⁡ k ⟼ x ∈ Base DVecH ⁡ k ⁡ w ∖ 0 DVecH ⁡ k ⁡ w ⟼ v ∈ Base DVecH ⁡ k ⁡ w ⟼ ι j ∈ Base Scalar ⁡ DVecH ⁡ k ⁡ w | ∃ t ∈ ocH ⁡ k ⁡ w ⁡ x v = t + DVecH ⁡ k ⁡ w j ⋅ DVecH ⁡ k ⁡ w x = w ∈ H ⟼ x ∈ Base DVecH ⁡ K ⁡ w ∖ 0 DVecH ⁡ K ⁡ w ⟼ v ∈ Base DVecH ⁡ K ⁡ w ⟼ ι j ∈ Base Scalar ⁡ DVecH ⁡ K ⁡ w | ∃ t ∈ ocH ⁡ K ⁡ w ⁡ x v = t + DVecH ⁡ K ⁡ w j ⋅ DVecH ⁡ K ⁡ w x
27 df-hvmap ⊢ HVMap = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ x ∈ Base DVecH ⁡ k ⁡ w ∖ 0 DVecH ⁡ k ⁡ w ⟼ v ∈ Base DVecH ⁡ k ⁡ w ⟼ ι j ∈ Base Scalar ⁡ DVecH ⁡ k ⁡ w | ∃ t ∈ ocH ⁡ k ⁡ w ⁡ x v = t + DVecH ⁡ k ⁡ w j ⋅ DVecH ⁡ k ⁡ w x
28 26 27 1 mptfvmpt ⊢ K ∈ V → HVMap ⁡ K = w ∈ H ⟼ x ∈ Base DVecH ⁡ K ⁡ w ∖ 0 DVecH ⁡ K ⁡ w ⟼ v ∈ Base DVecH ⁡ K ⁡ w ⟼ ι j ∈ Base Scalar ⁡ DVecH ⁡ K ⁡ w | ∃ t ∈ ocH ⁡ K ⁡ w ⁡ x v = t + DVecH ⁡ K ⁡ w j ⋅ DVecH ⁡ K ⁡ w x
29 2 28 syl ⊢ K ∈ X → HVMap ⁡ K = w ∈ H ⟼ x ∈ Base DVecH ⁡ K ⁡ w ∖ 0 DVecH ⁡ K ⁡ w ⟼ v ∈ Base DVecH ⁡ K ⁡ w ⟼ ι j ∈ Base Scalar ⁡ DVecH ⁡ K ⁡ w | ∃ t ∈ ocH ⁡ K ⁡ w ⁡ x v = t + DVecH ⁡ K ⁡ w j ⋅ DVecH ⁡ K ⁡ w x