Metamath Proof Explorer


Theorem grppropstr

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 )

Proof

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 )