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 syl5bir
 |-  ( ( 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 )