Metamath Proof Explorer


Theorem grpissubg

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 (base set of the) group is subgroup of the other group. (Contributed by AV, 14-Mar-2019)

Ref Expression
Hypotheses grpissubg.b B = Base G
grpissubg.s S = Base H
Assertion grpissubg G Grp H Grp S B + H = + G S × S S SubGrp G

Proof

Step Hyp Ref Expression
1 grpissubg.b B = Base G
2 grpissubg.s S = Base H
3 simpl S B + H = + G S × S S B
4 3 adantl G Grp H Grp S B + H = + G S × S S B
5 2 grpbn0 H Grp S
6 5 ad2antlr G Grp H Grp S B + H = + G S × S S
7 grpmnd G Grp G Mnd
8 mndmgm G Mnd G Mgm
9 7 8 syl G Grp G Mgm
10 grpmnd H Grp H Mnd
11 mndmgm H Mnd H Mgm
12 10 11 syl H Grp H Mgm
13 9 12 anim12i G Grp H Grp G Mgm H Mgm
14 13 adantr G Grp H Grp S B + H = + G S × S G Mgm H Mgm
15 14 ad2antrr G Grp H Grp S B + H = + G S × S a S b S G Mgm H Mgm
16 simpr G Grp H Grp S B + H = + G S × S S B + H = + G S × S
17 16 ad2antrr G Grp H Grp S B + H = + G S × S a S b S S B + H = + G S × S
18 simpr G Grp H Grp S B + H = + G S × S a S a S
19 18 anim1i G Grp H Grp S B + H = + G S × S a S b S a S b S
20 1 2 mgmsscl G Mgm H Mgm S B + H = + G S × S a S b S a + G b S
21 15 17 19 20 syl3anc G Grp H Grp S B + H = + G S × S a S b S a + G b S
22 21 ralrimiva G Grp H Grp S B + H = + G S × S a S b S a + G b S
23 simpl G Grp H Grp G Grp
24 23 adantr G Grp H Grp S B + H = + G S × S G Grp
25 simplr G Grp H Grp S B + H = + G S × S H Grp
26 1 sseq2i S B S Base G
27 26 biimpi S B S Base G
28 27 adantr S B + H = + G S × S S Base G
29 28 adantl G Grp H Grp S B + H = + G S × S S Base G
30 ovres x S y S x + G S × S y = x + G y
31 30 adantl G Grp H Grp S B + H = + G S × S x S y S x + G S × S y = x + G y
32 oveq + H = + G S × S x + H y = x + G S × S y
33 32 adantl S B + H = + G S × S x + H y = x + G S × S y
34 33 eqcomd S B + H = + G S × S x + G S × S y = x + H y
35 34 ad2antlr G Grp H Grp S B + H = + G S × S x S y S x + G S × S y = x + H y
36 31 35 eqtr3d G Grp H Grp S B + H = + G S × S x S y S x + G y = x + H y
37 36 ralrimivva G Grp H Grp S B + H = + G S × S x S y S x + G y = x + H y
38 24 25 2 29 37 grpinvssd G Grp H Grp S B + H = + G S × S a S inv g H a = inv g G a
39 38 imp G Grp H Grp S B + H = + G S × S a S inv g H a = inv g G a
40 eqid inv g H = inv g H
41 2 40 grpinvcl H Grp a S inv g H a S
42 41 ad4ant24 G Grp H Grp S B + H = + G S × S a S inv g H a S
43 39 42 eqeltrrd G Grp H Grp S B + H = + G S × S a S inv g G a S
44 22 43 jca G Grp H Grp S B + H = + G S × S a S b S a + G b S inv g G a S
45 44 ralrimiva G Grp H Grp S B + H = + G S × S a S b S a + G b S inv g G a S
46 eqid + G = + G
47 eqid inv g G = inv g G
48 1 46 47 issubg2 G Grp S SubGrp G S B S a S b S a + G b S inv g G a S
49 48 ad2antrr G Grp H Grp S B + H = + G S × S S SubGrp G S B S a S b S a + G b S inv g G a S
50 4 6 45 49 mpbir3and G Grp H Grp S B + H = + G S × S S SubGrp G
51 50 ex G Grp H Grp S B + H = + G S × S S SubGrp G