Theorem grpss

Description: Show that a structure extending a constructed group (e.g., a ring) is also a group. This allows us 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	⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ }
	grpss.r	⊢ 𝑅 ∈ V
	grpss.s	⊢ 𝐺 ⊆ 𝑅
	grpss.f	⊢ Fun 𝑅
Assertion	grpss	⊢ ( 𝐺 ∈ Grp ↔ 𝑅 ∈ Grp )

Proof

Step	Hyp	Ref	Expression
1		grpss.g	⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ }
2		grpss.r	⊢ 𝑅 ∈ V
3		grpss.s	⊢ 𝐺 ⊆ 𝑅
4		grpss.f	⊢ Fun 𝑅
5		baseid	⊢ Base = Slot ( Base ‘ ndx )
6		opex	⊢ ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ ∈ V
7	6	prid1	⊢ ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ ∈ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ }
8	7 1	eleqtrri	⊢ ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ ∈ 𝐺
9	2 4 3 5 8	strss	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝐺 )
10		plusgid	⊢ +g = Slot ( +g ‘ ndx )
11		opex	⊢ ⟨ ( +g ‘ ndx ) , + ⟩ ∈ V
12	11	prid2	⊢ ⟨ ( +g ‘ ndx ) , + ⟩ ∈ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ }
13	12 1	eleqtrri	⊢ ⟨ ( +g ‘ ndx ) , + ⟩ ∈ 𝐺
14	2 4 3 10 13	strss	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝐺 )
15	9 14	grpprop	⊢ ( 𝑅 ∈ Grp ↔ 𝐺 ∈ Grp )
16	15	bicomi	⊢ ( 𝐺 ∈ Grp ↔ 𝑅 ∈ Grp )