| Step |
Hyp |
Ref |
Expression |
| 1 |
|
cnlmod.w |
|- W = ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. } u. { <. ( Scalar ` ndx ) , CCfld >. , <. ( .s ` ndx ) , x. >. } ) |
| 2 |
1
|
cnlmod |
|- W e. LMod |
| 3 |
|
cnfldex |
|- CCfld e. _V |
| 4 |
|
cnfldbas |
|- CC = ( Base ` CCfld ) |
| 5 |
4
|
ressid |
|- ( CCfld e. _V -> ( CCfld |`s CC ) = CCfld ) |
| 6 |
3 5
|
ax-mp |
|- ( CCfld |`s CC ) = CCfld |
| 7 |
6
|
eqcomi |
|- CCfld = ( CCfld |`s CC ) |
| 8 |
|
id |
|- ( x e. CC -> x e. CC ) |
| 9 |
|
addcl |
|- ( ( x e. CC /\ y e. CC ) -> ( x + y ) e. CC ) |
| 10 |
|
negcl |
|- ( x e. CC -> -u x e. CC ) |
| 11 |
|
ax-1cn |
|- 1 e. CC |
| 12 |
|
mulcl |
|- ( ( x e. CC /\ y e. CC ) -> ( x x. y ) e. CC ) |
| 13 |
8 9 10 11 12
|
cnsubrglem |
|- CC e. ( SubRing ` CCfld ) |
| 14 |
|
qdass |
|- ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. } u. { <. ( Scalar ` ndx ) , CCfld >. , <. ( .s ` ndx ) , x. >. } ) = ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( Scalar ` ndx ) , CCfld >. } u. { <. ( .s ` ndx ) , x. >. } ) |
| 15 |
1 14
|
eqtri |
|- W = ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( Scalar ` ndx ) , CCfld >. } u. { <. ( .s ` ndx ) , x. >. } ) |
| 16 |
15
|
lmodsca |
|- ( CCfld e. _V -> CCfld = ( Scalar ` W ) ) |
| 17 |
3 16
|
ax-mp |
|- CCfld = ( Scalar ` W ) |
| 18 |
17
|
isclmi |
|- ( ( W e. LMod /\ CCfld = ( CCfld |`s CC ) /\ CC e. ( SubRing ` CCfld ) ) -> W e. CMod ) |
| 19 |
2 7 13 18
|
mp3an |
|- W e. CMod |
| 20 |
|
cndrng |
|- CCfld e. DivRing |
| 21 |
17
|
islvec |
|- ( W e. LVec <-> ( W e. LMod /\ CCfld e. DivRing ) ) |
| 22 |
2 20 21
|
mpbir2an |
|- W e. LVec |
| 23 |
19 22
|
elini |
|- W e. ( CMod i^i LVec ) |
| 24 |
|
df-cvs |
|- CVec = ( CMod i^i LVec ) |
| 25 |
23 24
|
eleqtrri |
|- W e. CVec |