Metamath Proof Explorer

Theorem aks6d1c1

Description: Claim 1 of Theorem 6.1 https://www3.nd.edu/%7eandyp/notes/AKS.pdf . (Contributed by metakunt, 30-Apr-2025)

Ref Expression
Hypotheses aks6d1c1.1 
|- .~ = { <. e , f >. | ( e e. NN /\ f e. B /\ A. y e. ( V PrimRoots R ) ( e .^ ( ( O ` f ) ` y ) ) = ( ( O ` f ) ` ( e .^ y ) ) ) }
aks6d1c1.2 
|- S = ( Poly1 ` K )
aks6d1c1.3 
|- B = ( Base ` S )
aks6d1c1.4 
|- X = ( var1 ` K )
aks6d1c1.5 
|- W = ( mulGrp ` S )
aks6d1c1.6 
|- V = ( mulGrp ` K )
aks6d1c1.7 
|- .^ = ( .g ` V )
aks6d1c1.8 
|- C = ( algSc ` S )
aks6d1c1.9 
|- D = ( .g ` W )
aks6d1c1.10 
|- P = ( chr ` K )
aks6d1c1.11 
|- O = ( eval1 ` K )
aks6d1c1.12 
|- .+ = ( +g ` S )
aks6d1c1.13 
|- ( ph -> K e. Field )
aks6d1c1.14 
|- ( ph -> P e. Prime )
aks6d1c1.15 
|- ( ph -> R e. NN )
aks6d1c1.16 
|- ( ph -> N e. NN )
aks6d1c1.17 
|- ( ph -> P || N )
aks6d1c1.18 
|- ( ph -> ( N gcd R ) = 1 )
aks6d1c1.19 
|- ( ph -> F : ( 0 ... A ) --> NN0 )
aks6d1c1.20 
|- G = ( g e. ( NN0 ^m ( 0 ... A ) ) |-> ( W gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
aks6d1c1.21 
|- ( ph -> A e. NN0 )
aks6d1c1.22 
|- ( ph -> U e. NN0 )
aks6d1c1.23 
|- ( ph -> L e. NN0 )
aks6d1c1.24 
|- E = ( ( P ^ U ) x. ( ( N / P ) ^ L ) )
aks6d1c1.25 
|- ( ph -> A. a e. ( 1 ... A ) N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) )
aks6d1c1.26 
|- ( ph -> ( x e. ( Base ` K ) |-> ( P .^ x ) ) e. ( K RingIso K ) )
Assertion aks6d1c1 
|- ( ph -> E .~ ( G ` F ) )

Proof

Step Hyp Ref Expression
1 aks6d1c1.1 
 |-  .~ = { <. e , f >. | ( e e. NN /\ f e. B /\ A. y e. ( V PrimRoots R ) ( e .^ ( ( O ` f ) ` y ) ) = ( ( O ` f ) ` ( e .^ y ) ) ) }
2 aks6d1c1.2 
 |-  S = ( Poly1 ` K )
3 aks6d1c1.3 
 |-  B = ( Base ` S )
4 aks6d1c1.4 
 |-  X = ( var1 ` K )
5 aks6d1c1.5 
 |-  W = ( mulGrp ` S )
6 aks6d1c1.6 
 |-  V = ( mulGrp ` K )
7 aks6d1c1.7 
 |-  .^ = ( .g ` V )
8 aks6d1c1.8 
 |-  C = ( algSc ` S )
9 aks6d1c1.9 
 |-  D = ( .g ` W )
10 aks6d1c1.10 
 |-  P = ( chr ` K )
11 aks6d1c1.11 
 |-  O = ( eval1 ` K )
12 aks6d1c1.12 
 |-  .+ = ( +g ` S )
13 aks6d1c1.13 
 |-  ( ph -> K e. Field )
14 aks6d1c1.14 
 |-  ( ph -> P e. Prime )
15 aks6d1c1.15 
 |-  ( ph -> R e. NN )
16 aks6d1c1.16 
 |-  ( ph -> N e. NN )
17 aks6d1c1.17 
 |-  ( ph -> P || N )
18 aks6d1c1.18 
 |-  ( ph -> ( N gcd R ) = 1 )
19 aks6d1c1.19 
 |-  ( ph -> F : ( 0 ... A ) --> NN0 )
20 aks6d1c1.20 
 |-  G = ( g e. ( NN0 ^m ( 0 ... A ) ) |-> ( W gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
21 aks6d1c1.21 
 |-  ( ph -> A e. NN0 )
22 aks6d1c1.22 
 |-  ( ph -> U e. NN0 )
23 aks6d1c1.23 
 |-  ( ph -> L e. NN0 )
24 aks6d1c1.24 
 |-  E = ( ( P ^ U ) x. ( ( N / P ) ^ L ) )
25 aks6d1c1.25 
 |-  ( ph -> A. a e. ( 1 ... A ) N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) )
26 aks6d1c1.26 
 |-  ( ph -> ( x e. ( Base ` K ) |-> ( P .^ x ) ) e. ( K RingIso K ) )
27 21 nn0zd 
 |-  ( ph -> A e. ZZ )
28 21 nn0ge0d 
 |-  ( ph -> 0 <_ A )
29 21 nn0red 
 |-  ( ph -> A e. RR )
30 29 leidd 
 |-  ( ph -> A <_ A )
31 27 28 30 3jca 
 |-  ( ph -> ( A e. ZZ /\ 0 <_ A /\ A <_ A ) )
32 oveq2 
 |-  ( h = 0 -> ( 0 ... h ) = ( 0 ... 0 ) )
33 32 mpteq1d 
 |-  ( h = 0 -> ( i e. ( 0 ... h ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) = ( i e. ( 0 ... 0 ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) )
34 33 oveq2d 
 |-  ( h = 0 -> ( W gsum ( i e. ( 0 ... h ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) = ( W gsum ( i e. ( 0 ... 0 ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
35 34 breq2d 
 |-  ( h = 0 -> ( E .~ ( W gsum ( i e. ( 0 ... h ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) <-> E .~ ( W gsum ( i e. ( 0 ... 0 ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) )
36 oveq2 
 |-  ( h = j -> ( 0 ... h ) = ( 0 ... j ) )
37 36 mpteq1d 
 |-  ( h = j -> ( i e. ( 0 ... h ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) = ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) )
38 37 oveq2d 
 |-  ( h = j -> ( W gsum ( i e. ( 0 ... h ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) = ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
39 38 breq2d 
 |-  ( h = j -> ( E .~ ( W gsum ( i e. ( 0 ... h ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) <-> E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) )
40 oveq2 
 |-  ( h = ( j + 1 ) -> ( 0 ... h ) = ( 0 ... ( j + 1 ) ) )
41 40 mpteq1d 
 |-  ( h = ( j + 1 ) -> ( i e. ( 0 ... h ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) = ( i e. ( 0 ... ( j + 1 ) ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) )
42 41 oveq2d 
 |-  ( h = ( j + 1 ) -> ( W gsum ( i e. ( 0 ... h ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) = ( W gsum ( i e. ( 0 ... ( j + 1 ) ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
43 42 breq2d 
 |-  ( h = ( j + 1 ) -> ( E .~ ( W gsum ( i e. ( 0 ... h ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) <-> E .~ ( W gsum ( i e. ( 0 ... ( j + 1 ) ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) )
44 oveq2 
 |-  ( h = A -> ( 0 ... h ) = ( 0 ... A ) )
45 44 mpteq1d 
 |-  ( h = A -> ( i e. ( 0 ... h ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) = ( i e. ( 0 ... A ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) )
46 45 oveq2d 
 |-  ( h = A -> ( W gsum ( i e. ( 0 ... h ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) = ( W gsum ( i e. ( 0 ... A ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
47 46 breq2d 
 |-  ( h = A -> ( E .~ ( W gsum ( i e. ( 0 ... h ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) <-> E .~ ( W gsum ( i e. ( 0 ... A ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) )
48 prmnn 
 |-  ( P e. Prime -> P e. NN )
49 14 48 syl 
 |-  ( ph -> P e. NN )
50 49 22 nnexpcld 
 |-  ( ph -> ( P ^ U ) e. NN )
51 49 nnzd 
 |-  ( ph -> P e. ZZ )
52 49 nnne0d 
 |-  ( ph -> P =/= 0 )
53 16 nnzd 
 |-  ( ph -> N e. ZZ )
54 dvdsval2 
 |-  ( ( P e. ZZ /\ P =/= 0 /\ N e. ZZ ) -> ( P || N <-> ( N / P ) e. ZZ ) )
55 51 52 53 54 syl3anc 
 |-  ( ph -> ( P || N <-> ( N / P ) e. ZZ ) )
56 17 55 mpbid 
 |-  ( ph -> ( N / P ) e. ZZ )
57 16 nnred 
 |-  ( ph -> N e. RR )
58 49 nnred 
 |-  ( ph -> P e. RR )
59 16 nngt0d 
 |-  ( ph -> 0 < N )
60 49 nngt0d 
 |-  ( ph -> 0 < P )
61 57 58 59 60 divgt0d 
 |-  ( ph -> 0 < ( N / P ) )
62 56 61 jca 
 |-  ( ph -> ( ( N / P ) e. ZZ /\ 0 < ( N / P ) ) )
63 elnnz 
 |-  ( ( N / P ) e. NN <-> ( ( N / P ) e. ZZ /\ 0 < ( N / P ) ) )
64 62 63 sylibr 
 |-  ( ph -> ( N / P ) e. NN )
65 64 23 nnexpcld 
 |-  ( ph -> ( ( N / P ) ^ L ) e. NN )
66 50 65 nnmulcld 
 |-  ( ph -> ( ( P ^ U ) x. ( ( N / P ) ^ L ) ) e. NN )
67 24 66 eqeltrid 
 |-  ( ph -> E e. NN )
68 1 2 3 4 6 7 10 11 13 14 15 16 17 18 67 aks6d1c1p7 
 |-  ( ph -> E .~ X )
69 13 fldcrngd 
 |-  ( ph -> K e. CRing )
70 2 ply1crng 
 |-  ( K e. CRing -> S e. CRing )
71 69 70 syl 
 |-  ( ph -> S e. CRing )
72 crngring 
 |-  ( S e. CRing -> S e. Ring )
73 ringcmn 
 |-  ( S e. Ring -> S e. CMnd )
74 72 73 syl 
 |-  ( S e. CRing -> S e. CMnd )
75 71 74 syl 
 |-  ( ph -> S e. CMnd )
76 cmnmnd 
 |-  ( S e. CMnd -> S e. Mnd )
77 75 76 syl 
 |-  ( ph -> S e. Mnd )
78 crngring 
 |-  ( K e. CRing -> K e. Ring )
79 69 78 syl 
 |-  ( ph -> K e. Ring )
80 eqid 
 |-  ( Base ` S ) = ( Base ` S )
81 4 2 80 vr1cl 
 |-  ( K e. Ring -> X e. ( Base ` S ) )
82 79 81 syl 
 |-  ( ph -> X e. ( Base ` S ) )
83 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
84 80 12 83 mndrid 
 |-  ( ( S e. Mnd /\ X e. ( Base ` S ) ) -> ( X .+ ( 0g ` S ) ) = X )
85 77 82 84 syl2anc 
 |-  ( ph -> ( X .+ ( 0g ` S ) ) = X )
86 68 85 breqtrrd 
 |-  ( ph -> E .~ ( X .+ ( 0g ` S ) ) )
87 eqid 
 |-  ( ZRHom ` K ) = ( ZRHom ` K )
88 eqid 
 |-  ( 0g ` K ) = ( 0g ` K )
89 87 88 zrh0 
 |-  ( K e. Ring -> ( ( ZRHom ` K ) ` 0 ) = ( 0g ` K ) )
90 79 89 syl 
 |-  ( ph -> ( ( ZRHom ` K ) ` 0 ) = ( 0g ` K ) )
91 90 fveq2d 
 |-  ( ph -> ( C ` ( ( ZRHom ` K ) ` 0 ) ) = ( C ` ( 0g ` K ) ) )
92 2 8 88 83 79 ply1ascl0 
 |-  ( ph -> ( C ` ( 0g ` K ) ) = ( 0g ` S ) )
93 91 92 eqtrd 
 |-  ( ph -> ( C ` ( ( ZRHom ` K ) ` 0 ) ) = ( 0g ` S ) )
94 93 oveq2d 
 |-  ( ph -> ( X .+ ( C ` ( ( ZRHom ` K ) ` 0 ) ) ) = ( X .+ ( 0g ` S ) ) )
95 86 94 breqtrrd 
 |-  ( ph -> E .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` 0 ) ) ) )
96 0zd 
 |-  ( ph -> 0 e. ZZ )
97 0red 
 |-  ( ph -> 0 e. RR )
98 97 leidd 
 |-  ( ph -> 0 <_ 0 )
99 96 27 96 98 28 elfzd 
 |-  ( ph -> 0 e. ( 0 ... A ) )
100 19 99 ffvelcdmd 
 |-  ( ph -> ( F ` 0 ) e. NN0 )
101 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 95 100 aks6d1c1p6 
 |-  ( ph -> E .~ ( ( F ` 0 ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` 0 ) ) ) ) )
102 5 crngmgp 
 |-  ( S e. CRing -> W e. CMnd )
103 71 102 syl 
 |-  ( ph -> W e. CMnd )
104 103 cmnmndd 
 |-  ( ph -> W e. Mnd )
105 0z 
 |-  0 e. ZZ
106 105 a1i 
 |-  ( ph -> 0 e. ZZ )
107 eqid 
 |-  ( Base ` W ) = ( Base ` W )
108 0le0 
 |-  0 <_ 0
109 108 a1i 
 |-  ( ph -> 0 <_ 0 )
110 106 27 106 109 28 elfzd 
 |-  ( ph -> 0 e. ( 0 ... A ) )
111 19 110 ffvelcdmd 
 |-  ( ph -> ( F ` 0 ) e. NN0 )
112 87 zrhrhm 
 |-  ( K e. Ring -> ( ZRHom ` K ) e. ( ZZring RingHom K ) )
113 79 112 syl 
 |-  ( ph -> ( ZRHom ` K ) e. ( ZZring RingHom K ) )
114 zringbas 
 |-  ZZ = ( Base ` ZZring )
115 eqid 
 |-  ( Base ` K ) = ( Base ` K )
116 114 115 rhmf 
 |-  ( ( ZRHom ` K ) e. ( ZZring RingHom K ) -> ( ZRHom ` K ) : ZZ --> ( Base ` K ) )
117 113 116 syl 
 |-  ( ph -> ( ZRHom ` K ) : ZZ --> ( Base ` K ) )
118 117 96 ffvelcdmd 
 |-  ( ph -> ( ( ZRHom ` K ) ` 0 ) e. ( Base ` K ) )
119 2 8 115 80 ply1sclcl 
 |-  ( ( K e. Ring /\ ( ( ZRHom ` K ) ` 0 ) e. ( Base ` K ) ) -> ( C ` ( ( ZRHom ` K ) ` 0 ) ) e. ( Base ` S ) )
120 79 118 119 syl2anc 
 |-  ( ph -> ( C ` ( ( ZRHom ` K ) ` 0 ) ) e. ( Base ` S ) )
121 80 12 mndcl 
 |-  ( ( S e. Mnd /\ X e. ( Base ` S ) /\ ( C ` ( ( ZRHom ` K ) ` 0 ) ) e. ( Base ` S ) ) -> ( X .+ ( C ` ( ( ZRHom ` K ) ` 0 ) ) ) e. ( Base ` S ) )
122 77 82 120 121 syl3anc 
 |-  ( ph -> ( X .+ ( C ` ( ( ZRHom ` K ) ` 0 ) ) ) e. ( Base ` S ) )
123 5 80 mgpbas 
 |-  ( Base ` S ) = ( Base ` W )
124 122 123 eleqtrdi 
 |-  ( ph -> ( X .+ ( C ` ( ( ZRHom ` K ) ` 0 ) ) ) e. ( Base ` W ) )
125 107 9 104 111 124 mulgnn0cld 
 |-  ( ph -> ( ( F ` 0 ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` 0 ) ) ) ) e. ( Base ` W ) )
126 fveq2 
 |-  ( i = 0 -> ( F ` i ) = ( F ` 0 ) )
127 2fveq3 
 |-  ( i = 0 -> ( C ` ( ( ZRHom ` K ) ` i ) ) = ( C ` ( ( ZRHom ` K ) ` 0 ) ) )
128 127 oveq2d 
 |-  ( i = 0 -> ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) = ( X .+ ( C ` ( ( ZRHom ` K ) ` 0 ) ) ) )
129 126 128 oveq12d 
 |-  ( i = 0 -> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) = ( ( F ` 0 ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` 0 ) ) ) ) )
130 107 129 gsumsn 
 |-  ( ( W e. Mnd /\ 0 e. ZZ /\ ( ( F ` 0 ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` 0 ) ) ) ) e. ( Base ` W ) ) -> ( W gsum ( i e. { 0 } |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) = ( ( F ` 0 ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` 0 ) ) ) ) )
131 104 106 125 130 syl3anc 
 |-  ( ph -> ( W gsum ( i e. { 0 } |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) = ( ( F ` 0 ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` 0 ) ) ) ) )
132 101 131 breqtrrd 
 |-  ( ph -> E .~ ( W gsum ( i e. { 0 } |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
133 fzsn 
 |-  ( 0 e. ZZ -> ( 0 ... 0 ) = { 0 } )
134 105 133 ax-mp 
 |-  ( 0 ... 0 ) = { 0 }
135 134 a1i 
 |-  ( ph -> ( 0 ... 0 ) = { 0 } )
136 135 mpteq1d 
 |-  ( ph -> ( i e. ( 0 ... 0 ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) = ( i e. { 0 } |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) )
137 136 oveq2d 
 |-  ( ph -> ( W gsum ( i e. ( 0 ... 0 ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) = ( W gsum ( i e. { 0 } |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
138 132 137 breqtrrd 
 |-  ( ph -> E .~ ( W gsum ( i e. ( 0 ... 0 ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
139 13 3ad2ant1 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) -> K e. Field )
140 14 3ad2ant1 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) -> P e. Prime )
141 15 3ad2ant1 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) -> R e. NN )
142 18 3ad2ant1 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) -> ( N gcd R ) = 1 )
143 17 3ad2ant1 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) -> P || N )
144 simp3 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) -> E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
145 nfcv 
 |-  F/_ k ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) )
146 nfcv 
 |-  F/_ i ( ( F ` k ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` k ) ) ) )
147 fveq2 
 |-  ( i = k -> ( F ` i ) = ( F ` k ) )
148 2fveq3 
 |-  ( i = k -> ( C ` ( ( ZRHom ` K ) ` i ) ) = ( C ` ( ( ZRHom ` K ) ` k ) ) )
149 148 oveq2d 
 |-  ( i = k -> ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) = ( X .+ ( C ` ( ( ZRHom ` K ) ` k ) ) ) )
150 147 149 oveq12d 
 |-  ( i = k -> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) = ( ( F ` k ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` k ) ) ) ) )
151 145 146 150 cbvmpt 
 |-  ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) = ( k e. ( 0 ... j ) |-> ( ( F ` k ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` k ) ) ) ) )
152 151 oveq2i 
 |-  ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) = ( W gsum ( k e. ( 0 ... j ) |-> ( ( F ` k ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` k ) ) ) ) ) )
153 152 a1i 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) -> ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) = ( W gsum ( k e. ( 0 ... j ) |-> ( ( F ` k ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` k ) ) ) ) ) ) )
154 144 153 breqtrd 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) -> E .~ ( W gsum ( k e. ( 0 ... j ) |-> ( ( F ` k ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` k ) ) ) ) ) ) )
155 13 adantr 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> K e. Field )
156 14 adantr 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> P e. Prime )
157 15 adantr 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> R e. NN )
158 16 adantr 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> N e. NN )
159 17 adantr 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> P || N )
160 18 adantr 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> ( N gcd R ) = 1 )
161 24 a1i 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> E = ( ( P ^ U ) x. ( ( N / P ) ^ L ) ) )
162 15 nnzd 
 |-  ( ph -> R e. ZZ )
163 56 162 23 3jca 
 |-  ( ph -> ( ( N / P ) e. ZZ /\ R e. ZZ /\ L e. NN0 ) )
164 162 56 53 3jca 
 |-  ( ph -> ( R e. ZZ /\ ( N / P ) e. ZZ /\ N e. ZZ ) )
165 53 162 jca 
 |-  ( ph -> ( N e. ZZ /\ R e. ZZ ) )
166 gcdcom 
 |-  ( ( N e. ZZ /\ R e. ZZ ) -> ( N gcd R ) = ( R gcd N ) )
167 165 166 syl 
 |-  ( ph -> ( N gcd R ) = ( R gcd N ) )
168 eqeq1 
 |-  ( ( N gcd R ) = ( R gcd N ) -> ( ( N gcd R ) = 1 <-> ( R gcd N ) = 1 ) )
169 167 168 syl 
 |-  ( ph -> ( ( N gcd R ) = 1 <-> ( R gcd N ) = 1 ) )
170 169 pm5.74i 
 |-  ( ( ph -> ( N gcd R ) = 1 ) <-> ( ph -> ( R gcd N ) = 1 ) )
171 18 170 mpbi 
 |-  ( ph -> ( R gcd N ) = 1 )
172 57 recnd 
 |-  ( ph -> N e. CC )
173 58 recnd 
 |-  ( ph -> P e. CC )
174 97 59 gtned 
 |-  ( ph -> N =/= 0 )
175 172 172 173 174 52 divdiv2d 
 |-  ( ph -> ( N / ( N / P ) ) = ( ( N x. P ) / N ) )
176 172 173 mulcomd 
 |-  ( ph -> ( N x. P ) = ( P x. N ) )
177 176 oveq1d 
 |-  ( ph -> ( ( N x. P ) / N ) = ( ( P x. N ) / N ) )
178 173 172 172 174 174 divdiv2d 
 |-  ( ph -> ( P / ( N / N ) ) = ( ( P x. N ) / N ) )
179 178 eqcomd 
 |-  ( ph -> ( ( P x. N ) / N ) = ( P / ( N / N ) ) )
180 177 179 eqtrd 
 |-  ( ph -> ( ( N x. P ) / N ) = ( P / ( N / N ) ) )
181 172 174 dividd 
 |-  ( ph -> ( N / N ) = 1 )
182 181 oveq2d 
 |-  ( ph -> ( P / ( N / N ) ) = ( P / 1 ) )
183 173 div1d 
 |-  ( ph -> ( P / 1 ) = P )
184 182 183 eqtrd 
 |-  ( ph -> ( P / ( N / N ) ) = P )
185 184 51 eqeltrd 
 |-  ( ph -> ( P / ( N / N ) ) e. ZZ )
186 180 185 eqeltrd 
 |-  ( ph -> ( ( N x. P ) / N ) e. ZZ )
187 175 186 eqeltrd 
 |-  ( ph -> ( N / ( N / P ) ) e. ZZ )
188 97 61 gtned 
 |-  ( ph -> ( N / P ) =/= 0 )
189 dvdsval2 
 |-  ( ( ( N / P ) e. ZZ /\ ( N / P ) =/= 0 /\ N e. ZZ ) -> ( ( N / P ) || N <-> ( N / ( N / P ) ) e. ZZ ) )
190 56 188 53 189 syl3anc 
 |-  ( ph -> ( ( N / P ) || N <-> ( N / ( N / P ) ) e. ZZ ) )
191 187 190 mpbird 
 |-  ( ph -> ( N / P ) || N )
192 171 191 jca 
 |-  ( ph -> ( ( R gcd N ) = 1 /\ ( N / P ) || N ) )
193 rpdvds 
 |-  ( ( ( R e. ZZ /\ ( N / P ) e. ZZ /\ N e. ZZ ) /\ ( ( R gcd N ) = 1 /\ ( N / P ) || N ) ) -> ( R gcd ( N / P ) ) = 1 )
194 164 192 193 syl2anc 
 |-  ( ph -> ( R gcd ( N / P ) ) = 1 )
195 162 56 jca 
 |-  ( ph -> ( R e. ZZ /\ ( N / P ) e. ZZ ) )
196 gcdcom 
 |-  ( ( R e. ZZ /\ ( N / P ) e. ZZ ) -> ( R gcd ( N / P ) ) = ( ( N / P ) gcd R ) )
197 195 196 syl 
 |-  ( ph -> ( R gcd ( N / P ) ) = ( ( N / P ) gcd R ) )
198 eqeq1 
 |-  ( ( R gcd ( N / P ) ) = ( ( N / P ) gcd R ) -> ( ( R gcd ( N / P ) ) = 1 <-> ( ( N / P ) gcd R ) = 1 ) )
199 197 198 syl 
 |-  ( ph -> ( ( R gcd ( N / P ) ) = 1 <-> ( ( N / P ) gcd R ) = 1 ) )
200 199 pm5.74i 
 |-  ( ( ph -> ( R gcd ( N / P ) ) = 1 ) <-> ( ph -> ( ( N / P ) gcd R ) = 1 ) )
201 194 200 mpbi 
 |-  ( ph -> ( ( N / P ) gcd R ) = 1 )
202 rpexp1i 
 |-  ( ( ( N / P ) e. ZZ /\ R e. ZZ /\ L e. NN0 ) -> ( ( ( N / P ) gcd R ) = 1 -> ( ( ( N / P ) ^ L ) gcd R ) = 1 ) )
203 202 imp 
 |-  ( ( ( ( N / P ) e. ZZ /\ R e. ZZ /\ L e. NN0 ) /\ ( ( N / P ) gcd R ) = 1 ) -> ( ( ( N / P ) ^ L ) gcd R ) = 1 )
204 163 201 203 syl2anc 
 |-  ( ph -> ( ( ( N / P ) ^ L ) gcd R ) = 1 )
205 204 adantr 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> ( ( ( N / P ) ^ L ) gcd R ) = 1 )
206 eqid 
 |-  ( X .+ ( C ` ( ( ZRHom ` K ) ` ( j + 1 ) ) ) ) = ( X .+ ( C ` ( ( ZRHom ` K ) ` ( j + 1 ) ) ) )
207 simpr1 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> j e. ZZ )
208 207 peano2zd 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> ( j + 1 ) e. ZZ )
209 1 2 3 4 5 6 7 8 9 10 11 12 155 156 157 160 159 206 208 aks6d1c1p2 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> P .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` ( j + 1 ) ) ) ) )
210 22 adantr 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> U e. NN0 )
211 162 51 53 3jca 
 |-  ( ph -> ( R e. ZZ /\ P e. ZZ /\ N e. ZZ ) )
212 171 17 jca 
 |-  ( ph -> ( ( R gcd N ) = 1 /\ P || N ) )
213 rpdvds 
 |-  ( ( ( R e. ZZ /\ P e. ZZ /\ N e. ZZ ) /\ ( ( R gcd N ) = 1 /\ P || N ) ) -> ( R gcd P ) = 1 )
214 211 212 213 syl2anc 
 |-  ( ph -> ( R gcd P ) = 1 )
215 162 51 jca 
 |-  ( ph -> ( R e. ZZ /\ P e. ZZ ) )
216 gcdcom 
 |-  ( ( R e. ZZ /\ P e. ZZ ) -> ( R gcd P ) = ( P gcd R ) )
217 215 216 syl 
 |-  ( ph -> ( R gcd P ) = ( P gcd R ) )
218 eqeq1 
 |-  ( ( R gcd P ) = ( P gcd R ) -> ( ( R gcd P ) = 1 <-> ( P gcd R ) = 1 ) )
219 217 218 syl 
 |-  ( ph -> ( ( R gcd P ) = 1 <-> ( P gcd R ) = 1 ) )
220 219 pm5.74i 
 |-  ( ( ph -> ( R gcd P ) = 1 ) <-> ( ph -> ( P gcd R ) = 1 ) )
221 214 220 mpbi 
 |-  ( ph -> ( P gcd R ) = 1 )
222 221 adantr 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> ( P gcd R ) = 1 )
223 1 2 3 4 5 6 7 8 9 10 11 12 155 156 157 158 159 160 209 210 222 aks6d1c1p8 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> ( P ^ U ) .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` ( j + 1 ) ) ) ) )
224 2fveq3 
 |-  ( a = ( j + 1 ) -> ( C ` ( ( ZRHom ` K ) ` a ) ) = ( C ` ( ( ZRHom ` K ) ` ( j + 1 ) ) ) )
225 224 oveq2d 
 |-  ( a = ( j + 1 ) -> ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) = ( X .+ ( C ` ( ( ZRHom ` K ) ` ( j + 1 ) ) ) ) )
226 225 breq2d 
 |-  ( a = ( j + 1 ) -> ( N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) <-> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` ( j + 1 ) ) ) ) ) )
227 1 2 3 4 6 7 10 11 13 14 15 16 17 18 16 aks6d1c1p7 
 |-  ( ph -> N .~ X )
228 227 85 breqtrrd 
 |-  ( ph -> N .~ ( X .+ ( 0g ` S ) ) )
229 228 94 breqtrrd 
 |-  ( ph -> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` 0 ) ) ) )
230 229 adantr 
 |-  ( ( ph /\ a = 0 ) -> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` 0 ) ) ) )
231 simpr 
 |-  ( ( ph /\ a = 0 ) -> a = 0 )
232 231 fveq2d 
 |-  ( ( ph /\ a = 0 ) -> ( ( ZRHom ` K ) ` a ) = ( ( ZRHom ` K ) ` 0 ) )
233 232 fveq2d 
 |-  ( ( ph /\ a = 0 ) -> ( C ` ( ( ZRHom ` K ) ` a ) ) = ( C ` ( ( ZRHom ` K ) ` 0 ) ) )
234 233 oveq2d 
 |-  ( ( ph /\ a = 0 ) -> ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) = ( X .+ ( C ` ( ( ZRHom ` K ) ` 0 ) ) ) )
235 230 234 breqtrrd 
 |-  ( ( ph /\ a = 0 ) -> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) )
236 235 ex 
 |-  ( ph -> ( a = 0 -> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) ) )
237 236 adantr 
 |-  ( ( ph /\ ( a e. ( 1 ... A ) -> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) ) ) -> ( a = 0 -> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) ) )
238 simpr 
 |-  ( ( ph /\ ( a e. ( 1 ... A ) -> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) ) ) -> ( a e. ( 1 ... A ) -> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) ) )
239 1cnd 
 |-  ( ( ph /\ ( a e. ( 1 ... A ) -> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) ) ) -> 1 e. CC )
240 239 addlidd 
 |-  ( ( ph /\ ( a e. ( 1 ... A ) -> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) ) ) -> ( 0 + 1 ) = 1 )
241 240 oveq1d 
 |-  ( ( ph /\ ( a e. ( 1 ... A ) -> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) ) ) -> ( ( 0 + 1 ) ... A ) = ( 1 ... A ) )
242 241 eleq2d 
 |-  ( ( ph /\ ( a e. ( 1 ... A ) -> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) ) ) -> ( a e. ( ( 0 + 1 ) ... A ) <-> a e. ( 1 ... A ) ) )
243 242 imbi1d 
 |-  ( ( ph /\ ( a e. ( 1 ... A ) -> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) ) ) -> ( ( a e. ( ( 0 + 1 ) ... A ) -> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) ) <-> ( a e. ( 1 ... A ) -> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) ) ) )
244 238 243 mpbird 
 |-  ( ( ph /\ ( a e. ( 1 ... A ) -> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) ) ) -> ( a e. ( ( 0 + 1 ) ... A ) -> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) ) )
245 237 244 jaod 
 |-  ( ( ph /\ ( a e. ( 1 ... A ) -> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) ) ) -> ( ( a = 0 \/ a e. ( ( 0 + 1 ) ... A ) ) -> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) ) )
246 27 28 jca 
 |-  ( ph -> ( A e. ZZ /\ 0 <_ A ) )
247 eluz1 
 |-  ( 0 e. ZZ -> ( A e. ( ZZ>= ` 0 ) <-> ( A e. ZZ /\ 0 <_ A ) ) )
248 96 247 syl 
 |-  ( ph -> ( A e. ( ZZ>= ` 0 ) <-> ( A e. ZZ /\ 0 <_ A ) ) )
249 246 248 mpbird 
 |-  ( ph -> A e. ( ZZ>= ` 0 ) )
250 249 adantr 
 |-  ( ( ph /\ ( a e. ( 1 ... A ) -> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) ) ) -> A e. ( ZZ>= ` 0 ) )
251 elfzp12 
 |-  ( A e. ( ZZ>= ` 0 ) -> ( a e. ( 0 ... A ) <-> ( a = 0 \/ a e. ( ( 0 + 1 ) ... A ) ) ) )
252 250 251 syl 
 |-  ( ( ph /\ ( a e. ( 1 ... A ) -> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) ) ) -> ( a e. ( 0 ... A ) <-> ( a = 0 \/ a e. ( ( 0 + 1 ) ... A ) ) ) )
253 252 imbi1d 
 |-  ( ( ph /\ ( a e. ( 1 ... A ) -> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) ) ) -> ( ( a e. ( 0 ... A ) -> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) ) <-> ( ( a = 0 \/ a e. ( ( 0 + 1 ) ... A ) ) -> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) ) ) )
254 245 253 mpbird 
 |-  ( ( ph /\ ( a e. ( 1 ... A ) -> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) ) ) -> ( a e. ( 0 ... A ) -> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) ) )
255 254 ex 
 |-  ( ph -> ( ( a e. ( 1 ... A ) -> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) ) -> ( a e. ( 0 ... A ) -> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) ) ) )
256 255 ralimdv2 
 |-  ( ph -> ( A. a e. ( 1 ... A ) N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) -> A. a e. ( 0 ... A ) N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) ) )
257 25 256 mpd 
 |-  ( ph -> A. a e. ( 0 ... A ) N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) )
258 257 adantr 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> A. a e. ( 0 ... A ) N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` a ) ) ) )
259 0zd 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> 0 e. ZZ )
260 27 adantr 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> A e. ZZ )
261 207 zred 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> j e. RR )
262 1red 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> 1 e. RR )
263 simpr2 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> 0 <_ j )
264 0le1 
 |-  0 <_ 1
265 264 a1i 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> 0 <_ 1 )
266 261 262 263 265 addge0d 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> 0 <_ ( j + 1 ) )
267 simpr3 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> j < A )
268 207 260 zltp1led 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> ( j < A <-> ( j + 1 ) <_ A ) )
269 267 268 mpbid 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> ( j + 1 ) <_ A )
270 259 260 208 266 269 elfzd 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> ( j + 1 ) e. ( 0 ... A ) )
271 226 258 270 rspcdva 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> N .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` ( j + 1 ) ) ) ) )
272 26 adantr 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> ( x e. ( Base ` K ) |-> ( P .^ x ) ) e. ( K RingIso K ) )
273 1 2 3 4 5 6 7 8 9 10 11 12 155 156 157 160 159 206 208 271 272 aks6d1c1p3 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> ( N / P ) .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` ( j + 1 ) ) ) ) )
274 23 adantr 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> L e. NN0 )
275 201 adantr 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> ( ( N / P ) gcd R ) = 1 )
276 1 2 3 4 5 6 7 8 9 10 11 12 155 156 157 158 159 160 273 274 275 aks6d1c1p8 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> ( ( N / P ) ^ L ) .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` ( j + 1 ) ) ) ) )
277 1 2 3 4 5 6 7 8 10 11 12 155 156 157 205 159 223 276 aks6d1c1p5 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> ( ( P ^ U ) x. ( ( N / P ) ^ L ) ) .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` ( j + 1 ) ) ) ) )
278 161 277 eqbrtrd 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> E .~ ( X .+ ( C ` ( ( ZRHom ` K ) ` ( j + 1 ) ) ) ) )
279 19 adantr 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> F : ( 0 ... A ) --> NN0 )
280 279 270 ffvelcdmd 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> ( F ` ( j + 1 ) ) e. NN0 )
281 1 2 3 4 5 6 7 8 9 10 11 12 155 156 157 158 159 160 278 280 aks6d1c1p6 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> E .~ ( ( F ` ( j + 1 ) ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` ( j + 1 ) ) ) ) ) )
282 104 adantr 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> W e. Mnd )
283 ovexd 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> ( j + 1 ) e. _V )
284 77 adantr 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> S e. Mnd )
285 82 adantr 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> X e. ( Base ` S ) )
286 79 adantr 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> K e. Ring )
287 117 adantr 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> ( ZRHom ` K ) : ZZ --> ( Base ` K ) )
288 287 208 ffvelcdmd 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> ( ( ZRHom ` K ) ` ( j + 1 ) ) e. ( Base ` K ) )
289 2 8 115 80 ply1sclcl 
 |-  ( ( K e. Ring /\ ( ( ZRHom ` K ) ` ( j + 1 ) ) e. ( Base ` K ) ) -> ( C ` ( ( ZRHom ` K ) ` ( j + 1 ) ) ) e. ( Base ` S ) )
290 286 288 289 syl2anc 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> ( C ` ( ( ZRHom ` K ) ` ( j + 1 ) ) ) e. ( Base ` S ) )
291 80 12 mndcl 
 |-  ( ( S e. Mnd /\ X e. ( Base ` S ) /\ ( C ` ( ( ZRHom ` K ) ` ( j + 1 ) ) ) e. ( Base ` S ) ) -> ( X .+ ( C ` ( ( ZRHom ` K ) ` ( j + 1 ) ) ) ) e. ( Base ` S ) )
292 284 285 290 291 syl3anc 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> ( X .+ ( C ` ( ( ZRHom ` K ) ` ( j + 1 ) ) ) ) e. ( Base ` S ) )
293 292 123 eleqtrdi 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> ( X .+ ( C ` ( ( ZRHom ` K ) ` ( j + 1 ) ) ) ) e. ( Base ` W ) )
294 107 9 282 280 293 mulgnn0cld 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> ( ( F ` ( j + 1 ) ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` ( j + 1 ) ) ) ) ) e. ( Base ` W ) )
295 fveq2 
 |-  ( k = ( j + 1 ) -> ( F ` k ) = ( F ` ( j + 1 ) ) )
296 2fveq3 
 |-  ( k = ( j + 1 ) -> ( C ` ( ( ZRHom ` K ) ` k ) ) = ( C ` ( ( ZRHom ` K ) ` ( j + 1 ) ) ) )
297 296 oveq2d 
 |-  ( k = ( j + 1 ) -> ( X .+ ( C ` ( ( ZRHom ` K ) ` k ) ) ) = ( X .+ ( C ` ( ( ZRHom ` K ) ` ( j + 1 ) ) ) ) )
298 295 297 oveq12d 
 |-  ( k = ( j + 1 ) -> ( ( F ` k ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` k ) ) ) ) = ( ( F ` ( j + 1 ) ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` ( j + 1 ) ) ) ) ) )
299 107 298 gsumsn 
 |-  ( ( W e. Mnd /\ ( j + 1 ) e. _V /\ ( ( F ` ( j + 1 ) ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` ( j + 1 ) ) ) ) ) e. ( Base ` W ) ) -> ( W gsum ( k e. { ( j + 1 ) } |-> ( ( F ` k ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` k ) ) ) ) ) ) = ( ( F ` ( j + 1 ) ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` ( j + 1 ) ) ) ) ) )
300 282 283 294 299 syl3anc 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> ( W gsum ( k e. { ( j + 1 ) } |-> ( ( F ` k ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` k ) ) ) ) ) ) = ( ( F ` ( j + 1 ) ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` ( j + 1 ) ) ) ) ) )
301 281 300 breqtrrd 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) ) -> E .~ ( W gsum ( k e. { ( j + 1 ) } |-> ( ( F ` k ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` k ) ) ) ) ) ) )
302 301 3adant3 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) -> E .~ ( W gsum ( k e. { ( j + 1 ) } |-> ( ( F ` k ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` k ) ) ) ) ) ) )
303 1 2 3 4 5 6 7 8 9 10 11 12 139 140 141 142 143 154 302 aks6d1c1p4 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) -> E .~ ( ( W gsum ( k e. ( 0 ... j ) |-> ( ( F ` k ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` k ) ) ) ) ) ) ( +g ` W ) ( W gsum ( k e. { ( j + 1 ) } |-> ( ( F ` k ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` k ) ) ) ) ) ) ) )
304 145 146 150 cbvmpt 
 |-  ( i e. ( 0 ... ( j + 1 ) ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) = ( k e. ( 0 ... ( j + 1 ) ) |-> ( ( F ` k ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` k ) ) ) ) )
305 304 a1i 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) -> ( i e. ( 0 ... ( j + 1 ) ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) = ( k e. ( 0 ... ( j + 1 ) ) |-> ( ( F ` k ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` k ) ) ) ) ) )
306 305 oveq2d 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) -> ( W gsum ( i e. ( 0 ... ( j + 1 ) ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) = ( W gsum ( k e. ( 0 ... ( j + 1 ) ) |-> ( ( F ` k ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` k ) ) ) ) ) ) )
307 eqid 
 |-  ( +g ` W ) = ( +g ` W )
308 103 3ad2ant1 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) -> W e. CMnd )
309 simp21 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) -> j e. ZZ )
310 simp22 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) -> 0 <_ j )
311 309 310 jca 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) -> ( j e. ZZ /\ 0 <_ j ) )
312 elnn0z 
 |-  ( j e. NN0 <-> ( j e. ZZ /\ 0 <_ j ) )
313 311 312 sylibr 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) -> j e. NN0 )
314 282 3adant3 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) -> W e. Mnd )
315 314 adantr 
 |-  ( ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) /\ k e. ( 0 ... ( j + 1 ) ) ) -> W e. Mnd )
316 19 3ad2ant1 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) -> F : ( 0 ... A ) --> NN0 )
317 316 adantr 
 |-  ( ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) /\ k e. ( 0 ... ( j + 1 ) ) ) -> F : ( 0 ... A ) --> NN0 )
318 0zd 
 |-  ( ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) /\ k e. ( 0 ... ( j + 1 ) ) ) -> 0 e. ZZ )
319 27 3ad2ant1 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) -> A e. ZZ )
320 319 adantr 
 |-  ( ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) /\ k e. ( 0 ... ( j + 1 ) ) ) -> A e. ZZ )
321 elfzelz 
 |-  ( k e. ( 0 ... ( j + 1 ) ) -> k e. ZZ )
322 321 adantl 
 |-  ( ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) /\ k e. ( 0 ... ( j + 1 ) ) ) -> k e. ZZ )
323 elfzle1 
 |-  ( k e. ( 0 ... ( j + 1 ) ) -> 0 <_ k )
324 323 adantl 
 |-  ( ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) /\ k e. ( 0 ... ( j + 1 ) ) ) -> 0 <_ k )
325 322 zred 
 |-  ( ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) /\ k e. ( 0 ... ( j + 1 ) ) ) -> k e. RR )
326 309 adantr 
 |-  ( ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) /\ k e. ( 0 ... ( j + 1 ) ) ) -> j e. ZZ )
327 326 zred 
 |-  ( ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) /\ k e. ( 0 ... ( j + 1 ) ) ) -> j e. RR )
328 1red 
 |-  ( ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) /\ k e. ( 0 ... ( j + 1 ) ) ) -> 1 e. RR )
329 327 328 readdcld 
 |-  ( ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) /\ k e. ( 0 ... ( j + 1 ) ) ) -> ( j + 1 ) e. RR )
330 320 zred 
 |-  ( ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) /\ k e. ( 0 ... ( j + 1 ) ) ) -> A e. RR )
331 elfzle2 
 |-  ( k e. ( 0 ... ( j + 1 ) ) -> k <_ ( j + 1 ) )
332 331 adantl 
 |-  ( ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) /\ k e. ( 0 ... ( j + 1 ) ) ) -> k <_ ( j + 1 ) )
333 simpl23 
 |-  ( ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) /\ k e. ( 0 ... ( j + 1 ) ) ) -> j < A )
334 326 320 zltp1led 
 |-  ( ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) /\ k e. ( 0 ... ( j + 1 ) ) ) -> ( j < A <-> ( j + 1 ) <_ A ) )
335 333 334 mpbid 
 |-  ( ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) /\ k e. ( 0 ... ( j + 1 ) ) ) -> ( j + 1 ) <_ A )
336 325 329 330 332 335 letrd 
 |-  ( ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) /\ k e. ( 0 ... ( j + 1 ) ) ) -> k <_ A )
337 318 320 322 324 336 elfzd 
 |-  ( ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) /\ k e. ( 0 ... ( j + 1 ) ) ) -> k e. ( 0 ... A ) )
338 317 337 ffvelcdmd 
 |-  ( ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) /\ k e. ( 0 ... ( j + 1 ) ) ) -> ( F ` k ) e. NN0 )
339 284 3adant3 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) -> S e. Mnd )
340 339 adantr 
 |-  ( ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) /\ k e. ( 0 ... ( j + 1 ) ) ) -> S e. Mnd )
341 285 3adant3 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) -> X e. ( Base ` S ) )
342 341 adantr 
 |-  ( ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) /\ k e. ( 0 ... ( j + 1 ) ) ) -> X e. ( Base ` S ) )
343 286 3adant3 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) -> K e. Ring )
344 343 adantr 
 |-  ( ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) /\ k e. ( 0 ... ( j + 1 ) ) ) -> K e. Ring )
345 344 112 116 3syl 
 |-  ( ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) /\ k e. ( 0 ... ( j + 1 ) ) ) -> ( ZRHom ` K ) : ZZ --> ( Base ` K ) )
346 345 322 ffvelcdmd 
 |-  ( ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) /\ k e. ( 0 ... ( j + 1 ) ) ) -> ( ( ZRHom ` K ) ` k ) e. ( Base ` K ) )
347 2 8 115 80 ply1sclcl 
 |-  ( ( K e. Ring /\ ( ( ZRHom ` K ) ` k ) e. ( Base ` K ) ) -> ( C ` ( ( ZRHom ` K ) ` k ) ) e. ( Base ` S ) )
348 344 346 347 syl2anc 
 |-  ( ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) /\ k e. ( 0 ... ( j + 1 ) ) ) -> ( C ` ( ( ZRHom ` K ) ` k ) ) e. ( Base ` S ) )
349 80 12 mndcl 
 |-  ( ( S e. Mnd /\ X e. ( Base ` S ) /\ ( C ` ( ( ZRHom ` K ) ` k ) ) e. ( Base ` S ) ) -> ( X .+ ( C ` ( ( ZRHom ` K ) ` k ) ) ) e. ( Base ` S ) )
350 340 342 348 349 syl3anc 
 |-  ( ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) /\ k e. ( 0 ... ( j + 1 ) ) ) -> ( X .+ ( C ` ( ( ZRHom ` K ) ` k ) ) ) e. ( Base ` S ) )
351 350 123 eleqtrdi 
 |-  ( ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) /\ k e. ( 0 ... ( j + 1 ) ) ) -> ( X .+ ( C ` ( ( ZRHom ` K ) ` k ) ) ) e. ( Base ` W ) )
352 107 9 315 338 351 mulgnn0cld 
 |-  ( ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) /\ k e. ( 0 ... ( j + 1 ) ) ) -> ( ( F ` k ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` k ) ) ) ) e. ( Base ` W ) )
353 107 307 308 313 352 gsummptfzsplit 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) -> ( W gsum ( k e. ( 0 ... ( j + 1 ) ) |-> ( ( F ` k ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` k ) ) ) ) ) ) = ( ( W gsum ( k e. ( 0 ... j ) |-> ( ( F ` k ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` k ) ) ) ) ) ) ( +g ` W ) ( W gsum ( k e. { ( j + 1 ) } |-> ( ( F ` k ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` k ) ) ) ) ) ) ) )
354 306 353 eqtrd 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) -> ( W gsum ( i e. ( 0 ... ( j + 1 ) ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) = ( ( W gsum ( k e. ( 0 ... j ) |-> ( ( F ` k ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` k ) ) ) ) ) ) ( +g ` W ) ( W gsum ( k e. { ( j + 1 ) } |-> ( ( F ` k ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` k ) ) ) ) ) ) ) )
355 303 354 breqtrrd 
 |-  ( ( ph /\ ( j e. ZZ /\ 0 <_ j /\ j < A ) /\ E .~ ( W gsum ( i e. ( 0 ... j ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) -> E .~ ( W gsum ( i e. ( 0 ... ( j + 1 ) ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
356 35 39 43 47 138 355 96 27 28 fzindd 
 |-  ( ( ph /\ ( A e. ZZ /\ 0 <_ A /\ A <_ A ) ) -> E .~ ( W gsum ( i e. ( 0 ... A ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
357 356 ex 
 |-  ( ph -> ( ( A e. ZZ /\ 0 <_ A /\ A <_ A ) -> E .~ ( W gsum ( i e. ( 0 ... A ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) )
358 31 357 mpd 
 |-  ( ph -> E .~ ( W gsum ( i e. ( 0 ... A ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
359 20 a1i 
 |-  ( ph -> G = ( g e. ( NN0 ^m ( 0 ... A ) ) |-> ( W gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) )
360 simplr 
 |-  ( ( ( ph /\ g = F ) /\ i e. ( 0 ... A ) ) -> g = F )
361 360 fveq1d 
 |-  ( ( ( ph /\ g = F ) /\ i e. ( 0 ... A ) ) -> ( g ` i ) = ( F ` i ) )
362 361 oveq1d 
 |-  ( ( ( ph /\ g = F ) /\ i e. ( 0 ... A ) ) -> ( ( g ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) = ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) )
363 362 mpteq2dva 
 |-  ( ( ph /\ g = F ) -> ( i e. ( 0 ... A ) |-> ( ( g ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) = ( i e. ( 0 ... A ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) )
364 363 oveq2d 
 |-  ( ( ph /\ g = F ) -> ( W gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) = ( W gsum ( i e. ( 0 ... A ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
365 nn0ex 
 |-  NN0 e. _V
366 365 a1i 
 |-  ( ph -> NN0 e. _V )
367 ovexd 
 |-  ( ph -> ( 0 ... A ) e. _V )
368 366 367 elmapd 
 |-  ( ph -> ( F e. ( NN0 ^m ( 0 ... A ) ) <-> F : ( 0 ... A ) --> NN0 ) )
369 19 368 mpbird 
 |-  ( ph -> F e. ( NN0 ^m ( 0 ... A ) ) )
370 ovexd 
 |-  ( ph -> ( W gsum ( i e. ( 0 ... A ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) e. _V )
371 359 364 369 370 fvmptd 
 |-  ( ph -> ( G ` F ) = ( W gsum ( i e. ( 0 ... A ) |-> ( ( F ` i ) D ( X .+ ( C ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
372 358 371 breqtrrd 
 |-  ( ph -> E .~ ( G ` F ) )