Step |
Hyp |
Ref |
Expression |
1 |
|
ablfac1.b |
|- B = ( Base ` G ) |
2 |
|
ablfac1.o |
|- O = ( od ` G ) |
3 |
|
ablfac1.s |
|- S = ( p e. A |-> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } ) |
4 |
|
ablfac1.g |
|- ( ph -> G e. Abel ) |
5 |
|
ablfac1.f |
|- ( ph -> B e. Fin ) |
6 |
|
ablfac1.1 |
|- ( ph -> A C_ Prime ) |
7 |
|
ablfac1c.d |
|- D = { w e. Prime | w || ( # ` B ) } |
8 |
|
ablfac1.2 |
|- ( ph -> D C_ A ) |
9 |
|
ablfac1eu.1 |
|- ( ph -> ( G dom DProd T /\ ( G DProd T ) = B ) ) |
10 |
|
ablfac1eu.2 |
|- ( ph -> dom T = A ) |
11 |
|
ablfac1eu.3 |
|- ( ( ph /\ q e. A ) -> C e. NN0 ) |
12 |
|
ablfac1eu.4 |
|- ( ( ph /\ q e. A ) -> ( # ` ( T ` q ) ) = ( q ^ C ) ) |
13 |
|
ablfac1eulem.1 |
|- ( ph -> P e. Prime ) |
14 |
|
ablfac1eulem.2 |
|- ( ph -> A e. Fin ) |
15 |
|
ssid |
|- A C_ A |
16 |
|
sseq1 |
|- ( y = (/) -> ( y C_ A <-> (/) C_ A ) ) |
17 |
|
difeq1 |
|- ( y = (/) -> ( y \ { P } ) = ( (/) \ { P } ) ) |
18 |
|
0dif |
|- ( (/) \ { P } ) = (/) |
19 |
17 18
|
eqtrdi |
|- ( y = (/) -> ( y \ { P } ) = (/) ) |
20 |
19
|
reseq2d |
|- ( y = (/) -> ( T |` ( y \ { P } ) ) = ( T |` (/) ) ) |
21 |
|
res0 |
|- ( T |` (/) ) = (/) |
22 |
20 21
|
eqtrdi |
|- ( y = (/) -> ( T |` ( y \ { P } ) ) = (/) ) |
23 |
22
|
oveq2d |
|- ( y = (/) -> ( G DProd ( T |` ( y \ { P } ) ) ) = ( G DProd (/) ) ) |
24 |
23
|
fveq2d |
|- ( y = (/) -> ( # ` ( G DProd ( T |` ( y \ { P } ) ) ) ) = ( # ` ( G DProd (/) ) ) ) |
25 |
24
|
breq2d |
|- ( y = (/) -> ( P || ( # ` ( G DProd ( T |` ( y \ { P } ) ) ) ) <-> P || ( # ` ( G DProd (/) ) ) ) ) |
26 |
25
|
notbid |
|- ( y = (/) -> ( -. P || ( # ` ( G DProd ( T |` ( y \ { P } ) ) ) ) <-> -. P || ( # ` ( G DProd (/) ) ) ) ) |
27 |
16 26
|
imbi12d |
|- ( y = (/) -> ( ( y C_ A -> -. P || ( # ` ( G DProd ( T |` ( y \ { P } ) ) ) ) ) <-> ( (/) C_ A -> -. P || ( # ` ( G DProd (/) ) ) ) ) ) |
28 |
27
|
imbi2d |
|- ( y = (/) -> ( ( ph -> ( y C_ A -> -. P || ( # ` ( G DProd ( T |` ( y \ { P } ) ) ) ) ) ) <-> ( ph -> ( (/) C_ A -> -. P || ( # ` ( G DProd (/) ) ) ) ) ) ) |
29 |
|
sseq1 |
|- ( y = z -> ( y C_ A <-> z C_ A ) ) |
30 |
|
difeq1 |
|- ( y = z -> ( y \ { P } ) = ( z \ { P } ) ) |
31 |
30
|
reseq2d |
|- ( y = z -> ( T |` ( y \ { P } ) ) = ( T |` ( z \ { P } ) ) ) |
32 |
31
|
oveq2d |
|- ( y = z -> ( G DProd ( T |` ( y \ { P } ) ) ) = ( G DProd ( T |` ( z \ { P } ) ) ) ) |
33 |
32
|
fveq2d |
|- ( y = z -> ( # ` ( G DProd ( T |` ( y \ { P } ) ) ) ) = ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) ) |
34 |
33
|
breq2d |
|- ( y = z -> ( P || ( # ` ( G DProd ( T |` ( y \ { P } ) ) ) ) <-> P || ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) ) ) |
35 |
34
|
notbid |
|- ( y = z -> ( -. P || ( # ` ( G DProd ( T |` ( y \ { P } ) ) ) ) <-> -. P || ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) ) ) |
36 |
29 35
|
imbi12d |
|- ( y = z -> ( ( y C_ A -> -. P || ( # ` ( G DProd ( T |` ( y \ { P } ) ) ) ) ) <-> ( z C_ A -> -. P || ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) ) ) ) |
37 |
36
|
imbi2d |
|- ( y = z -> ( ( ph -> ( y C_ A -> -. P || ( # ` ( G DProd ( T |` ( y \ { P } ) ) ) ) ) ) <-> ( ph -> ( z C_ A -> -. P || ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) ) ) ) ) |
38 |
|
sseq1 |
|- ( y = ( z u. { q } ) -> ( y C_ A <-> ( z u. { q } ) C_ A ) ) |
39 |
|
difeq1 |
|- ( y = ( z u. { q } ) -> ( y \ { P } ) = ( ( z u. { q } ) \ { P } ) ) |
40 |
39
|
reseq2d |
|- ( y = ( z u. { q } ) -> ( T |` ( y \ { P } ) ) = ( T |` ( ( z u. { q } ) \ { P } ) ) ) |
41 |
40
|
oveq2d |
|- ( y = ( z u. { q } ) -> ( G DProd ( T |` ( y \ { P } ) ) ) = ( G DProd ( T |` ( ( z u. { q } ) \ { P } ) ) ) ) |
42 |
41
|
fveq2d |
|- ( y = ( z u. { q } ) -> ( # ` ( G DProd ( T |` ( y \ { P } ) ) ) ) = ( # ` ( G DProd ( T |` ( ( z u. { q } ) \ { P } ) ) ) ) ) |
43 |
42
|
breq2d |
|- ( y = ( z u. { q } ) -> ( P || ( # ` ( G DProd ( T |` ( y \ { P } ) ) ) ) <-> P || ( # ` ( G DProd ( T |` ( ( z u. { q } ) \ { P } ) ) ) ) ) ) |
44 |
43
|
notbid |
|- ( y = ( z u. { q } ) -> ( -. P || ( # ` ( G DProd ( T |` ( y \ { P } ) ) ) ) <-> -. P || ( # ` ( G DProd ( T |` ( ( z u. { q } ) \ { P } ) ) ) ) ) ) |
45 |
38 44
|
imbi12d |
|- ( y = ( z u. { q } ) -> ( ( y C_ A -> -. P || ( # ` ( G DProd ( T |` ( y \ { P } ) ) ) ) ) <-> ( ( z u. { q } ) C_ A -> -. P || ( # ` ( G DProd ( T |` ( ( z u. { q } ) \ { P } ) ) ) ) ) ) ) |
46 |
45
|
imbi2d |
|- ( y = ( z u. { q } ) -> ( ( ph -> ( y C_ A -> -. P || ( # ` ( G DProd ( T |` ( y \ { P } ) ) ) ) ) ) <-> ( ph -> ( ( z u. { q } ) C_ A -> -. P || ( # ` ( G DProd ( T |` ( ( z u. { q } ) \ { P } ) ) ) ) ) ) ) ) |
47 |
|
sseq1 |
|- ( y = A -> ( y C_ A <-> A C_ A ) ) |
48 |
|
difeq1 |
|- ( y = A -> ( y \ { P } ) = ( A \ { P } ) ) |
49 |
48
|
reseq2d |
|- ( y = A -> ( T |` ( y \ { P } ) ) = ( T |` ( A \ { P } ) ) ) |
50 |
49
|
oveq2d |
|- ( y = A -> ( G DProd ( T |` ( y \ { P } ) ) ) = ( G DProd ( T |` ( A \ { P } ) ) ) ) |
51 |
50
|
fveq2d |
|- ( y = A -> ( # ` ( G DProd ( T |` ( y \ { P } ) ) ) ) = ( # ` ( G DProd ( T |` ( A \ { P } ) ) ) ) ) |
52 |
51
|
breq2d |
|- ( y = A -> ( P || ( # ` ( G DProd ( T |` ( y \ { P } ) ) ) ) <-> P || ( # ` ( G DProd ( T |` ( A \ { P } ) ) ) ) ) ) |
53 |
52
|
notbid |
|- ( y = A -> ( -. P || ( # ` ( G DProd ( T |` ( y \ { P } ) ) ) ) <-> -. P || ( # ` ( G DProd ( T |` ( A \ { P } ) ) ) ) ) ) |
54 |
47 53
|
imbi12d |
|- ( y = A -> ( ( y C_ A -> -. P || ( # ` ( G DProd ( T |` ( y \ { P } ) ) ) ) ) <-> ( A C_ A -> -. P || ( # ` ( G DProd ( T |` ( A \ { P } ) ) ) ) ) ) ) |
55 |
54
|
imbi2d |
|- ( y = A -> ( ( ph -> ( y C_ A -> -. P || ( # ` ( G DProd ( T |` ( y \ { P } ) ) ) ) ) ) <-> ( ph -> ( A C_ A -> -. P || ( # ` ( G DProd ( T |` ( A \ { P } ) ) ) ) ) ) ) ) |
56 |
|
nprmdvds1 |
|- ( P e. Prime -> -. P || 1 ) |
57 |
13 56
|
syl |
|- ( ph -> -. P || 1 ) |
58 |
|
ablgrp |
|- ( G e. Abel -> G e. Grp ) |
59 |
|
eqid |
|- ( 0g ` G ) = ( 0g ` G ) |
60 |
59
|
dprd0 |
|- ( G e. Grp -> ( G dom DProd (/) /\ ( G DProd (/) ) = { ( 0g ` G ) } ) ) |
61 |
4 58 60
|
3syl |
|- ( ph -> ( G dom DProd (/) /\ ( G DProd (/) ) = { ( 0g ` G ) } ) ) |
62 |
61
|
simprd |
|- ( ph -> ( G DProd (/) ) = { ( 0g ` G ) } ) |
63 |
62
|
fveq2d |
|- ( ph -> ( # ` ( G DProd (/) ) ) = ( # ` { ( 0g ` G ) } ) ) |
64 |
|
fvex |
|- ( 0g ` G ) e. _V |
65 |
|
hashsng |
|- ( ( 0g ` G ) e. _V -> ( # ` { ( 0g ` G ) } ) = 1 ) |
66 |
64 65
|
ax-mp |
|- ( # ` { ( 0g ` G ) } ) = 1 |
67 |
63 66
|
eqtrdi |
|- ( ph -> ( # ` ( G DProd (/) ) ) = 1 ) |
68 |
67
|
breq2d |
|- ( ph -> ( P || ( # ` ( G DProd (/) ) ) <-> P || 1 ) ) |
69 |
57 68
|
mtbird |
|- ( ph -> -. P || ( # ` ( G DProd (/) ) ) ) |
70 |
69
|
a1d |
|- ( ph -> ( (/) C_ A -> -. P || ( # ` ( G DProd (/) ) ) ) ) |
71 |
|
ssun1 |
|- z C_ ( z u. { q } ) |
72 |
|
sstr |
|- ( ( z C_ ( z u. { q } ) /\ ( z u. { q } ) C_ A ) -> z C_ A ) |
73 |
71 72
|
mpan |
|- ( ( z u. { q } ) C_ A -> z C_ A ) |
74 |
73
|
imim1i |
|- ( ( z C_ A -> -. P || ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) ) -> ( ( z u. { q } ) C_ A -> -. P || ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) ) ) |
75 |
9
|
simpld |
|- ( ph -> G dom DProd T ) |
76 |
75 10
|
dprdf2 |
|- ( ph -> T : A --> ( SubGrp ` G ) ) |
77 |
76
|
adantr |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> T : A --> ( SubGrp ` G ) ) |
78 |
|
simprr |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( z u. { q } ) C_ A ) |
79 |
78
|
ssdifssd |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( ( z u. { q } ) \ { P } ) C_ A ) |
80 |
77 79
|
fssresd |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( T |` ( ( z u. { q } ) \ { P } ) ) : ( ( z u. { q } ) \ { P } ) --> ( SubGrp ` G ) ) |
81 |
|
simprl |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> -. q e. z ) |
82 |
|
disjsn |
|- ( ( z i^i { q } ) = (/) <-> -. q e. z ) |
83 |
81 82
|
sylibr |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( z i^i { q } ) = (/) ) |
84 |
83
|
difeq1d |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( ( z i^i { q } ) \ { P } ) = ( (/) \ { P } ) ) |
85 |
|
difindir |
|- ( ( z i^i { q } ) \ { P } ) = ( ( z \ { P } ) i^i ( { q } \ { P } ) ) |
86 |
84 85 18
|
3eqtr3g |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( ( z \ { P } ) i^i ( { q } \ { P } ) ) = (/) ) |
87 |
|
difundir |
|- ( ( z u. { q } ) \ { P } ) = ( ( z \ { P } ) u. ( { q } \ { P } ) ) |
88 |
87
|
a1i |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( ( z u. { q } ) \ { P } ) = ( ( z \ { P } ) u. ( { q } \ { P } ) ) ) |
89 |
|
eqid |
|- ( LSSum ` G ) = ( LSSum ` G ) |
90 |
75
|
adantr |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> G dom DProd T ) |
91 |
10
|
adantr |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> dom T = A ) |
92 |
90 91 79
|
dprdres |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( G dom DProd ( T |` ( ( z u. { q } ) \ { P } ) ) /\ ( G DProd ( T |` ( ( z u. { q } ) \ { P } ) ) ) C_ ( G DProd T ) ) ) |
93 |
92
|
simpld |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> G dom DProd ( T |` ( ( z u. { q } ) \ { P } ) ) ) |
94 |
80 86 88 89 93
|
dprdsplit |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( G DProd ( T |` ( ( z u. { q } ) \ { P } ) ) ) = ( ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( z \ { P } ) ) ) ( LSSum ` G ) ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( { q } \ { P } ) ) ) ) ) |
95 |
94
|
fveq2d |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( # ` ( G DProd ( T |` ( ( z u. { q } ) \ { P } ) ) ) ) = ( # ` ( ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( z \ { P } ) ) ) ( LSSum ` G ) ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( { q } \ { P } ) ) ) ) ) ) |
96 |
|
eqid |
|- ( Cntz ` G ) = ( Cntz ` G ) |
97 |
80
|
fdmd |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> dom ( T |` ( ( z u. { q } ) \ { P } ) ) = ( ( z u. { q } ) \ { P } ) ) |
98 |
|
ssdif |
|- ( z C_ ( z u. { q } ) -> ( z \ { P } ) C_ ( ( z u. { q } ) \ { P } ) ) |
99 |
71 98
|
mp1i |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( z \ { P } ) C_ ( ( z u. { q } ) \ { P } ) ) |
100 |
93 97 99
|
dprdres |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( G dom DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( z \ { P } ) ) /\ ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( z \ { P } ) ) ) C_ ( G DProd ( T |` ( ( z u. { q } ) \ { P } ) ) ) ) ) |
101 |
100
|
simpld |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> G dom DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( z \ { P } ) ) ) |
102 |
|
dprdsubg |
|- ( G dom DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( z \ { P } ) ) -> ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( z \ { P } ) ) ) e. ( SubGrp ` G ) ) |
103 |
101 102
|
syl |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( z \ { P } ) ) ) e. ( SubGrp ` G ) ) |
104 |
|
ssun2 |
|- { q } C_ ( z u. { q } ) |
105 |
|
ssdif |
|- ( { q } C_ ( z u. { q } ) -> ( { q } \ { P } ) C_ ( ( z u. { q } ) \ { P } ) ) |
106 |
104 105
|
mp1i |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( { q } \ { P } ) C_ ( ( z u. { q } ) \ { P } ) ) |
107 |
93 97 106
|
dprdres |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( G dom DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( { q } \ { P } ) ) /\ ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( { q } \ { P } ) ) ) C_ ( G DProd ( T |` ( ( z u. { q } ) \ { P } ) ) ) ) ) |
108 |
107
|
simpld |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> G dom DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( { q } \ { P } ) ) ) |
109 |
|
dprdsubg |
|- ( G dom DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( { q } \ { P } ) ) -> ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( { q } \ { P } ) ) ) e. ( SubGrp ` G ) ) |
110 |
108 109
|
syl |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( { q } \ { P } ) ) ) e. ( SubGrp ` G ) ) |
111 |
93 97 99 106 86 59
|
dprddisj2 |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( z \ { P } ) ) ) i^i ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( { q } \ { P } ) ) ) ) = { ( 0g ` G ) } ) |
112 |
93 97 99 106 86 96
|
dprdcntz2 |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( z \ { P } ) ) ) C_ ( ( Cntz ` G ) ` ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( { q } \ { P } ) ) ) ) ) |
113 |
5
|
adantr |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> B e. Fin ) |
114 |
1
|
dprdssv |
|- ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( z \ { P } ) ) ) C_ B |
115 |
|
ssfi |
|- ( ( B e. Fin /\ ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( z \ { P } ) ) ) C_ B ) -> ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( z \ { P } ) ) ) e. Fin ) |
116 |
113 114 115
|
sylancl |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( z \ { P } ) ) ) e. Fin ) |
117 |
1
|
dprdssv |
|- ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( { q } \ { P } ) ) ) C_ B |
118 |
|
ssfi |
|- ( ( B e. Fin /\ ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( { q } \ { P } ) ) ) C_ B ) -> ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( { q } \ { P } ) ) ) e. Fin ) |
119 |
113 117 118
|
sylancl |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( { q } \ { P } ) ) ) e. Fin ) |
120 |
89 59 96 103 110 111 112 116 119
|
lsmhash |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( # ` ( ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( z \ { P } ) ) ) ( LSSum ` G ) ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( { q } \ { P } ) ) ) ) ) = ( ( # ` ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( z \ { P } ) ) ) ) x. ( # ` ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( { q } \ { P } ) ) ) ) ) ) |
121 |
99
|
resabs1d |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( z \ { P } ) ) = ( T |` ( z \ { P } ) ) ) |
122 |
121
|
oveq2d |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( z \ { P } ) ) ) = ( G DProd ( T |` ( z \ { P } ) ) ) ) |
123 |
122
|
fveq2d |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( # ` ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( z \ { P } ) ) ) ) = ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) ) |
124 |
106
|
resabs1d |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( { q } \ { P } ) ) = ( T |` ( { q } \ { P } ) ) ) |
125 |
124
|
oveq2d |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( { q } \ { P } ) ) ) = ( G DProd ( T |` ( { q } \ { P } ) ) ) ) |
126 |
125
|
fveq2d |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( # ` ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( { q } \ { P } ) ) ) ) = ( # ` ( G DProd ( T |` ( { q } \ { P } ) ) ) ) ) |
127 |
123 126
|
oveq12d |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( ( # ` ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( z \ { P } ) ) ) ) x. ( # ` ( G DProd ( ( T |` ( ( z u. { q } ) \ { P } ) ) |` ( { q } \ { P } ) ) ) ) ) = ( ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) x. ( # ` ( G DProd ( T |` ( { q } \ { P } ) ) ) ) ) ) |
128 |
95 120 127
|
3eqtrd |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( # ` ( G DProd ( T |` ( ( z u. { q } ) \ { P } ) ) ) ) = ( ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) x. ( # ` ( G DProd ( T |` ( { q } \ { P } ) ) ) ) ) ) |
129 |
128
|
breq2d |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( P || ( # ` ( G DProd ( T |` ( ( z u. { q } ) \ { P } ) ) ) ) <-> P || ( ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) x. ( # ` ( G DProd ( T |` ( { q } \ { P } ) ) ) ) ) ) ) |
130 |
13
|
adantr |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> P e. Prime ) |
131 |
1
|
dprdssv |
|- ( G DProd ( T |` ( z \ { P } ) ) ) C_ B |
132 |
|
ssfi |
|- ( ( B e. Fin /\ ( G DProd ( T |` ( z \ { P } ) ) ) C_ B ) -> ( G DProd ( T |` ( z \ { P } ) ) ) e. Fin ) |
133 |
113 131 132
|
sylancl |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( G DProd ( T |` ( z \ { P } ) ) ) e. Fin ) |
134 |
|
hashcl |
|- ( ( G DProd ( T |` ( z \ { P } ) ) ) e. Fin -> ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) e. NN0 ) |
135 |
133 134
|
syl |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) e. NN0 ) |
136 |
135
|
nn0zd |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) e. ZZ ) |
137 |
1
|
dprdssv |
|- ( G DProd ( T |` ( { q } \ { P } ) ) ) C_ B |
138 |
|
ssfi |
|- ( ( B e. Fin /\ ( G DProd ( T |` ( { q } \ { P } ) ) ) C_ B ) -> ( G DProd ( T |` ( { q } \ { P } ) ) ) e. Fin ) |
139 |
113 137 138
|
sylancl |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( G DProd ( T |` ( { q } \ { P } ) ) ) e. Fin ) |
140 |
|
hashcl |
|- ( ( G DProd ( T |` ( { q } \ { P } ) ) ) e. Fin -> ( # ` ( G DProd ( T |` ( { q } \ { P } ) ) ) ) e. NN0 ) |
141 |
139 140
|
syl |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( # ` ( G DProd ( T |` ( { q } \ { P } ) ) ) ) e. NN0 ) |
142 |
141
|
nn0zd |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( # ` ( G DProd ( T |` ( { q } \ { P } ) ) ) ) e. ZZ ) |
143 |
|
euclemma |
|- ( ( P e. Prime /\ ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) e. ZZ /\ ( # ` ( G DProd ( T |` ( { q } \ { P } ) ) ) ) e. ZZ ) -> ( P || ( ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) x. ( # ` ( G DProd ( T |` ( { q } \ { P } ) ) ) ) ) <-> ( P || ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) \/ P || ( # ` ( G DProd ( T |` ( { q } \ { P } ) ) ) ) ) ) ) |
144 |
130 136 142 143
|
syl3anc |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( P || ( ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) x. ( # ` ( G DProd ( T |` ( { q } \ { P } ) ) ) ) ) <-> ( P || ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) \/ P || ( # ` ( G DProd ( T |` ( { q } \ { P } ) ) ) ) ) ) ) |
145 |
129 144
|
bitrd |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( P || ( # ` ( G DProd ( T |` ( ( z u. { q } ) \ { P } ) ) ) ) <-> ( P || ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) \/ P || ( # ` ( G DProd ( T |` ( { q } \ { P } ) ) ) ) ) ) ) |
146 |
57
|
ad2antrr |
|- ( ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) /\ q = P ) -> -. P || 1 ) |
147 |
|
simpr |
|- ( ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) /\ q = P ) -> q = P ) |
148 |
147
|
sneqd |
|- ( ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) /\ q = P ) -> { q } = { P } ) |
149 |
148
|
difeq1d |
|- ( ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) /\ q = P ) -> ( { q } \ { P } ) = ( { P } \ { P } ) ) |
150 |
|
difid |
|- ( { P } \ { P } ) = (/) |
151 |
149 150
|
eqtrdi |
|- ( ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) /\ q = P ) -> ( { q } \ { P } ) = (/) ) |
152 |
151
|
reseq2d |
|- ( ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) /\ q = P ) -> ( T |` ( { q } \ { P } ) ) = ( T |` (/) ) ) |
153 |
152 21
|
eqtrdi |
|- ( ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) /\ q = P ) -> ( T |` ( { q } \ { P } ) ) = (/) ) |
154 |
153
|
oveq2d |
|- ( ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) /\ q = P ) -> ( G DProd ( T |` ( { q } \ { P } ) ) ) = ( G DProd (/) ) ) |
155 |
62
|
ad2antrr |
|- ( ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) /\ q = P ) -> ( G DProd (/) ) = { ( 0g ` G ) } ) |
156 |
154 155
|
eqtrd |
|- ( ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) /\ q = P ) -> ( G DProd ( T |` ( { q } \ { P } ) ) ) = { ( 0g ` G ) } ) |
157 |
156
|
fveq2d |
|- ( ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) /\ q = P ) -> ( # ` ( G DProd ( T |` ( { q } \ { P } ) ) ) ) = ( # ` { ( 0g ` G ) } ) ) |
158 |
157 66
|
eqtrdi |
|- ( ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) /\ q = P ) -> ( # ` ( G DProd ( T |` ( { q } \ { P } ) ) ) ) = 1 ) |
159 |
158
|
breq2d |
|- ( ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) /\ q = P ) -> ( P || ( # ` ( G DProd ( T |` ( { q } \ { P } ) ) ) ) <-> P || 1 ) ) |
160 |
146 159
|
mtbird |
|- ( ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) /\ q = P ) -> -. P || ( # ` ( G DProd ( T |` ( { q } \ { P } ) ) ) ) ) |
161 |
6
|
adantr |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> A C_ Prime ) |
162 |
78
|
unssbd |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> { q } C_ A ) |
163 |
|
vex |
|- q e. _V |
164 |
163
|
snss |
|- ( q e. A <-> { q } C_ A ) |
165 |
162 164
|
sylibr |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> q e. A ) |
166 |
161 165
|
sseldd |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> q e. Prime ) |
167 |
165 11
|
syldan |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> C e. NN0 ) |
168 |
|
prmdvdsexpr |
|- ( ( P e. Prime /\ q e. Prime /\ C e. NN0 ) -> ( P || ( q ^ C ) -> P = q ) ) |
169 |
130 166 167 168
|
syl3anc |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( P || ( q ^ C ) -> P = q ) ) |
170 |
|
eqcom |
|- ( P = q <-> q = P ) |
171 |
169 170
|
syl6ib |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( P || ( q ^ C ) -> q = P ) ) |
172 |
171
|
necon3ad |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( q =/= P -> -. P || ( q ^ C ) ) ) |
173 |
172
|
imp |
|- ( ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) /\ q =/= P ) -> -. P || ( q ^ C ) ) |
174 |
|
disjsn2 |
|- ( q =/= P -> ( { q } i^i { P } ) = (/) ) |
175 |
174
|
adantl |
|- ( ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) /\ q =/= P ) -> ( { q } i^i { P } ) = (/) ) |
176 |
|
disj3 |
|- ( ( { q } i^i { P } ) = (/) <-> { q } = ( { q } \ { P } ) ) |
177 |
175 176
|
sylib |
|- ( ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) /\ q =/= P ) -> { q } = ( { q } \ { P } ) ) |
178 |
177
|
reseq2d |
|- ( ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) /\ q =/= P ) -> ( T |` { q } ) = ( T |` ( { q } \ { P } ) ) ) |
179 |
178
|
oveq2d |
|- ( ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) /\ q =/= P ) -> ( G DProd ( T |` { q } ) ) = ( G DProd ( T |` ( { q } \ { P } ) ) ) ) |
180 |
75
|
ad2antrr |
|- ( ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) /\ q =/= P ) -> G dom DProd T ) |
181 |
10
|
ad2antrr |
|- ( ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) /\ q =/= P ) -> dom T = A ) |
182 |
165
|
adantr |
|- ( ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) /\ q =/= P ) -> q e. A ) |
183 |
180 181 182
|
dpjlem |
|- ( ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) /\ q =/= P ) -> ( G DProd ( T |` { q } ) ) = ( T ` q ) ) |
184 |
179 183
|
eqtr3d |
|- ( ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) /\ q =/= P ) -> ( G DProd ( T |` ( { q } \ { P } ) ) ) = ( T ` q ) ) |
185 |
184
|
fveq2d |
|- ( ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) /\ q =/= P ) -> ( # ` ( G DProd ( T |` ( { q } \ { P } ) ) ) ) = ( # ` ( T ` q ) ) ) |
186 |
165 12
|
syldan |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( # ` ( T ` q ) ) = ( q ^ C ) ) |
187 |
186
|
adantr |
|- ( ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) /\ q =/= P ) -> ( # ` ( T ` q ) ) = ( q ^ C ) ) |
188 |
185 187
|
eqtrd |
|- ( ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) /\ q =/= P ) -> ( # ` ( G DProd ( T |` ( { q } \ { P } ) ) ) ) = ( q ^ C ) ) |
189 |
188
|
breq2d |
|- ( ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) /\ q =/= P ) -> ( P || ( # ` ( G DProd ( T |` ( { q } \ { P } ) ) ) ) <-> P || ( q ^ C ) ) ) |
190 |
173 189
|
mtbird |
|- ( ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) /\ q =/= P ) -> -. P || ( # ` ( G DProd ( T |` ( { q } \ { P } ) ) ) ) ) |
191 |
160 190
|
pm2.61dane |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> -. P || ( # ` ( G DProd ( T |` ( { q } \ { P } ) ) ) ) ) |
192 |
|
orel2 |
|- ( -. P || ( # ` ( G DProd ( T |` ( { q } \ { P } ) ) ) ) -> ( ( P || ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) \/ P || ( # ` ( G DProd ( T |` ( { q } \ { P } ) ) ) ) ) -> P || ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) ) ) |
193 |
191 192
|
syl |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( ( P || ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) \/ P || ( # ` ( G DProd ( T |` ( { q } \ { P } ) ) ) ) ) -> P || ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) ) ) |
194 |
145 193
|
sylbid |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( P || ( # ` ( G DProd ( T |` ( ( z u. { q } ) \ { P } ) ) ) ) -> P || ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) ) ) |
195 |
194
|
con3d |
|- ( ( ph /\ ( -. q e. z /\ ( z u. { q } ) C_ A ) ) -> ( -. P || ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) -> -. P || ( # ` ( G DProd ( T |` ( ( z u. { q } ) \ { P } ) ) ) ) ) ) |
196 |
195
|
expr |
|- ( ( ph /\ -. q e. z ) -> ( ( z u. { q } ) C_ A -> ( -. P || ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) -> -. P || ( # ` ( G DProd ( T |` ( ( z u. { q } ) \ { P } ) ) ) ) ) ) ) |
197 |
196
|
a2d |
|- ( ( ph /\ -. q e. z ) -> ( ( ( z u. { q } ) C_ A -> -. P || ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) ) -> ( ( z u. { q } ) C_ A -> -. P || ( # ` ( G DProd ( T |` ( ( z u. { q } ) \ { P } ) ) ) ) ) ) ) |
198 |
74 197
|
syl5 |
|- ( ( ph /\ -. q e. z ) -> ( ( z C_ A -> -. P || ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) ) -> ( ( z u. { q } ) C_ A -> -. P || ( # ` ( G DProd ( T |` ( ( z u. { q } ) \ { P } ) ) ) ) ) ) ) |
199 |
198
|
expcom |
|- ( -. q e. z -> ( ph -> ( ( z C_ A -> -. P || ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) ) -> ( ( z u. { q } ) C_ A -> -. P || ( # ` ( G DProd ( T |` ( ( z u. { q } ) \ { P } ) ) ) ) ) ) ) ) |
200 |
199
|
adantl |
|- ( ( z e. Fin /\ -. q e. z ) -> ( ph -> ( ( z C_ A -> -. P || ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) ) -> ( ( z u. { q } ) C_ A -> -. P || ( # ` ( G DProd ( T |` ( ( z u. { q } ) \ { P } ) ) ) ) ) ) ) ) |
201 |
200
|
a2d |
|- ( ( z e. Fin /\ -. q e. z ) -> ( ( ph -> ( z C_ A -> -. P || ( # ` ( G DProd ( T |` ( z \ { P } ) ) ) ) ) ) -> ( ph -> ( ( z u. { q } ) C_ A -> -. P || ( # ` ( G DProd ( T |` ( ( z u. { q } ) \ { P } ) ) ) ) ) ) ) ) |
202 |
28 37 46 55 70 201
|
findcard2s |
|- ( A e. Fin -> ( ph -> ( A C_ A -> -. P || ( # ` ( G DProd ( T |` ( A \ { P } ) ) ) ) ) ) ) |
203 |
14 202
|
mpcom |
|- ( ph -> ( A C_ A -> -. P || ( # ` ( G DProd ( T |` ( A \ { P } ) ) ) ) ) ) |
204 |
15 203
|
mpi |
|- ( ph -> -. P || ( # ` ( G DProd ( T |` ( A \ { P } ) ) ) ) ) |