Step |
Hyp |
Ref |
Expression |
1 |
|
grpinveu.b |
|- B = ( Base ` G ) |
2 |
|
grpinveu.p |
|- .+ = ( +g ` G ) |
3 |
|
grpinveu.o |
|- .0. = ( 0g ` G ) |
4 |
1 2 3
|
grpid |
|- ( ( G e. Grp /\ Z e. B ) -> ( ( Z .+ Z ) = Z <-> .0. = Z ) ) |
5 |
4
|
biimpd |
|- ( ( G e. Grp /\ Z e. B ) -> ( ( Z .+ Z ) = Z -> .0. = Z ) ) |
6 |
5
|
expimpd |
|- ( G e. Grp -> ( ( Z e. B /\ ( Z .+ Z ) = Z ) -> .0. = Z ) ) |
7 |
1 3
|
grpidcl |
|- ( G e. Grp -> .0. e. B ) |
8 |
1 2 3
|
grplid |
|- ( ( G e. Grp /\ .0. e. B ) -> ( .0. .+ .0. ) = .0. ) |
9 |
7 8
|
mpdan |
|- ( G e. Grp -> ( .0. .+ .0. ) = .0. ) |
10 |
7 9
|
jca |
|- ( G e. Grp -> ( .0. e. B /\ ( .0. .+ .0. ) = .0. ) ) |
11 |
|
eleq1 |
|- ( .0. = Z -> ( .0. e. B <-> Z e. B ) ) |
12 |
|
id |
|- ( .0. = Z -> .0. = Z ) |
13 |
12 12
|
oveq12d |
|- ( .0. = Z -> ( .0. .+ .0. ) = ( Z .+ Z ) ) |
14 |
13 12
|
eqeq12d |
|- ( .0. = Z -> ( ( .0. .+ .0. ) = .0. <-> ( Z .+ Z ) = Z ) ) |
15 |
11 14
|
anbi12d |
|- ( .0. = Z -> ( ( .0. e. B /\ ( .0. .+ .0. ) = .0. ) <-> ( Z e. B /\ ( Z .+ Z ) = Z ) ) ) |
16 |
10 15
|
syl5ibcom |
|- ( G e. Grp -> ( .0. = Z -> ( Z e. B /\ ( Z .+ Z ) = Z ) ) ) |
17 |
6 16
|
impbid |
|- ( G e. Grp -> ( ( Z e. B /\ ( Z .+ Z ) = Z ) <-> .0. = Z ) ) |