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 Unicode version

Definition df-dvech 36368

Description: Define constructed full vector space H. (Contributed by NM, 17-Oct-2013.)

**Assertion**
Ref	Expression
df-dvech	Scalar

Distinct variable group:

**Detailed syntax breakdown of Definition df-dvech**
Step	Hyp	Ref	Expression
1		cdvh 36367	. 2
2		vk	. . 3
3		cvv 3200	. . 3
4		vw	. . . 4
5	2	cv 1482	. . . . 5
6		clh 35270	. . . . 5
7	5, 6	cfv 5888	. . . 4
8		cnx 15854	. . . . . . . 8
9		cbs 15857	. . . . . . . 8
10	8, 9	cfv 5888	. . . . . . 7
11	4	cv 1482	. . . . . . . . 9
12		cltrn 35387	. . . . . . . . . 10
13	5, 12	cfv 5888	. . . . . . . . 9
14	11, 13	cfv 5888	. . . . . . . 8
15		ctendo 36040	. . . . . . . . . 10
16	5, 15	cfv 5888	. . . . . . . . 9
17	11, 16	cfv 5888	. . . . . . . 8
18	14, 17	cxp 5112	. . . . . . 7
19	10, 18	cop 4183	. . . . . 6
20		cplusg 15941	. . . . . . . 8
21	8, 20	cfv 5888	. . . . . . 7
22		vf	. . . . . . . 8
23		vg	. . . . . . . 8
24	22	cv 1482	. . . . . . . . . . 11
25		c1st 7166	. . . . . . . . . . 11
26	24, 25	cfv 5888	. . . . . . . . . 10
27	23	cv 1482	. . . . . . . . . . 11
28	27, 25	cfv 5888	. . . . . . . . . 10
29	26, 28	ccom 5118	. . . . . . . . 9
30		vh	. . . . . . . . . 10
31	30	cv 1482	. . . . . . . . . . . 12
32		c2nd 7167	. . . . . . . . . . . . 13
33	24, 32	cfv 5888	. . . . . . . . . . . 12
34	31, 33	cfv 5888	. . . . . . . . . . 11
35	27, 32	cfv 5888	. . . . . . . . . . . 12
36	31, 35	cfv 5888	. . . . . . . . . . 11
37	34, 36	ccom 5118	. . . . . . . . . 10
38	30, 14, 37	cmpt 4729	. . . . . . . . 9
39	29, 38	cop 4183	. . . . . . . 8
40	22, 23, 18, 18, 39	cmpt2 6652	. . . . . . 7
41	21, 40	cop 4183	. . . . . 6
42		csca 15944	. . . . . . . 8 Scalar
43	8, 42	cfv 5888	. . . . . . 7 Scalar
44		cedring 36041	. . . . . . . . 9
45	5, 44	cfv 5888	. . . . . . . 8
46	11, 45	cfv 5888	. . . . . . 7
47	43, 46	cop 4183	. . . . . 6 Scalar
48	19, 41, 47	ctp 4181	. . . . 5 Scalar
49		cvsca 15945	. . . . . . . 8
50	8, 49	cfv 5888	. . . . . . 7
51		vs	. . . . . . . 8
52	51	cv 1482	. . . . . . . . . 10
53	26, 52	cfv 5888	. . . . . . . . 9
54	52, 33	ccom 5118	. . . . . . . . 9
55	53, 54	cop 4183	. . . . . . . 8
56	51, 22, 17, 18, 55	cmpt2 6652	. . . . . . 7
57	50, 56	cop 4183	. . . . . 6
58	57	csn 4177	. . . . 5
59	48, 58	cun 3572	. . . 4 Scalar
60	4, 7, 59	cmpt 4729	. . 3 Scalar
61	2, 3, 60	cmpt 4729	. 2 Scalar
62	1, 61	wceq 1483	1 Scalar

Colors of variables: wff setvar class

This definition is referenced by: dvhfset 36369

W3C validator