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 /s ( G ~QG S ) )
Assertion qusgrp 
|- ( S e. ( NrmSGrp ` G ) -> H e. Grp )

Proof

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