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 / 𝑠 G ~ QG B
Assertion qustriv G Grp Base Q = B

Proof

Step Hyp Ref Expression
1 qustriv.1 B = Base G
2 qustriv.2 Q = G / 𝑠 G ~ QG B
3 1 qusxpid G Grp G ~ QG B = B × B
4 3 qseq2d G Grp B / G ~ QG B = B / B × B
5 2 a1i G Grp Q = G / 𝑠 G ~ QG B
6 1 a1i G Grp B = Base G
7 ovexd G Grp G ~ QG B V
8 id G Grp G Grp
9 5 6 7 8 qusbas G Grp B / G ~ QG B = Base Q
10 1 grpbn0 G Grp B
11 qsxpid B B / B × B = B
12 10 11 syl G Grp B / B × B = B
13 4 9 12 3eqtr3d G Grp Base Q = B