Definition df-dveca 36291

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

Assertion

Ref	Expression
df-dveca	|- DVecA = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( { <. ( Base ` ndx ) , ( ( LTrn ` k ) ` w ) >. , <. ( +g ` ndx ) , ( f e. ( ( LTrn ` k ) ` w ) , g e. ( ( LTrn ` k ) ` w ) |-> ( f o. g ) ) >. , <. (Scalar ` ndx ) , ( ( EDRing ` k ) ` w ) >. } u. { <. ( .s ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , f e. ( ( LTrn ` k ) ` w ) |-> ( s ` f ) ) >. } ) ) )

Distinct variable group:   w, k, s, f, g

Detailed syntax breakdown of Definition df-dveca

Step	Hyp	Ref	Expression
1		cdveca 36290	. 2 class DVecA
2		vk	. . 3 setvar k
3		cvv 3200	. . 3 class _V
4		vw	. . . 4 setvar w
5	2	cv 1482	. . . . 5 class k
6		clh 35270	. . . . 5 class LHyp
7	5, 6	cfv 5888	. . . 4 class ( LHyp ` k )
8		cnx 15854	. . . . . . . 8 class ndx
9		cbs 15857	. . . . . . . 8 class Base
10	8, 9	cfv 5888	. . . . . . 7 class ( Base ` ndx )
11	4	cv 1482	. . . . . . . 8 class w
12		cltrn 35387	. . . . . . . . 9 class LTrn
13	5, 12	cfv 5888	. . . . . . . 8 class ( LTrn ` k )
14	11, 13	cfv 5888	. . . . . . 7 class ( ( LTrn ` k ) ` w )
15	10, 14	cop 4183	. . . . . 6 class <. ( Base ` ndx ) , ( ( LTrn ` k ) ` w ) >.
16		cplusg 15941	. . . . . . . 8 class +g
17	8, 16	cfv 5888	. . . . . . 7 class ( +g ` ndx )
18		vf	. . . . . . . 8 setvar f
19		vg	. . . . . . . 8 setvar g
20	18	cv 1482	. . . . . . . . 9 class f
21	19	cv 1482	. . . . . . . . 9 class g
22	20, 21	ccom 5118	. . . . . . . 8 class ( f o. g )
23	18, 19, 14, 14, 22	cmpt2 6652	. . . . . . 7 class ( f e. ( ( LTrn ` k ) ` w ) , g e. ( ( LTrn ` k ) ` w ) |-> ( f o. g ) )
24	17, 23	cop 4183	. . . . . 6 class <. ( +g ` ndx ) , ( f e. ( ( LTrn ` k ) ` w ) , g e. ( ( LTrn ` k ) ` w ) |-> ( f o. g ) ) >.
25		csca 15944	. . . . . . . 8 class Scalar
26	8, 25	cfv 5888	. . . . . . 7 class (Scalar ` ndx )
27		cedring 36041	. . . . . . . . 9 class EDRing
28	5, 27	cfv 5888	. . . . . . . 8 class ( EDRing ` k )
29	11, 28	cfv 5888	. . . . . . 7 class ( ( EDRing ` k ) ` w )
30	26, 29	cop 4183	. . . . . 6 class <. (Scalar ` ndx ) , ( ( EDRing ` k ) ` w ) >.
31	15, 24, 30	ctp 4181	. . . . 5 class { <. ( Base ` ndx ) , ( ( LTrn ` k ) ` w ) >. , <. ( +g ` ndx ) , ( f e. ( ( LTrn ` k ) ` w ) , g e. ( ( LTrn ` k ) ` w ) |-> ( f o. g ) ) >. , <. (Scalar ` ndx ) , ( ( EDRing ` k ) ` w ) >. }
32		cvsca 15945	. . . . . . . 8 class .s
33	8, 32	cfv 5888	. . . . . . 7 class ( .s ` ndx )
34		vs	. . . . . . . 8 setvar s
35		ctendo 36040	. . . . . . . . . 10 class TEndo
36	5, 35	cfv 5888	. . . . . . . . 9 class ( TEndo ` k )
37	11, 36	cfv 5888	. . . . . . . 8 class ( ( TEndo ` k ) ` w )
38	34	cv 1482	. . . . . . . . 9 class s
39	20, 38	cfv 5888	. . . . . . . 8 class ( s ` f )
40	34, 18, 37, 14, 39	cmpt2 6652	. . . . . . 7 class ( s e. ( ( TEndo ` k ) ` w ) , f e. ( ( LTrn ` k ) ` w ) |-> ( s ` f ) )
41	33, 40	cop 4183	. . . . . 6 class <. ( .s ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , f e. ( ( LTrn ` k ) ` w ) |-> ( s ` f ) ) >.
42	41	csn 4177	. . . . 5 class { <. ( .s ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , f e. ( ( LTrn ` k ) ` w ) |-> ( s ` f ) ) >. }
43	31, 42	cun 3572	. . . 4 class ( { <. ( Base ` ndx ) , ( ( LTrn ` k ) ` w ) >. , <. ( +g ` ndx ) , ( f e. ( ( LTrn ` k ) ` w ) , g e. ( ( LTrn ` k ) ` w ) |-> ( f o. g ) ) >. , <. (Scalar ` ndx ) , ( ( EDRing ` k ) ` w ) >. } u. { <. ( .s ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , f e. ( ( LTrn ` k ) ` w ) |-> ( s ` f ) ) >. } )
44	4, 7, 43	cmpt 4729	. . 3 class ( w e. ( LHyp ` k ) |-> ( { <. ( Base ` ndx ) , ( ( LTrn ` k ) ` w ) >. , <. ( +g ` ndx ) , ( f e. ( ( LTrn ` k ) ` w ) , g e. ( ( LTrn ` k ) ` w ) |-> ( f o. g ) ) >. , <. (Scalar ` ndx ) , ( ( EDRing ` k ) ` w ) >. } u. { <. ( .s ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , f e. ( ( LTrn ` k ) ` w ) |-> ( s ` f ) ) >. } ) )
45	2, 3, 44	cmpt 4729	. 2 class ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( { <. ( Base ` ndx ) , ( ( LTrn ` k ) ` w ) >. , <. ( +g ` ndx ) , ( f e. ( ( LTrn ` k ) ` w ) , g e. ( ( LTrn ` k ) ` w ) |-> ( f o. g ) ) >. , <. (Scalar ` ndx ) , ( ( EDRing ` k ) ` w ) >. } u. { <. ( .s ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , f e. ( ( LTrn ` k ) ` w ) |-> ( s ` f ) ) >. } ) ) )
46	1, 45	wceq 1483	1 wff DVecA = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( { <. ( Base ` ndx ) , ( ( LTrn ` k ) ` w ) >. , <. ( +g ` ndx ) , ( f e. ( ( LTrn ` k ) ` w ) , g e. ( ( LTrn ` k ) ` w ) |-> ( f o. g ) ) >. , <. (Scalar ` ndx ) , ( ( EDRing ` k ) ` w ) >. } u. { <. ( .s ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , f e. ( ( LTrn ` k ) ` w ) |-> ( s ` f ) ) >. } ) ) )

This definition is referenced by:  dvafset  36292