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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	qustriv.2	⊢ 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝐵 ) )
Assertion	qustriv	⊢ ( 𝐺 ∈ Grp → ( Base ‘ 𝑄 ) = { 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		qustriv.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		qustriv.2	⊢ 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝐵 ) )
3	1	qusxpid	⊢ ( 𝐺 ∈ Grp → ( 𝐺 ~QG 𝐵 ) = ( 𝐵 × 𝐵 ) )
4	3	qseq2d	⊢ ( 𝐺 ∈ Grp → ( 𝐵 / ( 𝐺 ~QG 𝐵 ) ) = ( 𝐵 / ( 𝐵 × 𝐵 ) ) )
5	2	a1i	⊢ ( 𝐺 ∈ Grp → 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝐵 ) ) )
6	1	a1i	⊢ ( 𝐺 ∈ Grp → 𝐵 = ( Base ‘ 𝐺 ) )
7		ovexd	⊢ ( 𝐺 ∈ Grp → ( 𝐺 ~QG 𝐵 ) ∈ V )
8		id	⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Grp )
9	5 6 7 8	qusbas	⊢ ( 𝐺 ∈ Grp → ( 𝐵 / ( 𝐺 ~QG 𝐵 ) ) = ( Base ‘ 𝑄 ) )
10	1	grpbn0	⊢ ( 𝐺 ∈ Grp → 𝐵 ≠ ∅ )
11		qsxpid	⊢ ( 𝐵 ≠ ∅ → ( 𝐵 / ( 𝐵 × 𝐵 ) ) = { 𝐵 } )
12	10 11	syl	⊢ ( 𝐺 ∈ Grp → ( 𝐵 / ( 𝐵 × 𝐵 ) ) = { 𝐵 } )
13	4 9 12	3eqtr3d	⊢ ( 𝐺 ∈ Grp → ( Base ‘ 𝑄 ) = { 𝐵 } )