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