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 / 𝑠 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