Step |
Hyp |
Ref |
Expression |
1 |
|
grpidd.b |
|- ( ph -> B = ( Base ` G ) ) |
2 |
|
grpidd.p |
|- ( ph -> .+ = ( +g ` G ) ) |
3 |
|
grpidd.z |
|- ( ph -> .0. e. B ) |
4 |
|
grpidd.i |
|- ( ( ph /\ x e. B ) -> ( .0. .+ x ) = x ) |
5 |
|
grpidd.j |
|- ( ( ph /\ x e. B ) -> ( x .+ .0. ) = x ) |
6 |
|
eqid |
|- ( Base ` G ) = ( Base ` G ) |
7 |
|
eqid |
|- ( 0g ` G ) = ( 0g ` G ) |
8 |
|
eqid |
|- ( +g ` G ) = ( +g ` G ) |
9 |
3 1
|
eleqtrd |
|- ( ph -> .0. e. ( Base ` G ) ) |
10 |
1
|
eleq2d |
|- ( ph -> ( x e. B <-> x e. ( Base ` G ) ) ) |
11 |
10
|
biimpar |
|- ( ( ph /\ x e. ( Base ` G ) ) -> x e. B ) |
12 |
2
|
adantr |
|- ( ( ph /\ x e. B ) -> .+ = ( +g ` G ) ) |
13 |
12
|
oveqd |
|- ( ( ph /\ x e. B ) -> ( .0. .+ x ) = ( .0. ( +g ` G ) x ) ) |
14 |
13 4
|
eqtr3d |
|- ( ( ph /\ x e. B ) -> ( .0. ( +g ` G ) x ) = x ) |
15 |
11 14
|
syldan |
|- ( ( ph /\ x e. ( Base ` G ) ) -> ( .0. ( +g ` G ) x ) = x ) |
16 |
12
|
oveqd |
|- ( ( ph /\ x e. B ) -> ( x .+ .0. ) = ( x ( +g ` G ) .0. ) ) |
17 |
16 5
|
eqtr3d |
|- ( ( ph /\ x e. B ) -> ( x ( +g ` G ) .0. ) = x ) |
18 |
11 17
|
syldan |
|- ( ( ph /\ x e. ( Base ` G ) ) -> ( x ( +g ` G ) .0. ) = x ) |
19 |
6 7 8 9 15 18
|
ismgmid2 |
|- ( ph -> .0. = ( 0g ` G ) ) |