Metamath Proof Explorer

Theorem ablfac1eulem

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

Ref Expression
Hypotheses ablfac1.b 
|- B = ( Base ` G )
ablfac1.o 
|- O = ( od ` G )
ablfac1.s 
|- S = ( p e. A |-> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } )
ablfac1.g 
|- ( ph -> G e. Abel )
ablfac1.f 
|- ( ph -> B e. Fin )
ablfac1.1 
|- ( ph -> A C_ Prime )
ablfac1c.d 
|- D = { w e. Prime | w || ( # ` B ) }
ablfac1.2 
|- ( ph -> D C_ A )
ablfac1eu.1 
|- ( ph -> ( G dom DProd T /\ ( G DProd T ) = B ) )
ablfac1eu.2 
|- ( ph -> dom T = A )
ablfac1eu.3 
|- ( ( ph /\ q e. A ) -> C e. NN0 )
ablfac1eu.4 
|- ( ( ph /\ q e. A ) -> ( # ` ( T ` q ) ) = ( q ^ C ) )
ablfac1eulem.1 
|- ( ph -> P e. Prime )
ablfac1eulem.2 
|- ( ph -> A e. Fin )
Assertion ablfac1eulem 
|- ( ph -> -. P || ( # ` ( G DProd ( T |` ( A \ { P } ) ) ) ) )

Proof

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 imbitrdi 
 |-  ( ( 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 } ) ) ) ) )