Metamath Proof Explorer


Theorem lsmsubm

Description: The sum of two commuting submonoids is a submonoid. (Contributed by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses lsmsubg.p ˙=LSSumG
lsmsubg.z Z=CntzG
Assertion lsmsubm TSubMndGUSubMndGTZUT˙USubMndG

Proof

Step Hyp Ref Expression
1 lsmsubg.p ˙=LSSumG
2 lsmsubg.z Z=CntzG
3 submrcl TSubMndGGMnd
4 3 3ad2ant1 TSubMndGUSubMndGTZUGMnd
5 eqid BaseG=BaseG
6 5 submss TSubMndGTBaseG
7 6 3ad2ant1 TSubMndGUSubMndGTZUTBaseG
8 5 submss USubMndGUBaseG
9 8 3ad2ant2 TSubMndGUSubMndGTZUUBaseG
10 5 1 lsmssv GMndTBaseGUBaseGT˙UBaseG
11 4 7 9 10 syl3anc TSubMndGUSubMndGTZUT˙UBaseG
12 simp2 TSubMndGUSubMndGTZUUSubMndG
13 5 1 lsmub1x TBaseGUSubMndGTT˙U
14 7 12 13 syl2anc TSubMndGUSubMndGTZUTT˙U
15 eqid 0G=0G
16 15 subm0cl TSubMndG0GT
17 16 3ad2ant1 TSubMndGUSubMndGTZU0GT
18 14 17 sseldd TSubMndGUSubMndGTZU0GT˙U
19 eqid +G=+G
20 5 19 1 lsmelvalx GMndTBaseGUBaseGxT˙UaTcUx=a+Gc
21 4 7 9 20 syl3anc TSubMndGUSubMndGTZUxT˙UaTcUx=a+Gc
22 5 19 1 lsmelvalx GMndTBaseGUBaseGyT˙UbTdUy=b+Gd
23 4 7 9 22 syl3anc TSubMndGUSubMndGTZUyT˙UbTdUy=b+Gd
24 21 23 anbi12d TSubMndGUSubMndGTZUxT˙UyT˙UaTcUx=a+GcbTdUy=b+Gd
25 reeanv aTbTcUx=a+GcdUy=b+GdaTcUx=a+GcbTdUy=b+Gd
26 reeanv cUdUx=a+Gcy=b+GdcUx=a+GcdUy=b+Gd
27 4 adantr TSubMndGUSubMndGTZUaTbTcUdUGMnd
28 7 adantr TSubMndGUSubMndGTZUaTbTcUdUTBaseG
29 simprll TSubMndGUSubMndGTZUaTbTcUdUaT
30 28 29 sseldd TSubMndGUSubMndGTZUaTbTcUdUaBaseG
31 simprlr TSubMndGUSubMndGTZUaTbTcUdUbT
32 28 31 sseldd TSubMndGUSubMndGTZUaTbTcUdUbBaseG
33 9 adantr TSubMndGUSubMndGTZUaTbTcUdUUBaseG
34 simprrl TSubMndGUSubMndGTZUaTbTcUdUcU
35 33 34 sseldd TSubMndGUSubMndGTZUaTbTcUdUcBaseG
36 simprrr TSubMndGUSubMndGTZUaTbTcUdUdU
37 33 36 sseldd TSubMndGUSubMndGTZUaTbTcUdUdBaseG
38 simpl3 TSubMndGUSubMndGTZUaTbTcUdUTZU
39 38 31 sseldd TSubMndGUSubMndGTZUaTbTcUdUbZU
40 19 2 cntzi bZUcUb+Gc=c+Gb
41 39 34 40 syl2anc TSubMndGUSubMndGTZUaTbTcUdUb+Gc=c+Gb
42 5 19 27 30 32 35 37 41 mnd4g TSubMndGUSubMndGTZUaTbTcUdUa+Gb+Gc+Gd=a+Gc+Gb+Gd
43 simpl1 TSubMndGUSubMndGTZUaTbTcUdUTSubMndG
44 19 submcl TSubMndGaTbTa+GbT
45 43 29 31 44 syl3anc TSubMndGUSubMndGTZUaTbTcUdUa+GbT
46 simpl2 TSubMndGUSubMndGTZUaTbTcUdUUSubMndG
47 19 submcl USubMndGcUdUc+GdU
48 46 34 36 47 syl3anc TSubMndGUSubMndGTZUaTbTcUdUc+GdU
49 5 19 1 lsmelvalix GMndTBaseGUBaseGa+GbTc+GdUa+Gb+Gc+GdT˙U
50 27 28 33 45 48 49 syl32anc TSubMndGUSubMndGTZUaTbTcUdUa+Gb+Gc+GdT˙U
51 42 50 eqeltrrd TSubMndGUSubMndGTZUaTbTcUdUa+Gc+Gb+GdT˙U
52 oveq12 x=a+Gcy=b+Gdx+Gy=a+Gc+Gb+Gd
53 52 eleq1d x=a+Gcy=b+Gdx+GyT˙Ua+Gc+Gb+GdT˙U
54 51 53 syl5ibrcom TSubMndGUSubMndGTZUaTbTcUdUx=a+Gcy=b+Gdx+GyT˙U
55 54 anassrs TSubMndGUSubMndGTZUaTbTcUdUx=a+Gcy=b+Gdx+GyT˙U
56 55 rexlimdvva TSubMndGUSubMndGTZUaTbTcUdUx=a+Gcy=b+Gdx+GyT˙U
57 26 56 syl5bir TSubMndGUSubMndGTZUaTbTcUx=a+GcdUy=b+Gdx+GyT˙U
58 57 rexlimdvva TSubMndGUSubMndGTZUaTbTcUx=a+GcdUy=b+Gdx+GyT˙U
59 25 58 syl5bir TSubMndGUSubMndGTZUaTcUx=a+GcbTdUy=b+Gdx+GyT˙U
60 24 59 sylbid TSubMndGUSubMndGTZUxT˙UyT˙Ux+GyT˙U
61 60 ralrimivv TSubMndGUSubMndGTZUxT˙UyT˙Ux+GyT˙U
62 5 15 19 issubm GMndT˙USubMndGT˙UBaseG0GT˙UxT˙UyT˙Ux+GyT˙U
63 4 62 syl TSubMndGUSubMndGTZUT˙USubMndGT˙UBaseG0GT˙UxT˙UyT˙Ux+GyT˙U
64 11 18 61 63 mpbir3and TSubMndGUSubMndGTZUT˙USubMndG