Step |
Hyp |
Ref |
Expression |
1 |
|
qusker.b |
|- V = ( Base ` M ) |
2 |
|
qusker.f |
|- F = ( x e. V |-> [ x ] ( M ~QG G ) ) |
3 |
|
qusker.n |
|- N = ( M /s ( M ~QG G ) ) |
4 |
|
qusker.1 |
|- .0. = ( 0g ` N ) |
5 |
3
|
a1i |
|- ( G e. ( NrmSGrp ` M ) -> N = ( M /s ( M ~QG G ) ) ) |
6 |
1
|
a1i |
|- ( G e. ( NrmSGrp ` M ) -> V = ( Base ` M ) ) |
7 |
|
ovex |
|- ( M ~QG G ) e. _V |
8 |
7
|
a1i |
|- ( G e. ( NrmSGrp ` M ) -> ( M ~QG G ) e. _V ) |
9 |
|
nsgsubg |
|- ( G e. ( NrmSGrp ` M ) -> G e. ( SubGrp ` M ) ) |
10 |
|
subgrcl |
|- ( G e. ( SubGrp ` M ) -> M e. Grp ) |
11 |
9 10
|
syl |
|- ( G e. ( NrmSGrp ` M ) -> M e. Grp ) |
12 |
5 6 2 8 11
|
quslem |
|- ( G e. ( NrmSGrp ` M ) -> F : V -onto-> ( V /. ( M ~QG G ) ) ) |
13 |
|
fofn |
|- ( F : V -onto-> ( V /. ( M ~QG G ) ) -> F Fn V ) |
14 |
|
fniniseg2 |
|- ( F Fn V -> ( `' F " { .0. } ) = { y e. V | ( F ` y ) = .0. } ) |
15 |
12 13 14
|
3syl |
|- ( G e. ( NrmSGrp ` M ) -> ( `' F " { .0. } ) = { y e. V | ( F ` y ) = .0. } ) |
16 |
|
eqid |
|- ( 0g ` M ) = ( 0g ` M ) |
17 |
3 16
|
qus0 |
|- ( G e. ( NrmSGrp ` M ) -> [ ( 0g ` M ) ] ( M ~QG G ) = ( 0g ` N ) ) |
18 |
4 17
|
eqtr4id |
|- ( G e. ( NrmSGrp ` M ) -> .0. = [ ( 0g ` M ) ] ( M ~QG G ) ) |
19 |
|
eceq1 |
|- ( x = y -> [ x ] ( M ~QG G ) = [ y ] ( M ~QG G ) ) |
20 |
|
ecexg |
|- ( ( M ~QG G ) e. _V -> [ y ] ( M ~QG G ) e. _V ) |
21 |
7 20
|
ax-mp |
|- [ y ] ( M ~QG G ) e. _V |
22 |
19 2 21
|
fvmpt |
|- ( y e. V -> ( F ` y ) = [ y ] ( M ~QG G ) ) |
23 |
18 22
|
eqeqan12d |
|- ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( .0. = ( F ` y ) <-> [ ( 0g ` M ) ] ( M ~QG G ) = [ y ] ( M ~QG G ) ) ) |
24 |
|
eqcom |
|- ( .0. = ( F ` y ) <-> ( F ` y ) = .0. ) |
25 |
24
|
a1i |
|- ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( .0. = ( F ` y ) <-> ( F ` y ) = .0. ) ) |
26 |
|
simpl |
|- ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> G e. ( NrmSGrp ` M ) ) |
27 |
|
simpr |
|- ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> y e. V ) |
28 |
1 16
|
grpidcl |
|- ( M e. Grp -> ( 0g ` M ) e. V ) |
29 |
26 11 28
|
3syl |
|- ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( 0g ` M ) e. V ) |
30 |
1
|
subgss |
|- ( G e. ( SubGrp ` M ) -> G C_ V ) |
31 |
9 30
|
syl |
|- ( G e. ( NrmSGrp ` M ) -> G C_ V ) |
32 |
|
eqid |
|- ( invg ` M ) = ( invg ` M ) |
33 |
|
eqid |
|- ( +g ` M ) = ( +g ` M ) |
34 |
|
eqid |
|- ( M ~QG G ) = ( M ~QG G ) |
35 |
1 32 33 34
|
eqgval |
|- ( ( M e. Grp /\ G C_ V ) -> ( ( 0g ` M ) ( M ~QG G ) y <-> ( ( 0g ` M ) e. V /\ y e. V /\ ( ( ( invg ` M ) ` ( 0g ` M ) ) ( +g ` M ) y ) e. G ) ) ) |
36 |
11 31 35
|
syl2anc |
|- ( G e. ( NrmSGrp ` M ) -> ( ( 0g ` M ) ( M ~QG G ) y <-> ( ( 0g ` M ) e. V /\ y e. V /\ ( ( ( invg ` M ) ` ( 0g ` M ) ) ( +g ` M ) y ) e. G ) ) ) |
37 |
36
|
adantr |
|- ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( ( 0g ` M ) ( M ~QG G ) y <-> ( ( 0g ` M ) e. V /\ y e. V /\ ( ( ( invg ` M ) ` ( 0g ` M ) ) ( +g ` M ) y ) e. G ) ) ) |
38 |
|
df-3an |
|- ( ( ( 0g ` M ) e. V /\ y e. V /\ ( ( ( invg ` M ) ` ( 0g ` M ) ) ( +g ` M ) y ) e. G ) <-> ( ( ( 0g ` M ) e. V /\ y e. V ) /\ ( ( ( invg ` M ) ` ( 0g ` M ) ) ( +g ` M ) y ) e. G ) ) |
39 |
38
|
biancomi |
|- ( ( ( 0g ` M ) e. V /\ y e. V /\ ( ( ( invg ` M ) ` ( 0g ` M ) ) ( +g ` M ) y ) e. G ) <-> ( ( ( ( invg ` M ) ` ( 0g ` M ) ) ( +g ` M ) y ) e. G /\ ( ( 0g ` M ) e. V /\ y e. V ) ) ) |
40 |
37 39
|
bitrdi |
|- ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( ( 0g ` M ) ( M ~QG G ) y <-> ( ( ( ( invg ` M ) ` ( 0g ` M ) ) ( +g ` M ) y ) e. G /\ ( ( 0g ` M ) e. V /\ y e. V ) ) ) ) |
41 |
40
|
rbaibd |
|- ( ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) /\ ( ( 0g ` M ) e. V /\ y e. V ) ) -> ( ( 0g ` M ) ( M ~QG G ) y <-> ( ( ( invg ` M ) ` ( 0g ` M ) ) ( +g ` M ) y ) e. G ) ) |
42 |
26 27 29 27 41
|
syl22anc |
|- ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( ( 0g ` M ) ( M ~QG G ) y <-> ( ( ( invg ` M ) ` ( 0g ` M ) ) ( +g ` M ) y ) e. G ) ) |
43 |
1 34
|
eqger |
|- ( G e. ( SubGrp ` M ) -> ( M ~QG G ) Er V ) |
44 |
9 43
|
syl |
|- ( G e. ( NrmSGrp ` M ) -> ( M ~QG G ) Er V ) |
45 |
44
|
adantr |
|- ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( M ~QG G ) Er V ) |
46 |
45 27
|
erth2 |
|- ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( ( 0g ` M ) ( M ~QG G ) y <-> [ ( 0g ` M ) ] ( M ~QG G ) = [ y ] ( M ~QG G ) ) ) |
47 |
16 32
|
grpinvid |
|- ( M e. Grp -> ( ( invg ` M ) ` ( 0g ` M ) ) = ( 0g ` M ) ) |
48 |
26 11 47
|
3syl |
|- ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( ( invg ` M ) ` ( 0g ` M ) ) = ( 0g ` M ) ) |
49 |
48
|
oveq1d |
|- ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( ( ( invg ` M ) ` ( 0g ` M ) ) ( +g ` M ) y ) = ( ( 0g ` M ) ( +g ` M ) y ) ) |
50 |
1 33 16
|
grplid |
|- ( ( M e. Grp /\ y e. V ) -> ( ( 0g ` M ) ( +g ` M ) y ) = y ) |
51 |
11 50
|
sylan |
|- ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( ( 0g ` M ) ( +g ` M ) y ) = y ) |
52 |
49 51
|
eqtrd |
|- ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( ( ( invg ` M ) ` ( 0g ` M ) ) ( +g ` M ) y ) = y ) |
53 |
52
|
eleq1d |
|- ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( ( ( ( invg ` M ) ` ( 0g ` M ) ) ( +g ` M ) y ) e. G <-> y e. G ) ) |
54 |
42 46 53
|
3bitr3d |
|- ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( [ ( 0g ` M ) ] ( M ~QG G ) = [ y ] ( M ~QG G ) <-> y e. G ) ) |
55 |
23 25 54
|
3bitr3d |
|- ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( ( F ` y ) = .0. <-> y e. G ) ) |
56 |
55
|
rabbidva |
|- ( G e. ( NrmSGrp ` M ) -> { y e. V | ( F ` y ) = .0. } = { y e. V | y e. G } ) |
57 |
|
dfss7 |
|- ( G C_ V <-> { y e. V | y e. G } = G ) |
58 |
31 57
|
sylib |
|- ( G e. ( NrmSGrp ` M ) -> { y e. V | y e. G } = G ) |
59 |
15 56 58
|
3eqtrd |
|- ( G e. ( NrmSGrp ` M ) -> ( `' F " { .0. } ) = G ) |