Metamath Proof Explorer

Theorem 0subg

Description: The zero subgroup of an arbitrary group. (Contributed by Stefan O'Rear, 10-Dec-2014) (Proof shortened by SN, 31-Jan-2025)

Ref Expression
Hypothesis 0subg.z ⊢ 0 ˙ = 0 G
Assertion 0subg ⊢ G ∈ Grp → 0 ˙ ∈ SubGrp ⁡ G

Proof

Step Hyp Ref Expression
1 0subg.z ⊢ 0 ˙ = 0 G
2 grpmnd ⊢ G ∈ Grp → G ∈ Mnd
3 1 0subm ⊢ G ∈ Mnd → 0 ˙ ∈ SubMnd ⁡ G
4 2 3 syl ⊢ G ∈ Grp → 0 ˙ ∈ SubMnd ⁡ G
5 eqid ⊢ inv g ⁡ G = inv g ⁡ G
6 1 5 grpinvid ⊢ G ∈ Grp → inv g ⁡ G ⁡ 0 ˙ = 0 ˙
7 fvex ⊢ inv g ⁡ G ⁡ 0 ˙ ∈ V
8 7 elsn ⊢ inv g ⁡ G ⁡ 0 ˙ ∈ 0 ˙ ↔ inv g ⁡ G ⁡ 0 ˙ = 0 ˙
9 6 8 sylibr ⊢ G ∈ Grp → inv g ⁡ G ⁡ 0 ˙ ∈ 0 ˙
10 1 fvexi ⊢ 0 ˙ ∈ V
11 fveq2 ⊢ a = 0 ˙ → inv g ⁡ G ⁡ a = inv g ⁡ G ⁡ 0 ˙
12 11 eleq1d ⊢ a = 0 ˙ → inv g ⁡ G ⁡ a ∈ 0 ˙ ↔ inv g ⁡ G ⁡ 0 ˙ ∈ 0 ˙
13 10 12 ralsn ⊢ ∀ a ∈ 0 ˙ inv g ⁡ G ⁡ a ∈ 0 ˙ ↔ inv g ⁡ G ⁡ 0 ˙ ∈ 0 ˙
14 9 13 sylibr ⊢ G ∈ Grp → ∀ a ∈ 0 ˙ inv g ⁡ G ⁡ a ∈ 0 ˙
15 5 issubg3 ⊢ G ∈ Grp → 0 ˙ ∈ SubGrp ⁡ G ↔ 0 ˙ ∈ SubMnd ⁡ G ∧ ∀ a ∈ 0 ˙ inv g ⁡ G ⁡ a ∈ 0 ˙
16 4 14 15 mpbir2and ⊢ G ∈ Grp → 0 ˙ ∈ SubGrp ⁡ G