This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqabdv ⊢ ( 𝐺 ∈ 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 ‘ 𝐵 ) )