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

Metamath Proof Explorer

Theorem submgmacs

Description: Submagmas are an algebraic closure system. (Contributed by AV, 27-Feb-2020)

Ref Expression
Hypothesis submgmacs.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion submgmacs ( 𝐺 ∈ Mgm → ( SubMgm ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 submgmacs.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
3 1 2 issubmgm ⊢ ( 𝐺 ∈ Mgm → ( 𝑠 ∈ ( SubMgm ‘ 𝐺 ) ↔ ( 𝑠 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑠 ) ) )
4 velpw ⊢ ( 𝑠 ∈ 𝒫 𝐵 ↔ 𝑠 ⊆ 𝐵 )
5 4 anbi1i ⊢ ( ( 𝑠 ∈ 𝒫 𝐵 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑠 ) ↔ ( 𝑠 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑠 ) )
6 3 5 bitr4di ⊢ ( 𝐺 ∈ Mgm → ( 𝑠 ∈ ( SubMgm ‘ 𝐺 ) ↔ ( 𝑠 ∈ 𝒫 𝐵 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑠 ) ) )
7 6 eqabdv ⊢ ( 𝐺 ∈ Mgm → ( SubMgm ‘ 𝐺 ) = { 𝑠 ∣ ( 𝑠 ∈ 𝒫 𝐵 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑠 ) } )
8 df-rab ⊢ { 𝑠 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑠 } = { 𝑠 ∣ ( 𝑠 ∈ 𝒫 𝐵 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑠 ) }
9 7 8 eqtr4di ⊢ ( 𝐺 ∈ Mgm → ( SubMgm ‘ 𝐺 ) = { 𝑠 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑠 } )
10 1 fvexi ⊢ 𝐵 ∈ V
11 1 2 mgmcl ⊢ ( ( 𝐺 ∈ Mgm ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐵 )
12 11 3expb ⊢ ( ( 𝐺 ∈ Mgm ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐵 )
13 12 ralrimivva ⊢ ( 𝐺 ∈ Mgm → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐵 )
14 acsfn2 ⊢ ( ( 𝐵 ∈ V ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐵 ) → { 𝑠 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑠 } ∈ ( ACS ‘ 𝐵 ) )
15 10 13 14 sylancr ⊢ ( 𝐺 ∈ Mgm → { 𝑠 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑠 } ∈ ( ACS ‘ 𝐵 ) )
16 9 15 eqeltrd ⊢ ( 𝐺 ∈ Mgm → ( SubMgm ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) )