df-dvech

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

		Ref	Expression
	Assertion	df-dvech	$⊢ DVecH = (k \in V ⟼ (w \in LHyp (k) ⟼ \{⟨{Base}_{ndx}, LTrn (k) (w) \times TEndo (k) (w)⟩, ⟨+_{ndx}, (f \in (LTrn (k) (w) \times TEndo (k) (w)), g \in (LTrn (k) (w) \times TEndo (k) (w)) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), (h \in LTrn (k) (w) ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))⟩)⟩, ⟨Scalar (ndx), EDRing (k) (w)⟩\} \cup \{⟨\cdot_{ndx}, (s \in TEndo (k) (w), f \in (LTrn (k) (w) \times TEndo (k) (w)) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)⟩\}))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdvh	$class DVecH$
1		vk	$setvar k$
2		cvv	$class V$
3		vw	$setvar w$
4		clh	$class LHyp$
5	1	cv	$setvar k$
6	5 4	cfv	$class LHyp (k)$
7		cbs	$class Base$
8		cnx	$class ndx$
9	8 7	cfv	$class {Base}_{ndx}$
10		cltrn	$class LTrn$
11	5 10	cfv	$class LTrn (k)$
12	3	cv	$setvar w$
13	12 11	cfv	$class LTrn (k) (w)$
14		ctendo	$class TEndo$
15	5 14	cfv	$class TEndo (k)$
16	12 15	cfv	$class TEndo (k) (w)$
17	13 16	cxp	$class (LTrn (k) (w) \times TEndo (k) (w))$
18	9 17	cop	$class ⟨{Base}_{ndx}, LTrn (k) (w) \times TEndo (k) (w)⟩$
19		cplusg	$class +_{𝑔}$
20	8 19	cfv	$class +_{ndx}$
21		vf	$setvar f$
22		vg	$setvar g$
23		c1st	$class 1^{st}$
24	21	cv	$setvar f$
25	24 23	cfv	$class 1^{st} (f)$
26	22	cv	$setvar g$
27	26 23	cfv	$class 1^{st} (g)$
28	25 27	ccom	$class (1^{st} (f) \circ 1^{st} (g))$
29		vh	$setvar h$
30		c2nd	$class 2^{nd}$
31	24 30	cfv	$class 2^{nd} (f)$
32	29	cv	$setvar h$
33	32 31	cfv	$class 2^{nd} (f) (h)$
34	26 30	cfv	$class 2^{nd} (g)$
35	32 34	cfv	$class 2^{nd} (g) (h)$
36	33 35	ccom	$class (2^{nd} (f) (h) \circ 2^{nd} (g) (h))$
37	29 13 36	cmpt	$class (h \in LTrn (k) (w) ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))$
38	28 37	cop	$class ⟨1^{st} (f) \circ 1^{st} (g), (h \in LTrn (k) (w) ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))⟩$
39	21 22 17 17 38	cmpo	$class (f \in (LTrn (k) (w) \times TEndo (k) (w)), g \in (LTrn (k) (w) \times TEndo (k) (w)) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), (h \in LTrn (k) (w) ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))⟩)$
40	20 39	cop	$class ⟨+_{ndx}, (f \in (LTrn (k) (w) \times TEndo (k) (w)), g \in (LTrn (k) (w) \times TEndo (k) (w)) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), (h \in LTrn (k) (w) ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))⟩)⟩$
41		csca	$class Scalar$
42	8 41	cfv	$class Scalar (ndx)$
43		cedring	$class EDRing$
44	5 43	cfv	$class EDRing (k)$
45	12 44	cfv	$class EDRing (k) (w)$
46	42 45	cop	$class ⟨Scalar (ndx), EDRing (k) (w)⟩$
47	18 40 46	ctp	$class \{⟨{Base}_{ndx}, LTrn (k) (w) \times TEndo (k) (w)⟩, ⟨+_{ndx}, (f \in (LTrn (k) (w) \times TEndo (k) (w)), g \in (LTrn (k) (w) \times TEndo (k) (w)) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), (h \in LTrn (k) (w) ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))⟩)⟩, ⟨Scalar (ndx), EDRing (k) (w)⟩\}$
48		cvsca	$class \cdot_{𝑠}$
49	8 48	cfv	$class \cdot_{ndx}$
50		vs	$setvar s$
51	50	cv	$setvar s$
52	25 51	cfv	$class s (1^{st} (f))$
53	51 31	ccom	$class (s \circ 2^{nd} (f))$
54	52 53	cop	$class ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩$
55	50 21 16 17 54	cmpo	$class (s \in TEndo (k) (w), f \in (LTrn (k) (w) \times TEndo (k) (w)) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)$
56	49 55	cop	$class ⟨\cdot_{ndx}, (s \in TEndo (k) (w), f \in (LTrn (k) (w) \times TEndo (k) (w)) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)⟩$
57	56	csn	$class \{⟨\cdot_{ndx}, (s \in TEndo (k) (w), f \in (LTrn (k) (w) \times TEndo (k) (w)) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)⟩\}$
58	47 57	cun	$class (\{⟨{Base}_{ndx}, LTrn (k) (w) \times TEndo (k) (w)⟩, ⟨+_{ndx}, (f \in (LTrn (k) (w) \times TEndo (k) (w)), g \in (LTrn (k) (w) \times TEndo (k) (w)) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), (h \in LTrn (k) (w) ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))⟩)⟩, ⟨Scalar (ndx), EDRing (k) (w)⟩\} \cup \{⟨\cdot_{ndx}, (s \in TEndo (k) (w), f \in (LTrn (k) (w) \times TEndo (k) (w)) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)⟩\})$
59	3 6 58	cmpt	$class (w \in LHyp (k) ⟼ \{⟨{Base}_{ndx}, LTrn (k) (w) \times TEndo (k) (w)⟩, ⟨+_{ndx}, (f \in (LTrn (k) (w) \times TEndo (k) (w)), g \in (LTrn (k) (w) \times TEndo (k) (w)) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), (h \in LTrn (k) (w) ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))⟩)⟩, ⟨Scalar (ndx), EDRing (k) (w)⟩\} \cup \{⟨\cdot_{ndx}, (s \in TEndo (k) (w), f \in (LTrn (k) (w) \times TEndo (k) (w)) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)⟩\})$
60	1 2 59	cmpt	$class (k \in V ⟼ (w \in LHyp (k) ⟼ \{⟨{Base}_{ndx}, LTrn (k) (w) \times TEndo (k) (w)⟩, ⟨+_{ndx}, (f \in (LTrn (k) (w) \times TEndo (k) (w)), g \in (LTrn (k) (w) \times TEndo (k) (w)) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), (h \in LTrn (k) (w) ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))⟩)⟩, ⟨Scalar (ndx), EDRing (k) (w)⟩\} \cup \{⟨\cdot_{ndx}, (s \in TEndo (k) (w), f \in (LTrn (k) (w) \times TEndo (k) (w)) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)⟩\}))$
61	0 60	wceq	$wff DVecH = (k \in V ⟼ (w \in LHyp (k) ⟼ \{⟨{Base}_{ndx}, LTrn (k) (w) \times TEndo (k) (w)⟩, ⟨+_{ndx}, (f \in (LTrn (k) (w) \times TEndo (k) (w)), g \in (LTrn (k) (w) \times TEndo (k) (w)) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), (h \in LTrn (k) (w) ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))⟩)⟩, ⟨Scalar (ndx), EDRing (k) (w)⟩\} \cup \{⟨\cdot_{ndx}, (s \in TEndo (k) (w), f \in (LTrn (k) (w) \times TEndo (k) (w)) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)⟩\}))$

Metamath Proof Explorer

Definition df-dvech

Detailed syntax breakdown