Theorem resgrpplusfrn

Description: The underlying set of a group operation which is a restriction of a structure. (Contributed by Paul Chapman, 25-Mar-2008) (Revised by AV, 30-Aug-2021)

	Ref	Expression
Hypotheses	resgrpplusfrn.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	resgrpplusfrn.h	⊢ 𝐻 = ( 𝐺 ↾s 𝑆 )
	resgrpplusfrn.o	⊢ 𝐹 = ( +𝑓 ‘ 𝐻 )
Assertion	resgrpplusfrn	⊢ ( ( 𝐻 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) → 𝑆 = ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		resgrpplusfrn.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		resgrpplusfrn.h	⊢ 𝐻 = ( 𝐺 ↾s 𝑆 )
3		resgrpplusfrn.o	⊢ 𝐹 = ( +𝑓 ‘ 𝐻 )
4		eqid	⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
5	4 3	grpplusfo	⊢ ( 𝐻 ∈ Grp → 𝐹 : ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) –onto→ ( Base ‘ 𝐻 ) )
6	5	adantr	⊢ ( ( 𝐻 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) → 𝐹 : ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) –onto→ ( Base ‘ 𝐻 ) )
7		eqidd	⊢ ( ( 𝐻 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) → 𝐹 = 𝐹 )
8	2 1	ressbas2	⊢ ( 𝑆 ⊆ 𝐵 → 𝑆 = ( Base ‘ 𝐻 ) )
9	8	adantl	⊢ ( ( 𝐻 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) → 𝑆 = ( Base ‘ 𝐻 ) )
10	9	sqxpeqd	⊢ ( ( 𝐻 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑆 × 𝑆 ) = ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) )
11	7 10 9	foeq123d	⊢ ( ( 𝐻 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) → ( 𝐹 : ( 𝑆 × 𝑆 ) –onto→ 𝑆 ↔ 𝐹 : ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) –onto→ ( Base ‘ 𝐻 ) ) )
12	6 11	mpbird	⊢ ( ( 𝐻 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) → 𝐹 : ( 𝑆 × 𝑆 ) –onto→ 𝑆 )
13		forn	⊢ ( 𝐹 : ( 𝑆 × 𝑆 ) –onto→ 𝑆 → ran 𝐹 = 𝑆 )
14	13	eqcomd	⊢ ( 𝐹 : ( 𝑆 × 𝑆 ) –onto→ 𝑆 → 𝑆 = ran 𝐹 )
15	12 14	syl	⊢ ( ( 𝐻 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) → 𝑆 = ran 𝐹 )