qus0subgbas

Description: The base set of a quotient of a group by the trivial (zero) subgroup. (Contributed by AV, 26-Feb-2025)

	Ref	Expression
Hypotheses	qus0subg.0	$⊢ \underset{˙}{0} = 0_{G}$
	qus0subg.s	$⊢ S = \{\underset{˙}{0}\}$
	qus0subg.e	$⊢ \underset{˙}{\sim} = G ~_{QG} S$
	qus0subg.u	$⊢ U = G /_{𝑠} \underset{˙}{\sim}$
	qus0subg.b	$⊢ B = {Base}_{G}$
Assertion	qus0subgbas	$⊢ G \in Grp \to {Base}_{U} = \{u \| \exists x \in B u = \{x\}\}$

Step	Hyp	Ref	Expression
1		qus0subg.0	$⊢ \underset{˙}{0} = 0_{G}$
2		qus0subg.s	$⊢ S = \{\underset{˙}{0}\}$
3		qus0subg.e	$⊢ \underset{˙}{\sim} = G ~_{QG} S$
4		qus0subg.u	$⊢ U = G /_{𝑠} \underset{˙}{\sim}$
5		qus0subg.b	$⊢ B = {Base}_{G}$
6		df-qs	$⊢ B / \underset{˙}{\sim} = \{u \| \exists x \in B u = [x] \underset{˙}{\sim}\}$
7	4	a1i	$⊢ G \in Grp \to U = G /_{𝑠} \underset{˙}{\sim}$
8	5	a1i	$⊢ G \in Grp \to B = {Base}_{G}$
9	3	ovexi	$⊢ \underset{˙}{\sim} \in V$
10	9	a1i	$⊢ G \in Grp \to \underset{˙}{\sim} \in V$
11		id	$⊢ G \in Grp \to G \in Grp$
12	7 8 10 11	qusbas	$⊢ G \in Grp \to B / \underset{˙}{\sim} = {Base}_{U}$
13	1 2 5 3	eqg0subgecsn	$⊢ (G \in Grp \land x \in B) \to [x] \underset{˙}{\sim} = \{x\}$
14	13	eqeq2d	$⊢ (G \in Grp \land x \in B) \to (u = [x] \underset{˙}{\sim} \leftrightarrow u = \{x\})$
15	14	rexbidva	$⊢ G \in Grp \to (\exists x \in B u = [x] \underset{˙}{\sim} \leftrightarrow \exists x \in B u = \{x\})$
16	15	abbidv	$⊢ G \in Grp \to \{u \| \exists x \in B u = [x] \underset{˙}{\sim}\} = \{u \| \exists x \in B u = \{x\}\}$
17	6 12 16	3eqtr3a	$⊢ G \in Grp \to {Base}_{U} = \{u \| \exists x \in B u = \{x\}\}$

Metamath Proof Explorer