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 36064
 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 35858, dochfl1 35783- 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 36063 . 2 class HVMap
2 vk . . 3 setvar 𝑘
3 cvv 3173 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1474 . . . . 5 class 𝑘
6 clh 34288 . . . . 5 class LHyp
75, 6cfv 5804 . . . 4 class (LHyp‘𝑘)
8 vx . . . . 5 setvar 𝑥
94cv 1474 . . . . . . . 8 class 𝑤
10 cdvh 35385 . . . . . . . . 9 class DVecH
115, 10cfv 5804 . . . . . . . 8 class (DVecH‘𝑘)
129, 11cfv 5804 . . . . . . 7 class ((DVecH‘𝑘)‘𝑤)
13 cbs 15695 . . . . . . 7 class Base
1412, 13cfv 5804 . . . . . 6 class (Base‘((DVecH‘𝑘)‘𝑤))
15 c0g 15923 . . . . . . . 8 class 0g
1612, 15cfv 5804 . . . . . . 7 class (0g‘((DVecH‘𝑘)‘𝑤))
1716csn 4125 . . . . . 6 class {(0g‘((DVecH‘𝑘)‘𝑤))}
1814, 17cdif 3537 . . . . 5 class ((Base‘((DVecH‘𝑘)‘𝑤)) ∖ {(0g‘((DVecH‘𝑘)‘𝑤))})
19 vv . . . . . 6 setvar 𝑣
2019cv 1474 . . . . . . . . 9 class 𝑣
21 vt . . . . . . . . . . 11 setvar 𝑡
2221cv 1474 . . . . . . . . . 10 class 𝑡
23 vj . . . . . . . . . . . 12 setvar 𝑗
2423cv 1474 . . . . . . . . . . 11 class 𝑗
258cv 1474 . . . . . . . . . . 11 class 𝑥
26 cvsca 15772 . . . . . . . . . . . 12 class ·𝑠
2712, 26cfv 5804 . . . . . . . . . . 11 class ( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))
2824, 25, 27co 6549 . . . . . . . . . 10 class (𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥)
29 cplusg 15768 . . . . . . . . . . 11 class +g
3012, 29cfv 5804 . . . . . . . . . 10 class (+g‘((DVecH‘𝑘)‘𝑤))
3122, 28, 30co 6549 . . . . . . . . 9 class (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥))
3220, 31wceq 1475 . . . . . . . 8 wff 𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥))
3325csn 4125 . . . . . . . . 9 class {𝑥}
34 coch 35654 . . . . . . . . . . 11 class ocH
355, 34cfv 5804 . . . . . . . . . 10 class (ocH‘𝑘)
369, 35cfv 5804 . . . . . . . . 9 class ((ocH‘𝑘)‘𝑤)
3733, 36cfv 5804 . . . . . . . 8 class (((ocH‘𝑘)‘𝑤)‘{𝑥})
3832, 21, 37wrex 2897 . . . . . . 7 wff 𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥))
39 csca 15771 . . . . . . . . 9 class Scalar
4012, 39cfv 5804 . . . . . . . 8 class (Scalar‘((DVecH‘𝑘)‘𝑤))
4140, 13cfv 5804 . . . . . . 7 class (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))
4238, 23, 41crio 6510 . . . . . 6 class (𝑗 ∈ (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥)))
4319, 14, 42cmpt 4643 . . . . 5 class (𝑣 ∈ (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (𝑗 ∈ (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥))))
448, 18, 43cmpt 4643 . . . 4 class (𝑥 ∈ ((Base‘((DVecH‘𝑘)‘𝑤)) ∖ {(0g‘((DVecH‘𝑘)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (𝑗 ∈ (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥)))))
454, 7, 44cmpt 4643 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ ((Base‘((DVecH‘𝑘)‘𝑤)) ∖ {(0g‘((DVecH‘𝑘)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (𝑗 ∈ (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥))))))
462, 3, 45cmpt 4643 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ ((Base‘((DVecH‘𝑘)‘𝑤)) ∖ {(0g‘((DVecH‘𝑘)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (𝑗 ∈ (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥)))))))
471, 46wceq 1475 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  36065
 Copyright terms: Public domain W3C validator