Metamath Proof Explorer

Theorem aks6d1c1p4

Description: The product of polynomials is introspective. (Contributed by metakunt, 25-Apr-2025)

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

Proof

Step Hyp Ref Expression
1 aks6d1c1p4.1 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝑒 ↑ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝑓 ) ‘ ( 𝑒 ↑ 𝑦 ) ) ) }
2 aks6d1c1p4.2 ⊢ 𝑆 = ( Poly1 ‘ 𝐾 )
3 aks6d1c1p4.3 ⊢ 𝐵 = ( Base ‘ 𝑆 )
4 aks6d1c1p4.4 ⊢ 𝑋 = ( var1 ‘ 𝐾 )
5 aks6d1c1p4.5 ⊢ 𝑊 = ( mulGrp ‘ 𝑆 )
6 aks6d1c1p4.6 ⊢ 𝑉 = ( mulGrp ‘ 𝐾 )
7 aks6d1c1p4.7 ⊢ ↑ = ( .g ‘ 𝑉 )
8 aks6d1c1p4.8 ⊢ 𝐶 = ( algSc ‘ 𝑆 )
9 aks6d1c1p4.9 ⊢ 𝐷 = ( .g ‘ 𝑊 )
10 aks6d1c1p4.10 ⊢ 𝑃 = ( chr ‘ 𝐾 )
11 aks6d1c1p4.11 ⊢ 𝑂 = ( eval1 ‘ 𝐾 )
12 aks6d1c1p4.12 ⊢ + = ( +g ‘ 𝑆 )
13 aks6d1c1p4.13 ⊢ ( 𝜑 → 𝐾 ∈ Field )
14 aks6d1c1p4.14 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
15 aks6d1c1p4.15 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
16 aks6d1c1p4.16 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
17 aks6d1c1p4.17 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
18 aks6d1c1p4.18 ⊢ ( 𝜑 → 𝐸 ∼ 𝐹 )
19 aks6d1c1p4.19 ⊢ ( 𝜑 → 𝐸 ∼ 𝐺 )
20 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
21 13 fldcrngd ⊢ ( 𝜑 → 𝐾 ∈ CRing )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝐾 ∈ CRing )
23 6 20 mgpbas ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝑉 )
24 6 crngmgp ⊢ ( 𝐾 ∈ CRing → 𝑉 ∈ CMnd )
25 21 24 syl ⊢ ( 𝜑 → 𝑉 ∈ CMnd )
26 25 cmnmndd ⊢ ( 𝜑 → 𝑉 ∈ Mnd )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑉 ∈ Mnd )
28 1 18 aks6d1c1p1rcl ⊢ ( 𝜑 → ( 𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵 ) )
29 28 simpld ⊢ ( 𝜑 → 𝐸 ∈ ℕ )
30 29 nnnn0d ⊢ ( 𝜑 → 𝐸 ∈ ℕ0 )
31 30 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝐸 ∈ ℕ0 )
32 15 nnnn0d ⊢ ( 𝜑 → 𝑅 ∈ ℕ0 )
33 eqid ⊢ ( .g ‘ 𝑉 ) = ( .g ‘ 𝑉 )
34 25 32 33 isprimroot ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ↔ ( 𝑦 ∈ ( Base ‘ 𝑉 ) ∧ ( 𝑅 ( .g ‘ 𝑉 ) 𝑦 ) = ( 0g ‘ 𝑉 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑉 ) 𝑦 ) = ( 0g ‘ 𝑉 ) → 𝑅 ∥ 𝑙 ) ) ) )
35 34 biimpd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) → ( 𝑦 ∈ ( Base ‘ 𝑉 ) ∧ ( 𝑅 ( .g ‘ 𝑉 ) 𝑦 ) = ( 0g ‘ 𝑉 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑉 ) 𝑦 ) = ( 0g ‘ 𝑉 ) → 𝑅 ∥ 𝑙 ) ) ) )
36 35 imp ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑦 ∈ ( Base ‘ 𝑉 ) ∧ ( 𝑅 ( .g ‘ 𝑉 ) 𝑦 ) = ( 0g ‘ 𝑉 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑉 ) 𝑦 ) = ( 0g ‘ 𝑉 ) → 𝑅 ∥ 𝑙 ) ) )
37 36 simp1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑦 ∈ ( Base ‘ 𝑉 ) )
38 37 23 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑦 ∈ ( Base ‘ 𝐾 ) )
39 23 7 27 31 38 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐸 ↑ 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
40 28 simprd ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
41 40 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝐹 ∈ 𝐵 )
42 eqidd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) )
43 41 42 jca ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐹 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) ) )
44 1 19 aks6d1c1p1rcl ⊢ ( 𝜑 → ( 𝐸 ∈ ℕ ∧ 𝐺 ∈ 𝐵 ) )
45 44 simprd ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
46 45 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝐺 ∈ 𝐵 )
47 eqidd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ 𝐺 ) ‘ ( 𝐸 ↑ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐺 ) ‘ ( 𝐸 ↑ 𝑦 ) ) )
48 46 47 jca ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐺 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝐺 ) ‘ ( 𝐸 ↑ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐺 ) ‘ ( 𝐸 ↑ 𝑦 ) ) ) )
49 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
50 5 49 mgpplusg ⊢ ( .r ‘ 𝑆 ) = ( +g ‘ 𝑊 )
51 50 eqcomi ⊢ ( +g ‘ 𝑊 ) = ( .r ‘ 𝑆 )
52 eqid ⊢ ( .r ‘ 𝐾 ) = ( .r ‘ 𝐾 )
53 11 2 20 3 22 39 43 48 51 52 evl1muld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝐹 ( +g ‘ 𝑊 ) 𝐺 ) ∈ 𝐵 ∧ ( ( 𝑂 ‘ ( 𝐹 ( +g ‘ 𝑊 ) 𝐺 ) ) ‘ ( 𝐸 ↑ 𝑦 ) ) = ( ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) ( .r ‘ 𝐾 ) ( ( 𝑂 ‘ 𝐺 ) ‘ ( 𝐸 ↑ 𝑦 ) ) ) ) )
54 53 simprd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ ( 𝐹 ( +g ‘ 𝑊 ) 𝐺 ) ) ‘ ( 𝐸 ↑ 𝑦 ) ) = ( ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) ( .r ‘ 𝐾 ) ( ( 𝑂 ‘ 𝐺 ) ‘ ( 𝐸 ↑ 𝑦 ) ) ) )
55 25 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑉 ∈ CMnd )
56 11 2 20 3 22 38 41 fveval1fvcl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
57 6 eqcomi ⊢ ( mulGrp ‘ 𝐾 ) = 𝑉
58 57 fveq2i ⊢ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) = ( Base ‘ 𝑉 )
59 23 58 eqtr4i ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ ( mulGrp ‘ 𝐾 ) )
60 59 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( Base ‘ 𝐾 ) = ( Base ‘ ( mulGrp ‘ 𝐾 ) ) )
61 60 eleq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐾 ) ↔ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ) )
62 56 61 mpbid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) )
63 11 2 20 3 22 38 46 fveval1fvcl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
64 60 eleq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐾 ) ↔ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ) )
65 63 64 mpbid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) )
66 31 62 65 3jca ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐸 ∈ ℕ0 ∧ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∧ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ) )
67 57 fveq2i ⊢ ( +g ‘ ( mulGrp ‘ 𝐾 ) ) = ( +g ‘ 𝑉 )
68 58 7 67 mulgnn0di ⊢ ( ( 𝑉 ∈ CMnd ∧ ( 𝐸 ∈ ℕ0 ∧ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∧ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ) ) → ( 𝐸 ↑ ( ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ( +g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ) ) = ( ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) ( +g ‘ ( mulGrp ‘ 𝐾 ) ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ) ) )
69 55 66 68 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐸 ↑ ( ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ( +g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ) ) = ( ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) ( +g ‘ ( mulGrp ‘ 𝐾 ) ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ) ) )
70 6 52 mgpplusg ⊢ ( .r ‘ 𝐾 ) = ( +g ‘ 𝑉 )
71 6 fveq2i ⊢ ( +g ‘ 𝑉 ) = ( +g ‘ ( mulGrp ‘ 𝐾 ) )
72 70 71 eqtri ⊢ ( .r ‘ 𝐾 ) = ( +g ‘ ( mulGrp ‘ 𝐾 ) )
73 72 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( .r ‘ 𝐾 ) = ( +g ‘ ( mulGrp ‘ 𝐾 ) ) )
74 73 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( +g ‘ ( mulGrp ‘ 𝐾 ) ) = ( .r ‘ 𝐾 ) )
75 fveq2 ⊢ ( 𝑧 = 𝑦 → ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑧 ) = ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) )
76 75 oveq2d ⊢ ( 𝑧 = 𝑦 → ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑧 ) ) = ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) )
77 oveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝐸 ↑ 𝑧 ) = ( 𝐸 ↑ 𝑦 ) )
78 77 fveq2d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑧 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) )
79 76 78 eqeq12d ⊢ ( 𝑧 = 𝑦 → ( ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑧 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑧 ) ) ↔ ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) ) )
80 1 40 29 aks6d1c1p1 ⊢ ( 𝜑 → ( 𝐸 ∼ 𝐹 ↔ ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) ) )
81 18 80 mpbid ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) )
82 fveq2 ⊢ ( 𝑦 = 𝑧 → ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) = ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑧 ) )
83 82 oveq2d ⊢ ( 𝑦 = 𝑧 → ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑧 ) ) )
84 oveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝐸 ↑ 𝑦 ) = ( 𝐸 ↑ 𝑧 ) )
85 84 fveq2d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑧 ) ) )
86 83 85 eqeq12d ⊢ ( 𝑦 = 𝑧 → ( ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) ↔ ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑧 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑧 ) ) ) )
87 86 cbvralvw ⊢ ( ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) ↔ ∀ 𝑧 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑧 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑧 ) ) )
88 81 87 sylib ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑧 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑧 ) ) )
89 88 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ∀ 𝑧 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑧 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑧 ) ) )
90 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) )
91 79 89 90 rspcdva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) )
92 fveq2 ⊢ ( 𝑧 = 𝑦 → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑧 ) = ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) )
93 92 oveq2d ⊢ ( 𝑧 = 𝑦 → ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑧 ) ) = ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ) )
94 77 fveq2d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑂 ‘ 𝐺 ) ‘ ( 𝐸 ↑ 𝑧 ) ) = ( ( 𝑂 ‘ 𝐺 ) ‘ ( 𝐸 ↑ 𝑦 ) ) )
95 93 94 eqeq12d ⊢ ( 𝑧 = 𝑦 → ( ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑧 ) ) = ( ( 𝑂 ‘ 𝐺 ) ‘ ( 𝐸 ↑ 𝑧 ) ) ↔ ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐺 ) ‘ ( 𝐸 ↑ 𝑦 ) ) ) )
96 1 45 29 aks6d1c1p1 ⊢ ( 𝜑 → ( 𝐸 ∼ 𝐺 ↔ ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐺 ) ‘ ( 𝐸 ↑ 𝑦 ) ) ) )
97 19 96 mpbid ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐺 ) ‘ ( 𝐸 ↑ 𝑦 ) ) )
98 fveq2 ⊢ ( 𝑦 = 𝑧 → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) = ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑧 ) )
99 98 oveq2d ⊢ ( 𝑦 = 𝑧 → ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ) = ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑧 ) ) )
100 84 fveq2d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑂 ‘ 𝐺 ) ‘ ( 𝐸 ↑ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐺 ) ‘ ( 𝐸 ↑ 𝑧 ) ) )
101 99 100 eqeq12d ⊢ ( 𝑦 = 𝑧 → ( ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐺 ) ‘ ( 𝐸 ↑ 𝑦 ) ) ↔ ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑧 ) ) = ( ( 𝑂 ‘ 𝐺 ) ‘ ( 𝐸 ↑ 𝑧 ) ) ) )
102 101 cbvralvw ⊢ ( ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐺 ) ‘ ( 𝐸 ↑ 𝑦 ) ) ↔ ∀ 𝑧 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑧 ) ) = ( ( 𝑂 ‘ 𝐺 ) ‘ ( 𝐸 ↑ 𝑧 ) ) )
103 97 102 sylib ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑧 ) ) = ( ( 𝑂 ‘ 𝐺 ) ‘ ( 𝐸 ↑ 𝑧 ) ) )
104 103 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ∀ 𝑧 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑧 ) ) = ( ( 𝑂 ‘ 𝐺 ) ‘ ( 𝐸 ↑ 𝑧 ) ) )
105 95 104 90 rspcdva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐺 ) ‘ ( 𝐸 ↑ 𝑦 ) ) )
106 74 91 105 oveq123d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) ( +g ‘ ( mulGrp ‘ 𝐾 ) ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ) ) = ( ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) ( .r ‘ 𝐾 ) ( ( 𝑂 ‘ 𝐺 ) ‘ ( 𝐸 ↑ 𝑦 ) ) ) )
107 69 106 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) ( .r ‘ 𝐾 ) ( ( 𝑂 ‘ 𝐺 ) ‘ ( 𝐸 ↑ 𝑦 ) ) ) = ( 𝐸 ↑ ( ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ( +g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ) ) )
108 72 eqcomi ⊢ ( +g ‘ ( mulGrp ‘ 𝐾 ) ) = ( .r ‘ 𝐾 )
109 108 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( +g ‘ ( mulGrp ‘ 𝐾 ) ) = ( .r ‘ 𝐾 ) )
110 109 oveqd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ( +g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ) = ( ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ( .r ‘ 𝐾 ) ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ) )
111 110 oveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐸 ↑ ( ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ( +g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ) ) = ( 𝐸 ↑ ( ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ( .r ‘ 𝐾 ) ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ) ) )
112 107 111 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) ( .r ‘ 𝐾 ) ( ( 𝑂 ‘ 𝐺 ) ‘ ( 𝐸 ↑ 𝑦 ) ) ) = ( 𝐸 ↑ ( ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ( .r ‘ 𝐾 ) ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ) ) )
113 eqidd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) = ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) )
114 41 113 jca ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐹 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) = ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) )
115 eqidd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) = ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) )
116 46 115 jca ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐺 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) = ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ) )
117 11 2 20 3 22 38 114 116 51 52 evl1muld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝐹 ( +g ‘ 𝑊 ) 𝐺 ) ∈ 𝐵 ∧ ( ( 𝑂 ‘ ( 𝐹 ( +g ‘ 𝑊 ) 𝐺 ) ) ‘ 𝑦 ) = ( ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ( .r ‘ 𝐾 ) ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ) ) )
118 117 simprd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ ( 𝐹 ( +g ‘ 𝑊 ) 𝐺 ) ) ‘ 𝑦 ) = ( ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ( .r ‘ 𝐾 ) ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ) )
119 118 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ( .r ‘ 𝐾 ) ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ ( 𝐹 ( +g ‘ 𝑊 ) 𝐺 ) ) ‘ 𝑦 ) )
120 119 oveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐸 ↑ ( ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ( .r ‘ 𝐾 ) ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑦 ) ) ) = ( 𝐸 ↑ ( ( 𝑂 ‘ ( 𝐹 ( +g ‘ 𝑊 ) 𝐺 ) ) ‘ 𝑦 ) ) )
121 112 120 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) ( .r ‘ 𝐾 ) ( ( 𝑂 ‘ 𝐺 ) ‘ ( 𝐸 ↑ 𝑦 ) ) ) = ( 𝐸 ↑ ( ( 𝑂 ‘ ( 𝐹 ( +g ‘ 𝑊 ) 𝐺 ) ) ‘ 𝑦 ) ) )
122 54 121 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ ( 𝐹 ( +g ‘ 𝑊 ) 𝐺 ) ) ‘ ( 𝐸 ↑ 𝑦 ) ) = ( 𝐸 ↑ ( ( 𝑂 ‘ ( 𝐹 ( +g ‘ 𝑊 ) 𝐺 ) ) ‘ 𝑦 ) ) )
123 122 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐸 ↑ ( ( 𝑂 ‘ ( 𝐹 ( +g ‘ 𝑊 ) 𝐺 ) ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ ( 𝐹 ( +g ‘ 𝑊 ) 𝐺 ) ) ‘ ( 𝐸 ↑ 𝑦 ) ) )
124 123 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ ( 𝐹 ( +g ‘ 𝑊 ) 𝐺 ) ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ ( 𝐹 ( +g ‘ 𝑊 ) 𝐺 ) ) ‘ ( 𝐸 ↑ 𝑦 ) ) )
125 2 ply1crng ⊢ ( 𝐾 ∈ CRing → 𝑆 ∈ CRing )
126 21 125 syl ⊢ ( 𝜑 → 𝑆 ∈ CRing )
127 126 crngringd ⊢ ( 𝜑 → 𝑆 ∈ Ring )
128 3 51 127 40 45 ringcld ⊢ ( 𝜑 → ( 𝐹 ( +g ‘ 𝑊 ) 𝐺 ) ∈ 𝐵 )
129 1 128 29 aks6d1c1p1 ⊢ ( 𝜑 → ( 𝐸 ∼ ( 𝐹 ( +g ‘ 𝑊 ) 𝐺 ) ↔ ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ ( 𝐹 ( +g ‘ 𝑊 ) 𝐺 ) ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ ( 𝐹 ( +g ‘ 𝑊 ) 𝐺 ) ) ‘ ( 𝐸 ↑ 𝑦 ) ) ) )
130 124 129 mpbird ⊢ ( 𝜑 → 𝐸 ∼ ( 𝐹 ( +g ‘ 𝑊 ) 𝐺 ) )