Metamath Proof Explorer

Theorem aks6d1c1p6

Description: If a polynomials F is introspective to E , then so are its powers. (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 )
aks6d1c1p6.1 ⊢ ( 𝜑 → 𝐸 ∼ 𝐹 )
aks6d1c1p6.2 ⊢ ( 𝜑 → 𝐿 ∈ ℕ0 )
Assertion aks6d1c1p6 ( 𝜑 → 𝐸 ∼ ( 𝐿 𝐷 𝐹 ) )

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 aks6d1c1p6.1 ⊢ ( 𝜑 → 𝐸 ∼ 𝐹 )
20 aks6d1c1p6.2 ⊢ ( 𝜑 → 𝐿 ∈ ℕ0 )
21 oveq1 ⊢ ( ℎ = 0 → ( ℎ 𝐷 𝐹 ) = ( 0 𝐷 𝐹 ) )
22 21 breq2d ⊢ ( ℎ = 0 → ( 𝐸 ∼ ( ℎ 𝐷 𝐹 ) ↔ 𝐸 ∼ ( 0 𝐷 𝐹 ) ) )
23 oveq1 ⊢ ( ℎ = 𝑖 → ( ℎ 𝐷 𝐹 ) = ( 𝑖 𝐷 𝐹 ) )
24 23 breq2d ⊢ ( ℎ = 𝑖 → ( 𝐸 ∼ ( ℎ 𝐷 𝐹 ) ↔ 𝐸 ∼ ( 𝑖 𝐷 𝐹 ) ) )
25 oveq1 ⊢ ( ℎ = ( 𝑖 + 1 ) → ( ℎ 𝐷 𝐹 ) = ( ( 𝑖 + 1 ) 𝐷 𝐹 ) )
26 25 breq2d ⊢ ( ℎ = ( 𝑖 + 1 ) → ( 𝐸 ∼ ( ℎ 𝐷 𝐹 ) ↔ 𝐸 ∼ ( ( 𝑖 + 1 ) 𝐷 𝐹 ) ) )
27 oveq1 ⊢ ( ℎ = 𝐿 → ( ℎ 𝐷 𝐹 ) = ( 𝐿 𝐷 𝐹 ) )
28 27 breq2d ⊢ ( ℎ = 𝐿 → ( 𝐸 ∼ ( ℎ 𝐷 𝐹 ) ↔ 𝐸 ∼ ( 𝐿 𝐷 𝐹 ) ) )
29 1 19 aks6d1c1p1rcl ⊢ ( 𝜑 → ( 𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵 ) )
30 29 simprd ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
31 30 3 eleqtrdi ⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ 𝑆 ) )
32 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
33 5 32 mgpbas ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑊 )
34 31 33 eleqtrdi ⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ 𝑊 ) )
35 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
36 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
37 35 36 9 mulg0 ⊢ ( 𝐹 ∈ ( Base ‘ 𝑊 ) → ( 0 𝐷 𝐹 ) = ( 0g ‘ 𝑊 ) )
38 34 37 syl ⊢ ( 𝜑 → ( 0 𝐷 𝐹 ) = ( 0g ‘ 𝑊 ) )
39 eqid ⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
40 5 39 ringidval ⊢ ( 1r ‘ 𝑆 ) = ( 0g ‘ 𝑊 )
41 40 eqcomi ⊢ ( 0g ‘ 𝑊 ) = ( 1r ‘ 𝑆 )
42 38 41 eqtrdi ⊢ ( 𝜑 → ( 0 𝐷 𝐹 ) = ( 1r ‘ 𝑆 ) )
43 42 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 0 𝐷 𝐹 ) = ( 1r ‘ 𝑆 ) )
44 43 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑂 ‘ ( 0 𝐷 𝐹 ) ) = ( 𝑂 ‘ ( 1r ‘ 𝑆 ) ) )
45 44 fveq1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ ( 0 𝐷 𝐹 ) ) ‘ 𝑦 ) = ( ( 𝑂 ‘ ( 1r ‘ 𝑆 ) ) ‘ 𝑦 ) )
46 45 oveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐸 ↑ ( ( 𝑂 ‘ ( 0 𝐷 𝐹 ) ) ‘ 𝑦 ) ) = ( 𝐸 ↑ ( ( 𝑂 ‘ ( 1r ‘ 𝑆 ) ) ‘ 𝑦 ) ) )
47 13 fldcrngd ⊢ ( 𝜑 → 𝐾 ∈ CRing )
48 crngring ⊢ ( 𝐾 ∈ CRing → 𝐾 ∈ Ring )
49 47 48 syl ⊢ ( 𝜑 → 𝐾 ∈ Ring )
50 eqid ⊢ ( 1r ‘ 𝐾 ) = ( 1r ‘ 𝐾 )
51 2 8 50 39 ply1scl1 ⊢ ( 𝐾 ∈ Ring → ( 𝐶 ‘ ( 1r ‘ 𝐾 ) ) = ( 1r ‘ 𝑆 ) )
52 49 51 syl ⊢ ( 𝜑 → ( 𝐶 ‘ ( 1r ‘ 𝐾 ) ) = ( 1r ‘ 𝑆 ) )
53 52 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐶 ‘ ( 1r ‘ 𝐾 ) ) = ( 1r ‘ 𝑆 ) )
54 53 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 1r ‘ 𝑆 ) = ( 𝐶 ‘ ( 1r ‘ 𝐾 ) ) )
55 54 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑂 ‘ ( 1r ‘ 𝑆 ) ) = ( 𝑂 ‘ ( 𝐶 ‘ ( 1r ‘ 𝐾 ) ) ) )
56 55 fveq1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ ( 1r ‘ 𝑆 ) ) ‘ 𝑦 ) = ( ( 𝑂 ‘ ( 𝐶 ‘ ( 1r ‘ 𝐾 ) ) ) ‘ 𝑦 ) )
57 56 oveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐸 ↑ ( ( 𝑂 ‘ ( 1r ‘ 𝑆 ) ) ‘ 𝑦 ) ) = ( 𝐸 ↑ ( ( 𝑂 ‘ ( 𝐶 ‘ ( 1r ‘ 𝐾 ) ) ) ‘ 𝑦 ) ) )
58 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
59 47 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝐾 ∈ CRing )
60 58 50 ringidcl ⊢ ( 𝐾 ∈ Ring → ( 1r ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
61 49 60 syl ⊢ ( 𝜑 → ( 1r ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
62 61 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 1r ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
63 6 crngmgp ⊢ ( 𝐾 ∈ CRing → 𝑉 ∈ CMnd )
64 47 63 syl ⊢ ( 𝜑 → 𝑉 ∈ CMnd )
65 15 nnnn0d ⊢ ( 𝜑 → 𝑅 ∈ ℕ0 )
66 eqid ⊢ ( .g ‘ 𝑉 ) = ( .g ‘ 𝑉 )
67 64 65 66 isprimroot ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ↔ ( 𝑦 ∈ ( Base ‘ 𝑉 ) ∧ ( 𝑅 ( .g ‘ 𝑉 ) 𝑦 ) = ( 0g ‘ 𝑉 ) ∧ ∀ 𝑧 ∈ ℕ0 ( ( 𝑧 ( .g ‘ 𝑉 ) 𝑦 ) = ( 0g ‘ 𝑉 ) → 𝑅 ∥ 𝑧 ) ) ) )
68 67 biimpd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) → ( 𝑦 ∈ ( Base ‘ 𝑉 ) ∧ ( 𝑅 ( .g ‘ 𝑉 ) 𝑦 ) = ( 0g ‘ 𝑉 ) ∧ ∀ 𝑧 ∈ ℕ0 ( ( 𝑧 ( .g ‘ 𝑉 ) 𝑦 ) = ( 0g ‘ 𝑉 ) → 𝑅 ∥ 𝑧 ) ) ) )
69 68 imp ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑦 ∈ ( Base ‘ 𝑉 ) ∧ ( 𝑅 ( .g ‘ 𝑉 ) 𝑦 ) = ( 0g ‘ 𝑉 ) ∧ ∀ 𝑧 ∈ ℕ0 ( ( 𝑧 ( .g ‘ 𝑉 ) 𝑦 ) = ( 0g ‘ 𝑉 ) → 𝑅 ∥ 𝑧 ) ) )
70 69 simp1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑦 ∈ ( Base ‘ 𝑉 ) )
71 6 58 mgpbas ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝑉 )
72 71 eqcomi ⊢ ( Base ‘ 𝑉 ) = ( Base ‘ 𝐾 )
73 70 72 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑦 ∈ ( Base ‘ 𝐾 ) )
74 11 2 58 8 3 59 62 73 evl1scad ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝐶 ‘ ( 1r ‘ 𝐾 ) ) ∈ 𝐵 ∧ ( ( 𝑂 ‘ ( 𝐶 ‘ ( 1r ‘ 𝐾 ) ) ) ‘ 𝑦 ) = ( 1r ‘ 𝐾 ) ) )
75 74 simprd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ ( 𝐶 ‘ ( 1r ‘ 𝐾 ) ) ) ‘ 𝑦 ) = ( 1r ‘ 𝐾 ) )
76 75 oveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐸 ↑ ( ( 𝑂 ‘ ( 𝐶 ‘ ( 1r ‘ 𝐾 ) ) ) ‘ 𝑦 ) ) = ( 𝐸 ↑ ( 1r ‘ 𝐾 ) ) )
77 64 cmnmndd ⊢ ( 𝜑 → 𝑉 ∈ Mnd )
78 29 simpld ⊢ ( 𝜑 → 𝐸 ∈ ℕ )
79 78 nnnn0d ⊢ ( 𝜑 → 𝐸 ∈ ℕ0 )
80 eqid ⊢ ( Base ‘ 𝑉 ) = ( Base ‘ 𝑉 )
81 6 50 ringidval ⊢ ( 1r ‘ 𝐾 ) = ( 0g ‘ 𝑉 )
82 80 7 81 mulgnn0z ⊢ ( ( 𝑉 ∈ Mnd ∧ 𝐸 ∈ ℕ0 ) → ( 𝐸 ↑ ( 1r ‘ 𝐾 ) ) = ( 1r ‘ 𝐾 ) )
83 77 79 82 syl2anc ⊢ ( 𝜑 → ( 𝐸 ↑ ( 1r ‘ 𝐾 ) ) = ( 1r ‘ 𝐾 ) )
84 83 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐸 ↑ ( 1r ‘ 𝐾 ) ) = ( 1r ‘ 𝐾 ) )
85 77 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑉 ∈ Mnd )
86 79 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝐸 ∈ ℕ0 )
87 71 7 mulgnn0cl ⊢ ( ( 𝑉 ∈ Mnd ∧ 𝐸 ∈ ℕ0 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( 𝐸 ↑ 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
88 85 86 73 87 syl3anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐸 ↑ 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
89 11 2 58 8 3 59 62 88 evl1scad ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝐶 ‘ ( 1r ‘ 𝐾 ) ) ∈ 𝐵 ∧ ( ( 𝑂 ‘ ( 𝐶 ‘ ( 1r ‘ 𝐾 ) ) ) ‘ ( 𝐸 ↑ 𝑦 ) ) = ( 1r ‘ 𝐾 ) ) )
90 89 simprd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ ( 𝐶 ‘ ( 1r ‘ 𝐾 ) ) ) ‘ ( 𝐸 ↑ 𝑦 ) ) = ( 1r ‘ 𝐾 ) )
91 90 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 1r ‘ 𝐾 ) = ( ( 𝑂 ‘ ( 𝐶 ‘ ( 1r ‘ 𝐾 ) ) ) ‘ ( 𝐸 ↑ 𝑦 ) ) )
92 76 84 91 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐸 ↑ ( ( 𝑂 ‘ ( 𝐶 ‘ ( 1r ‘ 𝐾 ) ) ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ ( 𝐶 ‘ ( 1r ‘ 𝐾 ) ) ) ‘ ( 𝐸 ↑ 𝑦 ) ) )
93 53 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑂 ‘ ( 𝐶 ‘ ( 1r ‘ 𝐾 ) ) ) = ( 𝑂 ‘ ( 1r ‘ 𝑆 ) ) )
94 93 fveq1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ ( 𝐶 ‘ ( 1r ‘ 𝐾 ) ) ) ‘ ( 𝐸 ↑ 𝑦 ) ) = ( ( 𝑂 ‘ ( 1r ‘ 𝑆 ) ) ‘ ( 𝐸 ↑ 𝑦 ) ) )
95 57 92 94 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐸 ↑ ( ( 𝑂 ‘ ( 1r ‘ 𝑆 ) ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ ( 1r ‘ 𝑆 ) ) ‘ ( 𝐸 ↑ 𝑦 ) ) )
96 43 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 1r ‘ 𝑆 ) = ( 0 𝐷 𝐹 ) )
97 96 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑂 ‘ ( 1r ‘ 𝑆 ) ) = ( 𝑂 ‘ ( 0 𝐷 𝐹 ) ) )
98 97 fveq1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ ( 1r ‘ 𝑆 ) ) ‘ ( 𝐸 ↑ 𝑦 ) ) = ( ( 𝑂 ‘ ( 0 𝐷 𝐹 ) ) ‘ ( 𝐸 ↑ 𝑦 ) ) )
99 46 95 98 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐸 ↑ ( ( 𝑂 ‘ ( 0 𝐷 𝐹 ) ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ ( 0 𝐷 𝐹 ) ) ‘ ( 𝐸 ↑ 𝑦 ) ) )
100 99 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ ( 0 𝐷 𝐹 ) ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ ( 0 𝐷 𝐹 ) ) ‘ ( 𝐸 ↑ 𝑦 ) ) )
101 2 ply1ring ⊢ ( 𝐾 ∈ Ring → 𝑆 ∈ Ring )
102 49 101 syl ⊢ ( 𝜑 → 𝑆 ∈ Ring )
103 32 39 ringidcl ⊢ ( 𝑆 ∈ Ring → ( 1r ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
104 102 103 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
105 42 eqcomd ⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) = ( 0 𝐷 𝐹 ) )
106 3 a1i ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑆 ) )
107 106 eqcomd ⊢ ( 𝜑 → ( Base ‘ 𝑆 ) = 𝐵 )
108 105 107 eleq12d ⊢ ( 𝜑 → ( ( 1r ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) ↔ ( 0 𝐷 𝐹 ) ∈ 𝐵 ) )
109 104 108 mpbid ⊢ ( 𝜑 → ( 0 𝐷 𝐹 ) ∈ 𝐵 )
110 1 109 78 aks6d1c1p1 ⊢ ( 𝜑 → ( 𝐸 ∼ ( 0 𝐷 𝐹 ) ↔ ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ ( 0 𝐷 𝐹 ) ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ ( 0 𝐷 𝐹 ) ) ‘ ( 𝐸 ↑ 𝑦 ) ) ) )
111 100 110 mpbird ⊢ ( 𝜑 → 𝐸 ∼ ( 0 𝐷 𝐹 ) )
112 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝐸 ∼ ( 𝑖 𝐷 𝐹 ) ) → 𝐾 ∈ Field )
113 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝐸 ∼ ( 𝑖 𝐷 𝐹 ) ) → 𝑃 ∈ ℙ )
114 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝐸 ∼ ( 𝑖 𝐷 𝐹 ) ) → 𝑅 ∈ ℕ )
115 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝐸 ∼ ( 𝑖 𝐷 𝐹 ) ) → ( 𝑁 gcd 𝑅 ) = 1 )
116 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝐸 ∼ ( 𝑖 𝐷 𝐹 ) ) → 𝑃 ∥ 𝑁 )
117 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝐸 ∼ ( 𝑖 𝐷 𝐹 ) ) → 𝐸 ∼ ( 𝑖 𝐷 𝐹 ) )
118 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝐸 ∼ ( 𝑖 𝐷 𝐹 ) ) → 𝐸 ∼ 𝐹 )
119 1 2 3 4 5 6 7 8 9 10 11 12 112 113 114 115 116 117 118 aks6d1c1p4 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝐸 ∼ ( 𝑖 𝐷 𝐹 ) ) → 𝐸 ∼ ( ( 𝑖 𝐷 𝐹 ) ( +g ‘ 𝑊 ) 𝐹 ) )
120 5 ringmgp ⊢ ( 𝑆 ∈ Ring → 𝑊 ∈ Mnd )
121 102 120 syl ⊢ ( 𝜑 → 𝑊 ∈ Mnd )
122 121 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑊 ∈ Mnd )
123 122 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝐸 ∼ ( 𝑖 𝐷 𝐹 ) ) → 𝑊 ∈ Mnd )
124 simplr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝐸 ∼ ( 𝑖 𝐷 𝐹 ) ) → 𝑖 ∈ ℕ0 )
125 33 a1i ⊢ ( 𝜑 → ( Base ‘ 𝑆 ) = ( Base ‘ 𝑊 ) )
126 106 125 eqtrd ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑊 ) )
127 126 eleq2d ⊢ ( 𝜑 → ( 𝐹 ∈ 𝐵 ↔ 𝐹 ∈ ( Base ‘ 𝑊 ) ) )
128 30 127 mpbid ⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ 𝑊 ) )
129 128 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝐹 ∈ ( Base ‘ 𝑊 ) )
130 129 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝐸 ∼ ( 𝑖 𝐷 𝐹 ) ) → 𝐹 ∈ ( Base ‘ 𝑊 ) )
131 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
132 35 9 131 mulgnn0p1 ⊢ ( ( 𝑊 ∈ Mnd ∧ 𝑖 ∈ ℕ0 ∧ 𝐹 ∈ ( Base ‘ 𝑊 ) ) → ( ( 𝑖 + 1 ) 𝐷 𝐹 ) = ( ( 𝑖 𝐷 𝐹 ) ( +g ‘ 𝑊 ) 𝐹 ) )
133 123 124 130 132 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝐸 ∼ ( 𝑖 𝐷 𝐹 ) ) → ( ( 𝑖 + 1 ) 𝐷 𝐹 ) = ( ( 𝑖 𝐷 𝐹 ) ( +g ‘ 𝑊 ) 𝐹 ) )
134 119 133 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝐸 ∼ ( 𝑖 𝐷 𝐹 ) ) → 𝐸 ∼ ( ( 𝑖 + 1 ) 𝐷 𝐹 ) )
135 22 24 26 28 111 134 nn0indd ⊢ ( ( 𝜑 ∧ 𝐿 ∈ ℕ0 ) → 𝐸 ∼ ( 𝐿 𝐷 𝐹 ) )
136 20 135 mpdan ⊢ ( 𝜑 → 𝐸 ∼ ( 𝐿 𝐷 𝐹 ) )