Theorem qusbas2

Description: Alternate definition of the group quotient set, as the set of all cosets of the form ( { x } .(+) N ) . (Contributed by Thierry Arnoux, 22-Mar-2025)

	Ref	Expression
Hypotheses	qusbas2.1	$$⊢B={\mathrm{Base}}_G$$
	qusbas2.2	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(G\right)$$
	qusbas2.3	$$⊢\left(\phi \wedge x\in B\right)\to N\in \mathrm{SubGrp}\left(G\right)$$
Assertion	qusbas2	$$⊢\phi \to B/\left(G{~}_{\mathit{QG}}N\right)=\mathrm{ran}\left(x\in B⟼\left\{x\right\}\underset{\dot{}}{\oplus }N\right)$$

Proof

Step	Hyp	Ref	Expression
1		qusbas2.1	$$⊢B={\mathrm{Base}}_G$$
2		qusbas2.2	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(G\right)$$
3		qusbas2.3	$$⊢\left(\phi \wedge x\in B\right)\to N\in \mathrm{SubGrp}\left(G\right)$$
4		df-qs	$$⊢B/\left(G{~}_{\mathit{QG}}N\right)=\left\{y|\exists x\in By=\left[x\right]\left(G{~}_{\mathit{QG}}N\right)\right\}$$
5		eqid	$$⊢\left(x\in B⟼\left[x\right]\left(G{~}_{\mathit{QG}}N\right)\right)=\left(x\in B⟼\left[x\right]\left(G{~}_{\mathit{QG}}N\right)\right)$$
6	5	rnmpt	$$⊢\mathrm{ran}\left(x\in B⟼\left[x\right]\left(G{~}_{\mathit{QG}}N\right)\right)=\left\{y|\exists x\in By=\left[x\right]\left(G{~}_{\mathit{QG}}N\right)\right\}$$
7	4 6	eqtr4i	$$⊢B/\left(G{~}_{\mathit{QG}}N\right)=\mathrm{ran}\left(x\in B⟼\left[x\right]\left(G{~}_{\mathit{QG}}N\right)\right)$$
8		simpr	$$⊢\left(\phi \wedge x\in B\right)\to x\in B$$
9	1 2 3 8	quslsm	$$⊢\left(\phi \wedge x\in B\right)\to \left[x\right]\left(G{~}_{\mathit{QG}}N\right)=\left\{x\right\}\underset{\dot{}}{\oplus }N$$
10	9	mpteq2dva	$$⊢\phi \to \left(x\in B⟼\left[x\right]\left(G{~}_{\mathit{QG}}N\right)\right)=\left(x\in B⟼\left\{x\right\}\underset{\dot{}}{\oplus }N\right)$$
11	10	rneqd	$$⊢\phi \to \mathrm{ran}\left(x\in B⟼\left[x\right]\left(G{~}_{\mathit{QG}}N\right)\right)=\mathrm{ran}\left(x\in B⟼\left\{x\right\}\underset{\dot{}}{\oplus }N\right)$$
12	7 11	eqtrid	$$⊢\phi \to B/\left(G{~}_{\mathit{QG}}N\right)=\mathrm{ran}\left(x\in B⟼\left\{x\right\}\underset{\dot{}}{\oplus }N\right)$$