Metamath Proof Explorer

Theorem quseccl

Description: Closure of the quotient map for a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015) (Proof shortened by AV, 9-Mar-2025)

Ref Expression
Hypotheses qusgrp.h ⊢ H = G / 𝑠 G ~ QG S
qusadd.v ⊢ V = Base G
quseccl.b ⊢ B = Base H
Assertion quseccl ⊢ S ∈ NrmSGrp ⁡ G ∧ X ∈ V → X G ~ QG S ∈ B

Proof

Step Hyp Ref Expression
1 qusgrp.h ⊢ H = G / 𝑠 G ~ QG S
2 qusadd.v ⊢ V = Base G
3 quseccl.b ⊢ B = Base H
4 nsgsubg ⊢ S ∈ NrmSGrp ⁡ G → S ∈ SubGrp ⁡ G
5 subgrcl ⊢ S ∈ SubGrp ⁡ G → G ∈ Grp
6 4 5 syl ⊢ S ∈ NrmSGrp ⁡ G → G ∈ Grp
7 eqid ⊢ G ~ QG S = G ~ QG S
8 7 1 2 3 quseccl0 ⊢ G ∈ Grp ∧ X ∈ V → X G ~ QG S ∈ B
9 6 8 sylan ⊢ S ∈ NrmSGrp ⁡ G ∧ X ∈ V → X G ~ QG S ∈ B