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 )