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 39874
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 39873 . 2 class DVecA
2 vk . . 3 setvar π‘˜
3 cvv 3475 . . 3 class V
4 vw . . . 4 setvar 𝑀
52cv 1541 . . . . 5 class π‘˜
6 clh 38855 . . . . 5 class LHyp
75, 6cfv 6544 . . . 4 class (LHypβ€˜π‘˜)
8 cnx 17126 . . . . . . . 8 class ndx
9 cbs 17144 . . . . . . . 8 class Base
108, 9cfv 6544 . . . . . . 7 class (Baseβ€˜ndx)
114cv 1541 . . . . . . . 8 class 𝑀
12 cltrn 38972 . . . . . . . . 9 class LTrn
135, 12cfv 6544 . . . . . . . 8 class (LTrnβ€˜π‘˜)
1411, 13cfv 6544 . . . . . . 7 class ((LTrnβ€˜π‘˜)β€˜π‘€)
1510, 14cop 4635 . . . . . 6 class ⟨(Baseβ€˜ndx), ((LTrnβ€˜π‘˜)β€˜π‘€)⟩
16 cplusg 17197 . . . . . . . 8 class +g
178, 16cfv 6544 . . . . . . 7 class (+gβ€˜ndx)
18 vf . . . . . . . 8 setvar 𝑓
19 vg . . . . . . . 8 setvar 𝑔
2018cv 1541 . . . . . . . . 9 class 𝑓
2119cv 1541 . . . . . . . . 9 class 𝑔
2220, 21ccom 5681 . . . . . . . 8 class (𝑓 ∘ 𝑔)
2318, 19, 14, 14, 22cmpo 7411 . . . . . . 7 class (𝑓 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€), 𝑔 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€) ↦ (𝑓 ∘ 𝑔))
2417, 23cop 4635 . . . . . 6 class ⟨(+gβ€˜ndx), (𝑓 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€), 𝑔 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€) ↦ (𝑓 ∘ 𝑔))⟩
25 csca 17200 . . . . . . . 8 class Scalar
268, 25cfv 6544 . . . . . . 7 class (Scalarβ€˜ndx)
27 cedring 39624 . . . . . . . . 9 class EDRing
285, 27cfv 6544 . . . . . . . 8 class (EDRingβ€˜π‘˜)
2911, 28cfv 6544 . . . . . . 7 class ((EDRingβ€˜π‘˜)β€˜π‘€)
3026, 29cop 4635 . . . . . 6 class ⟨(Scalarβ€˜ndx), ((EDRingβ€˜π‘˜)β€˜π‘€)⟩
3115, 24, 30ctp 4633 . . . . 5 class {⟨(Baseβ€˜ndx), ((LTrnβ€˜π‘˜)β€˜π‘€)⟩, ⟨(+gβ€˜ndx), (𝑓 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€), 𝑔 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€) ↦ (𝑓 ∘ 𝑔))⟩, ⟨(Scalarβ€˜ndx), ((EDRingβ€˜π‘˜)β€˜π‘€)⟩}
32 cvsca 17201 . . . . . . . 8 class ·𝑠
338, 32cfv 6544 . . . . . . 7 class ( ·𝑠 β€˜ndx)
34 vs . . . . . . . 8 setvar 𝑠
35 ctendo 39623 . . . . . . . . . 10 class TEndo
365, 35cfv 6544 . . . . . . . . 9 class (TEndoβ€˜π‘˜)
3711, 36cfv 6544 . . . . . . . 8 class ((TEndoβ€˜π‘˜)β€˜π‘€)
3834cv 1541 . . . . . . . . 9 class 𝑠
3920, 38cfv 6544 . . . . . . . 8 class (π‘ β€˜π‘“)
4034, 18, 37, 14, 39cmpo 7411 . . . . . . 7 class (𝑠 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€), 𝑓 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€) ↦ (π‘ β€˜π‘“))
4133, 40cop 4635 . . . . . 6 class ⟨( ·𝑠 β€˜ndx), (𝑠 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€), 𝑓 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€) ↦ (π‘ β€˜π‘“))⟩
4241csn 4629 . . . . 5 class {⟨( ·𝑠 β€˜ndx), (𝑠 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€), 𝑓 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€) ↦ (π‘ β€˜π‘“))⟩}
4331, 42cun 3947 . . . 4 class ({⟨(Baseβ€˜ndx), ((LTrnβ€˜π‘˜)β€˜π‘€)⟩, ⟨(+gβ€˜ndx), (𝑓 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€), 𝑔 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€) ↦ (𝑓 ∘ 𝑔))⟩, ⟨(Scalarβ€˜ndx), ((EDRingβ€˜π‘˜)β€˜π‘€)⟩} βˆͺ {⟨( ·𝑠 β€˜ndx), (𝑠 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€), 𝑓 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€) ↦ (π‘ β€˜π‘“))⟩})
444, 7, 43cmpt 5232 . . 3 class (𝑀 ∈ (LHypβ€˜π‘˜) ↦ ({⟨(Baseβ€˜ndx), ((LTrnβ€˜π‘˜)β€˜π‘€)⟩, ⟨(+gβ€˜ndx), (𝑓 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€), 𝑔 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€) ↦ (𝑓 ∘ 𝑔))⟩, ⟨(Scalarβ€˜ndx), ((EDRingβ€˜π‘˜)β€˜π‘€)⟩} βˆͺ {⟨( ·𝑠 β€˜ndx), (𝑠 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€), 𝑓 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€) ↦ (π‘ β€˜π‘“))⟩}))
452, 3, 44cmpt 5232 . 2 class (π‘˜ ∈ V ↦ (𝑀 ∈ (LHypβ€˜π‘˜) ↦ ({⟨(Baseβ€˜ndx), ((LTrnβ€˜π‘˜)β€˜π‘€)⟩, ⟨(+gβ€˜ndx), (𝑓 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€), 𝑔 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€) ↦ (𝑓 ∘ 𝑔))⟩, ⟨(Scalarβ€˜ndx), ((EDRingβ€˜π‘˜)β€˜π‘€)⟩} βˆͺ {⟨( ·𝑠 β€˜ndx), (𝑠 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€), 𝑓 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€) ↦ (π‘ β€˜π‘“))⟩})))
461, 45wceq 1542 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  39875
  Copyright terms: Public domain W3C validator