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 ⊢ 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑆 ) )
Assertion qusgrp ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝐻 ∈ Grp )

Proof

Step Hyp Ref Expression
1 qusgrp.h ⊢ 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑆 ) )
2 1 a1i ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑆 ) ) )
3 eqidd ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
4 eqidd ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) )
5 nsgsubg ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
6 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
7 eqid ⊢ ( 𝐺 ~QG 𝑆 ) = ( 𝐺 ~QG 𝑆 )
8 6 7 eqger ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ~QG 𝑆 ) Er ( Base ‘ 𝐺 ) )
9 5 8 syl ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → ( 𝐺 ~QG 𝑆 ) Er ( Base ‘ 𝐺 ) )
10 subgrcl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
11 5 10 syl ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
12 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
13 6 7 12 eqgcpbl ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → ( ( 𝑎 ( 𝐺 ~QG 𝑆 ) 𝑐 ∧ 𝑏 ( 𝐺 ~QG 𝑆 ) 𝑑 ) → ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ( 𝐺 ~QG 𝑆 ) ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ) )
14 6 12 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑢 ( +g ‘ 𝐺 ) 𝑣 ) ∈ ( Base ‘ 𝐺 ) )
15 11 14 syl3an1 ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑢 ( +g ‘ 𝐺 ) 𝑣 ) ∈ ( Base ‘ 𝐺 ) )
16 9 adantr ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ∧ 𝑤 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝐺 ~QG 𝑆 ) Er ( Base ‘ 𝐺 ) )
17 11 adantr ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ∧ 𝑤 ∈ ( Base ‘ 𝐺 ) ) ) → 𝐺 ∈ Grp )
18 simpr1 ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ∧ 𝑤 ∈ ( Base ‘ 𝐺 ) ) ) → 𝑢 ∈ ( Base ‘ 𝐺 ) )
19 simpr2 ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ∧ 𝑤 ∈ ( Base ‘ 𝐺 ) ) ) → 𝑣 ∈ ( Base ‘ 𝐺 ) )
20 17 18 19 14 syl3anc ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ∧ 𝑤 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑢 ( +g ‘ 𝐺 ) 𝑣 ) ∈ ( Base ‘ 𝐺 ) )
21 simpr3 ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ∧ 𝑤 ∈ ( Base ‘ 𝐺 ) ) ) → 𝑤 ∈ ( Base ‘ 𝐺 ) )
22 6 12 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑢 ( +g ‘ 𝐺 ) 𝑣 ) ∈ ( Base ‘ 𝐺 ) ∧ 𝑤 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑢 ( +g ‘ 𝐺 ) 𝑣 ) ( +g ‘ 𝐺 ) 𝑤 ) ∈ ( Base ‘ 𝐺 ) )
23 17 20 21 22 syl3anc ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ∧ 𝑤 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑢 ( +g ‘ 𝐺 ) 𝑣 ) ( +g ‘ 𝐺 ) 𝑤 ) ∈ ( Base ‘ 𝐺 ) )
24 16 23 erref ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ∧ 𝑤 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑢 ( +g ‘ 𝐺 ) 𝑣 ) ( +g ‘ 𝐺 ) 𝑤 ) ( 𝐺 ~QG 𝑆 ) ( ( 𝑢 ( +g ‘ 𝐺 ) 𝑣 ) ( +g ‘ 𝐺 ) 𝑤 ) )
25 6 12 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ∧ 𝑤 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑢 ( +g ‘ 𝐺 ) 𝑣 ) ( +g ‘ 𝐺 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐺 ) ( 𝑣 ( +g ‘ 𝐺 ) 𝑤 ) ) )
26 11 25 sylan ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ∧ 𝑤 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑢 ( +g ‘ 𝐺 ) 𝑣 ) ( +g ‘ 𝐺 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐺 ) ( 𝑣 ( +g ‘ 𝐺 ) 𝑤 ) ) )
27 24 26 breqtrd ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝑢 ∈ ( Base ‘ 𝐺 ) ∧ 𝑣 ∈ ( Base ‘ 𝐺 ) ∧ 𝑤 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑢 ( +g ‘ 𝐺 ) 𝑣 ) ( +g ‘ 𝐺 ) 𝑤 ) ( 𝐺 ~QG 𝑆 ) ( 𝑢 ( +g ‘ 𝐺 ) ( 𝑣 ( +g ‘ 𝐺 ) 𝑤 ) ) )
28 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
29 6 28 grpidcl ⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) )
30 11 29 syl ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) )
31 6 12 28 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑢 ∈ ( Base ‘ 𝐺 ) ) → ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) 𝑢 ) = 𝑢 )
32 11 31 sylan ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑢 ∈ ( Base ‘ 𝐺 ) ) → ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) 𝑢 ) = 𝑢 )
33 9 adantr ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑢 ∈ ( Base ‘ 𝐺 ) ) → ( 𝐺 ~QG 𝑆 ) Er ( Base ‘ 𝐺 ) )
34 simpr ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑢 ∈ ( Base ‘ 𝐺 ) ) → 𝑢 ∈ ( Base ‘ 𝐺 ) )
35 33 34 erref ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑢 ∈ ( Base ‘ 𝐺 ) ) → 𝑢 ( 𝐺 ~QG 𝑆 ) 𝑢 )
36 32 35 eqbrtrd ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑢 ∈ ( Base ‘ 𝐺 ) ) → ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) 𝑢 ) ( 𝐺 ~QG 𝑆 ) 𝑢 )
37 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
38 6 37 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑢 ∈ ( Base ‘ 𝐺 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑢 ) ∈ ( Base ‘ 𝐺 ) )
39 11 38 sylan ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑢 ∈ ( Base ‘ 𝐺 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑢 ) ∈ ( Base ‘ 𝐺 ) )
40 6 12 28 37 grplinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑢 ∈ ( Base ‘ 𝐺 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑢 ) ( +g ‘ 𝐺 ) 𝑢 ) = ( 0g ‘ 𝐺 ) )
41 11 40 sylan ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑢 ∈ ( Base ‘ 𝐺 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑢 ) ( +g ‘ 𝐺 ) 𝑢 ) = ( 0g ‘ 𝐺 ) )
42 30 adantr ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑢 ∈ ( Base ‘ 𝐺 ) ) → ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) )
43 33 42 erref ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑢 ∈ ( Base ‘ 𝐺 ) ) → ( 0g ‘ 𝐺 ) ( 𝐺 ~QG 𝑆 ) ( 0g ‘ 𝐺 ) )
44 41 43 eqbrtrd ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑢 ∈ ( Base ‘ 𝐺 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑢 ) ( +g ‘ 𝐺 ) 𝑢 ) ( 𝐺 ~QG 𝑆 ) ( 0g ‘ 𝐺 ) )
45 2 3 4 9 11 13 15 27 30 36 39 44 qusgrp2 ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → ( 𝐻 ∈ Grp ∧ [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑆 ) = ( 0g ‘ 𝐻 ) ) )
46 45 simpld ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝐻 ∈ Grp )