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