Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-hvmap Structured version   Visualization version   GIF version

Definition df-hvmap 38773
Description: Extend class notation with a map from each nonzero vector 𝑥 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 38567, dochfl1 38492- should we update those to use this definition? (Contributed by NM, 23-Mar-2015.)
Assertion
Ref Expression
df-hvmap HVMap = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ ((Base‘((DVecH‘𝑘)‘𝑤)) ∖ {(0g‘((DVecH‘𝑘)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (𝑗 ∈ (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥)))))))
Distinct variable group:   𝑤,𝑘,𝑥,𝑣,𝑗,𝑡

Detailed syntax breakdown of Definition df-hvmap
StepHypRef Expression
1 chvm 38772 . 2 class HVMap
2 vk . . 3 setvar 𝑘
3 cvv 3492 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1527 . . . . 5 class 𝑘
6 clh 37000 . . . . 5 class LHyp
75, 6cfv 6348 . . . 4 class (LHyp‘𝑘)
8 vx . . . . 5 setvar 𝑥
94cv 1527 . . . . . . . 8 class 𝑤
10 cdvh 38094 . . . . . . . . 9 class DVecH
115, 10cfv 6348 . . . . . . . 8 class (DVecH‘𝑘)
129, 11cfv 6348 . . . . . . 7 class ((DVecH‘𝑘)‘𝑤)
13 cbs 16471 . . . . . . 7 class Base
1412, 13cfv 6348 . . . . . 6 class (Base‘((DVecH‘𝑘)‘𝑤))
15 c0g 16701 . . . . . . . 8 class 0g
1612, 15cfv 6348 . . . . . . 7 class (0g‘((DVecH‘𝑘)‘𝑤))
1716csn 4557 . . . . . 6 class {(0g‘((DVecH‘𝑘)‘𝑤))}
1814, 17cdif 3930 . . . . 5 class ((Base‘((DVecH‘𝑘)‘𝑤)) ∖ {(0g‘((DVecH‘𝑘)‘𝑤))})
19 vv . . . . . 6 setvar 𝑣
2019cv 1527 . . . . . . . . 9 class 𝑣
21 vt . . . . . . . . . . 11 setvar 𝑡
2221cv 1527 . . . . . . . . . 10 class 𝑡
23 vj . . . . . . . . . . . 12 setvar 𝑗
2423cv 1527 . . . . . . . . . . 11 class 𝑗
258cv 1527 . . . . . . . . . . 11 class 𝑥
26 cvsca 16557 . . . . . . . . . . . 12 class ·𝑠
2712, 26cfv 6348 . . . . . . . . . . 11 class ( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))
2824, 25, 27co 7145 . . . . . . . . . 10 class (𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥)
29 cplusg 16553 . . . . . . . . . . 11 class +g
3012, 29cfv 6348 . . . . . . . . . 10 class (+g‘((DVecH‘𝑘)‘𝑤))
3122, 28, 30co 7145 . . . . . . . . 9 class (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥))
3220, 31wceq 1528 . . . . . . . 8 wff 𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥))
3325csn 4557 . . . . . . . . 9 class {𝑥}
34 coch 38363 . . . . . . . . . . 11 class ocH
355, 34cfv 6348 . . . . . . . . . 10 class (ocH‘𝑘)
369, 35cfv 6348 . . . . . . . . 9 class ((ocH‘𝑘)‘𝑤)
3733, 36cfv 6348 . . . . . . . 8 class (((ocH‘𝑘)‘𝑤)‘{𝑥})
3832, 21, 37wrex 3136 . . . . . . 7 wff 𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥))
39 csca 16556 . . . . . . . . 9 class Scalar
4012, 39cfv 6348 . . . . . . . 8 class (Scalar‘((DVecH‘𝑘)‘𝑤))
4140, 13cfv 6348 . . . . . . 7 class (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))
4238, 23, 41crio 7102 . . . . . 6 class (𝑗 ∈ (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥)))
4319, 14, 42cmpt 5137 . . . . 5 class (𝑣 ∈ (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (𝑗 ∈ (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥))))
448, 18, 43cmpt 5137 . . . 4 class (𝑥 ∈ ((Base‘((DVecH‘𝑘)‘𝑤)) ∖ {(0g‘((DVecH‘𝑘)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (𝑗 ∈ (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥)))))
454, 7, 44cmpt 5137 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ ((Base‘((DVecH‘𝑘)‘𝑤)) ∖ {(0g‘((DVecH‘𝑘)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (𝑗 ∈ (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥))))))
462, 3, 45cmpt 5137 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ ((Base‘((DVecH‘𝑘)‘𝑤)) ∖ {(0g‘((DVecH‘𝑘)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (𝑗 ∈ (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥)))))))
471, 46wceq 1528 1 wff HVMap = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ ((Base‘((DVecH‘𝑘)‘𝑤)) ∖ {(0g‘((DVecH‘𝑘)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (𝑗 ∈ (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥)))))))
Colors of variables: wff setvar class
This definition is referenced by:  hvmapffval  38774
  Copyright terms: Public domain W3C validator