Metamath Proof Explorer

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 syl6bbr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → ( ( 𝐺 ↾s 𝑆 ) ∈ Grp ↔ ( 𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑆 ) ∈ Grp ) ) )
9 1 issubg ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑆 ) ∈ Grp ) )
10 8 9 syl6bbr ⊢ ( ( ( 𝐺 ∈ 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 ) )