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 )

Metamath Proof Explorer

Theorem grpss

Proof