Users' Mathboxes 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 35848
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 35847 . 2 class DVecH
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 cnx 15778 . . . . . . . 8 class ndx
9 cbs 15781 . . . . . . . 8 class Base
108, 9cfv 5847 . . . . . . 7 class (Base‘ndx)
114cv 1479 . . . . . . . . 9 class 𝑤
12 cltrn 34867 . . . . . . . . . 10 class LTrn
135, 12cfv 5847 . . . . . . . . 9 class (LTrn‘𝑘)
1411, 13cfv 5847 . . . . . . . 8 class ((LTrn‘𝑘)‘𝑤)
15 ctendo 35520 . . . . . . . . . 10 class TEndo
165, 15cfv 5847 . . . . . . . . 9 class (TEndo‘𝑘)
1711, 16cfv 5847 . . . . . . . 8 class ((TEndo‘𝑘)‘𝑤)
1814, 17cxp 5072 . . . . . . 7 class (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤))
1910, 18cop 4154 . . . . . 6 class ⟨(Base‘ndx), (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤))⟩
20 cplusg 15862 . . . . . . . 8 class +g
218, 20cfv 5847 . . . . . . 7 class (+g‘ndx)
22 vf . . . . . . . 8 setvar 𝑓
23 vg . . . . . . . 8 setvar 𝑔
2422cv 1479 . . . . . . . . . . 11 class 𝑓
25 c1st 7111 . . . . . . . . . . 11 class 1st
2624, 25cfv 5847 . . . . . . . . . 10 class (1st𝑓)
2723cv 1479 . . . . . . . . . . 11 class 𝑔
2827, 25cfv 5847 . . . . . . . . . 10 class (1st𝑔)
2926, 28ccom 5078 . . . . . . . . 9 class ((1st𝑓) ∘ (1st𝑔))
30 vh . . . . . . . . . 10 setvar
3130cv 1479 . . . . . . . . . . . 12 class
32 c2nd 7112 . . . . . . . . . . . . 13 class 2nd
3324, 32cfv 5847 . . . . . . . . . . . 12 class (2nd𝑓)
3431, 33cfv 5847 . . . . . . . . . . 11 class ((2nd𝑓)‘)
3527, 32cfv 5847 . . . . . . . . . . . 12 class (2nd𝑔)
3631, 35cfv 5847 . . . . . . . . . . 11 class ((2nd𝑔)‘)
3734, 36ccom 5078 . . . . . . . . . 10 class (((2nd𝑓)‘) ∘ ((2nd𝑔)‘))
3830, 14, 37cmpt 4673 . . . . . . . . 9 class ( ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd𝑓)‘) ∘ ((2nd𝑔)‘)))
3929, 38cop 4154 . . . . . . . 8 class ⟨((1st𝑓) ∘ (1st𝑔)), ( ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd𝑓)‘) ∘ ((2nd𝑔)‘)))⟩
4022, 23, 18, 18, 39cmpt2 6606 . . . . . . 7 class (𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)), 𝑔 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨((1st𝑓) ∘ (1st𝑔)), ( ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd𝑓)‘) ∘ ((2nd𝑔)‘)))⟩)
4121, 40cop 4154 . . . . . 6 class ⟨(+g‘ndx), (𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)), 𝑔 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨((1st𝑓) ∘ (1st𝑔)), ( ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd𝑓)‘) ∘ ((2nd𝑔)‘)))⟩)⟩
42 csca 15865 . . . . . . . 8 class Scalar
438, 42cfv 5847 . . . . . . 7 class (Scalar‘ndx)
44 cedring 35521 . . . . . . . . 9 class EDRing
455, 44cfv 5847 . . . . . . . 8 class (EDRing‘𝑘)
4611, 45cfv 5847 . . . . . . 7 class ((EDRing‘𝑘)‘𝑤)
4743, 46cop 4154 . . . . . 6 class ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩
4819, 41, 47ctp 4152 . . . . 5 class {⟨(Base‘ndx), (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤))⟩, ⟨(+g‘ndx), (𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)), 𝑔 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨((1st𝑓) ∘ (1st𝑔)), ( ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd𝑓)‘) ∘ ((2nd𝑔)‘)))⟩)⟩, ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩}
49 cvsca 15866 . . . . . . . 8 class ·𝑠
508, 49cfv 5847 . . . . . . 7 class ( ·𝑠 ‘ndx)
51 vs . . . . . . . 8 setvar 𝑠
5251cv 1479 . . . . . . . . . 10 class 𝑠
5326, 52cfv 5847 . . . . . . . . 9 class (𝑠‘(1st𝑓))
5452, 33ccom 5078 . . . . . . . . 9 class (𝑠 ∘ (2nd𝑓))
5553, 54cop 4154 . . . . . . . 8 class ⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩
5651, 22, 17, 18, 55cmpt2 6606 . . . . . . 7 class (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩)
5750, 56cop 4154 . . . . . 6 class ⟨( ·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩)⟩
5857csn 4148 . . . . 5 class {⟨( ·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩)⟩}
5948, 58cun 3553 . . . 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 4673 . . 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 4673 . 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 1480 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  35849
  Copyright terms: Public domain W3C validator