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