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 𝐵 = ( Base ‘ 𝐺 )
Assertion submacs ( 𝐺 ∈ Mnd → ( SubMnd ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 submacs.b 𝐵 = ( Base ‘ 𝐺 )
2 eqid ( 0g𝐺 ) = ( 0g𝐺 )
3 eqid ( +g𝐺 ) = ( +g𝐺 )
4 1 2 3 issubm ( 𝐺 ∈ Mnd → ( 𝑠 ∈ ( SubMnd ‘ 𝐺 ) ↔ ( 𝑠𝐵 ∧ ( 0g𝐺 ) ∈ 𝑠 ∧ ∀ 𝑥𝑠𝑦𝑠 ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝑠 ) ) )
5 velpw ( 𝑠 ∈ 𝒫 𝐵𝑠𝐵 )
6 5 anbi1i ( ( 𝑠 ∈ 𝒫 𝐵 ∧ ( ( 0g𝐺 ) ∈ 𝑠 ∧ ∀ 𝑥𝑠𝑦𝑠 ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝑠 ) ) ↔ ( 𝑠𝐵 ∧ ( ( 0g𝐺 ) ∈ 𝑠 ∧ ∀ 𝑥𝑠𝑦𝑠 ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝑠 ) ) )
7 3anass ( ( 𝑠𝐵 ∧ ( 0g𝐺 ) ∈ 𝑠 ∧ ∀ 𝑥𝑠𝑦𝑠 ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝑠 ) ↔ ( 𝑠𝐵 ∧ ( ( 0g𝐺 ) ∈ 𝑠 ∧ ∀ 𝑥𝑠𝑦𝑠 ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝑠 ) ) )
8 6 7 bitr4i ( ( 𝑠 ∈ 𝒫 𝐵 ∧ ( ( 0g𝐺 ) ∈ 𝑠 ∧ ∀ 𝑥𝑠𝑦𝑠 ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝑠 ) ) ↔ ( 𝑠𝐵 ∧ ( 0g𝐺 ) ∈ 𝑠 ∧ ∀ 𝑥𝑠𝑦𝑠 ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝑠 ) )
9 4 8 bitr4di ( 𝐺 ∈ Mnd → ( 𝑠 ∈ ( SubMnd ‘ 𝐺 ) ↔ ( 𝑠 ∈ 𝒫 𝐵 ∧ ( ( 0g𝐺 ) ∈ 𝑠 ∧ ∀ 𝑥𝑠𝑦𝑠 ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝑠 ) ) ) )
10 9 abbi2dv ( 𝐺 ∈ Mnd → ( SubMnd ‘ 𝐺 ) = { 𝑠 ∣ ( 𝑠 ∈ 𝒫 𝐵 ∧ ( ( 0g𝐺 ) ∈ 𝑠 ∧ ∀ 𝑥𝑠𝑦𝑠 ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝑠 ) ) } )
11 df-rab { 𝑠 ∈ 𝒫 𝐵 ∣ ( ( 0g𝐺 ) ∈ 𝑠 ∧ ∀ 𝑥𝑠𝑦𝑠 ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝑠 ) } = { 𝑠 ∣ ( 𝑠 ∈ 𝒫 𝐵 ∧ ( ( 0g𝐺 ) ∈ 𝑠 ∧ ∀ 𝑥𝑠𝑦𝑠 ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝑠 ) ) }
12 10 11 eqtr4di ( 𝐺 ∈ Mnd → ( SubMnd ‘ 𝐺 ) = { 𝑠 ∈ 𝒫 𝐵 ∣ ( ( 0g𝐺 ) ∈ 𝑠 ∧ ∀ 𝑥𝑠𝑦𝑠 ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝑠 ) } )
13 inrab ( { 𝑠 ∈ 𝒫 𝐵 ∣ ( 0g𝐺 ) ∈ 𝑠 } ∩ { 𝑠 ∈ 𝒫 𝐵 ∣ ∀ 𝑥𝑠𝑦𝑠 ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝑠 } ) = { 𝑠 ∈ 𝒫 𝐵 ∣ ( ( 0g𝐺 ) ∈ 𝑠 ∧ ∀ 𝑥𝑠𝑦𝑠 ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝑠 ) }
14 1 fvexi 𝐵 ∈ V
15 mreacs ( 𝐵 ∈ V → ( ACS ‘ 𝐵 ) ∈ ( Moore ‘ 𝒫 𝐵 ) )
16 14 15 mp1i ( 𝐺 ∈ Mnd → ( ACS ‘ 𝐵 ) ∈ ( Moore ‘ 𝒫 𝐵 ) )
17 1 2 mndidcl ( 𝐺 ∈ Mnd → ( 0g𝐺 ) ∈ 𝐵 )
18 acsfn0 ( ( 𝐵 ∈ V ∧ ( 0g𝐺 ) ∈ 𝐵 ) → { 𝑠 ∈ 𝒫 𝐵 ∣ ( 0g𝐺 ) ∈ 𝑠 } ∈ ( ACS ‘ 𝐵 ) )
19 14 17 18 sylancr ( 𝐺 ∈ Mnd → { 𝑠 ∈ 𝒫 𝐵 ∣ ( 0g𝐺 ) ∈ 𝑠 } ∈ ( ACS ‘ 𝐵 ) )
20 1 3 mndcl ( ( 𝐺 ∈ Mnd ∧ 𝑥𝐵𝑦𝐵 ) → ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝐵 )
21 20 3expb ( ( 𝐺 ∈ Mnd ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝐵 )
22 21 ralrimivva ( 𝐺 ∈ Mnd → ∀ 𝑥𝐵𝑦𝐵 ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝐵 )
23 acsfn2 ( ( 𝐵 ∈ V ∧ ∀ 𝑥𝐵𝑦𝐵 ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝐵 ) → { 𝑠 ∈ 𝒫 𝐵 ∣ ∀ 𝑥𝑠𝑦𝑠 ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝑠 } ∈ ( ACS ‘ 𝐵 ) )
24 14 22 23 sylancr ( 𝐺 ∈ Mnd → { 𝑠 ∈ 𝒫 𝐵 ∣ ∀ 𝑥𝑠𝑦𝑠 ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝑠 } ∈ ( ACS ‘ 𝐵 ) )
25 mreincl ( ( ( ACS ‘ 𝐵 ) ∈ ( Moore ‘ 𝒫 𝐵 ) ∧ { 𝑠 ∈ 𝒫 𝐵 ∣ ( 0g𝐺 ) ∈ 𝑠 } ∈ ( ACS ‘ 𝐵 ) ∧ { 𝑠 ∈ 𝒫 𝐵 ∣ ∀ 𝑥𝑠𝑦𝑠 ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝑠 } ∈ ( ACS ‘ 𝐵 ) ) → ( { 𝑠 ∈ 𝒫 𝐵 ∣ ( 0g𝐺 ) ∈ 𝑠 } ∩ { 𝑠 ∈ 𝒫 𝐵 ∣ ∀ 𝑥𝑠𝑦𝑠 ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝑠 } ) ∈ ( ACS ‘ 𝐵 ) )
26 16 19 24 25 syl3anc ( 𝐺 ∈ Mnd → ( { 𝑠 ∈ 𝒫 𝐵 ∣ ( 0g𝐺 ) ∈ 𝑠 } ∩ { 𝑠 ∈ 𝒫 𝐵 ∣ ∀ 𝑥𝑠𝑦𝑠 ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝑠 } ) ∈ ( ACS ‘ 𝐵 ) )
27 13 26 eqeltrrid ( 𝐺 ∈ Mnd → { 𝑠 ∈ 𝒫 𝐵 ∣ ( ( 0g𝐺 ) ∈ 𝑠 ∧ ∀ 𝑥𝑠𝑦𝑠 ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝑠 ) } ∈ ( ACS ‘ 𝐵 ) )
28 12 27 eqeltrd ( 𝐺 ∈ Mnd → ( SubMnd ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) )