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

Definition df-dvech 36870
 Description: Define constructed full vector space H. (Contributed by NM, 17-Oct-2013.)
Assertion
Ref Expression
df-dvech DVecH = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ ({⟨(Base‘ndx), (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤))⟩, ⟨(+g‘ndx), (𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)), 𝑔 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨((1st𝑓) ∘ (1st𝑔)), ( ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd𝑓)‘) ∘ ((2nd𝑔)‘)))⟩)⟩, ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩)⟩})))
Distinct variable group:   𝑓,𝑔,,𝑘,𝑠,𝑤

Detailed syntax breakdown of Definition df-dvech
StepHypRef Expression
1 cdvh 36869 . 2 class DVecH
2 vk . . 3 setvar 𝑘
3 cvv 3340 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1631 . . . . 5 class 𝑘
6 clh 35773 . . . . 5 class LHyp
75, 6cfv 6049 . . . 4 class (LHyp‘𝑘)
8 cnx 16056 . . . . . . . 8 class ndx
9 cbs 16059 . . . . . . . 8 class Base
108, 9cfv 6049 . . . . . . 7 class (Base‘ndx)
114cv 1631 . . . . . . . . 9 class 𝑤
12 cltrn 35890 . . . . . . . . . 10 class LTrn
135, 12cfv 6049 . . . . . . . . 9 class (LTrn‘𝑘)
1411, 13cfv 6049 . . . . . . . 8 class ((LTrn‘𝑘)‘𝑤)
15 ctendo 36542 . . . . . . . . . 10 class TEndo
165, 15cfv 6049 . . . . . . . . 9 class (TEndo‘𝑘)
1711, 16cfv 6049 . . . . . . . 8 class ((TEndo‘𝑘)‘𝑤)
1814, 17cxp 5264 . . . . . . 7 class (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤))
1910, 18cop 4327 . . . . . 6 class ⟨(Base‘ndx), (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤))⟩
20 cplusg 16143 . . . . . . . 8 class +g
218, 20cfv 6049 . . . . . . 7 class (+g‘ndx)
22 vf . . . . . . . 8 setvar 𝑓
23 vg . . . . . . . 8 setvar 𝑔
2422cv 1631 . . . . . . . . . . 11 class 𝑓
25 c1st 7331 . . . . . . . . . . 11 class 1st
2624, 25cfv 6049 . . . . . . . . . 10 class (1st𝑓)
2723cv 1631 . . . . . . . . . . 11 class 𝑔
2827, 25cfv 6049 . . . . . . . . . 10 class (1st𝑔)
2926, 28ccom 5270 . . . . . . . . 9 class ((1st𝑓) ∘ (1st𝑔))
30 vh . . . . . . . . . 10 setvar
3130cv 1631 . . . . . . . . . . . 12 class
32 c2nd 7332 . . . . . . . . . . . . 13 class 2nd
3324, 32cfv 6049 . . . . . . . . . . . 12 class (2nd𝑓)
3431, 33cfv 6049 . . . . . . . . . . 11 class ((2nd𝑓)‘)
3527, 32cfv 6049 . . . . . . . . . . . 12 class (2nd𝑔)
3631, 35cfv 6049 . . . . . . . . . . 11 class ((2nd𝑔)‘)
3734, 36ccom 5270 . . . . . . . . . 10 class (((2nd𝑓)‘) ∘ ((2nd𝑔)‘))
3830, 14, 37cmpt 4881 . . . . . . . . 9 class ( ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd𝑓)‘) ∘ ((2nd𝑔)‘)))
3929, 38cop 4327 . . . . . . . 8 class ⟨((1st𝑓) ∘ (1st𝑔)), ( ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd𝑓)‘) ∘ ((2nd𝑔)‘)))⟩
4022, 23, 18, 18, 39cmpt2 6815 . . . . . . 7 class (𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)), 𝑔 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨((1st𝑓) ∘ (1st𝑔)), ( ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd𝑓)‘) ∘ ((2nd𝑔)‘)))⟩)
4121, 40cop 4327 . . . . . 6 class ⟨(+g‘ndx), (𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)), 𝑔 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨((1st𝑓) ∘ (1st𝑔)), ( ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd𝑓)‘) ∘ ((2nd𝑔)‘)))⟩)⟩
42 csca 16146 . . . . . . . 8 class Scalar
438, 42cfv 6049 . . . . . . 7 class (Scalar‘ndx)
44 cedring 36543 . . . . . . . . 9 class EDRing
455, 44cfv 6049 . . . . . . . 8 class (EDRing‘𝑘)
4611, 45cfv 6049 . . . . . . 7 class ((EDRing‘𝑘)‘𝑤)
4743, 46cop 4327 . . . . . 6 class ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩
4819, 41, 47ctp 4325 . . . . 5 class {⟨(Base‘ndx), (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤))⟩, ⟨(+g‘ndx), (𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)), 𝑔 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨((1st𝑓) ∘ (1st𝑔)), ( ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd𝑓)‘) ∘ ((2nd𝑔)‘)))⟩)⟩, ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩}
49 cvsca 16147 . . . . . . . 8 class ·𝑠
508, 49cfv 6049 . . . . . . 7 class ( ·𝑠 ‘ndx)
51 vs . . . . . . . 8 setvar 𝑠
5251cv 1631 . . . . . . . . . 10 class 𝑠
5326, 52cfv 6049 . . . . . . . . 9 class (𝑠‘(1st𝑓))
5452, 33ccom 5270 . . . . . . . . 9 class (𝑠 ∘ (2nd𝑓))
5553, 54cop 4327 . . . . . . . 8 class ⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩
5651, 22, 17, 18, 55cmpt2 6815 . . . . . . 7 class (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩)
5750, 56cop 4327 . . . . . 6 class ⟨( ·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩)⟩
5857csn 4321 . . . . 5 class {⟨( ·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩)⟩}
5948, 58cun 3713 . . . 4 class ({⟨(Base‘ndx), (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤))⟩, ⟨(+g‘ndx), (𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)), 𝑔 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨((1st𝑓) ∘ (1st𝑔)), ( ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd𝑓)‘) ∘ ((2nd𝑔)‘)))⟩)⟩, ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩)⟩})
604, 7, 59cmpt 4881 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ ({⟨(Base‘ndx), (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤))⟩, ⟨(+g‘ndx), (𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)), 𝑔 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨((1st𝑓) ∘ (1st𝑔)), ( ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd𝑓)‘) ∘ ((2nd𝑔)‘)))⟩)⟩, ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩)⟩}))
612, 3, 60cmpt 4881 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ ({⟨(Base‘ndx), (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤))⟩, ⟨(+g‘ndx), (𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)), 𝑔 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨((1st𝑓) ∘ (1st𝑔)), ( ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd𝑓)‘) ∘ ((2nd𝑔)‘)))⟩)⟩, ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩)⟩})))
621, 61wceq 1632 1 wff DVecH = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ ({⟨(Base‘ndx), (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤))⟩, ⟨(+g‘ndx), (𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)), 𝑔 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨((1st𝑓) ∘ (1st𝑔)), ( ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd𝑓)‘) ∘ ((2nd𝑔)‘)))⟩)⟩, ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩)⟩})))
 Colors of variables: wff setvar class This definition is referenced by:  dvhfset  36871
 Copyright terms: Public domain W3C validator