This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐹 )