Theorem 0subg

Description: The zero subgroup of an arbitrary group. (Contributed by Stefan O'Rear, 10-Dec-2014)

	Ref	Expression
Hypothesis	0subg.z	⊢ 0 = ( 0g ‘ 𝐺 )
Assertion	0subg	⊢ ( 𝐺 ∈ Grp → { 0 } ∈ ( SubGrp ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		0subg.z	⊢ 0 = ( 0g ‘ 𝐺 )
2		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
3	2 1	grpidcl	⊢ ( 𝐺 ∈ Grp → 0 ∈ ( Base ‘ 𝐺 ) )
4	3	snssd	⊢ ( 𝐺 ∈ Grp → { 0 } ⊆ ( Base ‘ 𝐺 ) )
5	1	fvexi	⊢ 0 ∈ V
6	5	snnz	⊢ { 0 } ≠ ∅
7	6	a1i	⊢ ( 𝐺 ∈ Grp → { 0 } ≠ ∅ )
8		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
9	2 8 1	grplid	⊢ ( ( 𝐺 ∈ Grp ∧ 0 ∈ ( Base ‘ 𝐺 ) ) → ( 0 ( +g ‘ 𝐺 ) 0 ) = 0 )
10	3 9	mpdan	⊢ ( 𝐺 ∈ Grp → ( 0 ( +g ‘ 𝐺 ) 0 ) = 0 )
11		ovex	⊢ ( 0 ( +g ‘ 𝐺 ) 0 ) ∈ V
12	11	elsn	⊢ ( ( 0 ( +g ‘ 𝐺 ) 0 ) ∈ { 0 } ↔ ( 0 ( +g ‘ 𝐺 ) 0 ) = 0 )
13	10 12	sylibr	⊢ ( 𝐺 ∈ Grp → ( 0 ( +g ‘ 𝐺 ) 0 ) ∈ { 0 } )
14		eqid	⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
15	1 14	grpinvid	⊢ ( 𝐺 ∈ Grp → ( ( invg ‘ 𝐺 ) ‘ 0 ) = 0 )
16		fvex	⊢ ( ( invg ‘ 𝐺 ) ‘ 0 ) ∈ V
17	16	elsn	⊢ ( ( ( invg ‘ 𝐺 ) ‘ 0 ) ∈ { 0 } ↔ ( ( invg ‘ 𝐺 ) ‘ 0 ) = 0 )
18	15 17	sylibr	⊢ ( 𝐺 ∈ Grp → ( ( invg ‘ 𝐺 ) ‘ 0 ) ∈ { 0 } )
19		oveq1	⊢ ( 𝑎 = 0 → ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) = ( 0 ( +g ‘ 𝐺 ) 𝑏 ) )
20	19	eleq1d	⊢ ( 𝑎 = 0 → ( ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ { 0 } ↔ ( 0 ( +g ‘ 𝐺 ) 𝑏 ) ∈ { 0 } ) )
21	20	ralbidv	⊢ ( 𝑎 = 0 → ( ∀ 𝑏 ∈ { 0 } ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ { 0 } ↔ ∀ 𝑏 ∈ { 0 } ( 0 ( +g ‘ 𝐺 ) 𝑏 ) ∈ { 0 } ) )
22		oveq2	⊢ ( 𝑏 = 0 → ( 0 ( +g ‘ 𝐺 ) 𝑏 ) = ( 0 ( +g ‘ 𝐺 ) 0 ) )
23	22	eleq1d	⊢ ( 𝑏 = 0 → ( ( 0 ( +g ‘ 𝐺 ) 𝑏 ) ∈ { 0 } ↔ ( 0 ( +g ‘ 𝐺 ) 0 ) ∈ { 0 } ) )
24	5 23	ralsn	⊢ ( ∀ 𝑏 ∈ { 0 } ( 0 ( +g ‘ 𝐺 ) 𝑏 ) ∈ { 0 } ↔ ( 0 ( +g ‘ 𝐺 ) 0 ) ∈ { 0 } )
25	21 24	bitrdi	⊢ ( 𝑎 = 0 → ( ∀ 𝑏 ∈ { 0 } ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ { 0 } ↔ ( 0 ( +g ‘ 𝐺 ) 0 ) ∈ { 0 } ) )
26		fveq2	⊢ ( 𝑎 = 0 → ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) = ( ( invg ‘ 𝐺 ) ‘ 0 ) )
27	26	eleq1d	⊢ ( 𝑎 = 0 → ( ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ { 0 } ↔ ( ( invg ‘ 𝐺 ) ‘ 0 ) ∈ { 0 } ) )
28	25 27	anbi12d	⊢ ( 𝑎 = 0 → ( ( ∀ 𝑏 ∈ { 0 } ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ { 0 } ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ { 0 } ) ↔ ( ( 0 ( +g ‘ 𝐺 ) 0 ) ∈ { 0 } ∧ ( ( invg ‘ 𝐺 ) ‘ 0 ) ∈ { 0 } ) ) )
29	5 28	ralsn	⊢ ( ∀ 𝑎 ∈ { 0 } ( ∀ 𝑏 ∈ { 0 } ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ { 0 } ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ { 0 } ) ↔ ( ( 0 ( +g ‘ 𝐺 ) 0 ) ∈ { 0 } ∧ ( ( invg ‘ 𝐺 ) ‘ 0 ) ∈ { 0 } ) )
30	13 18 29	sylanbrc	⊢ ( 𝐺 ∈ Grp → ∀ 𝑎 ∈ { 0 } ( ∀ 𝑏 ∈ { 0 } ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ { 0 } ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ { 0 } ) )
31	2 8 14	issubg2	⊢ ( 𝐺 ∈ Grp → ( { 0 } ∈ ( SubGrp ‘ 𝐺 ) ↔ ( { 0 } ⊆ ( Base ‘ 𝐺 ) ∧ { 0 } ≠ ∅ ∧ ∀ 𝑎 ∈ { 0 } ( ∀ 𝑏 ∈ { 0 } ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ { 0 } ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ { 0 } ) ) ) )
32	4 7 30 31	mpbir3and	⊢ ( 𝐺 ∈ Grp → { 0 } ∈ ( SubGrp ‘ 𝐺 ) )