Metamath Proof Explorer

Theorem quseccl

Description: Closure of the quotient map for a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015)

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 ovex ⊢ G ~ QG S ∈ V
5 4 ecelqsi ⊢ X ∈ V → X G ~ QG S ∈ V / G ~ QG S
6 5 adantl ⊢ S ∈ NrmSGrp ⁡ G ∧ X ∈ V → X G ~ QG S ∈ V / G ~ QG S
7 1 a1i ⊢ S ∈ NrmSGrp ⁡ G ∧ X ∈ V → H = G / 𝑠 G ~ QG S
8 2 a1i ⊢ S ∈ NrmSGrp ⁡ G ∧ X ∈ V → V = Base G
9 4 a1i ⊢ S ∈ NrmSGrp ⁡ G ∧ X ∈ V → G ~ QG S ∈ V
10 nsgsubg ⊢ S ∈ NrmSGrp ⁡ G → S ∈ SubGrp ⁡ G
11 subgrcl ⊢ S ∈ SubGrp ⁡ G → G ∈ Grp
12 10 11 syl ⊢ S ∈ NrmSGrp ⁡ G → G ∈ Grp
13 12 adantr ⊢ S ∈ NrmSGrp ⁡ G ∧ X ∈ V → G ∈ Grp
14 7 8 9 13 qusbas ⊢ S ∈ NrmSGrp ⁡ G ∧ X ∈ V → V / G ~ QG S = Base H
15 14 3 eqtr4di ⊢ S ∈ NrmSGrp ⁡ G ∧ X ∈ V → V / G ~ QG S = B
16 6 15 eleqtrd ⊢ S ∈ NrmSGrp ⁡ G ∧ X ∈ V → X G ~ QG S ∈ B