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 ‘ 𝐵 ) )