Metamath Proof Explorer


Theorem submacs

Description: Submonoids are an algebraic closure system. (Contributed by Stefan O'Rear, 22-Aug-2015)

Ref Expression
Hypothesis submacs.b B = Base G
Assertion submacs G Mnd SubMnd G ACS B

Proof

Step Hyp Ref Expression
1 submacs.b B = Base G
2 eqid 0 G = 0 G
3 eqid + G = + G
4 1 2 3 issubm G Mnd s SubMnd G s B 0 G s x s y s x + G y s
5 velpw s 𝒫 B s B
6 5 anbi1i s 𝒫 B 0 G s x s y s x + G y s s B 0 G s x s y s x + G y s
7 3anass s B 0 G s x s y s x + G y s s B 0 G s x s y s x + G y s
8 6 7 bitr4i s 𝒫 B 0 G s x s y s x + G y s s B 0 G s x s y s x + G y s
9 4 8 bitr4di G Mnd s SubMnd G s 𝒫 B 0 G s x s y s x + G y s
10 9 abbi2dv G Mnd SubMnd G = s | s 𝒫 B 0 G s x s y s x + G y s
11 df-rab s 𝒫 B | 0 G s x s y s x + G y s = s | s 𝒫 B 0 G s x s y s x + G y s
12 10 11 eqtr4di G Mnd SubMnd G = s 𝒫 B | 0 G s x s y s x + G y s
13 inrab s 𝒫 B | 0 G s s 𝒫 B | x s y s x + G y s = s 𝒫 B | 0 G s x s y s x + G y s
14 1 fvexi B V
15 mreacs B V ACS B Moore 𝒫 B
16 14 15 mp1i G Mnd ACS B Moore 𝒫 B
17 1 2 mndidcl G Mnd 0 G B
18 acsfn0 B V 0 G B s 𝒫 B | 0 G s ACS B
19 14 17 18 sylancr G Mnd s 𝒫 B | 0 G s ACS B
20 1 3 mndcl G Mnd x B y B x + G y B
21 20 3expb G Mnd x B y B x + G y B
22 21 ralrimivva G Mnd x B y B x + G y B
23 acsfn2 B V x B y B x + G y B s 𝒫 B | x s y s x + G y s ACS B
24 14 22 23 sylancr G Mnd s 𝒫 B | x s y s x + G y s ACS B
25 mreincl ACS B Moore 𝒫 B s 𝒫 B | 0 G s ACS B s 𝒫 B | x s y s x + G y s ACS B s 𝒫 B | 0 G s s 𝒫 B | x s y s x + G y s ACS B
26 16 19 24 25 syl3anc G Mnd s 𝒫 B | 0 G s s 𝒫 B | x s y s x + G y s ACS B
27 13 26 eqeltrrid G Mnd s 𝒫 B | 0 G s x s y s x + G y s ACS B
28 12 27 eqeltrd G Mnd SubMnd G ACS B