Metamath Proof Explorer

Definition df-dveca

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

Ref Expression
Assertion 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 ) ) >. } ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdveca 
 |-  DVecA
1 vk 
 |-  k
2 cvv 
 |-  _V
3 vw 
 |-  w
4 clh 
 |-  LHyp
5 1 cv 
 |-  k
6 5 4 cfv 
 |-  ( LHyp ` k )
7 cbs 
 |-  Base
8 cnx 
 |-  ndx
9 8 7 cfv 
 |-  ( Base ` ndx )
10 cltrn 
 |-  LTrn
11 5 10 cfv 
 |-  ( LTrn ` k )
12 3 cv 
 |-  w
13 12 11 cfv 
 |-  ( ( LTrn ` k ) ` w )
14 9 13 cop 
 |-  <. ( Base ` ndx ) , ( ( LTrn ` k ) ` w ) >.
15 cplusg 
 |-  +g
16 8 15 cfv 
 |-  ( +g ` ndx )
17 vf 
 |-  f
18 vg 
 |-  g
19 17 cv 
 |-  f
20 18 cv 
 |-  g
21 19 20 ccom 
 |-  ( f o. g )
22 17 18 13 13 21 cmpo 
 |-  ( f e. ( ( LTrn ` k ) ` w ) , g e. ( ( LTrn ` k ) ` w ) |-> ( f o. g ) )
23 16 22 cop 
 |-  <. ( +g ` ndx ) , ( f e. ( ( LTrn ` k ) ` w ) , g e. ( ( LTrn ` k ) ` w ) |-> ( f o. g ) ) >.
24 csca 
 |-  Scalar
25 8 24 cfv 
 |-  ( Scalar ` ndx )
26 cedring 
 |-  EDRing
27 5 26 cfv 
 |-  ( EDRing ` k )
28 12 27 cfv 
 |-  ( ( EDRing ` k ) ` w )
29 25 28 cop 
 |-  <. ( Scalar ` ndx ) , ( ( EDRing ` k ) ` w ) >.
30 14 23 29 ctp 
 |-  { <. ( 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 ) >. }
31 cvsca 
 |-  .s
32 8 31 cfv 
 |-  ( .s ` ndx )
33 vs 
 |-  s
34 ctendo 
 |-  TEndo
35 5 34 cfv 
 |-  ( TEndo ` k )
36 12 35 cfv 
 |-  ( ( TEndo ` k ) ` w )
37 33 cv 
 |-  s
38 19 37 cfv 
 |-  ( s ` f )
39 33 17 36 13 38 cmpo 
 |-  ( s e. ( ( TEndo ` k ) ` w ) , f e. ( ( LTrn ` k ) ` w ) |-> ( s ` f ) )
40 32 39 cop 
 |-  <. ( .s ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , f e. ( ( LTrn ` k ) ` w ) |-> ( s ` f ) ) >.
41 40 csn 
 |-  { <. ( .s ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , f e. ( ( LTrn ` k ) ` w ) |-> ( s ` f ) ) >. }
42 30 41 cun 
 |-  ( { <. ( 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 ) ) >. } )
43 3 6 42 cmpt 
 |-  ( 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 ) ) >. } ) )
44 1 2 43 cmpt 
 |-  ( 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 ) ) >. } ) ) )
45 0 44 wceq 
 |-  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 ) ) >. } ) ) )