This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } )