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 ` G )
	eqg0subg.s	|- S = { .0. }
	eqg0subg.b	|- B = ( Base ` G )
	eqg0subg.r	|- R = ( G ~QG S )
Assertion	eqg0subgecsn	|- ( ( G e. Grp /\ X e. B ) -> [ X ] R = { X } )

Proof

Step	Hyp	Ref	Expression
1		eqg0subg.0	|- .0. = ( 0g ` G )
2		eqg0subg.s	|- S = { .0. }
3		eqg0subg.b	|- B = ( Base ` G )
4		eqg0subg.r	|- R = ( G ~QG S )
5		df-ec	|- [ X ] R = ( R " { X } )
6	1 2 3 4	eqg0subg	|- ( G e. Grp -> R = ( _I |` B ) )
7	6	adantr	|- ( ( G e. Grp /\ X e. B ) -> R = ( _I |` B ) )
8	7	imaeq1d	|- ( ( G e. Grp /\ X e. B ) -> ( R " { X } ) = ( ( _I |` B ) " { X } ) )
9		snssi	|- ( X e. B -> { X } C_ B )
10	9	adantl	|- ( ( G e. Grp /\ X e. B ) -> { X } C_ B )
11		resima2	|- ( { X } C_ B -> ( ( _I |` B ) " { X } ) = ( _I " { X } ) )
12	10 11	syl	|- ( ( G e. Grp /\ X e. B ) -> ( ( _I |` B ) " { X } ) = ( _I " { X } ) )
13		imai	|- ( _I " { X } ) = { X }
14	12 13	eqtrdi	|- ( ( G e. Grp /\ X e. B ) -> ( ( _I |` B ) " { X } ) = { X } )
15	8 14	eqtrd	|- ( ( G e. Grp /\ X e. B ) -> ( R " { X } ) = { X } )
16	5 15	eqtrid	|- ( ( G e. Grp /\ X e. B ) -> [ X ] R = { X } )