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

Metamath Proof Explorer

Theorem subgacs

Description: Subgroups are an algebraic closure system. (Contributed by Stefan O'Rear, 4-Apr-2015) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypothesis subgacs.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion subgacs ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 subgacs.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
3 2 issubg3 ⊢ ( 𝐺 ∈ Grp → ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑠 ∈ ( SubMnd ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑠 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑠 ) ) )
4 1 submss ⊢ ( 𝑠 ∈ ( SubMnd ‘ 𝐺 ) → 𝑠 ⊆ 𝐵 )
5 4 adantl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑠 ∈ ( SubMnd ‘ 𝐺 ) ) → 𝑠 ⊆ 𝐵 )
6 velpw ⊢ ( 𝑠 ∈ 𝒫 𝐵 ↔ 𝑠 ⊆ 𝐵 )
7 5 6 sylibr ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑠 ∈ ( SubMnd ‘ 𝐺 ) ) → 𝑠 ∈ 𝒫 𝐵 )
8 eleq2w ⊢ ( 𝑦 = 𝑠 → ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 ↔ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑠 ) )
9 8 raleqbi1dv ⊢ ( 𝑦 = 𝑠 → ( ∀ 𝑥 ∈ 𝑦 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 ↔ ∀ 𝑥 ∈ 𝑠 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑠 ) )
10 9 elrab3 ⊢ ( 𝑠 ∈ 𝒫 𝐵 → ( 𝑠 ∈ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 } ↔ ∀ 𝑥 ∈ 𝑠 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑠 ) )
11 7 10 syl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑠 ∈ ( SubMnd ‘ 𝐺 ) ) → ( 𝑠 ∈ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 } ↔ ∀ 𝑥 ∈ 𝑠 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑠 ) )
12 11 pm5.32da ⊢ ( 𝐺 ∈ Grp → ( ( 𝑠 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑠 ∈ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 } ) ↔ ( 𝑠 ∈ ( SubMnd ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑠 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑠 ) ) )
13 3 12 bitr4d ⊢ ( 𝐺 ∈ Grp → ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑠 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑠 ∈ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 } ) ) )
14 elin ⊢ ( 𝑠 ∈ ( ( SubMnd ‘ 𝐺 ) ∩ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 } ) ↔ ( 𝑠 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑠 ∈ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 } ) )
15 13 14 bitr4di ⊢ ( 𝐺 ∈ Grp → ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ↔ 𝑠 ∈ ( ( SubMnd ‘ 𝐺 ) ∩ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 } ) ) )
16 15 eqrdv ⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) = ( ( SubMnd ‘ 𝐺 ) ∩ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 } ) )
17 1 fvexi ⊢ 𝐵 ∈ V
18 mreacs ⊢ ( 𝐵 ∈ V → ( ACS ‘ 𝐵 ) ∈ ( Moore ‘ 𝒫 𝐵 ) )
19 17 18 mp1i ⊢ ( 𝐺 ∈ Grp → ( ACS ‘ 𝐵 ) ∈ ( Moore ‘ 𝒫 𝐵 ) )
20 grpmnd ⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
21 1 submacs ⊢ ( 𝐺 ∈ Mnd → ( SubMnd ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) )
22 20 21 syl ⊢ ( 𝐺 ∈ Grp → ( SubMnd ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) )
23 1 2 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐵 )
24 23 ralrimiva ⊢ ( 𝐺 ∈ Grp → ∀ 𝑥 ∈ 𝐵 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐵 )
25 acsfn1 ⊢ ( ( 𝐵 ∈ V ∧ ∀ 𝑥 ∈ 𝐵 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐵 ) → { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 } ∈ ( ACS ‘ 𝐵 ) )
26 17 24 25 sylancr ⊢ ( 𝐺 ∈ Grp → { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 } ∈ ( ACS ‘ 𝐵 ) )
27 mreincl ⊢ ( ( ( ACS ‘ 𝐵 ) ∈ ( Moore ‘ 𝒫 𝐵 ) ∧ ( SubMnd ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) ∧ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 } ∈ ( ACS ‘ 𝐵 ) ) → ( ( SubMnd ‘ 𝐺 ) ∩ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 } ) ∈ ( ACS ‘ 𝐵 ) )
28 19 22 26 27 syl3anc ⊢ ( 𝐺 ∈ Grp → ( ( SubMnd ‘ 𝐺 ) ∩ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 } ) ∈ ( ACS ‘ 𝐵 ) )
29 16 28 eqeltrd ⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) )