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	$$⊢\underset{\dot{}}{0}=0_G$$
	eqg0subg.s	$$⊢S=\left\{\underset{\dot{}}{0}\right\}$$
	eqg0subg.b	$$⊢B={\mathrm{Base}}_G$$
	eqg0subg.r	$$⊢R=G{~}_{\mathit{QG}}S$$
Assertion	eqg0subgecsn	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to \left[X\right]R=\left\{X\right\}$$

Proof

Step	Hyp	Ref	Expression
1		eqg0subg.0	$$⊢\underset{\dot{}}{0}=0_G$$
2		eqg0subg.s	$$⊢S=\left\{\underset{\dot{}}{0}\right\}$$
3		eqg0subg.b	$$⊢B={\mathrm{Base}}_G$$
4		eqg0subg.r	$$⊢R=G{~}_{\mathit{QG}}S$$
5		df-ec	$$⊢\left[X\right]R=R\left[\left\{X\right\}\right]$$
6	1 2 3 4	eqg0subg	$$⊢G\in \mathrm{Grp}\to R={\mathrm{I}\upharpoonright }_B$$
7	6	adantr	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to R={\mathrm{I}\upharpoonright }_B$$
8	7	imaeq1d	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to R\left[\left\{X\right\}\right]=\left({\mathrm{I}\upharpoonright }_B\right)\left[\left\{X\right\}\right]$$
9		snssi	$$⊢X\in B\to \left\{X\right\}\subseteq B$$
10	9	adantl	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to \left\{X\right\}\subseteq B$$
11		resima2	$$⊢\left\{X\right\}\subseteq B\to \left({\mathrm{I}\upharpoonright }_B\right)\left[\left\{X\right\}\right]=\mathrm{I}\left[\left\{X\right\}\right]$$
12	10 11	syl	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to \left({\mathrm{I}\upharpoonright }_B\right)\left[\left\{X\right\}\right]=\mathrm{I}\left[\left\{X\right\}\right]$$
13		imai	$$⊢\mathrm{I}\left[\left\{X\right\}\right]=\left\{X\right\}$$
14	12 13	eqtrdi	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to \left({\mathrm{I}\upharpoonright }_B\right)\left[\left\{X\right\}\right]=\left\{X\right\}$$
15	8 14	eqtrd	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to R\left[\left\{X\right\}\right]=\left\{X\right\}$$
16	5 15	eqtrid	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to \left[X\right]R=\left\{X\right\}$$