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