Step |
Hyp |
Ref |
Expression |
1 |
|
vsfval.2 |
|- G = ( +v ` U ) |
2 |
|
vsfval.3 |
|- M = ( -v ` U ) |
3 |
|
df-vs |
|- -v = ( /g o. +v ) |
4 |
3
|
fveq1i |
|- ( -v ` U ) = ( ( /g o. +v ) ` U ) |
5 |
|
fo1st |
|- 1st : _V -onto-> _V |
6 |
|
fof |
|- ( 1st : _V -onto-> _V -> 1st : _V --> _V ) |
7 |
5 6
|
ax-mp |
|- 1st : _V --> _V |
8 |
|
fco |
|- ( ( 1st : _V --> _V /\ 1st : _V --> _V ) -> ( 1st o. 1st ) : _V --> _V ) |
9 |
7 7 8
|
mp2an |
|- ( 1st o. 1st ) : _V --> _V |
10 |
|
df-va |
|- +v = ( 1st o. 1st ) |
11 |
10
|
feq1i |
|- ( +v : _V --> _V <-> ( 1st o. 1st ) : _V --> _V ) |
12 |
9 11
|
mpbir |
|- +v : _V --> _V |
13 |
|
fvco3 |
|- ( ( +v : _V --> _V /\ U e. _V ) -> ( ( /g o. +v ) ` U ) = ( /g ` ( +v ` U ) ) ) |
14 |
12 13
|
mpan |
|- ( U e. _V -> ( ( /g o. +v ) ` U ) = ( /g ` ( +v ` U ) ) ) |
15 |
4 14
|
syl5eq |
|- ( U e. _V -> ( -v ` U ) = ( /g ` ( +v ` U ) ) ) |
16 |
|
0ngrp |
|- -. (/) e. GrpOp |
17 |
|
vex |
|- g e. _V |
18 |
17
|
rnex |
|- ran g e. _V |
19 |
18 18
|
mpoex |
|- ( x e. ran g , y e. ran g |-> ( x g ( ( inv ` g ) ` y ) ) ) e. _V |
20 |
|
df-gdiv |
|- /g = ( g e. GrpOp |-> ( x e. ran g , y e. ran g |-> ( x g ( ( inv ` g ) ` y ) ) ) ) |
21 |
19 20
|
dmmpti |
|- dom /g = GrpOp |
22 |
21
|
eleq2i |
|- ( (/) e. dom /g <-> (/) e. GrpOp ) |
23 |
16 22
|
mtbir |
|- -. (/) e. dom /g |
24 |
|
ndmfv |
|- ( -. (/) e. dom /g -> ( /g ` (/) ) = (/) ) |
25 |
23 24
|
mp1i |
|- ( -. U e. _V -> ( /g ` (/) ) = (/) ) |
26 |
|
fvprc |
|- ( -. U e. _V -> ( +v ` U ) = (/) ) |
27 |
26
|
fveq2d |
|- ( -. U e. _V -> ( /g ` ( +v ` U ) ) = ( /g ` (/) ) ) |
28 |
|
fvprc |
|- ( -. U e. _V -> ( -v ` U ) = (/) ) |
29 |
25 27 28
|
3eqtr4rd |
|- ( -. U e. _V -> ( -v ` U ) = ( /g ` ( +v ` U ) ) ) |
30 |
15 29
|
pm2.61i |
|- ( -v ` U ) = ( /g ` ( +v ` U ) ) |
31 |
1
|
fveq2i |
|- ( /g ` G ) = ( /g ` ( +v ` U ) ) |
32 |
30 2 31
|
3eqtr4i |
|- M = ( /g ` G ) |