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