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 36526
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 36320, dochfl1 36245- 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 36525 . 2 class HVMap
2 vk . . 3 setvar 𝑘
3 cvv 3186 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1479 . . . . 5 class 𝑘
6 clh 34750 . . . . 5 class LHyp
75, 6cfv 5847 . . . 4 class (LHyp‘𝑘)
8 vx . . . . 5 setvar 𝑥
94cv 1479 . . . . . . . 8 class 𝑤
10 cdvh 35847 . . . . . . . . 9 class DVecH
115, 10cfv 5847 . . . . . . . 8 class (DVecH‘𝑘)
129, 11cfv 5847 . . . . . . 7 class ((DVecH‘𝑘)‘𝑤)
13 cbs 15781 . . . . . . 7 class Base
1412, 13cfv 5847 . . . . . 6 class (Base‘((DVecH‘𝑘)‘𝑤))
15 c0g 16021 . . . . . . . 8 class 0g
1612, 15cfv 5847 . . . . . . 7 class (0g‘((DVecH‘𝑘)‘𝑤))
1716csn 4148 . . . . . 6 class {(0g‘((DVecH‘𝑘)‘𝑤))}
1814, 17cdif 3552 . . . . 5 class ((Base‘((DVecH‘𝑘)‘𝑤)) ∖ {(0g‘((DVecH‘𝑘)‘𝑤))})
19 vv . . . . . 6 setvar 𝑣
2019cv 1479 . . . . . . . . 9 class 𝑣
21 vt . . . . . . . . . . 11 setvar 𝑡
2221cv 1479 . . . . . . . . . 10 class 𝑡
23 vj . . . . . . . . . . . 12 setvar 𝑗
2423cv 1479 . . . . . . . . . . 11 class 𝑗
258cv 1479 . . . . . . . . . . 11 class 𝑥
26 cvsca 15866 . . . . . . . . . . . 12 class ·𝑠
2712, 26cfv 5847 . . . . . . . . . . 11 class ( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))
2824, 25, 27co 6604 . . . . . . . . . 10 class (𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥)
29 cplusg 15862 . . . . . . . . . . 11 class +g
3012, 29cfv 5847 . . . . . . . . . 10 class (+g‘((DVecH‘𝑘)‘𝑤))
3122, 28, 30co 6604 . . . . . . . . 9 class (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥))
3220, 31wceq 1480 . . . . . . . 8 wff 𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥))
3325csn 4148 . . . . . . . . 9 class {𝑥}
34 coch 36116 . . . . . . . . . . 11 class ocH
355, 34cfv 5847 . . . . . . . . . 10 class (ocH‘𝑘)
369, 35cfv 5847 . . . . . . . . 9 class ((ocH‘𝑘)‘𝑤)
3733, 36cfv 5847 . . . . . . . 8 class (((ocH‘𝑘)‘𝑤)‘{𝑥})
3832, 21, 37wrex 2908 . . . . . . 7 wff 𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥))
39 csca 15865 . . . . . . . . 9 class Scalar
4012, 39cfv 5847 . . . . . . . 8 class (Scalar‘((DVecH‘𝑘)‘𝑤))
4140, 13cfv 5847 . . . . . . 7 class (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))
4238, 23, 41crio 6564 . . . . . 6 class (𝑗 ∈ (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥)))
4319, 14, 42cmpt 4673 . . . . 5 class (𝑣 ∈ (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (𝑗 ∈ (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥))))
448, 18, 43cmpt 4673 . . . 4 class (𝑥 ∈ ((Base‘((DVecH‘𝑘)‘𝑤)) ∖ {(0g‘((DVecH‘𝑘)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (𝑗 ∈ (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥)))))
454, 7, 44cmpt 4673 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ ((Base‘((DVecH‘𝑘)‘𝑤)) ∖ {(0g‘((DVecH‘𝑘)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (𝑗 ∈ (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥))))))
462, 3, 45cmpt 4673 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ ((Base‘((DVecH‘𝑘)‘𝑤)) ∖ {(0g‘((DVecH‘𝑘)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (𝑗 ∈ (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥)))))))
471, 46wceq 1480 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  36527
  Copyright terms: Public domain W3C validator