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 ⊢ 𝐵 = ( 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 ‘ 𝑄 ) = { 𝐵 } )