Theorem eqg0subgecsn

Description: The equivalence classes modulo the coset equivalence relation for the trivial (zero) subgroup of a group are singletons. (Contributed by AV, 26-Feb-2025)

	Ref	Expression
Hypotheses	eqg0subg.0	⊢ 0 = ( 0g ‘ 𝐺 )
	eqg0subg.s	⊢ 𝑆 = { 0 }
	eqg0subg.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	eqg0subg.r	⊢ 𝑅 = ( 𝐺 ~QG 𝑆 )
Assertion	eqg0subgecsn	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → [ 𝑋 ] 𝑅 = { 𝑋 } )

Proof

Step	Hyp	Ref	Expression
1		eqg0subg.0	⊢ 0 = ( 0g ‘ 𝐺 )
2		eqg0subg.s	⊢ 𝑆 = { 0 }
3		eqg0subg.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
4		eqg0subg.r	⊢ 𝑅 = ( 𝐺 ~QG 𝑆 )
5		df-ec	⊢ [ 𝑋 ] 𝑅 = ( 𝑅 “ { 𝑋 } )
6	1 2 3 4	eqg0subg	⊢ ( 𝐺 ∈ Grp → 𝑅 = ( I ↾ 𝐵 ) )
7	6	adantr	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → 𝑅 = ( I ↾ 𝐵 ) )
8	7	imaeq1d	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑅 “ { 𝑋 } ) = ( ( I ↾ 𝐵 ) “ { 𝑋 } ) )
9		snssi	⊢ ( 𝑋 ∈ 𝐵 → { 𝑋 } ⊆ 𝐵 )
10	9	adantl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → { 𝑋 } ⊆ 𝐵 )
11		resima2	⊢ ( { 𝑋 } ⊆ 𝐵 → ( ( I ↾ 𝐵 ) “ { 𝑋 } ) = ( I “ { 𝑋 } ) )
12	10 11	syl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( ( I ↾ 𝐵 ) “ { 𝑋 } ) = ( I “ { 𝑋 } ) )
13		imai	⊢ ( I “ { 𝑋 } ) = { 𝑋 }
14	12 13	eqtrdi	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( ( I ↾ 𝐵 ) “ { 𝑋 } ) = { 𝑋 } )
15	8 14	eqtrd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑅 “ { 𝑋 } ) = { 𝑋 } )
16	5 15	eqtrid	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → [ 𝑋 ] 𝑅 = { 𝑋 } )