Metamath Proof Explorer

Theorem aks6d1c1p2

Description: P and linear factors are introspective. (Contributed by metakunt, 25-Apr-2025)

Ref Expression
Hypotheses aks6d1c1p2.1 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝑒 ↑ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝑓 ) ‘ ( 𝑒 ↑ 𝑦 ) ) ) }
aks6d1c1p2.2 ⊢ 𝑆 = ( Poly1 ‘ 𝐾 )
aks6d1c1p2.3 ⊢ 𝐵 = ( Base ‘ 𝑆 )
aks6d1c1p2.4 ⊢ 𝑋 = ( var1 ‘ 𝐾 )
aks6d1c1p2.5 ⊢ 𝑊 = ( mulGrp ‘ 𝑆 )
aks6d1c1p2.6 ⊢ 𝑉 = ( mulGrp ‘ 𝐾 )
aks6d1c1p2.7 ⊢ ↑ = ( .g ‘ 𝑉 )
aks6d1c1p2.8 ⊢ 𝐶 = ( algSc ‘ 𝑆 )
aks6d1c1p2.9 ⊢ 𝐷 = ( .g ‘ 𝑊 )
aks6d1c1p2.10 ⊢ 𝑃 = ( chr ‘ 𝐾 )
aks6d1c1p2.11 ⊢ 𝑂 = ( eval1 ‘ 𝐾 )
aks6d1c1p2.12 ⊢ + = ( +g ‘ 𝑆 )
aks6d1c1p2.13 ⊢ ( 𝜑 → 𝐾 ∈ Field )
aks6d1c1p2.14 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
aks6d1c1p2.15 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
aks6d1c1p2.16 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
aks6d1c1p2.17 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
aks6d1c1p2.18 ⊢ 𝐹 = ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
aks6d1c1p2.19 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
Assertion aks6d1c1p2 ( 𝜑 → 𝑃 ∼ 𝐹 )

Proof

Step Hyp Ref Expression
1 aks6d1c1p2.1 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝑒 ↑ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝑓 ) ‘ ( 𝑒 ↑ 𝑦 ) ) ) }
2 aks6d1c1p2.2 ⊢ 𝑆 = ( Poly1 ‘ 𝐾 )
3 aks6d1c1p2.3 ⊢ 𝐵 = ( Base ‘ 𝑆 )
4 aks6d1c1p2.4 ⊢ 𝑋 = ( var1 ‘ 𝐾 )
5 aks6d1c1p2.5 ⊢ 𝑊 = ( mulGrp ‘ 𝑆 )
6 aks6d1c1p2.6 ⊢ 𝑉 = ( mulGrp ‘ 𝐾 )
7 aks6d1c1p2.7 ⊢ ↑ = ( .g ‘ 𝑉 )
8 aks6d1c1p2.8 ⊢ 𝐶 = ( algSc ‘ 𝑆 )
9 aks6d1c1p2.9 ⊢ 𝐷 = ( .g ‘ 𝑊 )
10 aks6d1c1p2.10 ⊢ 𝑃 = ( chr ‘ 𝐾 )
11 aks6d1c1p2.11 ⊢ 𝑂 = ( eval1 ‘ 𝐾 )
12 aks6d1c1p2.12 ⊢ + = ( +g ‘ 𝑆 )
13 aks6d1c1p2.13 ⊢ ( 𝜑 → 𝐾 ∈ Field )
14 aks6d1c1p2.14 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
15 aks6d1c1p2.15 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
16 aks6d1c1p2.16 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
17 aks6d1c1p2.17 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
18 aks6d1c1p2.18 ⊢ 𝐹 = ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
19 aks6d1c1p2.19 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
20 isfld ⊢ ( 𝐾 ∈ Field ↔ ( 𝐾 ∈ DivRing ∧ 𝐾 ∈ CRing ) )
21 13 20 sylib ⊢ ( 𝜑 → ( 𝐾 ∈ DivRing ∧ 𝐾 ∈ CRing ) )
22 21 simprd ⊢ ( 𝜑 → 𝐾 ∈ CRing )
23 6 crngmgp ⊢ ( 𝐾 ∈ CRing → 𝑉 ∈ CMnd )
24 22 23 syl ⊢ ( 𝜑 → 𝑉 ∈ CMnd )
25 15 nnnn0d ⊢ ( 𝜑 → 𝑅 ∈ ℕ0 )
26 24 25 7 isprimroot ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ↔ ( 𝑦 ∈ ( Base ‘ 𝑉 ) ∧ ( 𝑅 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) → 𝑅 ∥ 𝑙 ) ) ) )
27 26 biimpd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) → ( 𝑦 ∈ ( Base ‘ 𝑉 ) ∧ ( 𝑅 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) → 𝑅 ∥ 𝑙 ) ) ) )
28 27 imp ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑦 ∈ ( Base ‘ 𝑉 ) ∧ ( 𝑅 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) → 𝑅 ∥ 𝑙 ) ) )
29 28 simp1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑦 ∈ ( Base ‘ 𝑉 ) )
30 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
31 6 30 mgpbas ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝑉 )
32 31 eqcomi ⊢ ( Base ‘ 𝑉 ) = ( Base ‘ 𝐾 )
33 32 a1i ⊢ ( 𝜑 → ( Base ‘ 𝑉 ) = ( Base ‘ 𝐾 ) )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( Base ‘ 𝑉 ) = ( Base ‘ 𝐾 ) )
35 34 eleq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑦 ∈ ( Base ‘ 𝑉 ) ↔ 𝑦 ∈ ( Base ‘ 𝐾 ) ) )
36 29 35 mpbid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑦 ∈ ( Base ‘ 𝐾 ) )
37 36 ex ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) → 𝑦 ∈ ( Base ‘ 𝐾 ) ) )
38 18 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → 𝐹 = ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
39 38 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑂 ‘ 𝐹 ) = ( 𝑂 ‘ ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) )
40 39 fveq1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) = ( ( 𝑂 ‘ ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ 𝑦 ) )
41 40 oveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( 𝑃 ↑ ( ( 𝑂 ‘ ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ 𝑦 ) ) )
42 22 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → 𝐾 ∈ CRing )
43 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → 𝑦 ∈ ( Base ‘ 𝐾 ) )
44 crngring ⊢ ( 𝐾 ∈ CRing → 𝐾 ∈ Ring )
45 4 2 3 vr1cl ⊢ ( 𝐾 ∈ Ring → 𝑋 ∈ 𝐵 )
46 42 44 45 3syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → 𝑋 ∈ 𝐵 )
47 11 4 30 2 3 42 43 evl1vard ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝑋 ) ‘ 𝑦 ) = 𝑦 ) )
48 47 simprd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑂 ‘ 𝑋 ) ‘ 𝑦 ) = 𝑦 )
49 46 48 jca ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝑋 ) ‘ 𝑦 ) = 𝑦 ) )
50 22 44 syl ⊢ ( 𝜑 → 𝐾 ∈ Ring )
51 22 crngringd ⊢ ( 𝜑 → 𝐾 ∈ Ring )
52 eqid ⊢ ( ℤRHom ‘ 𝐾 ) = ( ℤRHom ‘ 𝐾 )
53 52 zrhrhm ⊢ ( 𝐾 ∈ Ring → ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring RingHom 𝐾 ) )
54 rhmghm ⊢ ( ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring RingHom 𝐾 ) → ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring GrpHom 𝐾 ) )
55 zringbas ⊢ ℤ = ( Base ‘ ℤring )
56 55 30 ghmf ⊢ ( ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring GrpHom 𝐾 ) → ( ℤRHom ‘ 𝐾 ) : ℤ ⟶ ( Base ‘ 𝐾 ) )
57 51 53 54 56 4syl ⊢ ( 𝜑 → ( ℤRHom ‘ 𝐾 ) : ℤ ⟶ ( Base ‘ 𝐾 ) )
58 57 19 ffvelcdmd ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ∈ ( Base ‘ 𝐾 ) )
59 2 8 30 3 ply1sclcl ⊢ ( ( 𝐾 ∈ Ring ∧ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ∈ 𝐵 )
60 50 58 59 syl2anc ⊢ ( 𝜑 → ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ∈ 𝐵 )
61 60 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ∈ 𝐵 )
62 58 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ∈ ( Base ‘ 𝐾 ) )
63 11 2 30 8 3 42 62 43 evl1scad ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ∈ 𝐵 ∧ ( ( 𝑂 ‘ ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ‘ 𝑦 ) = ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
64 63 simprd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑂 ‘ ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ‘ 𝑦 ) = ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) )
65 61 64 jca ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ∈ 𝐵 ∧ ( ( 𝑂 ‘ ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ‘ 𝑦 ) = ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
66 eqid ⊢ ( +g ‘ 𝐾 ) = ( +g ‘ 𝐾 )
67 11 2 30 3 42 43 49 65 12 66 evl1addd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ∈ 𝐵 ∧ ( ( 𝑂 ‘ ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ 𝑦 ) = ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
68 67 simprd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑂 ‘ ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ 𝑦 ) = ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
69 68 oveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ↑ ( ( 𝑂 ‘ ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ 𝑦 ) ) = ( 𝑃 ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
70 41 69 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( 𝑃 ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
71 39 fveq1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝑃 ↑ 𝑦 ) ) = ( ( 𝑂 ‘ ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ ( 𝑃 ↑ 𝑦 ) ) )
72 eqid ⊢ ( Base ‘ 𝑉 ) = ( Base ‘ 𝑉 )
73 6 ringmgp ⊢ ( 𝐾 ∈ Ring → 𝑉 ∈ Mnd )
74 42 44 73 3syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → 𝑉 ∈ Mnd )
75 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
76 14 75 syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
77 76 nnnn0d ⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
78 77 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → 𝑃 ∈ ℕ0 )
79 43 31 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → 𝑦 ∈ ( Base ‘ 𝑉 ) )
80 72 7 74 78 79 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ↑ 𝑦 ) ∈ ( Base ‘ 𝑉 ) )
81 80 32 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ↑ 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
82 11 4 30 2 3 42 81 evl1vard ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝑋 ) ‘ ( 𝑃 ↑ 𝑦 ) ) = ( 𝑃 ↑ 𝑦 ) ) )
83 11 2 30 8 3 42 62 81 evl1scad ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ∈ 𝐵 ∧ ( ( 𝑂 ‘ ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ‘ ( 𝑃 ↑ 𝑦 ) ) = ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
84 83 simprd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑂 ‘ ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ‘ ( 𝑃 ↑ 𝑦 ) ) = ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) )
85 61 84 jca ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ∈ 𝐵 ∧ ( ( 𝑂 ‘ ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ‘ ( 𝑃 ↑ 𝑦 ) ) = ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
86 11 2 30 3 42 81 82 85 12 66 evl1addd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ∈ 𝐵 ∧ ( ( 𝑂 ‘ ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ ( 𝑃 ↑ 𝑦 ) ) = ( ( 𝑃 ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
87 86 simprd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑂 ‘ ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ ( 𝑃 ↑ 𝑦 ) ) = ( ( 𝑃 ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
88 71 87 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝑃 ↑ 𝑦 ) ) = ( ( 𝑃 ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
89 5 fveq2i ⊢ ( .g ‘ 𝑊 ) = ( .g ‘ ( mulGrp ‘ 𝑆 ) )
90 9 89 eqtri ⊢ 𝐷 = ( .g ‘ ( mulGrp ‘ 𝑆 ) )
91 6 fveq2i ⊢ ( .g ‘ 𝑉 ) = ( .g ‘ ( mulGrp ‘ 𝐾 ) )
92 7 91 eqtri ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝐾 ) )
93 11 2 30 3 42 43 47 90 92 78 evl1expd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 𝐷 𝑋 ) ∈ 𝐵 ∧ ( ( 𝑂 ‘ ( 𝑃 𝐷 𝑋 ) ) ‘ 𝑦 ) = ( 𝑃 ↑ 𝑦 ) ) )
94 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
95 11 2 30 3 42 43 93 65 94 66 evl1addd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( ( ( 𝑃 𝐷 𝑋 ) ( +g ‘ 𝑆 ) ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ∈ 𝐵 ∧ ( ( 𝑂 ‘ ( ( 𝑃 𝐷 𝑋 ) ( +g ‘ 𝑆 ) ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ 𝑦 ) = ( ( 𝑃 ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
96 95 simprd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑂 ‘ ( ( 𝑃 𝐷 𝑋 ) ( +g ‘ 𝑆 ) ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ 𝑦 ) = ( ( 𝑃 ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
97 eqidd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) = ( ( 𝑃 ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
98 96 97 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑂 ‘ ( ( 𝑃 𝐷 𝑋 ) ( +g ‘ 𝑆 ) ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ 𝑦 ) = ( ( 𝑃 ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
99 98 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) = ( ( 𝑂 ‘ ( ( 𝑃 𝐷 𝑋 ) ( +g ‘ 𝑆 ) ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ 𝑦 ) )
100 eqid ⊢ ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) = ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) )
101 2 4 94 5 9 8 100 10 22 14 19 ply1fermltlchr ⊢ ( 𝜑 → ( 𝑃 𝐷 ( 𝑋 ( +g ‘ 𝑆 ) ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) = ( ( 𝑃 𝐷 𝑋 ) ( +g ‘ 𝑆 ) ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
102 101 fveq2d ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝑃 𝐷 ( 𝑋 ( +g ‘ 𝑆 ) ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ) = ( 𝑂 ‘ ( ( 𝑃 𝐷 𝑋 ) ( +g ‘ 𝑆 ) ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) )
103 102 fveq1d ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝑃 𝐷 ( 𝑋 ( +g ‘ 𝑆 ) ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ) ‘ 𝑦 ) = ( ( 𝑂 ‘ ( ( 𝑃 𝐷 𝑋 ) ( +g ‘ 𝑆 ) ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ 𝑦 ) )
104 103 eqcomd ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( ( 𝑃 𝐷 𝑋 ) ( +g ‘ 𝑆 ) ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ 𝑦 ) = ( ( 𝑂 ‘ ( 𝑃 𝐷 ( 𝑋 ( +g ‘ 𝑆 ) ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ) ‘ 𝑦 ) )
105 104 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑂 ‘ ( ( 𝑃 𝐷 𝑋 ) ( +g ‘ 𝑆 ) ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ 𝑦 ) = ( ( 𝑂 ‘ ( 𝑃 𝐷 ( 𝑋 ( +g ‘ 𝑆 ) ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ) ‘ 𝑦 ) )
106 11 2 30 3 42 43 47 63 94 66 evl1addd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑋 ( +g ‘ 𝑆 ) ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ∈ 𝐵 ∧ ( ( 𝑂 ‘ ( 𝑋 ( +g ‘ 𝑆 ) ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ 𝑦 ) = ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
107 11 2 30 3 42 43 106 90 92 78 evl1expd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 𝐷 ( 𝑋 ( +g ‘ 𝑆 ) ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ∈ 𝐵 ∧ ( ( 𝑂 ‘ ( 𝑃 𝐷 ( 𝑋 ( +g ‘ 𝑆 ) ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ) ‘ 𝑦 ) = ( 𝑃 ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) )
108 107 simprd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑂 ‘ ( 𝑃 𝐷 ( 𝑋 ( +g ‘ 𝑆 ) ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ) ‘ 𝑦 ) = ( 𝑃 ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
109 99 105 108 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) = ( 𝑃 ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
110 88 109 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝑃 ↑ 𝑦 ) ) = ( 𝑃 ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
111 110 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝑃 ↑ 𝑦 ) ) )
112 70 111 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝑃 ↑ 𝑦 ) ) )
113 112 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝑃 ↑ 𝑦 ) ) )
114 113 ex ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐾 ) → ( 𝑃 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝑃 ↑ 𝑦 ) ) ) )
115 114 ex ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) → ( 𝑦 ∈ ( Base ‘ 𝐾 ) → ( 𝑃 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝑃 ↑ 𝑦 ) ) ) ) )
116 37 115 mpdd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) → ( 𝑃 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝑃 ↑ 𝑦 ) ) ) )
117 116 imp ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑃 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝑃 ↑ 𝑦 ) ) )
118 117 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝑃 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝑃 ↑ 𝑦 ) ) )
119 2 ply1crng ⊢ ( 𝐾 ∈ CRing → 𝑆 ∈ CRing )
120 22 119 syl ⊢ ( 𝜑 → 𝑆 ∈ CRing )
121 crngring ⊢ ( 𝑆 ∈ CRing → 𝑆 ∈ Ring )
122 120 121 syl ⊢ ( 𝜑 → 𝑆 ∈ Ring )
123 122 ringgrpd ⊢ ( 𝜑 → 𝑆 ∈ Grp )
124 51 45 syl ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
125 123 124 60 3jca ⊢ ( 𝜑 → ( 𝑆 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ∈ 𝐵 ) )
126 3 12 grpcl ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ∈ 𝐵 ) → ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ∈ 𝐵 )
127 125 126 syl ⊢ ( 𝜑 → ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ∈ 𝐵 )
128 18 a1i ⊢ ( 𝜑 → 𝐹 = ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
129 128 eleq1d ⊢ ( 𝜑 → ( 𝐹 ∈ 𝐵 ↔ ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ∈ 𝐵 ) )
130 127 129 mpbird ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
131 1 130 76 aks6d1c1p1 ⊢ ( 𝜑 → ( 𝑃 ∼ 𝐹 ↔ ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝑃 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝑃 ↑ 𝑦 ) ) ) )
132 118 131 mpbird ⊢ ( 𝜑 → 𝑃 ∼ 𝐹 )