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 | ⊢ 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑆 ) ) | |
| qusadd.v | ⊢ 𝑉 = ( Base ‘ 𝐺 ) | ||
| quseccl.b | ⊢ 𝐵 = ( Base ‘ 𝐻 ) | ||
| Assertion | quseccl | ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ) → [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) ∈ 𝐵 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | qusgrp.h | ⊢ 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑆 ) ) | |
| 2 | qusadd.v | ⊢ 𝑉 = ( Base ‘ 𝐺 ) | |
| 3 | quseccl.b | ⊢ 𝐵 = ( Base ‘ 𝐻 ) | |
| 4 | nsgsubg | ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) | |
| 5 | subgrcl | ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp ) | |
| 6 | 4 5 | syl | ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝐺 ∈ Grp ) |
| 7 | eqid | ⊢ ( 𝐺 ~QG 𝑆 ) = ( 𝐺 ~QG 𝑆 ) | |
| 8 | 7 1 2 3 | quseccl0 | ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝑉 ) → [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) ∈ 𝐵 ) |
| 9 | 6 8 | sylan | ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ) → [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) ∈ 𝐵 ) |