Description: The sum of two commuting submonoids is a submonoid. (Contributed by Mario Carneiro, 19-Apr-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lsmsubg.p | |
|
lsmsubg.z | |
||
Assertion | lsmsubm | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lsmsubg.p | |
|
2 | lsmsubg.z | |
|
3 | submrcl | |
|
4 | 3 | 3ad2ant1 | |
5 | eqid | |
|
6 | 5 | submss | |
7 | 6 | 3ad2ant1 | |
8 | 5 | submss | |
9 | 8 | 3ad2ant2 | |
10 | 5 1 | lsmssv | |
11 | 4 7 9 10 | syl3anc | |
12 | simp2 | |
|
13 | 5 1 | lsmub1x | |
14 | 7 12 13 | syl2anc | |
15 | eqid | |
|
16 | 15 | subm0cl | |
17 | 16 | 3ad2ant1 | |
18 | 14 17 | sseldd | |
19 | eqid | |
|
20 | 5 19 1 | lsmelvalx | |
21 | 4 7 9 20 | syl3anc | |
22 | 5 19 1 | lsmelvalx | |
23 | 4 7 9 22 | syl3anc | |
24 | 21 23 | anbi12d | |
25 | reeanv | |
|
26 | reeanv | |
|
27 | 4 | adantr | |
28 | 7 | adantr | |
29 | simprll | |
|
30 | 28 29 | sseldd | |
31 | simprlr | |
|
32 | 28 31 | sseldd | |
33 | 9 | adantr | |
34 | simprrl | |
|
35 | 33 34 | sseldd | |
36 | simprrr | |
|
37 | 33 36 | sseldd | |
38 | simpl3 | |
|
39 | 38 31 | sseldd | |
40 | 19 2 | cntzi | |
41 | 39 34 40 | syl2anc | |
42 | 5 19 27 30 32 35 37 41 | mnd4g | |
43 | simpl1 | |
|
44 | 19 | submcl | |
45 | 43 29 31 44 | syl3anc | |
46 | simpl2 | |
|
47 | 19 | submcl | |
48 | 46 34 36 47 | syl3anc | |
49 | 5 19 1 | lsmelvalix | |
50 | 27 28 33 45 48 49 | syl32anc | |
51 | 42 50 | eqeltrrd | |
52 | oveq12 | |
|
53 | 52 | eleq1d | |
54 | 51 53 | syl5ibrcom | |
55 | 54 | anassrs | |
56 | 55 | rexlimdvva | |
57 | 26 56 | syl5bir | |
58 | 57 | rexlimdvva | |
59 | 25 58 | syl5bir | |
60 | 24 59 | sylbid | |
61 | 60 | ralrimivv | |
62 | 5 15 19 | issubm | |
63 | 4 62 | syl | |
64 | 11 18 61 63 | mpbir3and | |