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 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝑒 ↑ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝑓 ) ‘ ( 𝑒 ↑ 𝑦 ) ) ) }
aks6d1c1.2 ⊢ 𝑆 = ( Poly1 ‘ 𝐾 )
aks6d1c1.3 ⊢ 𝐵 = ( Base ‘ 𝑆 )
aks6d1c1.4 ⊢ 𝑋 = ( var1 ‘ 𝐾 )
aks6d1c1.5 ⊢ 𝑊 = ( mulGrp ‘ 𝑆 )
aks6d1c1.6 ⊢ 𝑉 = ( mulGrp ‘ 𝐾 )
aks6d1c1.7 ⊢ ↑ = ( .g ‘ 𝑉 )
aks6d1c1.8 ⊢ 𝐶 = ( algSc ‘ 𝑆 )
aks6d1c1.9 ⊢ 𝐷 = ( .g ‘ 𝑊 )
aks6d1c1.10 ⊢ 𝑃 = ( chr ‘ 𝐾 )
aks6d1c1.11 ⊢ 𝑂 = ( eval1 ‘ 𝐾 )
aks6d1c1.12 ⊢ + = ( +g ‘ 𝑆 )
aks6d1c1.13 ⊢ ( 𝜑 → 𝐾 ∈ Field )
aks6d1c1.14 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
aks6d1c1.15 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
aks6d1c1.16 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
aks6d1c1.17 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
aks6d1c1.18 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
aks6d1c1.19 ⊢ ( 𝜑 → 𝐹 : ( 0 ... 𝐴 ) ⟶ ℕ0 )
aks6d1c1.20 ⊢ 𝐺 = ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( 𝑊 Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) 𝐷 ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
aks6d1c1.21 ⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
aks6d1c1.22 ⊢ ( 𝜑 → 𝑈 ∈ ℕ0 )
aks6d1c1.23 ⊢ ( 𝜑 → 𝐿 ∈ ℕ0 )
aks6d1c1.24 ⊢ 𝐸 = ( ( 𝑃 ↑ 𝑈 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝐿 ) )
aks6d1c1.25 ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) 𝑁 ∼ ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) )
aks6d1c1.26 ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
Assertion aks6d1c1 ( 𝜑 → 𝐸 ∼ ( 𝐺 ‘ 𝐹 ) )

Proof

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