Metamath Proof Explorer

Theorem pgpfac1lem5

Description: Lemma for pgpfac1 . (Contributed by Mario Carneiro, 27-Apr-2016)

Ref Expression
Hypotheses pgpfac1.k 
|- K = ( mrCls ` ( SubGrp ` G ) )
pgpfac1.s 
|- S = ( K ` { A } )
pgpfac1.b 
|- B = ( Base ` G )
pgpfac1.o 
|- O = ( od ` G )
pgpfac1.e 
|- E = ( gEx ` G )
pgpfac1.z 
|- .0. = ( 0g ` G )
pgpfac1.l 
|- .(+) = ( LSSum ` G )
pgpfac1.p 
|- ( ph -> P pGrp G )
pgpfac1.g 
|- ( ph -> G e. Abel )
pgpfac1.n 
|- ( ph -> B e. Fin )
pgpfac1.oe 
|- ( ph -> ( O ` A ) = E )
pgpfac1.u 
|- ( ph -> U e. ( SubGrp ` G ) )
pgpfac1.au 
|- ( ph -> A e. U )
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 ) ) )
Assertion pgpfac1lem5 
|- ( ph -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = U ) )

Proof

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