Metamath Proof Explorer

Theorem qusabl

Description: If Y is a subgroup of the abelian group G , then H = G / Y is an abelian group. (Contributed by Mario Carneiro, 26-Apr-2016)

Ref Expression
Hypothesis qusabl.h 
|- H = ( G /s ( G ~QG S ) )
Assertion qusabl 
|- ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) -> H e. Abel )

Proof

Step Hyp Ref Expression
1 qusabl.h 
 |-  H = ( G /s ( G ~QG S ) )
2 ablnsg 
 |-  ( G e. Abel -> ( NrmSGrp ` G ) = ( SubGrp ` G ) )
3 2 eleq2d 
 |-  ( G e. Abel -> ( S e. ( NrmSGrp ` G ) <-> S e. ( SubGrp ` G ) ) )
4 3 biimpar 
 |-  ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) -> S e. ( NrmSGrp ` G ) )
5 1 qusgrp 
 |-  ( S e. ( NrmSGrp ` G ) -> H e. Grp )
6 4 5 syl 
 |-  ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) -> H e. Grp )
7 vex 
 |-  x e. _V
8 7 elqs 
 |-  ( x e. ( ( Base ` G ) /. ( G ~QG S ) ) <-> E. a e. ( Base ` G ) x = [ a ] ( G ~QG S ) )
9 1 a1i 
 |-  ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) -> H = ( G /s ( G ~QG S ) ) )
10 eqidd 
 |-  ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) -> ( Base ` G ) = ( Base ` G ) )
11 ovexd 
 |-  ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) -> ( G ~QG S ) e. _V )
12 simpl 
 |-  ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) -> G e. Abel )
13 9 10 11 12 qusbas 
 |-  ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) -> ( ( Base ` G ) /. ( G ~QG S ) ) = ( Base ` H ) )
14 13 eleq2d 
 |-  ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) -> ( x e. ( ( Base ` G ) /. ( G ~QG S ) ) <-> x e. ( Base ` H ) ) )
15 8 14 bitr3id 
 |-  ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) -> ( E. a e. ( Base ` G ) x = [ a ] ( G ~QG S ) <-> x e. ( Base ` H ) ) )
16 vex 
 |-  y e. _V
17 16 elqs 
 |-  ( y e. ( ( Base ` G ) /. ( G ~QG S ) ) <-> E. b e. ( Base ` G ) y = [ b ] ( G ~QG S ) )
18 13 eleq2d 
 |-  ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) -> ( y e. ( ( Base ` G ) /. ( G ~QG S ) ) <-> y e. ( Base ` H ) ) )
19 17 18 bitr3id 
 |-  ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) -> ( E. b e. ( Base ` G ) y = [ b ] ( G ~QG S ) <-> y e. ( Base ` H ) ) )
20 15 19 anbi12d 
 |-  ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) -> ( ( E. a e. ( Base ` G ) x = [ a ] ( G ~QG S ) /\ E. b e. ( Base ` G ) y = [ b ] ( G ~QG S ) ) <-> ( x e. ( Base ` H ) /\ y e. ( Base ` H ) ) ) )
21 reeanv 
 |-  ( E. a e. ( Base ` G ) E. b e. ( Base ` G ) ( x = [ a ] ( G ~QG S ) /\ y = [ b ] ( G ~QG S ) ) <-> ( E. a e. ( Base ` G ) x = [ a ] ( G ~QG S ) /\ E. b e. ( Base ` G ) y = [ b ] ( G ~QG S ) ) )
22 eqid 
 |-  ( Base ` G ) = ( Base ` G )
23 eqid 
 |-  ( +g ` G ) = ( +g ` G )
24 22 23 ablcom 
 |-  ( ( G e. Abel /\ a e. ( Base ` G ) /\ b e. ( Base ` G ) ) -> ( a ( +g ` G ) b ) = ( b ( +g ` G ) a ) )
25 24 3expb 
 |-  ( ( G e. Abel /\ ( a e. ( Base ` G ) /\ b e. ( Base ` G ) ) ) -> ( a ( +g ` G ) b ) = ( b ( +g ` G ) a ) )
26 25 adantlr 
 |-  ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ ( a e. ( Base ` G ) /\ b e. ( Base ` G ) ) ) -> ( a ( +g ` G ) b ) = ( b ( +g ` G ) a ) )
27 26 eceq1d 
 |-  ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ ( a e. ( Base ` G ) /\ b e. ( Base ` G ) ) ) -> [ ( a ( +g ` G ) b ) ] ( G ~QG S ) = [ ( b ( +g ` G ) a ) ] ( G ~QG S ) )
28 4 adantr 
 |-  ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ ( a e. ( Base ` G ) /\ b e. ( Base ` G ) ) ) -> S e. ( NrmSGrp ` G ) )
29 simprl 
 |-  ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ ( a e. ( Base ` G ) /\ b e. ( Base ` G ) ) ) -> a e. ( Base ` G ) )
30 simprr 
 |-  ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ ( a e. ( Base ` G ) /\ b e. ( Base ` G ) ) ) -> b e. ( Base ` G ) )
31 eqid 
 |-  ( +g ` H ) = ( +g ` H )
32 1 22 23 31 qusadd 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ a e. ( Base ` G ) /\ b e. ( Base ` G ) ) -> ( [ a ] ( G ~QG S ) ( +g ` H ) [ b ] ( G ~QG S ) ) = [ ( a ( +g ` G ) b ) ] ( G ~QG S ) )
33 28 29 30 32 syl3anc 
 |-  ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ ( a e. ( Base ` G ) /\ b e. ( Base ` G ) ) ) -> ( [ a ] ( G ~QG S ) ( +g ` H ) [ b ] ( G ~QG S ) ) = [ ( a ( +g ` G ) b ) ] ( G ~QG S ) )
34 1 22 23 31 qusadd 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ b e. ( Base ` G ) /\ a e. ( Base ` G ) ) -> ( [ b ] ( G ~QG S ) ( +g ` H ) [ a ] ( G ~QG S ) ) = [ ( b ( +g ` G ) a ) ] ( G ~QG S ) )
35 28 30 29 34 syl3anc 
 |-  ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ ( a e. ( Base ` G ) /\ b e. ( Base ` G ) ) ) -> ( [ b ] ( G ~QG S ) ( +g ` H ) [ a ] ( G ~QG S ) ) = [ ( b ( +g ` G ) a ) ] ( G ~QG S ) )
36 27 33 35 3eqtr4d 
 |-  ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ ( a e. ( Base ` G ) /\ b e. ( Base ` G ) ) ) -> ( [ a ] ( G ~QG S ) ( +g ` H ) [ b ] ( G ~QG S ) ) = ( [ b ] ( G ~QG S ) ( +g ` H ) [ a ] ( G ~QG S ) ) )
37 oveq12 
 |-  ( ( x = [ a ] ( G ~QG S ) /\ y = [ b ] ( G ~QG S ) ) -> ( x ( +g ` H ) y ) = ( [ a ] ( G ~QG S ) ( +g ` H ) [ b ] ( G ~QG S ) ) )
38 oveq12 
 |-  ( ( y = [ b ] ( G ~QG S ) /\ x = [ a ] ( G ~QG S ) ) -> ( y ( +g ` H ) x ) = ( [ b ] ( G ~QG S ) ( +g ` H ) [ a ] ( G ~QG S ) ) )
39 38 ancoms 
 |-  ( ( x = [ a ] ( G ~QG S ) /\ y = [ b ] ( G ~QG S ) ) -> ( y ( +g ` H ) x ) = ( [ b ] ( G ~QG S ) ( +g ` H ) [ a ] ( G ~QG S ) ) )
40 37 39 eqeq12d 
 |-  ( ( x = [ a ] ( G ~QG S ) /\ y = [ b ] ( G ~QG S ) ) -> ( ( x ( +g ` H ) y ) = ( y ( +g ` H ) x ) <-> ( [ a ] ( G ~QG S ) ( +g ` H ) [ b ] ( G ~QG S ) ) = ( [ b ] ( G ~QG S ) ( +g ` H ) [ a ] ( G ~QG S ) ) ) )
41 36 40 syl5ibrcom 
 |-  ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ ( a e. ( Base ` G ) /\ b e. ( Base ` G ) ) ) -> ( ( x = [ a ] ( G ~QG S ) /\ y = [ b ] ( G ~QG S ) ) -> ( x ( +g ` H ) y ) = ( y ( +g ` H ) x ) ) )
42 41 rexlimdvva 
 |-  ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) -> ( E. a e. ( Base ` G ) E. b e. ( Base ` G ) ( x = [ a ] ( G ~QG S ) /\ y = [ b ] ( G ~QG S ) ) -> ( x ( +g ` H ) y ) = ( y ( +g ` H ) x ) ) )
43 21 42 biimtrrid 
 |-  ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) -> ( ( E. a e. ( Base ` G ) x = [ a ] ( G ~QG S ) /\ E. b e. ( Base ` G ) y = [ b ] ( G ~QG S ) ) -> ( x ( +g ` H ) y ) = ( y ( +g ` H ) x ) ) )
44 20 43 sylbird 
 |-  ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) -> ( ( x e. ( Base ` H ) /\ y e. ( Base ` H ) ) -> ( x ( +g ` H ) y ) = ( y ( +g ` H ) x ) ) )
45 44 ralrimivv 
 |-  ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) -> A. x e. ( Base ` H ) A. y e. ( Base ` H ) ( x ( +g ` H ) y ) = ( y ( +g ` H ) x ) )
46 eqid 
 |-  ( Base ` H ) = ( Base ` H )
47 46 31 isabl2 
 |-  ( H e. Abel <-> ( H e. Grp /\ A. x e. ( Base ` H ) A. y e. ( Base ` H ) ( x ( +g ` H ) y ) = ( y ( +g ` H ) x ) ) )
48 6 45 47 sylanbrc 
 |-  ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) -> H e. Abel )