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 ) ) >. } ) ) )