Step |
Hyp |
Ref |
Expression |
1 |
|
pgpfac1.k |
|- K = ( mrCls ` ( SubGrp ` G ) ) |
2 |
|
pgpfac1.s |
|- S = ( K ` { A } ) |
3 |
|
pgpfac1.b |
|- B = ( Base ` G ) |
4 |
|
pgpfac1.o |
|- O = ( od ` G ) |
5 |
|
pgpfac1.e |
|- E = ( gEx ` G ) |
6 |
|
pgpfac1.z |
|- .0. = ( 0g ` G ) |
7 |
|
pgpfac1.l |
|- .(+) = ( LSSum ` G ) |
8 |
|
pgpfac1.p |
|- ( ph -> P pGrp G ) |
9 |
|
pgpfac1.g |
|- ( ph -> G e. Abel ) |
10 |
|
pgpfac1.n |
|- ( ph -> B e. Fin ) |
11 |
|
pgpfac1.oe |
|- ( ph -> ( O ` A ) = E ) |
12 |
|
pgpfac1.u |
|- ( ph -> U e. ( SubGrp ` G ) ) |
13 |
|
pgpfac1.au |
|- ( ph -> A e. U ) |
14 |
|
pgpfac1.3 |
|- ( ph -> A. s e. ( SubGrp ` G ) ( ( s C. U /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) |
15 |
|
pwfi |
|- ( B e. Fin <-> ~P B e. Fin ) |
16 |
10 15
|
sylib |
|- ( ph -> ~P B e. Fin ) |
17 |
16
|
adantr |
|- ( ( ph /\ S C. U ) -> ~P B e. Fin ) |
18 |
3
|
subgss |
|- ( v e. ( SubGrp ` G ) -> v C_ B ) |
19 |
18
|
3ad2ant2 |
|- ( ( ( ph /\ S C. U ) /\ v e. ( SubGrp ` G ) /\ ( v C. U /\ A e. v ) ) -> v C_ B ) |
20 |
|
velpw |
|- ( v e. ~P B <-> v C_ B ) |
21 |
19 20
|
sylibr |
|- ( ( ( ph /\ S C. U ) /\ v e. ( SubGrp ` G ) /\ ( v C. U /\ A e. v ) ) -> v e. ~P B ) |
22 |
21
|
rabssdv |
|- ( ( ph /\ S C. U ) -> { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } C_ ~P B ) |
23 |
17 22
|
ssfid |
|- ( ( ph /\ S C. U ) -> { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } e. Fin ) |
24 |
|
finnum |
|- ( { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } e. Fin -> { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } e. dom card ) |
25 |
23 24
|
syl |
|- ( ( ph /\ S C. U ) -> { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } e. dom card ) |
26 |
|
ablgrp |
|- ( G e. Abel -> G e. Grp ) |
27 |
9 26
|
syl |
|- ( ph -> G e. Grp ) |
28 |
3
|
subgacs |
|- ( G e. Grp -> ( SubGrp ` G ) e. ( ACS ` B ) ) |
29 |
|
acsmre |
|- ( ( SubGrp ` G ) e. ( ACS ` B ) -> ( SubGrp ` G ) e. ( Moore ` B ) ) |
30 |
27 28 29
|
3syl |
|- ( ph -> ( SubGrp ` G ) e. ( Moore ` B ) ) |
31 |
3
|
subgss |
|- ( U e. ( SubGrp ` G ) -> U C_ B ) |
32 |
12 31
|
syl |
|- ( ph -> U C_ B ) |
33 |
32 13
|
sseldd |
|- ( ph -> A e. B ) |
34 |
1
|
mrcsncl |
|- ( ( ( SubGrp ` G ) e. ( Moore ` B ) /\ A e. B ) -> ( K ` { A } ) e. ( SubGrp ` G ) ) |
35 |
30 33 34
|
syl2anc |
|- ( ph -> ( K ` { A } ) e. ( SubGrp ` G ) ) |
36 |
2 35
|
eqeltrid |
|- ( ph -> S e. ( SubGrp ` G ) ) |
37 |
36
|
adantr |
|- ( ( ph /\ S C. U ) -> S e. ( SubGrp ` G ) ) |
38 |
|
simpr |
|- ( ( ph /\ S C. U ) -> S C. U ) |
39 |
13
|
snssd |
|- ( ph -> { A } C_ U ) |
40 |
39 32
|
sstrd |
|- ( ph -> { A } C_ B ) |
41 |
30 1 40
|
mrcssidd |
|- ( ph -> { A } C_ ( K ` { A } ) ) |
42 |
41 2
|
sseqtrrdi |
|- ( ph -> { A } C_ S ) |
43 |
|
snssg |
|- ( A e. B -> ( A e. S <-> { A } C_ S ) ) |
44 |
33 43
|
syl |
|- ( ph -> ( A e. S <-> { A } C_ S ) ) |
45 |
42 44
|
mpbird |
|- ( ph -> A e. S ) |
46 |
45
|
adantr |
|- ( ( ph /\ S C. U ) -> A e. S ) |
47 |
|
psseq1 |
|- ( v = S -> ( v C. U <-> S C. U ) ) |
48 |
|
eleq2 |
|- ( v = S -> ( A e. v <-> A e. S ) ) |
49 |
47 48
|
anbi12d |
|- ( v = S -> ( ( v C. U /\ A e. v ) <-> ( S C. U /\ A e. S ) ) ) |
50 |
49
|
rspcev |
|- ( ( S e. ( SubGrp ` G ) /\ ( S C. U /\ A e. S ) ) -> E. v e. ( SubGrp ` G ) ( v C. U /\ A e. v ) ) |
51 |
37 38 46 50
|
syl12anc |
|- ( ( ph /\ S C. U ) -> E. v e. ( SubGrp ` G ) ( v C. U /\ A e. v ) ) |
52 |
|
rabn0 |
|- ( { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } =/= (/) <-> E. v e. ( SubGrp ` G ) ( v C. U /\ A e. v ) ) |
53 |
51 52
|
sylibr |
|- ( ( ph /\ S C. U ) -> { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } =/= (/) ) |
54 |
|
simpr1 |
|- ( ( ( ph /\ S C. U ) /\ ( u C_ { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } /\ u =/= (/) /\ [C.] Or u ) ) -> u C_ { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } ) |
55 |
|
simpr2 |
|- ( ( ( ph /\ S C. U ) /\ ( u C_ { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } /\ u =/= (/) /\ [C.] Or u ) ) -> u =/= (/) ) |
56 |
23
|
adantr |
|- ( ( ( ph /\ S C. U ) /\ ( u C_ { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } /\ u =/= (/) /\ [C.] Or u ) ) -> { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } e. Fin ) |
57 |
56 54
|
ssfid |
|- ( ( ( ph /\ S C. U ) /\ ( u C_ { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } /\ u =/= (/) /\ [C.] Or u ) ) -> u e. Fin ) |
58 |
|
simpr3 |
|- ( ( ( ph /\ S C. U ) /\ ( u C_ { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } /\ u =/= (/) /\ [C.] Or u ) ) -> [C.] Or u ) |
59 |
|
fin1a2lem10 |
|- ( ( u =/= (/) /\ u e. Fin /\ [C.] Or u ) -> U. u e. u ) |
60 |
55 57 58 59
|
syl3anc |
|- ( ( ( ph /\ S C. U ) /\ ( u C_ { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } /\ u =/= (/) /\ [C.] Or u ) ) -> U. u e. u ) |
61 |
54 60
|
sseldd |
|- ( ( ( ph /\ S C. U ) /\ ( u C_ { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } /\ u =/= (/) /\ [C.] Or u ) ) -> U. u e. { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } ) |
62 |
61
|
ex |
|- ( ( ph /\ S C. U ) -> ( ( u C_ { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } /\ u =/= (/) /\ [C.] Or u ) -> U. u e. { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } ) ) |
63 |
62
|
alrimiv |
|- ( ( ph /\ S C. U ) -> A. u ( ( u C_ { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } /\ u =/= (/) /\ [C.] Or u ) -> U. u e. { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } ) ) |
64 |
|
zornn0g |
|- ( ( { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } e. dom card /\ { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } =/= (/) /\ A. u ( ( u C_ { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } /\ u =/= (/) /\ [C.] Or u ) -> U. u e. { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } ) ) -> E. s e. { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } A. w e. { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } -. s C. w ) |
65 |
25 53 63 64
|
syl3anc |
|- ( ( ph /\ S C. U ) -> E. s e. { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } A. w e. { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } -. s C. w ) |
66 |
|
psseq1 |
|- ( v = w -> ( v C. U <-> w C. U ) ) |
67 |
|
eleq2 |
|- ( v = w -> ( A e. v <-> A e. w ) ) |
68 |
66 67
|
anbi12d |
|- ( v = w -> ( ( v C. U /\ A e. v ) <-> ( w C. U /\ A e. w ) ) ) |
69 |
68
|
ralrab |
|- ( A. w e. { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } -. s C. w <-> A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) |
70 |
69
|
rexbii |
|- ( E. s e. { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } A. w e. { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } -. s C. w <-> E. s e. { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) |
71 |
65 70
|
sylib |
|- ( ( ph /\ S C. U ) -> E. s e. { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) |
72 |
71
|
ex |
|- ( ph -> ( S C. U -> E. s e. { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) ) |
73 |
|
psseq1 |
|- ( v = s -> ( v C. U <-> s C. U ) ) |
74 |
|
eleq2 |
|- ( v = s -> ( A e. v <-> A e. s ) ) |
75 |
73 74
|
anbi12d |
|- ( v = s -> ( ( v C. U /\ A e. v ) <-> ( s C. U /\ A e. s ) ) ) |
76 |
75
|
ralrab |
|- ( A. s e. { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) <-> A. s e. ( SubGrp ` G ) ( ( s C. U /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) |
77 |
14 76
|
sylibr |
|- ( ph -> A. s e. { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) |
78 |
|
r19.29 |
|- ( ( A. s e. { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) /\ E. s e. { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) -> E. s e. { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } ( E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) /\ A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) ) |
79 |
75
|
elrab |
|- ( s e. { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } <-> ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) |
80 |
|
ineq2 |
|- ( t = v -> ( S i^i t ) = ( S i^i v ) ) |
81 |
80
|
eqeq1d |
|- ( t = v -> ( ( S i^i t ) = { .0. } <-> ( S i^i v ) = { .0. } ) ) |
82 |
|
oveq2 |
|- ( t = v -> ( S .(+) t ) = ( S .(+) v ) ) |
83 |
82
|
eqeq1d |
|- ( t = v -> ( ( S .(+) t ) = s <-> ( S .(+) v ) = s ) ) |
84 |
81 83
|
anbi12d |
|- ( t = v -> ( ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) <-> ( ( S i^i v ) = { .0. } /\ ( S .(+) v ) = s ) ) ) |
85 |
84
|
cbvrexvw |
|- ( E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) <-> E. v e. ( SubGrp ` G ) ( ( S i^i v ) = { .0. } /\ ( S .(+) v ) = s ) ) |
86 |
|
simprrl |
|- ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) -> s C. U ) |
87 |
86
|
ad2antrr |
|- ( ( ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) /\ v e. ( SubGrp ` G ) ) /\ ( ( S i^i v ) = { .0. } /\ ( S .(+) v ) = s /\ A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) ) -> s C. U ) |
88 |
|
simpr2 |
|- ( ( ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) /\ v e. ( SubGrp ` G ) ) /\ ( ( S i^i v ) = { .0. } /\ ( S .(+) v ) = s /\ A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) ) -> ( S .(+) v ) = s ) |
89 |
88
|
psseq1d |
|- ( ( ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) /\ v e. ( SubGrp ` G ) ) /\ ( ( S i^i v ) = { .0. } /\ ( S .(+) v ) = s /\ A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) ) -> ( ( S .(+) v ) C. U <-> s C. U ) ) |
90 |
87 89
|
mpbird |
|- ( ( ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) /\ v e. ( SubGrp ` G ) ) /\ ( ( S i^i v ) = { .0. } /\ ( S .(+) v ) = s /\ A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) ) -> ( S .(+) v ) C. U ) |
91 |
|
pssdif |
|- ( ( S .(+) v ) C. U -> ( U \ ( S .(+) v ) ) =/= (/) ) |
92 |
|
n0 |
|- ( ( U \ ( S .(+) v ) ) =/= (/) <-> E. b b e. ( U \ ( S .(+) v ) ) ) |
93 |
91 92
|
sylib |
|- ( ( S .(+) v ) C. U -> E. b b e. ( U \ ( S .(+) v ) ) ) |
94 |
90 93
|
syl |
|- ( ( ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) /\ v e. ( SubGrp ` G ) ) /\ ( ( S i^i v ) = { .0. } /\ ( S .(+) v ) = s /\ A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) ) -> E. b b e. ( U \ ( S .(+) v ) ) ) |
95 |
8
|
ad3antrrr |
|- ( ( ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) /\ v e. ( SubGrp ` G ) ) /\ ( ( ( S i^i v ) = { .0. } /\ ( S .(+) v ) = s /\ A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) /\ b e. ( U \ ( S .(+) v ) ) ) ) -> P pGrp G ) |
96 |
9
|
ad3antrrr |
|- ( ( ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) /\ v e. ( SubGrp ` G ) ) /\ ( ( ( S i^i v ) = { .0. } /\ ( S .(+) v ) = s /\ A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) /\ b e. ( U \ ( S .(+) v ) ) ) ) -> G e. Abel ) |
97 |
10
|
ad3antrrr |
|- ( ( ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) /\ v e. ( SubGrp ` G ) ) /\ ( ( ( S i^i v ) = { .0. } /\ ( S .(+) v ) = s /\ A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) /\ b e. ( U \ ( S .(+) v ) ) ) ) -> B e. Fin ) |
98 |
11
|
ad3antrrr |
|- ( ( ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) /\ v e. ( SubGrp ` G ) ) /\ ( ( ( S i^i v ) = { .0. } /\ ( S .(+) v ) = s /\ A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) /\ b e. ( U \ ( S .(+) v ) ) ) ) -> ( O ` A ) = E ) |
99 |
12
|
ad3antrrr |
|- ( ( ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) /\ v e. ( SubGrp ` G ) ) /\ ( ( ( S i^i v ) = { .0. } /\ ( S .(+) v ) = s /\ A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) /\ b e. ( U \ ( S .(+) v ) ) ) ) -> U e. ( SubGrp ` G ) ) |
100 |
13
|
ad3antrrr |
|- ( ( ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) /\ v e. ( SubGrp ` G ) ) /\ ( ( ( S i^i v ) = { .0. } /\ ( S .(+) v ) = s /\ A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) /\ b e. ( U \ ( S .(+) v ) ) ) ) -> A e. U ) |
101 |
|
simplr |
|- ( ( ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) /\ v e. ( SubGrp ` G ) ) /\ ( ( ( S i^i v ) = { .0. } /\ ( S .(+) v ) = s /\ A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) /\ b e. ( U \ ( S .(+) v ) ) ) ) -> v e. ( SubGrp ` G ) ) |
102 |
|
simprl1 |
|- ( ( ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) /\ v e. ( SubGrp ` G ) ) /\ ( ( ( S i^i v ) = { .0. } /\ ( S .(+) v ) = s /\ A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) /\ b e. ( U \ ( S .(+) v ) ) ) ) -> ( S i^i v ) = { .0. } ) |
103 |
90
|
adantrr |
|- ( ( ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) /\ v e. ( SubGrp ` G ) ) /\ ( ( ( S i^i v ) = { .0. } /\ ( S .(+) v ) = s /\ A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) /\ b e. ( U \ ( S .(+) v ) ) ) ) -> ( S .(+) v ) C. U ) |
104 |
103
|
pssssd |
|- ( ( ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) /\ v e. ( SubGrp ` G ) ) /\ ( ( ( S i^i v ) = { .0. } /\ ( S .(+) v ) = s /\ A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) /\ b e. ( U \ ( S .(+) v ) ) ) ) -> ( S .(+) v ) C_ U ) |
105 |
|
simprl3 |
|- ( ( ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) /\ v e. ( SubGrp ` G ) ) /\ ( ( ( S i^i v ) = { .0. } /\ ( S .(+) v ) = s /\ A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) /\ b e. ( U \ ( S .(+) v ) ) ) ) -> A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) |
106 |
88
|
adantrr |
|- ( ( ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) /\ v e. ( SubGrp ` G ) ) /\ ( ( ( S i^i v ) = { .0. } /\ ( S .(+) v ) = s /\ A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) /\ b e. ( U \ ( S .(+) v ) ) ) ) -> ( S .(+) v ) = s ) |
107 |
|
psseq1 |
|- ( ( S .(+) v ) = s -> ( ( S .(+) v ) C. y <-> s C. y ) ) |
108 |
107
|
notbid |
|- ( ( S .(+) v ) = s -> ( -. ( S .(+) v ) C. y <-> -. s C. y ) ) |
109 |
108
|
imbi2d |
|- ( ( S .(+) v ) = s -> ( ( ( y C. U /\ A e. y ) -> -. ( S .(+) v ) C. y ) <-> ( ( y C. U /\ A e. y ) -> -. s C. y ) ) ) |
110 |
109
|
ralbidv |
|- ( ( S .(+) v ) = s -> ( A. y e. ( SubGrp ` G ) ( ( y C. U /\ A e. y ) -> -. ( S .(+) v ) C. y ) <-> A. y e. ( SubGrp ` G ) ( ( y C. U /\ A e. y ) -> -. s C. y ) ) ) |
111 |
|
psseq1 |
|- ( y = w -> ( y C. U <-> w C. U ) ) |
112 |
|
eleq2 |
|- ( y = w -> ( A e. y <-> A e. w ) ) |
113 |
111 112
|
anbi12d |
|- ( y = w -> ( ( y C. U /\ A e. y ) <-> ( w C. U /\ A e. w ) ) ) |
114 |
|
psseq2 |
|- ( y = w -> ( s C. y <-> s C. w ) ) |
115 |
114
|
notbid |
|- ( y = w -> ( -. s C. y <-> -. s C. w ) ) |
116 |
113 115
|
imbi12d |
|- ( y = w -> ( ( ( y C. U /\ A e. y ) -> -. s C. y ) <-> ( ( w C. U /\ A e. w ) -> -. s C. w ) ) ) |
117 |
116
|
cbvralvw |
|- ( A. y e. ( SubGrp ` G ) ( ( y C. U /\ A e. y ) -> -. s C. y ) <-> A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) |
118 |
110 117
|
bitrdi |
|- ( ( S .(+) v ) = s -> ( A. y e. ( SubGrp ` G ) ( ( y C. U /\ A e. y ) -> -. ( S .(+) v ) C. y ) <-> A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) ) |
119 |
106 118
|
syl |
|- ( ( ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) /\ v e. ( SubGrp ` G ) ) /\ ( ( ( S i^i v ) = { .0. } /\ ( S .(+) v ) = s /\ A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) /\ b e. ( U \ ( S .(+) v ) ) ) ) -> ( A. y e. ( SubGrp ` G ) ( ( y C. U /\ A e. y ) -> -. ( S .(+) v ) C. y ) <-> A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) ) |
120 |
105 119
|
mpbird |
|- ( ( ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) /\ v e. ( SubGrp ` G ) ) /\ ( ( ( S i^i v ) = { .0. } /\ ( S .(+) v ) = s /\ A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) /\ b e. ( U \ ( S .(+) v ) ) ) ) -> A. y e. ( SubGrp ` G ) ( ( y C. U /\ A e. y ) -> -. ( S .(+) v ) C. y ) ) |
121 |
|
simprr |
|- ( ( ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) /\ v e. ( SubGrp ` G ) ) /\ ( ( ( S i^i v ) = { .0. } /\ ( S .(+) v ) = s /\ A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) /\ b e. ( U \ ( S .(+) v ) ) ) ) -> b e. ( U \ ( S .(+) v ) ) ) |
122 |
|
eqid |
|- ( .g ` G ) = ( .g ` G ) |
123 |
1 2 3 4 5 6 7 95 96 97 98 99 100 101 102 104 120 121 122
|
pgpfac1lem4 |
|- ( ( ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) /\ v e. ( SubGrp ` G ) ) /\ ( ( ( S i^i v ) = { .0. } /\ ( S .(+) v ) = s /\ A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) /\ b e. ( U \ ( S .(+) v ) ) ) ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = U ) ) |
124 |
123
|
expr |
|- ( ( ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) /\ v e. ( SubGrp ` G ) ) /\ ( ( S i^i v ) = { .0. } /\ ( S .(+) v ) = s /\ A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) ) -> ( b e. ( U \ ( S .(+) v ) ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = U ) ) ) |
125 |
124
|
exlimdv |
|- ( ( ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) /\ v e. ( SubGrp ` G ) ) /\ ( ( S i^i v ) = { .0. } /\ ( S .(+) v ) = s /\ A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) ) -> ( E. b b e. ( U \ ( S .(+) v ) ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = U ) ) ) |
126 |
94 125
|
mpd |
|- ( ( ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) /\ v e. ( SubGrp ` G ) ) /\ ( ( S i^i v ) = { .0. } /\ ( S .(+) v ) = s /\ A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = U ) ) |
127 |
126
|
3exp2 |
|- ( ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) /\ v e. ( SubGrp ` G ) ) -> ( ( S i^i v ) = { .0. } -> ( ( S .(+) v ) = s -> ( A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = U ) ) ) ) ) |
128 |
127
|
impd |
|- ( ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) /\ v e. ( SubGrp ` G ) ) -> ( ( ( S i^i v ) = { .0. } /\ ( S .(+) v ) = s ) -> ( A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = U ) ) ) ) |
129 |
128
|
rexlimdva |
|- ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) -> ( E. v e. ( SubGrp ` G ) ( ( S i^i v ) = { .0. } /\ ( S .(+) v ) = s ) -> ( A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = U ) ) ) ) |
130 |
85 129
|
syl5bi |
|- ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) -> ( E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) -> ( A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = U ) ) ) ) |
131 |
130
|
impd |
|- ( ( ph /\ ( s e. ( SubGrp ` G ) /\ ( s C. U /\ A e. s ) ) ) -> ( ( E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) /\ A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = U ) ) ) |
132 |
79 131
|
sylan2b |
|- ( ( ph /\ s e. { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } ) -> ( ( E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) /\ A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = U ) ) ) |
133 |
132
|
rexlimdva |
|- ( ph -> ( E. s e. { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } ( E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) /\ A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = U ) ) ) |
134 |
78 133
|
syl5 |
|- ( ph -> ( ( A. s e. { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) /\ E. s e. { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = U ) ) ) |
135 |
77 134
|
mpand |
|- ( ph -> ( E. s e. { v e. ( SubGrp ` G ) | ( v C. U /\ A e. v ) } A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. s C. w ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = U ) ) ) |
136 |
72 135
|
syld |
|- ( ph -> ( S C. U -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = U ) ) ) |
137 |
6
|
0subg |
|- ( G e. Grp -> { .0. } e. ( SubGrp ` G ) ) |
138 |
27 137
|
syl |
|- ( ph -> { .0. } e. ( SubGrp ` G ) ) |
139 |
138
|
adantr |
|- ( ( ph /\ S = U ) -> { .0. } e. ( SubGrp ` G ) ) |
140 |
6
|
subg0cl |
|- ( S e. ( SubGrp ` G ) -> .0. e. S ) |
141 |
36 140
|
syl |
|- ( ph -> .0. e. S ) |
142 |
141
|
snssd |
|- ( ph -> { .0. } C_ S ) |
143 |
142
|
adantr |
|- ( ( ph /\ S = U ) -> { .0. } C_ S ) |
144 |
|
sseqin2 |
|- ( { .0. } C_ S <-> ( S i^i { .0. } ) = { .0. } ) |
145 |
143 144
|
sylib |
|- ( ( ph /\ S = U ) -> ( S i^i { .0. } ) = { .0. } ) |
146 |
7
|
lsmss2 |
|- ( ( S e. ( SubGrp ` G ) /\ { .0. } e. ( SubGrp ` G ) /\ { .0. } C_ S ) -> ( S .(+) { .0. } ) = S ) |
147 |
36 138 142 146
|
syl3anc |
|- ( ph -> ( S .(+) { .0. } ) = S ) |
148 |
147
|
eqeq1d |
|- ( ph -> ( ( S .(+) { .0. } ) = U <-> S = U ) ) |
149 |
148
|
biimpar |
|- ( ( ph /\ S = U ) -> ( S .(+) { .0. } ) = U ) |
150 |
|
ineq2 |
|- ( t = { .0. } -> ( S i^i t ) = ( S i^i { .0. } ) ) |
151 |
150
|
eqeq1d |
|- ( t = { .0. } -> ( ( S i^i t ) = { .0. } <-> ( S i^i { .0. } ) = { .0. } ) ) |
152 |
|
oveq2 |
|- ( t = { .0. } -> ( S .(+) t ) = ( S .(+) { .0. } ) ) |
153 |
152
|
eqeq1d |
|- ( t = { .0. } -> ( ( S .(+) t ) = U <-> ( S .(+) { .0. } ) = U ) ) |
154 |
151 153
|
anbi12d |
|- ( t = { .0. } -> ( ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = U ) <-> ( ( S i^i { .0. } ) = { .0. } /\ ( S .(+) { .0. } ) = U ) ) ) |
155 |
154
|
rspcev |
|- ( ( { .0. } e. ( SubGrp ` G ) /\ ( ( S i^i { .0. } ) = { .0. } /\ ( S .(+) { .0. } ) = U ) ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = U ) ) |
156 |
139 145 149 155
|
syl12anc |
|- ( ( ph /\ S = U ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = U ) ) |
157 |
156
|
ex |
|- ( ph -> ( S = U -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = U ) ) ) |
158 |
1
|
mrcsscl |
|- ( ( ( SubGrp ` G ) e. ( Moore ` B ) /\ { A } C_ U /\ U e. ( SubGrp ` G ) ) -> ( K ` { A } ) C_ U ) |
159 |
30 39 12 158
|
syl3anc |
|- ( ph -> ( K ` { A } ) C_ U ) |
160 |
2 159
|
eqsstrid |
|- ( ph -> S C_ U ) |
161 |
|
sspss |
|- ( S C_ U <-> ( S C. U \/ S = U ) ) |
162 |
160 161
|
sylib |
|- ( ph -> ( S C. U \/ S = U ) ) |
163 |
136 157 162
|
mpjaod |
|- ( ph -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = U ) ) |