Metamath Proof Explorer


Theorem submmulg

Description: A group multiple is the same if evaluated in a submonoid. (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Hypotheses submmulgcl.t ˙=G
submmulg.h H=G𝑠S
submmulg.t ·˙=H
Assertion submmulg SSubMndGN0XSN˙X=N·˙X

Proof

Step Hyp Ref Expression
1 submmulgcl.t ˙=G
2 submmulg.h H=G𝑠S
3 submmulg.t ·˙=H
4 simpl1 SSubMndGN0XSNSSubMndG
5 eqid +G=+G
6 2 5 ressplusg SSubMndG+G=+H
7 4 6 syl SSubMndGN0XSN+G=+H
8 7 seqeq2d SSubMndGN0XSNseq1+G×X=seq1+H×X
9 8 fveq1d SSubMndGN0XSNseq1+G×XN=seq1+H×XN
10 simpr SSubMndGN0XSNN
11 eqid BaseG=BaseG
12 11 submss SSubMndGSBaseG
13 12 3ad2ant1 SSubMndGN0XSSBaseG
14 simp3 SSubMndGN0XSXS
15 13 14 sseldd SSubMndGN0XSXBaseG
16 15 adantr SSubMndGN0XSNXBaseG
17 eqid seq1+G×X=seq1+G×X
18 11 5 1 17 mulgnn NXBaseGN˙X=seq1+G×XN
19 10 16 18 syl2anc SSubMndGN0XSNN˙X=seq1+G×XN
20 2 submbas SSubMndGS=BaseH
21 20 3ad2ant1 SSubMndGN0XSS=BaseH
22 14 21 eleqtrd SSubMndGN0XSXBaseH
23 22 adantr SSubMndGN0XSNXBaseH
24 eqid BaseH=BaseH
25 eqid +H=+H
26 eqid seq1+H×X=seq1+H×X
27 24 25 3 26 mulgnn NXBaseHN·˙X=seq1+H×XN
28 10 23 27 syl2anc SSubMndGN0XSNN·˙X=seq1+H×XN
29 9 19 28 3eqtr4d SSubMndGN0XSNN˙X=N·˙X
30 simpl1 SSubMndGN0XSN=0SSubMndG
31 eqid 0G=0G
32 2 31 subm0 SSubMndG0G=0H
33 30 32 syl SSubMndGN0XSN=00G=0H
34 15 adantr SSubMndGN0XSN=0XBaseG
35 11 31 1 mulg0 XBaseG0˙X=0G
36 34 35 syl SSubMndGN0XSN=00˙X=0G
37 22 adantr SSubMndGN0XSN=0XBaseH
38 eqid 0H=0H
39 24 38 3 mulg0 XBaseH0·˙X=0H
40 37 39 syl SSubMndGN0XSN=00·˙X=0H
41 33 36 40 3eqtr4d SSubMndGN0XSN=00˙X=0·˙X
42 simpr SSubMndGN0XSN=0N=0
43 42 oveq1d SSubMndGN0XSN=0N˙X=0˙X
44 42 oveq1d SSubMndGN0XSN=0N·˙X=0·˙X
45 41 43 44 3eqtr4d SSubMndGN0XSN=0N˙X=N·˙X
46 simp2 SSubMndGN0XSN0
47 elnn0 N0NN=0
48 46 47 sylib SSubMndGN0XSNN=0
49 29 45 48 mpjaodan SSubMndGN0XSN˙X=N·˙X