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

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 = ( 0g ‘ 𝐺 )
Assertion 0subg ( 𝐺 ∈ Grp → { 0 } ∈ ( SubGrp ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 0subg.z ⊢ 0 = ( 0g ‘ 𝐺 )
2 grpmnd ⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
3 1 0subm ⊢ ( 𝐺 ∈ Mnd → { 0 } ∈ ( SubMnd ‘ 𝐺 ) )
4 2 3 syl ⊢ ( 𝐺 ∈ Grp → { 0 } ∈ ( SubMnd ‘ 𝐺 ) )
5 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
6 1 5 grpinvid ⊢ ( 𝐺 ∈ Grp → ( ( invg ‘ 𝐺 ) ‘ 0 ) = 0 )
7 fvex ⊢ ( ( invg ‘ 𝐺 ) ‘ 0 ) ∈ V
8 7 elsn ⊢ ( ( ( invg ‘ 𝐺 ) ‘ 0 ) ∈ { 0 } ↔ ( ( invg ‘ 𝐺 ) ‘ 0 ) = 0 )
9 6 8 sylibr ⊢ ( 𝐺 ∈ Grp → ( ( invg ‘ 𝐺 ) ‘ 0 ) ∈ { 0 } )
10 1 fvexi ⊢ 0 ∈ V
11 fveq2 ⊢ ( 𝑎 = 0 → ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) = ( ( invg ‘ 𝐺 ) ‘ 0 ) )
12 11 eleq1d ⊢ ( 𝑎 = 0 → ( ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ { 0 } ↔ ( ( invg ‘ 𝐺 ) ‘ 0 ) ∈ { 0 } ) )
13 10 12 ralsn ⊢ ( ∀ 𝑎 ∈ { 0 } ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ { 0 } ↔ ( ( invg ‘ 𝐺 ) ‘ 0 ) ∈ { 0 } )
14 9 13 sylibr ⊢ ( 𝐺 ∈ Grp → ∀ 𝑎 ∈ { 0 } ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ { 0 } )
15 5 issubg3 ⊢ ( 𝐺 ∈ Grp → ( { 0 } ∈ ( SubGrp ‘ 𝐺 ) ↔ ( { 0 } ∈ ( SubMnd ‘ 𝐺 ) ∧ ∀ 𝑎 ∈ { 0 } ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ { 0 } ) ) )
16 4 14 15 mpbir2and ⊢ ( 𝐺 ∈ Grp → { 0 } ∈ ( SubGrp ‘ 𝐺 ) )