df-dvech - Mathbox for Norm Megill

	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 39938

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‘𝑘)‘𝑤)) ↦ ⟨((1^st ‘𝑓) ∘ (1^st ‘𝑔)), (ℎ ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2^nd ‘𝑓)‘ℎ) ∘ ((2^nd ‘𝑔)‘ℎ)))⟩)⟩, ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩} ∪ {⟨( ·_𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨(𝑠‘(1^st ‘𝑓)), (𝑠 ∘ (2^nd ‘𝑓))⟩)⟩})))

Distinct variable group: 𝑓,𝑔,ℎ,𝑘,𝑠,𝑤

**Detailed syntax breakdown of Definition df-dvech**
Step	Hyp	Ref	Expression
1		cdvh 39937	. 2 class DVecH
2		vk	. . 3 setvar 𝑘
3		cvv 3474	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1540	. . . . 5 class 𝑘
6		clh 38843	. . . . 5 class LHyp
7	5, 6	cfv 6540	. . . 4 class (LHyp‘𝑘)
8		cnx 17122	. . . . . . . 8 class ndx
9		cbs 17140	. . . . . . . 8 class Base
10	8, 9	cfv 6540	. . . . . . 7 class (Base‘ndx)
11	4	cv 1540	. . . . . . . . 9 class 𝑤
12		cltrn 38960	. . . . . . . . . 10 class LTrn
13	5, 12	cfv 6540	. . . . . . . . 9 class (LTrn‘𝑘)
14	11, 13	cfv 6540	. . . . . . . 8 class ((LTrn‘𝑘)‘𝑤)
15		ctendo 39611	. . . . . . . . . 10 class TEndo
16	5, 15	cfv 6540	. . . . . . . . 9 class (TEndo‘𝑘)
17	11, 16	cfv 6540	. . . . . . . 8 class ((TEndo‘𝑘)‘𝑤)
18	14, 17	cxp 5673	. . . . . . 7 class (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤))
19	10, 18	cop 4633	. . . . . 6 class ⟨(Base‘ndx), (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤))⟩
20		cplusg 17193	. . . . . . . 8 class +_g
21	8, 20	cfv 6540	. . . . . . 7 class (+_g‘ndx)
22		vf	. . . . . . . 8 setvar 𝑓
23		vg	. . . . . . . 8 setvar 𝑔
24	22	cv 1540	. . . . . . . . . . 11 class 𝑓
25		c1st 7969	. . . . . . . . . . 11 class 1^st
26	24, 25	cfv 6540	. . . . . . . . . 10 class (1^st ‘𝑓)
27	23	cv 1540	. . . . . . . . . . 11 class 𝑔
28	27, 25	cfv 6540	. . . . . . . . . 10 class (1^st ‘𝑔)
29	26, 28	ccom 5679	. . . . . . . . 9 class ((1^st ‘𝑓) ∘ (1^st ‘𝑔))
30		vh	. . . . . . . . . 10 setvar ℎ
31	30	cv 1540	. . . . . . . . . . . 12 class ℎ
32		c2nd 7970	. . . . . . . . . . . . 13 class 2^nd
33	24, 32	cfv 6540	. . . . . . . . . . . 12 class (2^nd ‘𝑓)
34	31, 33	cfv 6540	. . . . . . . . . . 11 class ((2^nd ‘𝑓)‘ℎ)
35	27, 32	cfv 6540	. . . . . . . . . . . 12 class (2^nd ‘𝑔)
36	31, 35	cfv 6540	. . . . . . . . . . 11 class ((2^nd ‘𝑔)‘ℎ)
37	34, 36	ccom 5679	. . . . . . . . . 10 class (((2^nd ‘𝑓)‘ℎ) ∘ ((2^nd ‘𝑔)‘ℎ))
38	30, 14, 37	cmpt 5230	. . . . . . . . 9 class (ℎ ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2^nd ‘𝑓)‘ℎ) ∘ ((2^nd ‘𝑔)‘ℎ)))
39	29, 38	cop 4633	. . . . . . . 8 class ⟨((1^st ‘𝑓) ∘ (1^st ‘𝑔)), (ℎ ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2^nd ‘𝑓)‘ℎ) ∘ ((2^nd ‘𝑔)‘ℎ)))⟩
40	22, 23, 18, 18, 39	cmpo 7407	. . . . . . 7 class (𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)), 𝑔 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨((1^st ‘𝑓) ∘ (1^st ‘𝑔)), (ℎ ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2^nd ‘𝑓)‘ℎ) ∘ ((2^nd ‘𝑔)‘ℎ)))⟩)
41	21, 40	cop 4633	. . . . . 6 class ⟨(+_g‘ndx), (𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)), 𝑔 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨((1^st ‘𝑓) ∘ (1^st ‘𝑔)), (ℎ ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2^nd ‘𝑓)‘ℎ) ∘ ((2^nd ‘𝑔)‘ℎ)))⟩)⟩
42		csca 17196	. . . . . . . 8 class Scalar
43	8, 42	cfv 6540	. . . . . . 7 class (Scalar‘ndx)
44		cedring 39612	. . . . . . . . 9 class EDRing
45	5, 44	cfv 6540	. . . . . . . 8 class (EDRing‘𝑘)
46	11, 45	cfv 6540	. . . . . . 7 class ((EDRing‘𝑘)‘𝑤)
47	43, 46	cop 4633	. . . . . 6 class ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩
48	19, 41, 47	ctp 4631	. . . . 5 class {⟨(Base‘ndx), (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤))⟩, ⟨(+_g‘ndx), (𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)), 𝑔 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨((1^st ‘𝑓) ∘ (1^st ‘𝑔)), (ℎ ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2^nd ‘𝑓)‘ℎ) ∘ ((2^nd ‘𝑔)‘ℎ)))⟩)⟩, ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩}
49		cvsca 17197	. . . . . . . 8 class ·_𝑠
50	8, 49	cfv 6540	. . . . . . 7 class ( ·_𝑠 ‘ndx)
51		vs	. . . . . . . 8 setvar 𝑠
52	51	cv 1540	. . . . . . . . . 10 class 𝑠
53	26, 52	cfv 6540	. . . . . . . . 9 class (𝑠‘(1^st ‘𝑓))
54	52, 33	ccom 5679	. . . . . . . . 9 class (𝑠 ∘ (2^nd ‘𝑓))
55	53, 54	cop 4633	. . . . . . . 8 class ⟨(𝑠‘(1^st ‘𝑓)), (𝑠 ∘ (2^nd ‘𝑓))⟩
56	51, 22, 17, 18, 55	cmpo 7407	. . . . . . 7 class (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨(𝑠‘(1^st ‘𝑓)), (𝑠 ∘ (2^nd ‘𝑓))⟩)
57	50, 56	cop 4633	. . . . . 6 class ⟨( ·_𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨(𝑠‘(1^st ‘𝑓)), (𝑠 ∘ (2^nd ‘𝑓))⟩)⟩
58	57	csn 4627	. . . . 5 class {⟨( ·_𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨(𝑠‘(1^st ‘𝑓)), (𝑠 ∘ (2^nd ‘𝑓))⟩)⟩}
59	48, 58	cun 3945	. . . 4 class ({⟨(Base‘ndx), (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤))⟩, ⟨(+_g‘ndx), (𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)), 𝑔 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨((1^st ‘𝑓) ∘ (1^st ‘𝑔)), (ℎ ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2^nd ‘𝑓)‘ℎ) ∘ ((2^nd ‘𝑔)‘ℎ)))⟩)⟩, ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩} ∪ {⟨( ·_𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨(𝑠‘(1^st ‘𝑓)), (𝑠 ∘ (2^nd ‘𝑓))⟩)⟩})
60	4, 7, 59	cmpt 5230	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ ({⟨(Base‘ndx), (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤))⟩, ⟨(+_g‘ndx), (𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)), 𝑔 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨((1^st ‘𝑓) ∘ (1^st ‘𝑔)), (ℎ ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2^nd ‘𝑓)‘ℎ) ∘ ((2^nd ‘𝑔)‘ℎ)))⟩)⟩, ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩} ∪ {⟨( ·_𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨(𝑠‘(1^st ‘𝑓)), (𝑠 ∘ (2^nd ‘𝑓))⟩)⟩}))
61	2, 3, 60	cmpt 5230	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ ({⟨(Base‘ndx), (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤))⟩, ⟨(+_g‘ndx), (𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)), 𝑔 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨((1^st ‘𝑓) ∘ (1^st ‘𝑔)), (ℎ ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2^nd ‘𝑓)‘ℎ) ∘ ((2^nd ‘𝑔)‘ℎ)))⟩)⟩, ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩} ∪ {⟨( ·_𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨(𝑠‘(1^st ‘𝑓)), (𝑠 ∘ (2^nd ‘𝑓))⟩)⟩})))
62	1, 61	wceq 1541	1 wff DVecH = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ ({⟨(Base‘ndx), (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤))⟩, ⟨(+_g‘ndx), (𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)), 𝑔 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨((1^st ‘𝑓) ∘ (1^st ‘𝑔)), (ℎ ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2^nd ‘𝑓)‘ℎ) ∘ ((2^nd ‘𝑔)‘ℎ)))⟩)⟩, ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩} ∪ {⟨( ·_𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨(𝑠‘(1^st ‘𝑓)), (𝑠 ∘ (2^nd ‘𝑓))⟩)⟩})))

Colors of variables: wff setvar class

This definition is referenced by: dvhfset 39939

W3C validator