Description: Generalize a specific 2-element group L to show that any set K with the same (relevant) properties is also a group. (Contributed by NM, 28-Oct-2012) (Revised by Mario Carneiro, 6-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | grppropstr.b | |- ( Base ` K ) = B |
|
grppropstr.p | |- ( +g ` K ) = .+ |
||
grppropstr.l | |- L = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. } |
||
Assertion | grppropstr | |- ( K e. Grp <-> L e. Grp ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | grppropstr.b | |- ( Base ` K ) = B |
|
2 | grppropstr.p | |- ( +g ` K ) = .+ |
|
3 | grppropstr.l | |- L = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. } |
|
4 | fvex | |- ( Base ` K ) e. _V |
|
5 | 1 4 | eqeltrri | |- B e. _V |
6 | 3 | grpbase | |- ( B e. _V -> B = ( Base ` L ) ) |
7 | 5 6 | ax-mp | |- B = ( Base ` L ) |
8 | 1 7 | eqtri | |- ( Base ` K ) = ( Base ` L ) |
9 | fvex | |- ( +g ` K ) e. _V |
|
10 | 2 9 | eqeltrri | |- .+ e. _V |
11 | 3 | grpplusg | |- ( .+ e. _V -> .+ = ( +g ` L ) ) |
12 | 10 11 | ax-mp | |- .+ = ( +g ` L ) |
13 | 2 12 | eqtri | |- ( +g ` K ) = ( +g ` L ) |
14 | 8 13 | grpprop | |- ( K e. Grp <-> L e. Grp ) |