Theorem resgrpisgrp

Description: If the base set of a group is contained in the base set of another group, and the group operation of the group is the restriction of the group operation of the other group to its base set, then the other group restricted to the base set of the group is a group. (Contributed by AV, 14-Mar-2019)

	Ref	Expression
Hypotheses	grpissubg.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	grpissubg.s	⊢ 𝑆 = ( Base ‘ 𝐻 )
Assertion	resgrpisgrp	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) → ( ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) → ( 𝐺 ↾s 𝑆 ) ∈ Grp ) )

Proof

Step	Hyp	Ref	Expression
1		grpissubg.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		grpissubg.s	⊢ 𝑆 = ( Base ‘ 𝐻 )
3	1 2	grpissubg	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) → ( ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) )
4	3	imp	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
5		ibar	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) → ( ( 𝐺 ↾s 𝑆 ) ∈ Grp ↔ ( ( 𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝐺 ↾s 𝑆 ) ∈ Grp ) ) )
6	5	ad2ant2r	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → ( ( 𝐺 ↾s 𝑆 ) ∈ Grp ↔ ( ( 𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝐺 ↾s 𝑆 ) ∈ Grp ) ) )
7		df-3an	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑆 ) ∈ Grp ) ↔ ( ( 𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝐺 ↾s 𝑆 ) ∈ Grp ) )
8	6 7	bitr4di	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → ( ( 𝐺 ↾s 𝑆 ) ∈ Grp ↔ ( 𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑆 ) ∈ Grp ) ) )
9	1	issubg	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑆 ) ∈ Grp ) )
10	8 9	bitr4di	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → ( ( 𝐺 ↾s 𝑆 ) ∈ Grp ↔ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) )
11	4 10	mpbird	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → ( 𝐺 ↾s 𝑆 ) ∈ Grp )
12	11	ex	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) → ( ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) → ( 𝐺 ↾s 𝑆 ) ∈ Grp ) )