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

Definition df-dveca 35771
Description: Define constructed partial vector space A. (Contributed by NM, 8-Oct-2013.)
Assertion
Ref Expression
df-dveca DVecA = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ ({⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓𝑔))⟩, ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠𝑓))⟩})))
Distinct variable group:   𝑤,𝑘,𝑠,𝑓,𝑔

Detailed syntax breakdown of Definition df-dveca
StepHypRef Expression
1 cdveca 35770 . 2 class DVecA
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 . . . . . . . 8 class 𝑤
12 cltrn 34867 . . . . . . . . 9 class LTrn
135, 12cfv 5847 . . . . . . . 8 class (LTrn‘𝑘)
1411, 13cfv 5847 . . . . . . 7 class ((LTrn‘𝑘)‘𝑤)
1510, 14cop 4154 . . . . . 6 class ⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩
16 cplusg 15862 . . . . . . . 8 class +g
178, 16cfv 5847 . . . . . . 7 class (+g‘ndx)
18 vf . . . . . . . 8 setvar 𝑓
19 vg . . . . . . . 8 setvar 𝑔
2018cv 1479 . . . . . . . . 9 class 𝑓
2119cv 1479 . . . . . . . . 9 class 𝑔
2220, 21ccom 5078 . . . . . . . 8 class (𝑓𝑔)
2318, 19, 14, 14, 22cmpt2 6606 . . . . . . 7 class (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓𝑔))
2417, 23cop 4154 . . . . . 6 class ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓𝑔))⟩
25 csca 15865 . . . . . . . 8 class Scalar
268, 25cfv 5847 . . . . . . 7 class (Scalar‘ndx)
27 cedring 35521 . . . . . . . . 9 class EDRing
285, 27cfv 5847 . . . . . . . 8 class (EDRing‘𝑘)
2911, 28cfv 5847 . . . . . . 7 class ((EDRing‘𝑘)‘𝑤)
3026, 29cop 4154 . . . . . 6 class ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩
3115, 24, 30ctp 4152 . . . . 5 class {⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓𝑔))⟩, ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩}
32 cvsca 15866 . . . . . . . 8 class ·𝑠
338, 32cfv 5847 . . . . . . 7 class ( ·𝑠 ‘ndx)
34 vs . . . . . . . 8 setvar 𝑠
35 ctendo 35520 . . . . . . . . . 10 class TEndo
365, 35cfv 5847 . . . . . . . . 9 class (TEndo‘𝑘)
3711, 36cfv 5847 . . . . . . . 8 class ((TEndo‘𝑘)‘𝑤)
3834cv 1479 . . . . . . . . 9 class 𝑠
3920, 38cfv 5847 . . . . . . . 8 class (𝑠𝑓)
4034, 18, 37, 14, 39cmpt2 6606 . . . . . . 7 class (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠𝑓))
4133, 40cop 4154 . . . . . 6 class ⟨( ·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠𝑓))⟩
4241csn 4148 . . . . 5 class {⟨( ·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠𝑓))⟩}
4331, 42cun 3553 . . . 4 class ({⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓𝑔))⟩, ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠𝑓))⟩})
444, 7, 43cmpt 4673 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ ({⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓𝑔))⟩, ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠𝑓))⟩}))
452, 3, 44cmpt 4673 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ ({⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓𝑔))⟩, ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠𝑓))⟩})))
461, 45wceq 1480 1 wff DVecA = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ ({⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓𝑔))⟩, ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠𝑓))⟩})))
Colors of variables: wff setvar class
This definition is referenced by:  dvafset  35772
  Copyright terms: Public domain W3C validator