Definition df-dvech 39100

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

Step	Hyp	Ref	Expression
1		cdvh 39099	. 2 class DVecH
2		vk	. . 3 setvar 𝑘
3		cvv 3433	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1538	. . . . 5 class 𝑘
6		clh 38005	. . . . 5 class LHyp
7	5, 6	cfv 6437	. . . 4 class (LHyp‘𝑘)
8		cnx 16903	. . . . . . . 8 class ndx
9		cbs 16921	. . . . . . . 8 class Base
10	8, 9	cfv 6437	. . . . . . 7 class (Base‘ndx)
11	4	cv 1538	. . . . . . . . 9 class 𝑤
12		cltrn 38122	. . . . . . . . . 10 class LTrn
13	5, 12	cfv 6437	. . . . . . . . 9 class (LTrn‘𝑘)
14	11, 13	cfv 6437	. . . . . . . 8 class ((LTrn‘𝑘)‘𝑤)
15		ctendo 38773	. . . . . . . . . 10 class TEndo
16	5, 15	cfv 6437	. . . . . . . . 9 class (TEndo‘𝑘)
17	11, 16	cfv 6437	. . . . . . . 8 class ((TEndo‘𝑘)‘𝑤)
18	14, 17	cxp 5588	. . . . . . 7 class (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤))
19	10, 18	cop 4568	. . . . . 6 class ⟨(Base‘ndx), (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤))⟩
20		cplusg 16971	. . . . . . . 8 class +g
21	8, 20	cfv 6437	. . . . . . 7 class (+g‘ndx)
22		vf	. . . . . . . 8 setvar 𝑓
23		vg	. . . . . . . 8 setvar 𝑔
24	22	cv 1538	. . . . . . . . . . 11 class 𝑓
25		c1st 7838	. . . . . . . . . . 11 class 1st
26	24, 25	cfv 6437	. . . . . . . . . 10 class (1st ‘𝑓)
27	23	cv 1538	. . . . . . . . . . 11 class 𝑔
28	27, 25	cfv 6437	. . . . . . . . . 10 class (1st ‘𝑔)
29	26, 28	ccom 5594	. . . . . . . . 9 class ((1st ‘𝑓) ∘ (1st ‘𝑔))
30		vh	. . . . . . . . . 10 setvar ℎ
31	30	cv 1538	. . . . . . . . . . . 12 class ℎ
32		c2nd 7839	. . . . . . . . . . . . 13 class 2nd
33	24, 32	cfv 6437	. . . . . . . . . . . 12 class (2nd ‘𝑓)
34	31, 33	cfv 6437	. . . . . . . . . . 11 class ((2nd ‘𝑓)‘ℎ)
35	27, 32	cfv 6437	. . . . . . . . . . . 12 class (2nd ‘𝑔)
36	31, 35	cfv 6437	. . . . . . . . . . 11 class ((2nd ‘𝑔)‘ℎ)
37	34, 36	ccom 5594	. . . . . . . . . 10 class (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ))
38	30, 14, 37	cmpt 5158	. . . . . . . . 9 class (ℎ ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ)))
39	29, 38	cop 4568	. . . . . . . 8 class ⟨((1st ‘𝑓) ∘ (1st ‘𝑔)), (ℎ ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ)))⟩
40	22, 23, 18, 18, 39	cmpo 7286	. . . . . . 7 class (𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)), 𝑔 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨((1st ‘𝑓) ∘ (1st ‘𝑔)), (ℎ ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ)))⟩)
41	21, 40	cop 4568	. . . . . 6 class ⟨(+g‘ndx), (𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)), 𝑔 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨((1st ‘𝑓) ∘ (1st ‘𝑔)), (ℎ ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ)))⟩)⟩
42		csca 16974	. . . . . . . 8 class Scalar
43	8, 42	cfv 6437	. . . . . . 7 class (Scalar‘ndx)
44		cedring 38774	. . . . . . . . 9 class EDRing
45	5, 44	cfv 6437	. . . . . . . 8 class (EDRing‘𝑘)
46	11, 45	cfv 6437	. . . . . . 7 class ((EDRing‘𝑘)‘𝑤)
47	43, 46	cop 4568	. . . . . 6 class ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩
48	19, 41, 47	ctp 4566	. . . . 5 class {⟨(Base‘ndx), (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤))⟩, ⟨(+g‘ndx), (𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)), 𝑔 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨((1st ‘𝑓) ∘ (1st ‘𝑔)), (ℎ ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ)))⟩)⟩, ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩}
49		cvsca 16975	. . . . . . . 8 class ·𝑠
50	8, 49	cfv 6437	. . . . . . 7 class ( ·𝑠 ‘ndx)
51		vs	. . . . . . . 8 setvar 𝑠
52	51	cv 1538	. . . . . . . . . 10 class 𝑠
53	26, 52	cfv 6437	. . . . . . . . 9 class (𝑠‘(1st ‘𝑓))
54	52, 33	ccom 5594	. . . . . . . . 9 class (𝑠 ∘ (2nd ‘𝑓))
55	53, 54	cop 4568	. . . . . . . 8 class ⟨(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))⟩
56	51, 22, 17, 18, 55	cmpo 7286	. . . . . . 7 class (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))⟩)
57	50, 56	cop 4568	. . . . . 6 class ⟨( ·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))⟩)⟩
58	57	csn 4562	. . . . 5 class {⟨( ·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))⟩)⟩}
59	48, 58	cun 3886	. . . 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 ‘𝑓))⟩)⟩})
60	4, 7, 59	cmpt 5158	. . 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 ‘𝑓))⟩)⟩}))
61	2, 3, 60	cmpt 5158	. 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 ‘𝑓))⟩)⟩})))
62	1, 61	wceq 1539	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 ‘𝑓))⟩)⟩})))

This definition is referenced by:  dvhfset  39101