df-dveca

Description: Define constructed partial vector space A. (Contributed by NM, 8-Oct-2013)

		Ref	Expression
	Assertion	df-dveca	$⊢ DVecA = (k \in V ⟼ (w \in LHyp (k) ⟼ \{⟨{Base}_{ndx}, LTrn (k) (w)⟩, ⟨+_{ndx}, (f \in LTrn (k) (w), g \in LTrn (k) (w) ⟼ f \circ g)⟩, ⟨Scalar (ndx), EDRing (k) (w)⟩\} \cup \{⟨\cdot_{ndx}, (s \in TEndo (k) (w), f \in LTrn (k) (w) ⟼ s (f))⟩\}))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdveca	$class DVecA$
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	9 13	cop	$class ⟨{Base}_{ndx}, LTrn (k) (w)⟩$
15		cplusg	$class +_{𝑔}$
16	8 15	cfv	$class +_{ndx}$
17		vf	$setvar f$
18		vg	$setvar g$
19	17	cv	$setvar f$
20	18	cv	$setvar g$
21	19 20	ccom	$class (f \circ g)$
22	17 18 13 13 21	cmpo	$class (f \in LTrn (k) (w), g \in LTrn (k) (w) ⟼ f \circ g)$
23	16 22	cop	$class ⟨+_{ndx}, (f \in LTrn (k) (w), g \in LTrn (k) (w) ⟼ f \circ g)⟩$
24		csca	$class Scalar$
25	8 24	cfv	$class Scalar (ndx)$
26		cedring	$class EDRing$
27	5 26	cfv	$class EDRing (k)$
28	12 27	cfv	$class EDRing (k) (w)$
29	25 28	cop	$class ⟨Scalar (ndx), EDRing (k) (w)⟩$
30	14 23 29	ctp	$class \{⟨{Base}_{ndx}, LTrn (k) (w)⟩, ⟨+_{ndx}, (f \in LTrn (k) (w), g \in LTrn (k) (w) ⟼ f \circ g)⟩, ⟨Scalar (ndx), EDRing (k) (w)⟩\}$
31		cvsca	$class \cdot_{𝑠}$
32	8 31	cfv	$class \cdot_{ndx}$
33		vs	$setvar s$
34		ctendo	$class TEndo$
35	5 34	cfv	$class TEndo (k)$
36	12 35	cfv	$class TEndo (k) (w)$
37	33	cv	$setvar s$
38	19 37	cfv	$class s (f)$
39	33 17 36 13 38	cmpo	$class (s \in TEndo (k) (w), f \in LTrn (k) (w) ⟼ s (f))$
40	32 39	cop	$class ⟨\cdot_{ndx}, (s \in TEndo (k) (w), f \in LTrn (k) (w) ⟼ s (f))⟩$
41	40	csn	$class \{⟨\cdot_{ndx}, (s \in TEndo (k) (w), f \in LTrn (k) (w) ⟼ s (f))⟩\}$
42	30 41	cun	$class (\{⟨{Base}_{ndx}, LTrn (k) (w)⟩, ⟨+_{ndx}, (f \in LTrn (k) (w), g \in LTrn (k) (w) ⟼ f \circ g)⟩, ⟨Scalar (ndx), EDRing (k) (w)⟩\} \cup \{⟨\cdot_{ndx}, (s \in TEndo (k) (w), f \in LTrn (k) (w) ⟼ s (f))⟩\})$
43	3 6 42	cmpt	$class (w \in LHyp (k) ⟼ \{⟨{Base}_{ndx}, LTrn (k) (w)⟩, ⟨+_{ndx}, (f \in LTrn (k) (w), g \in LTrn (k) (w) ⟼ f \circ g)⟩, ⟨Scalar (ndx), EDRing (k) (w)⟩\} \cup \{⟨\cdot_{ndx}, (s \in TEndo (k) (w), f \in LTrn (k) (w) ⟼ s (f))⟩\})$
44	1 2 43	cmpt	$class (k \in V ⟼ (w \in LHyp (k) ⟼ \{⟨{Base}_{ndx}, LTrn (k) (w)⟩, ⟨+_{ndx}, (f \in LTrn (k) (w), g \in LTrn (k) (w) ⟼ f \circ g)⟩, ⟨Scalar (ndx), EDRing (k) (w)⟩\} \cup \{⟨\cdot_{ndx}, (s \in TEndo (k) (w), f \in LTrn (k) (w) ⟼ s (f))⟩\}))$
45	0 44	wceq	$wff DVecA = (k \in V ⟼ (w \in LHyp (k) ⟼ \{⟨{Base}_{ndx}, LTrn (k) (w)⟩, ⟨+_{ndx}, (f \in LTrn (k) (w), g \in LTrn (k) (w) ⟼ f \circ g)⟩, ⟨Scalar (ndx), EDRing (k) (w)⟩\} \cup \{⟨\cdot_{ndx}, (s \in TEndo (k) (w), f \in LTrn (k) (w) ⟼ s (f))⟩\}))$

Metamath Proof Explorer

Definition df-dveca

Detailed syntax breakdown