| Step |
Hyp |
Ref |
Expression |
| 1 |
|
zlmbas.w |
|- W = ( ZMod ` G ) |
| 2 |
|
zlmvsca.2 |
|- .x. = ( .g ` G ) |
| 3 |
|
ovex |
|- ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) e. _V |
| 4 |
2
|
fvexi |
|- .x. e. _V |
| 5 |
|
vscaid |
|- .s = Slot ( .s ` ndx ) |
| 6 |
5
|
setsid |
|- ( ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) e. _V /\ .x. e. _V ) -> .x. = ( .s ` ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , .x. >. ) ) ) |
| 7 |
3 4 6
|
mp2an |
|- .x. = ( .s ` ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , .x. >. ) ) |
| 8 |
1 2
|
zlmval |
|- ( G e. _V -> W = ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , .x. >. ) ) |
| 9 |
8
|
fveq2d |
|- ( G e. _V -> ( .s ` W ) = ( .s ` ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , .x. >. ) ) ) |
| 10 |
7 9
|
eqtr4id |
|- ( G e. _V -> .x. = ( .s ` W ) ) |
| 11 |
5
|
str0 |
|- (/) = ( .s ` (/) ) |
| 12 |
|
fvprc |
|- ( -. G e. _V -> ( .g ` G ) = (/) ) |
| 13 |
2 12
|
eqtrid |
|- ( -. G e. _V -> .x. = (/) ) |
| 14 |
|
fvprc |
|- ( -. G e. _V -> ( ZMod ` G ) = (/) ) |
| 15 |
1 14
|
eqtrid |
|- ( -. G e. _V -> W = (/) ) |
| 16 |
15
|
fveq2d |
|- ( -. G e. _V -> ( .s ` W ) = ( .s ` (/) ) ) |
| 17 |
11 13 16
|
3eqtr4a |
|- ( -. G e. _V -> .x. = ( .s ` W ) ) |
| 18 |
10 17
|
pm2.61i |
|- .x. = ( .s ` W ) |