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 = ( Base ` G )
	qustriv.2	|- Q = ( G /s ( G ~QG B ) )
Assertion	qustriv	|- ( G e. Grp -> ( Base ` Q ) = { B } )

Proof

Step	Hyp	Ref	Expression
1		qustriv.1	|- B = ( Base ` G )
2		qustriv.2	|- Q = ( G /s ( G ~QG B ) )
3	1	qusxpid	|- ( G e. Grp -> ( G ~QG B ) = ( B X. B ) )
4	3	qseq2d	|- ( G e. Grp -> ( B /. ( G ~QG B ) ) = ( B /. ( B X. B ) ) )
5	2	a1i	|- ( G e. Grp -> Q = ( G /s ( G ~QG B ) ) )
6	1	a1i	|- ( G e. Grp -> B = ( Base ` G ) )
7		ovexd	|- ( G e. Grp -> ( G ~QG B ) e. _V )
8		id	|- ( G e. Grp -> G e. Grp )
9	5 6 7 8	qusbas	|- ( G e. Grp -> ( B /. ( G ~QG B ) ) = ( Base ` Q ) )
10	1	grpbn0	|- ( G e. Grp -> B =/= (/) )
11		qsxpid	|- ( B =/= (/) -> ( B /. ( B X. B ) ) = { B } )
12	10 11	syl	|- ( G e. Grp -> ( B /. ( B X. B ) ) = { B } )
13	4 9 12	3eqtr3d	|- ( G e. Grp -> ( Base ` Q ) = { B } )