Step |
Hyp |
Ref |
Expression |
1 |
|
mulgfvi.t |
|- .x. = ( .g ` G ) |
2 |
|
fvi |
|- ( G e. _V -> ( _I ` G ) = G ) |
3 |
2
|
eqcomd |
|- ( G e. _V -> G = ( _I ` G ) ) |
4 |
3
|
fveq2d |
|- ( G e. _V -> ( .g ` G ) = ( .g ` ( _I ` G ) ) ) |
5 |
|
fvprc |
|- ( -. G e. _V -> ( .g ` G ) = (/) ) |
6 |
|
fvprc |
|- ( -. G e. _V -> ( _I ` G ) = (/) ) |
7 |
6
|
fveq2d |
|- ( -. G e. _V -> ( .g ` ( _I ` G ) ) = ( .g ` (/) ) ) |
8 |
|
base0 |
|- (/) = ( Base ` (/) ) |
9 |
|
eqid |
|- ( .g ` (/) ) = ( .g ` (/) ) |
10 |
8 9
|
mulgfn |
|- ( .g ` (/) ) Fn ( ZZ X. (/) ) |
11 |
|
xp0 |
|- ( ZZ X. (/) ) = (/) |
12 |
11
|
fneq2i |
|- ( ( .g ` (/) ) Fn ( ZZ X. (/) ) <-> ( .g ` (/) ) Fn (/) ) |
13 |
10 12
|
mpbi |
|- ( .g ` (/) ) Fn (/) |
14 |
|
fn0 |
|- ( ( .g ` (/) ) Fn (/) <-> ( .g ` (/) ) = (/) ) |
15 |
13 14
|
mpbi |
|- ( .g ` (/) ) = (/) |
16 |
7 15
|
eqtrdi |
|- ( -. G e. _V -> ( .g ` ( _I ` G ) ) = (/) ) |
17 |
5 16
|
eqtr4d |
|- ( -. G e. _V -> ( .g ` G ) = ( .g ` ( _I ` G ) ) ) |
18 |
4 17
|
pm2.61i |
|- ( .g ` G ) = ( .g ` ( _I ` G ) ) |
19 |
1 18
|
eqtri |
|- .x. = ( .g ` ( _I ` G ) ) |