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 B = Base G
grpissubg.s S = Base H
Assertion resgrpisgrp G Grp H Grp S B + H = + G S × S G 𝑠 S Grp

Proof

Step Hyp Ref Expression
1 grpissubg.b B = Base G
2 grpissubg.s S = Base H
3 1 2 grpissubg G Grp H Grp S B + H = + G S × S S SubGrp G
4 3 imp G Grp H Grp S B + H = + G S × S S SubGrp G
5 ibar G Grp S B G 𝑠 S Grp G Grp S B G 𝑠 S Grp
6 5 ad2ant2r G Grp H Grp S B + H = + G S × S G 𝑠 S Grp G Grp S B G 𝑠 S Grp
7 df-3an G Grp S B G 𝑠 S Grp G Grp S B G 𝑠 S Grp
8 6 7 bitr4di G Grp H Grp S B + H = + G S × S G 𝑠 S Grp G Grp S B G 𝑠 S Grp
9 1 issubg S SubGrp G G Grp S B G 𝑠 S Grp
10 8 9 bitr4di G Grp H Grp S B + H = + G S × S G 𝑠 S Grp S SubGrp G
11 4 10 mpbird G Grp H Grp S B + H = + G S × S G 𝑠 S Grp
12 11 ex G Grp H Grp S B + H = + G S × S G 𝑠 S Grp