Theorem qustriv

Description: The quotient of a group G by itself is trivial. (Contributed by Thierry Arnoux, 15-Jan-2024)

	Ref	Expression
Hypotheses	qustriv.1	$$⊢B={\mathrm{Base}}_G$$
	qustriv.2	$$⊢Q=G{/}_{𝑠}\left(G{~}_{\mathit{QG}}B\right)$$
Assertion	qustriv	$$⊢G\in \mathrm{Grp}\to {\mathrm{Base}}_Q=\left\{B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		qustriv.1	$$⊢B={\mathrm{Base}}_G$$
2		qustriv.2	$$⊢Q=G{/}_{𝑠}\left(G{~}_{\mathit{QG}}B\right)$$
3	1	qusxpid	$$⊢G\in \mathrm{Grp}\to G{~}_{\mathit{QG}}B=B\times B$$
4	3	qseq2d	$$⊢G\in \mathrm{Grp}\to B/\left(G{~}_{\mathit{QG}}B\right)=B/\left(B\times B\right)$$
5	2	a1i	$$⊢G\in \mathrm{Grp}\to Q=G{/}_{𝑠}\left(G{~}_{\mathit{QG}}B\right)$$
6	1	a1i	$$⊢G\in \mathrm{Grp}\to B={\mathrm{Base}}_G$$
7		ovexd	$$⊢G\in \mathrm{Grp}\to G{~}_{\mathit{QG}}B\in \mathrm{V}$$
8		id	$$⊢G\in \mathrm{Grp}\to G\in \mathrm{Grp}$$
9	5 6 7 8	qusbas	$$⊢G\in \mathrm{Grp}\to B/\left(G{~}_{\mathit{QG}}B\right)={\mathrm{Base}}_Q$$
10	1	grpbn0	$$⊢G\in \mathrm{Grp}\to B\ne \varnothing$$
11		qsxpid	$$⊢B\ne \varnothing \to B/\left(B\times B\right)=\left\{B\right\}$$
12	10 11	syl	$$⊢G\in \mathrm{Grp}\to B/\left(B\times B\right)=\left\{B\right\}$$
13	4 9 12	3eqtr3d	$$⊢G\in \mathrm{Grp}\to {\mathrm{Base}}_Q=\left\{B\right\}$$