Metamath Proof Explorer

Theorem qusgrp

Description: If Y is a normal subgroup of G , then H = G / Y is a group, called the quotient of G by Y . (Contributed by Mario Carneiro, 14-Jun-2015) (Revised by Mario Carneiro, 12-Aug-2015)

Ref Expression
Hypothesis qusgrp.h ⊢ H = G / 𝑠 G ~ QG S
Assertion qusgrp ⊢ S ∈ NrmSGrp ⁡ G → H ∈ Grp

Proof

Step Hyp Ref Expression
1 qusgrp.h ⊢ H = G / 𝑠 G ~ QG S
2 1 a1i ⊢ S ∈ NrmSGrp ⁡ G → H = G / 𝑠 G ~ QG S
3 eqidd ⊢ S ∈ NrmSGrp ⁡ G → Base G = Base G
4 eqidd ⊢ S ∈ NrmSGrp ⁡ G → + G = + G
5 nsgsubg ⊢ S ∈ NrmSGrp ⁡ G → S ∈ SubGrp ⁡ G
6 eqid ⊢ Base G = Base G
7 eqid ⊢ G ~ QG S = G ~ QG S
8 6 7 eqger ⊢ S ∈ SubGrp ⁡ G → G ~ QG S Er Base G
9 5 8 syl ⊢ S ∈ NrmSGrp ⁡ G → G ~ QG S Er Base G
10 subgrcl ⊢ S ∈ SubGrp ⁡ G → G ∈ Grp
11 5 10 syl ⊢ S ∈ NrmSGrp ⁡ G → G ∈ Grp
12 eqid ⊢ + G = + G
13 6 7 12 eqgcpbl ⊢ S ∈ NrmSGrp ⁡ G → a G ~ QG S c ∧ b G ~ QG S d → a + G b G ~ QG S c + G d
14 6 12 grpcl ⊢ G ∈ Grp ∧ u ∈ Base G ∧ v ∈ Base G → u + G v ∈ Base G
15 11 14 syl3an1 ⊢ S ∈ NrmSGrp ⁡ G ∧ u ∈ Base G ∧ v ∈ Base G → u + G v ∈ Base G
16 9 adantr ⊢ S ∈ NrmSGrp ⁡ G ∧ u ∈ Base G ∧ v ∈ Base G ∧ w ∈ Base G → G ~ QG S Er Base G
17 11 adantr ⊢ S ∈ NrmSGrp ⁡ G ∧ u ∈ Base G ∧ v ∈ Base G ∧ w ∈ Base G → G ∈ Grp
18 simpr1 ⊢ S ∈ NrmSGrp ⁡ G ∧ u ∈ Base G ∧ v ∈ Base G ∧ w ∈ Base G → u ∈ Base G
19 simpr2 ⊢ S ∈ NrmSGrp ⁡ G ∧ u ∈ Base G ∧ v ∈ Base G ∧ w ∈ Base G → v ∈ Base G
20 17 18 19 14 syl3anc ⊢ S ∈ NrmSGrp ⁡ G ∧ u ∈ Base G ∧ v ∈ Base G ∧ w ∈ Base G → u + G v ∈ Base G
21 simpr3 ⊢ S ∈ NrmSGrp ⁡ G ∧ u ∈ Base G ∧ v ∈ Base G ∧ w ∈ Base G → w ∈ Base G
22 6 12 grpcl ⊢ G ∈ Grp ∧ u + G v ∈ Base G ∧ w ∈ Base G → u + G v + G w ∈ Base G
23 17 20 21 22 syl3anc ⊢ S ∈ NrmSGrp ⁡ G ∧ u ∈ Base G ∧ v ∈ Base G ∧ w ∈ Base G → u + G v + G w ∈ Base G
24 16 23 erref ⊢ S ∈ NrmSGrp ⁡ G ∧ u ∈ Base G ∧ v ∈ Base G ∧ w ∈ Base G → u + G v + G w G ~ QG S u + G v + G w
25 6 12 grpass ⊢ G ∈ Grp ∧ u ∈ Base G ∧ v ∈ Base G ∧ w ∈ Base G → u + G v + G w = u + G v + G w
26 11 25 sylan ⊢ S ∈ NrmSGrp ⁡ G ∧ u ∈ Base G ∧ v ∈ Base G ∧ w ∈ Base G → u + G v + G w = u + G v + G w
27 24 26 breqtrd ⊢ S ∈ NrmSGrp ⁡ G ∧ u ∈ Base G ∧ v ∈ Base G ∧ w ∈ Base G → u + G v + G w G ~ QG S u + G v + G w
28 eqid ⊢ 0 G = 0 G
29 6 28 grpidcl ⊢ G ∈ Grp → 0 G ∈ Base G
30 11 29 syl ⊢ S ∈ NrmSGrp ⁡ G → 0 G ∈ Base G
31 6 12 28 grplid ⊢ G ∈ Grp ∧ u ∈ Base G → 0 G + G u = u
32 11 31 sylan ⊢ S ∈ NrmSGrp ⁡ G ∧ u ∈ Base G → 0 G + G u = u
33 9 adantr ⊢ S ∈ NrmSGrp ⁡ G ∧ u ∈ Base G → G ~ QG S Er Base G
34 simpr ⊢ S ∈ NrmSGrp ⁡ G ∧ u ∈ Base G → u ∈ Base G
35 33 34 erref ⊢ S ∈ NrmSGrp ⁡ G ∧ u ∈ Base G → u G ~ QG S u
36 32 35 eqbrtrd ⊢ S ∈ NrmSGrp ⁡ G ∧ u ∈ Base G → 0 G + G u G ~ QG S u
37 eqid ⊢ inv g ⁡ G = inv g ⁡ G
38 6 37 grpinvcl ⊢ G ∈ Grp ∧ u ∈ Base G → inv g ⁡ G ⁡ u ∈ Base G
39 11 38 sylan ⊢ S ∈ NrmSGrp ⁡ G ∧ u ∈ Base G → inv g ⁡ G ⁡ u ∈ Base G
40 6 12 28 37 grplinv ⊢ G ∈ Grp ∧ u ∈ Base G → inv g ⁡ G ⁡ u + G u = 0 G
41 11 40 sylan ⊢ S ∈ NrmSGrp ⁡ G ∧ u ∈ Base G → inv g ⁡ G ⁡ u + G u = 0 G
42 30 adantr ⊢ S ∈ NrmSGrp ⁡ G ∧ u ∈ Base G → 0 G ∈ Base G
43 33 42 erref ⊢ S ∈ NrmSGrp ⁡ G ∧ u ∈ Base G → 0 G G ~ QG S 0 G
44 41 43 eqbrtrd ⊢ S ∈ NrmSGrp ⁡ G ∧ u ∈ Base G → inv g ⁡ G ⁡ u + G u G ~ QG S 0 G
45 2 3 4 9 11 13 15 27 30 36 39 44 qusgrp2 ⊢ S ∈ NrmSGrp ⁡ G → H ∈ Grp ∧ 0 G G ~ QG S = 0 H
46 45 simpld ⊢ S ∈ NrmSGrp ⁡ G → H ∈ Grp