Theorem grpss

Description: Show that a structure extending a constructed group (e.g., a ring) is also a group. This allows to prove that a constructed potential ring R is a group before we know that it is also a ring. (Theorem ringgrp , on the other hand, requires that we know in advance that R is a ring.) (Contributed by NM, 11-Oct-2013)

	Ref	Expression
Hypotheses	grpss.g	|- G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. }
	grpss.r	|- R e. _V
	grpss.s	|- G C_ R
	grpss.f	|- Fun R
Assertion	grpss	|- ( G e. Grp <-> R e. Grp )

Proof

Step	Hyp	Ref	Expression
1		grpss.g	|- G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. }
2		grpss.r	|- R e. _V
3		grpss.s	|- G C_ R
4		grpss.f	|- Fun R
5		baseid	|- Base = Slot ( Base ` ndx )
6		opex	|- <. ( Base ` ndx ) , B >. e. _V
7	6	prid1	|- <. ( Base ` ndx ) , B >. e. { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. }
8	7 1	eleqtrri	|- <. ( Base ` ndx ) , B >. e. G
9	2 4 3 5 8	strss	|- ( Base ` R ) = ( Base ` G )
10		plusgid	|- +g = Slot ( +g ` ndx )
11		opex	|- <. ( +g ` ndx ) , .+ >. e. _V
12	11	prid2	|- <. ( +g ` ndx ) , .+ >. e. { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. }
13	12 1	eleqtrri	|- <. ( +g ` ndx ) , .+ >. e. G
14	2 4 3 10 13	strss	|- ( +g ` R ) = ( +g ` G )
15	9 14	grpprop	|- ( R e. Grp <-> G e. Grp )
16	15	bicomi	|- ( G e. Grp <-> R e. Grp )