Metamath Proof Explorer

Definition df-hvmap

Description: Extend class notation with a map from each nonzero vector x to a unique nonzero functional in the closed kernel dual space. (We could extend it to include the zero vector, but that is unnecessary for our purposes.) TODO: This pattern is used several times earlier, e.g., lcf1o , dochfl1 - should we update those to use this definition? (Contributed by NM, 23-Mar-2015)

Ref Expression
Assertion 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

Detailed syntax breakdown

Step Hyp Ref Expression
0 chvm class HVMap
1 vk setvar k
2 cvv class V
3 vw setvar w
4 clh class LHyp
5 1 cv setvar k
6 5 4 cfv class LHyp ⁡ k
7 vx setvar x
8 cbs class Base
9 cdvh class DVecH
10 5 9 cfv class DVecH ⁡ k
11 3 cv setvar w
12 11 10 cfv class DVecH ⁡ k ⁡ w
13 12 8 cfv class Base DVecH ⁡ k ⁡ w
14 c0g class 0 𝑔
15 12 14 cfv class 0 DVecH ⁡ k ⁡ w
16 15 csn class 0 DVecH ⁡ k ⁡ w
17 13 16 cdif class Base DVecH ⁡ k ⁡ w ∖ 0 DVecH ⁡ k ⁡ w
18 vv setvar v
19 vj setvar j
20 csca class Scalar
21 12 20 cfv class Scalar ⁡ DVecH ⁡ k ⁡ w
22 21 8 cfv class Base Scalar ⁡ DVecH ⁡ k ⁡ w
23 vt setvar t
24 coch class ocH
25 5 24 cfv class ocH ⁡ k
26 11 25 cfv class ocH ⁡ k ⁡ w
27 7 cv setvar x
28 27 csn class x
29 28 26 cfv class ocH ⁡ k ⁡ w ⁡ x
30 18 cv setvar v
31 23 cv setvar t
32 cplusg class + 𝑔
33 12 32 cfv class + DVecH ⁡ k ⁡ w
34 19 cv setvar j
35 cvsca class ⋅ 𝑠
36 12 35 cfv class ⋅ DVecH ⁡ k ⁡ w
37 34 27 36 co class j ⋅ DVecH ⁡ k ⁡ w x
38 31 37 33 co class t + DVecH ⁡ k ⁡ w j ⋅ DVecH ⁡ k ⁡ w x
39 30 38 wceq wff v = t + DVecH ⁡ k ⁡ w j ⋅ DVecH ⁡ k ⁡ w x
40 39 23 29 wrex wff ∃ t ∈ ocH ⁡ k ⁡ w ⁡ x v = t + DVecH ⁡ k ⁡ w j ⋅ DVecH ⁡ k ⁡ w x
41 40 19 22 crio class ι j ∈ Base Scalar ⁡ DVecH ⁡ k ⁡ w | ∃ t ∈ ocH ⁡ k ⁡ w ⁡ x v = t + DVecH ⁡ k ⁡ w j ⋅ DVecH ⁡ k ⁡ w x
42 18 13 41 cmpt class 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
43 7 17 42 cmpt class 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
44 3 6 43 cmpt class 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
45 1 2 44 cmpt class 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
46 0 45 wceq wff 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