Theorem 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{\dot{}}{0}=0_G$$
	qus0subg.s	$$⊢S=\left\{\underset{\dot{}}{0}\right\}$$
	qus0subg.e	$$⊢\underset{\dot{}}{\sim }=G{~}_{\mathit{QG}}S$$
	qus0subg.u	$$⊢U=G{/}_{𝑠}\underset{\dot{}}{\sim }$$
	qus0subg.b	$$⊢B={\mathrm{Base}}_G$$
Assertion	qus0subgbas	$$⊢G\in \mathrm{Grp}\to {\mathrm{Base}}_U=\left\{u|\exists x\in Bu=\left\{x\right\}\right\}$$

Proof

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