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=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩\right\}$$
	grpss.r	$$⊢R\in \mathrm{V}$$
	grpss.s	$$⊢G\subseteq R$$
	grpss.f	$$⊢\mathrm{Fun}R$$
Assertion	grpss	$$⊢G\in \mathrm{Grp}\leftrightarrow R\in \mathrm{Grp}$$

Proof

Step	Hyp	Ref	Expression
1		grpss.g	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩\right\}$$
2		grpss.r	$$⊢R\in \mathrm{V}$$
3		grpss.s	$$⊢G\subseteq R$$
4		grpss.f	$$⊢\mathrm{Fun}R$$
5		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
6		opex	$$⊢⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩\in \mathrm{V}$$
7	6	prid1	$$⊢⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩\in \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩\right\}$$
8	7 1	eleqtrri	$$⊢⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩\in G$$
9	2 4 3 5 8	strss	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_G$$
10		plusgid	$$⊢{+}_{𝑔}=\mathrm{Slot}{+}_{\mathrm{ndx}}$$
11		opex	$$⊢⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩\in \mathrm{V}$$
12	11	prid2	$$⊢⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩\in \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩\right\}$$
13	12 1	eleqtrri	$$⊢⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩\in G$$
14	2 4 3 10 13	strss	$$⊢{+}_R={+}_G$$
15	9 14	grpprop	$$⊢R\in \mathrm{Grp}\leftrightarrow G\in \mathrm{Grp}$$
16	15	bicomi	$$⊢G\in \mathrm{Grp}\leftrightarrow R\in \mathrm{Grp}$$