Definition df-dveca 40177

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

Step	Hyp	Ref	Expression
1		cdveca 40176	. 2 class DVecA
2		vk	. . 3 setvar 𝑘
3		cvv 3472	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1538	. . . . 5 class 𝑘
6		clh 39158	. . . . 5 class LHyp
7	5, 6	cfv 6542	. . . 4 class (LHyp‘𝑘)
8		cnx 17130	. . . . . . . 8 class ndx
9		cbs 17148	. . . . . . . 8 class Base
10	8, 9	cfv 6542	. . . . . . 7 class (Base‘ndx)
11	4	cv 1538	. . . . . . . 8 class 𝑤
12		cltrn 39275	. . . . . . . . 9 class LTrn
13	5, 12	cfv 6542	. . . . . . . 8 class (LTrn‘𝑘)
14	11, 13	cfv 6542	. . . . . . 7 class ((LTrn‘𝑘)‘𝑤)
15	10, 14	cop 4633	. . . . . 6 class ⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩
16		cplusg 17201	. . . . . . . 8 class +g
17	8, 16	cfv 6542	. . . . . . 7 class (+g‘ndx)
18		vf	. . . . . . . 8 setvar 𝑓
19		vg	. . . . . . . 8 setvar 𝑔
20	18	cv 1538	. . . . . . . . 9 class 𝑓
21	19	cv 1538	. . . . . . . . 9 class 𝑔
22	20, 21	ccom 5679	. . . . . . . 8 class (𝑓 ∘ 𝑔)
23	18, 19, 14, 14, 22	cmpo 7413	. . . . . . 7 class (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))
24	17, 23	cop 4633	. . . . . 6 class ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))⟩
25		csca 17204	. . . . . . . 8 class Scalar
26	8, 25	cfv 6542	. . . . . . 7 class (Scalar‘ndx)
27		cedring 39927	. . . . . . . . 9 class EDRing
28	5, 27	cfv 6542	. . . . . . . 8 class (EDRing‘𝑘)
29	11, 28	cfv 6542	. . . . . . 7 class ((EDRing‘𝑘)‘𝑤)
30	26, 29	cop 4633	. . . . . 6 class ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩
31	15, 24, 30	ctp 4631	. . . . 5 class {⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))⟩, ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩}
32		cvsca 17205	. . . . . . . 8 class ·𝑠
33	8, 32	cfv 6542	. . . . . . 7 class ( ·𝑠 ‘ndx)
34		vs	. . . . . . . 8 setvar 𝑠
35		ctendo 39926	. . . . . . . . . 10 class TEndo
36	5, 35	cfv 6542	. . . . . . . . 9 class (TEndo‘𝑘)
37	11, 36	cfv 6542	. . . . . . . 8 class ((TEndo‘𝑘)‘𝑤)
38	34	cv 1538	. . . . . . . . 9 class 𝑠
39	20, 38	cfv 6542	. . . . . . . 8 class (𝑠‘𝑓)
40	34, 18, 37, 14, 39	cmpo 7413	. . . . . . 7 class (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠‘𝑓))
41	33, 40	cop 4633	. . . . . 6 class ⟨( ·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠‘𝑓))⟩
42	41	csn 4627	. . . . 5 class {⟨( ·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠‘𝑓))⟩}
43	31, 42	cun 3945	. . . 4 class ({⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))⟩, ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠‘𝑓))⟩})
44	4, 7, 43	cmpt 5230	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ ({⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))⟩, ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠‘𝑓))⟩}))
45	2, 3, 44	cmpt 5230	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ ({⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))⟩, ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠‘𝑓))⟩})))
46	1, 45	wceq 1539	1 wff DVecA = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ ({⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))⟩, ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠‘𝑓))⟩})))

This definition is referenced by:  dvafset  40178