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

Proof

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

Metamath Proof Explorer

Theorem grpss

Proof