Step |
Hyp |
Ref |
Expression |
1 |
|
isgrp.b |
|- B = ( Base ` G ) |
2 |
|
isgrp.p |
|- .+ = ( +g ` G ) |
3 |
|
isgrp.z |
|- .0. = ( 0g ` G ) |
4 |
|
fveq2 |
|- ( g = G -> ( Base ` g ) = ( Base ` G ) ) |
5 |
4 1
|
eqtr4di |
|- ( g = G -> ( Base ` g ) = B ) |
6 |
|
fveq2 |
|- ( g = G -> ( +g ` g ) = ( +g ` G ) ) |
7 |
6 2
|
eqtr4di |
|- ( g = G -> ( +g ` g ) = .+ ) |
8 |
7
|
oveqd |
|- ( g = G -> ( m ( +g ` g ) a ) = ( m .+ a ) ) |
9 |
|
fveq2 |
|- ( g = G -> ( 0g ` g ) = ( 0g ` G ) ) |
10 |
9 3
|
eqtr4di |
|- ( g = G -> ( 0g ` g ) = .0. ) |
11 |
8 10
|
eqeq12d |
|- ( g = G -> ( ( m ( +g ` g ) a ) = ( 0g ` g ) <-> ( m .+ a ) = .0. ) ) |
12 |
5 11
|
rexeqbidv |
|- ( g = G -> ( E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g ) <-> E. m e. B ( m .+ a ) = .0. ) ) |
13 |
5 12
|
raleqbidv |
|- ( g = G -> ( A. a e. ( Base ` g ) E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g ) <-> A. a e. B E. m e. B ( m .+ a ) = .0. ) ) |
14 |
|
df-grp |
|- Grp = { g e. Mnd | A. a e. ( Base ` g ) E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g ) } |
15 |
13 14
|
elrab2 |
|- ( G e. Grp <-> ( G e. Mnd /\ A. a e. B E. m e. B ( m .+ a ) = .0. ) ) |