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 ⊢ B = Base G
Assertion subgacs ⊢ G ∈ Grp → SubGrp ⁡ G ∈ ACS ⁡ B

Proof

Step Hyp Ref Expression
1 subgacs.b ⊢ B = Base G
2 eqid ⊢ inv g ⁡ G = inv g ⁡ G
3 2 issubg3 ⊢ G ∈ Grp → s ∈ SubGrp ⁡ G ↔ s ∈ SubMnd ⁡ G ∧ ∀ x ∈ s inv g ⁡ G ⁡ x ∈ s
4 1 submss ⊢ s ∈ SubMnd ⁡ G → s ⊆ B
5 4 adantl ⊢ G ∈ Grp ∧ s ∈ SubMnd ⁡ G → s ⊆ B
6 velpw ⊢ s ∈ 𝒫 B ↔ s ⊆ B
7 5 6 sylibr ⊢ G ∈ Grp ∧ s ∈ SubMnd ⁡ G → s ∈ 𝒫 B
8 eleq2w ⊢ y = s → inv g ⁡ G ⁡ x ∈ y ↔ inv g ⁡ G ⁡ x ∈ s
9 8 raleqbi1dv ⊢ y = s → ∀ x ∈ y inv g ⁡ G ⁡ x ∈ y ↔ ∀ x ∈ s inv g ⁡ G ⁡ x ∈ s
10 9 elrab3 ⊢ s ∈ 𝒫 B → s ∈ y ∈ 𝒫 B | ∀ x ∈ y inv g ⁡ G ⁡ x ∈ y ↔ ∀ x ∈ s inv g ⁡ G ⁡ x ∈ s
11 7 10 syl ⊢ G ∈ Grp ∧ s ∈ SubMnd ⁡ G → s ∈ y ∈ 𝒫 B | ∀ x ∈ y inv g ⁡ G ⁡ x ∈ y ↔ ∀ x ∈ s inv g ⁡ G ⁡ x ∈ s
12 11 pm5.32da ⊢ G ∈ Grp → s ∈ SubMnd ⁡ G ∧ s ∈ y ∈ 𝒫 B | ∀ x ∈ y inv g ⁡ G ⁡ x ∈ y ↔ s ∈ SubMnd ⁡ G ∧ ∀ x ∈ s inv g ⁡ G ⁡ x ∈ s
13 3 12 bitr4d ⊢ G ∈ Grp → s ∈ SubGrp ⁡ G ↔ s ∈ SubMnd ⁡ G ∧ s ∈ y ∈ 𝒫 B | ∀ x ∈ y inv g ⁡ G ⁡ x ∈ y
14 elin ⊢ s ∈ SubMnd ⁡ G ∩ y ∈ 𝒫 B | ∀ x ∈ y inv g ⁡ G ⁡ x ∈ y ↔ s ∈ SubMnd ⁡ G ∧ s ∈ y ∈ 𝒫 B | ∀ x ∈ y inv g ⁡ G ⁡ x ∈ y
15 13 14 bitr4di ⊢ G ∈ Grp → s ∈ SubGrp ⁡ G ↔ s ∈ SubMnd ⁡ G ∩ y ∈ 𝒫 B | ∀ x ∈ y inv g ⁡ G ⁡ x ∈ y
16 15 eqrdv ⊢ G ∈ Grp → SubGrp ⁡ G = SubMnd ⁡ G ∩ y ∈ 𝒫 B | ∀ x ∈ y inv g ⁡ G ⁡ x ∈ y
17 1 fvexi ⊢ B ∈ V
18 mreacs ⊢ B ∈ V → ACS ⁡ B ∈ Moore ⁡ 𝒫 B
19 17 18 mp1i ⊢ G ∈ Grp → ACS ⁡ B ∈ Moore ⁡ 𝒫 B
20 grpmnd ⊢ G ∈ Grp → G ∈ Mnd
21 1 submacs ⊢ G ∈ Mnd → SubMnd ⁡ G ∈ ACS ⁡ B
22 20 21 syl ⊢ G ∈ Grp → SubMnd ⁡ G ∈ ACS ⁡ B
23 1 2 grpinvcl ⊢ G ∈ Grp ∧ x ∈ B → inv g ⁡ G ⁡ x ∈ B
24 23 ralrimiva ⊢ G ∈ Grp → ∀ x ∈ B inv g ⁡ G ⁡ x ∈ B
25 acsfn1 ⊢ B ∈ V ∧ ∀ x ∈ B inv g ⁡ G ⁡ x ∈ B → y ∈ 𝒫 B | ∀ x ∈ y inv g ⁡ G ⁡ x ∈ y ∈ ACS ⁡ B
26 17 24 25 sylancr ⊢ G ∈ Grp → y ∈ 𝒫 B | ∀ x ∈ y inv g ⁡ G ⁡ x ∈ y ∈ ACS ⁡ B
27 mreincl ⊢ ACS ⁡ B ∈ Moore ⁡ 𝒫 B ∧ SubMnd ⁡ G ∈ ACS ⁡ B ∧ y ∈ 𝒫 B | ∀ x ∈ y inv g ⁡ G ⁡ x ∈ y ∈ ACS ⁡ B → SubMnd ⁡ G ∩ y ∈ 𝒫 B | ∀ x ∈ y inv g ⁡ G ⁡ x ∈ y ∈ ACS ⁡ B
28 19 22 26 27 syl3anc ⊢ G ∈ Grp → SubMnd ⁡ G ∩ y ∈ 𝒫 B | ∀ x ∈ y inv g ⁡ G ⁡ x ∈ y ∈ ACS ⁡ B
29 16 28 eqeltrd ⊢ G ∈ Grp → SubGrp ⁡ G ∈ ACS ⁡ B