This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

Proof

Step	Hyp	Ref	Expression
1		eqg0subg.0	$⊢ \underset{˙}{0} = 0_{G}$
2		eqg0subg.s	$⊢ S = \{\underset{˙}{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 \in Grp \to R = {I ↾}_{B}$
7	6	adantr	$⊢ (G \in Grp \land X \in B) \to R = {I ↾}_{B}$
8	7	imaeq1d	$⊢ (G \in Grp \land X \in B) \to R [\{X\}] = ({I ↾}_{B}) [\{X\}]$
9		snssi	$⊢ X \in B \to \{X\} \subseteq B$
10	9	adantl	$⊢ (G \in Grp \land X \in B) \to \{X\} \subseteq B$
11		resima2	$⊢ \{X\} \subseteq B \to ({I ↾}_{B}) [\{X\}] = I [\{X\}]$
12	10 11	syl	$⊢ (G \in Grp \land X \in B) \to ({I ↾}_{B}) [\{X\}] = I [\{X\}]$
13		imai	$⊢ I [\{X\}] = \{X\}$
14	12 13	eqtrdi	$⊢ (G \in Grp \land X \in B) \to ({I ↾}_{B}) [\{X\}] = \{X\}$
15	8 14	eqtrd	$⊢ (G \in Grp \land X \in B) \to R [\{X\}] = \{X\}$
16	5 15	eqtrid	$⊢ (G \in Grp \land X \in B) \to [X] R = \{X\}$