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 ⊢ B = Base G
resgrpplusfrn.h ⊢ H = G ↾ 𝑠 S
resgrpplusfrn.o ⊢ F = + 𝑓 ⁡ H
Assertion resgrpplusfrn ⊢ H ∈ Grp ∧ S ⊆ B → S = ran ⁡ F

Proof

Step Hyp Ref Expression
1 resgrpplusfrn.b ⊢ B = Base G
2 resgrpplusfrn.h ⊢ H = G ↾ 𝑠 S
3 resgrpplusfrn.o ⊢ F = + 𝑓 ⁡ H
4 eqid ⊢ Base H = Base H
5 4 3 grpplusfo ⊢ H ∈ Grp → F : Base H × Base H ⟶ onto Base H
6 5 adantr ⊢ H ∈ Grp ∧ S ⊆ B → F : Base H × Base H ⟶ onto Base H
7 eqidd ⊢ H ∈ Grp ∧ S ⊆ B → F = F
8 2 1 ressbas2 ⊢ S ⊆ B → S = Base H
9 8 adantl ⊢ H ∈ Grp ∧ S ⊆ B → S = Base H
10 9 sqxpeqd ⊢ H ∈ Grp ∧ S ⊆ B → S × S = Base H × Base H
11 7 10 9 foeq123d ⊢ H ∈ Grp ∧ S ⊆ B → F : S × S ⟶ onto S ↔ F : Base H × Base H ⟶ onto Base H
12 6 11 mpbird ⊢ H ∈ Grp ∧ S ⊆ B → F : S × S ⟶ onto S
13 forn ⊢ F : S × S ⟶ onto S → ran ⁡ F = S
14 13 eqcomd ⊢ F : S × S ⟶ onto S → S = ran ⁡ F
15 12 14 syl ⊢ H ∈ Grp ∧ S ⊆ B → S = ran ⁡ F