Metamath Proof Explorer

Theorem aks6d1c1p5

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

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

Proof

Step Hyp Ref Expression
1 aks6d1c1p5.1 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝑒 ↑ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝑓 ) ‘ ( 𝑒 ↑ 𝑦 ) ) ) }
2 aks6d1c1p5.2 ⊢ 𝑆 = ( Poly1 ‘ 𝐾 )
3 aks6d1c1p5.3 ⊢ 𝐵 = ( Base ‘ 𝑆 )
4 aks6d1c1p5.4 ⊢ 𝑋 = ( var1 ‘ 𝐾 )
5 aks6d1c1p5.5 ⊢ 𝑊 = ( mulGrp ‘ 𝑆 )
6 aks6d1c1p5.6 ⊢ 𝑉 = ( mulGrp ‘ 𝐾 )
7 aks6d1c1p5.7 ⊢ ↑ = ( .g ‘ 𝑉 )
8 aks6d1c1p5.8 ⊢ 𝐶 = ( algSc ‘ 𝑆 )
9 aks6d1c1p5.10 ⊢ 𝑃 = ( chr ‘ 𝐾 )
10 aks6d1c1p5.11 ⊢ 𝑂 = ( eval1 ‘ 𝐾 )
11 aks6d1c1p5.12 ⊢ + = ( +g ‘ 𝑆 )
12 aks6d1c1p5.13 ⊢ ( 𝜑 → 𝐾 ∈ Field )
13 aks6d1c1p5.14 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
14 aks6d1c1p5.15 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
15 aks6d1c1p5.16 ⊢ ( 𝜑 → ( 𝐸 gcd 𝑅 ) = 1 )
16 aks6d1c1p5.17 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
17 aks6d1c1p5.18 ⊢ ( 𝜑 → 𝐷 ∼ 𝐹 )
18 aks6d1c1p5.19 ⊢ ( 𝜑 → 𝐸 ∼ 𝐹 )
19 12 fldcrngd ⊢ ( 𝜑 → 𝐾 ∈ CRing )
20 6 crngmgp ⊢ ( 𝐾 ∈ CRing → 𝑉 ∈ CMnd )
21 19 20 syl ⊢ ( 𝜑 → 𝑉 ∈ CMnd )
22 21 cmnmndd ⊢ ( 𝜑 → 𝑉 ∈ Mnd )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑉 ∈ Mnd )
24 1 17 aks6d1c1p1rcl ⊢ ( 𝜑 → ( 𝐷 ∈ ℕ ∧ 𝐹 ∈ 𝐵 ) )
25 24 simpld ⊢ ( 𝜑 → 𝐷 ∈ ℕ )
26 25 nnnn0d ⊢ ( 𝜑 → 𝐷 ∈ ℕ0 )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝐷 ∈ ℕ0 )
28 1 18 aks6d1c1p1rcl ⊢ ( 𝜑 → ( 𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵 ) )
29 28 simpld ⊢ ( 𝜑 → 𝐸 ∈ ℕ )
30 29 nnnn0d ⊢ ( 𝜑 → 𝐸 ∈ ℕ0 )
31 30 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝐸 ∈ ℕ0 )
32 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
33 19 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝐾 ∈ CRing )
34 14 nnnn0d ⊢ ( 𝜑 → 𝑅 ∈ ℕ0 )
35 21 34 7 isprimroot ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ↔ ( 𝑦 ∈ ( Base ‘ 𝑉 ) ∧ ( 𝑅 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) ∧ ∀ 𝑞 ∈ ℕ0 ( ( 𝑞 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) → 𝑅 ∥ 𝑞 ) ) ) )
36 35 biimpd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) → ( 𝑦 ∈ ( Base ‘ 𝑉 ) ∧ ( 𝑅 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) ∧ ∀ 𝑞 ∈ ℕ0 ( ( 𝑞 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) → 𝑅 ∥ 𝑞 ) ) ) )
37 36 imp ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑦 ∈ ( Base ‘ 𝑉 ) ∧ ( 𝑅 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) ∧ ∀ 𝑞 ∈ ℕ0 ( ( 𝑞 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) → 𝑅 ∥ 𝑞 ) ) )
38 37 simp1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑦 ∈ ( Base ‘ 𝑉 ) )
39 6 32 mgpbas ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝑉 )
40 39 a1i ⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝑉 ) )
41 40 eqcomd ⊢ ( 𝜑 → ( Base ‘ 𝑉 ) = ( Base ‘ 𝐾 ) )
42 41 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( Base ‘ 𝑉 ) = ( Base ‘ 𝐾 ) )
43 38 42 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑦 ∈ ( Base ‘ 𝐾 ) )
44 24 simprd ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
45 44 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝐹 ∈ 𝐵 )
46 10 2 32 3 33 43 45 fveval1fvcl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
47 42 eleq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝑉 ) ↔ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐾 ) ) )
48 46 47 mpbird ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝑉 ) )
49 27 31 48 3jca ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ∧ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝑉 ) ) )
50 eqid ⊢ ( Base ‘ 𝑉 ) = ( Base ‘ 𝑉 )
51 50 7 mulgnn0ass ⊢ ( ( 𝑉 ∈ Mnd ∧ ( 𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ∧ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝑉 ) ) ) → ( ( 𝐷 · 𝐸 ) ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( 𝐷 ↑ ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) ) )
52 23 49 51 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝐷 · 𝐸 ) ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( 𝐷 ↑ ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) ) )
53 eqidd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) = ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) )
54 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) ∧ 𝑙 = 𝑦 ) → 𝑙 = 𝑦 )
55 54 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) ∧ 𝑙 = 𝑦 ) → ( 𝐸 ↑ 𝑙 ) = ( 𝐸 ↑ 𝑦 ) )
56 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) )
57 50 7 23 31 38 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐸 ↑ 𝑦 ) ∈ ( Base ‘ 𝑉 ) )
58 53 55 56 57 fvmptd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑦 ) = ( 𝐸 ↑ 𝑦 ) )
59 58 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ 𝐹 ) ‘ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) )
60 59 oveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐷 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑦 ) ) ) = ( 𝐷 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) ) )
61 60 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐷 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) ) = ( 𝐷 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑦 ) ) ) )
62 2fveq3 ⊢ ( 𝑖 = 𝑦 → ( ( 𝑂 ‘ 𝐹 ) ‘ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑖 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑦 ) ) )
63 62 oveq2d ⊢ ( 𝑖 = 𝑦 → ( 𝐷 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑖 ) ) ) = ( 𝐷 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑦 ) ) ) )
64 fveq2 ⊢ ( 𝑖 = 𝑦 → ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑖 ) = ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑦 ) )
65 64 oveq2d ⊢ ( 𝑖 = 𝑦 → ( 𝐷 ↑ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑖 ) ) = ( 𝐷 ↑ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑦 ) ) )
66 65 fveq2d ⊢ ( 𝑖 = 𝑦 → ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐷 ↑ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑖 ) ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐷 ↑ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑦 ) ) ) )
67 63 66 eqeq12d ⊢ ( 𝑖 = 𝑦 → ( ( 𝐷 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑖 ) ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐷 ↑ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑖 ) ) ) ↔ ( 𝐷 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑦 ) ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐷 ↑ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑦 ) ) ) ) )
68 1 44 25 aks6d1c1p1 ⊢ ( 𝜑 → ( 𝐷 ∼ 𝐹 ↔ ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐷 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐷 ↑ 𝑦 ) ) ) )
69 68 biimpd ⊢ ( 𝜑 → ( 𝐷 ∼ 𝐹 → ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐷 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐷 ↑ 𝑦 ) ) ) )
70 17 69 mpd ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐷 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐷 ↑ 𝑦 ) ) )
71 7 oveqi ⊢ ( 𝐸 ↑ 𝑙 ) = ( 𝐸 ( .g ‘ 𝑉 ) 𝑙 )
72 71 a1i ⊢ ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) → ( 𝐸 ↑ 𝑙 ) = ( 𝐸 ( .g ‘ 𝑉 ) 𝑙 ) )
73 72 mpteq2ia ⊢ ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) = ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ( .g ‘ 𝑉 ) 𝑙 ) )
74 73 21 14 29 15 primrootscoprbij2 ⊢ ( 𝜑 → ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) : ( 𝑉 PrimRoots 𝑅 ) –1-1-onto→ ( 𝑉 PrimRoots 𝑅 ) )
75 f1ofo ⊢ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) : ( 𝑉 PrimRoots 𝑅 ) –1-1-onto→ ( 𝑉 PrimRoots 𝑅 ) → ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) : ( 𝑉 PrimRoots 𝑅 ) –onto→ ( 𝑉 PrimRoots 𝑅 ) )
76 74 75 syl ⊢ ( 𝜑 → ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) : ( 𝑉 PrimRoots 𝑅 ) –onto→ ( 𝑉 PrimRoots 𝑅 ) )
77 fveq2 ⊢ ( ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑖 ) = 𝑦 → ( ( 𝑂 ‘ 𝐹 ) ‘ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑖 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) )
78 77 oveq2d ⊢ ( ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑖 ) = 𝑦 → ( 𝐷 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑖 ) ) ) = ( 𝐷 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) )
79 oveq2 ⊢ ( ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑖 ) = 𝑦 → ( 𝐷 ↑ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑖 ) ) = ( 𝐷 ↑ 𝑦 ) )
80 79 fveq2d ⊢ ( ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑖 ) = 𝑦 → ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐷 ↑ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑖 ) ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐷 ↑ 𝑦 ) ) )
81 78 80 eqeq12d ⊢ ( ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑖 ) = 𝑦 → ( ( 𝐷 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑖 ) ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐷 ↑ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑖 ) ) ) ↔ ( 𝐷 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐷 ↑ 𝑦 ) ) ) )
82 81 cbvfo ⊢ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) : ( 𝑉 PrimRoots 𝑅 ) –onto→ ( 𝑉 PrimRoots 𝑅 ) → ( ∀ 𝑖 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐷 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑖 ) ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐷 ↑ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑖 ) ) ) ↔ ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐷 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐷 ↑ 𝑦 ) ) ) )
83 76 82 syl ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐷 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑖 ) ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐷 ↑ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑖 ) ) ) ↔ ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐷 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐷 ↑ 𝑦 ) ) ) )
84 70 83 mpbird ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐷 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑖 ) ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐷 ↑ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑖 ) ) ) )
85 84 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ∀ 𝑖 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐷 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑖 ) ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐷 ↑ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑖 ) ) ) )
86 67 85 56 rspcdva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐷 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑦 ) ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐷 ↑ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑦 ) ) ) )
87 58 oveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐷 ↑ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑦 ) ) = ( 𝐷 ↑ ( 𝐸 ↑ 𝑦 ) ) )
88 87 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐷 ↑ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑦 ) ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐷 ↑ ( 𝐸 ↑ 𝑦 ) ) ) )
89 86 88 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐷 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ ( ( 𝑙 ∈ ( 𝑉 PrimRoots 𝑅 ) ↦ ( 𝐸 ↑ 𝑙 ) ) ‘ 𝑦 ) ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐷 ↑ ( 𝐸 ↑ 𝑦 ) ) ) )
90 61 89 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐷 ↑ ( 𝐸 ↑ 𝑦 ) ) ) = ( 𝐷 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) ) )
91 fveq2 ⊢ ( 𝑧 = 𝑦 → ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑧 ) = ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) )
92 91 oveq2d ⊢ ( 𝑧 = 𝑦 → ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑧 ) ) = ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) )
93 oveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝐸 ↑ 𝑧 ) = ( 𝐸 ↑ 𝑦 ) )
94 93 fveq2d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑧 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) )
95 92 94 eqeq12d ⊢ ( 𝑧 = 𝑦 → ( ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑧 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑧 ) ) ↔ ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) ) )
96 1 44 29 aks6d1c1p1 ⊢ ( 𝜑 → ( 𝐸 ∼ 𝐹 ↔ ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) ) )
97 96 biimpd ⊢ ( 𝜑 → ( 𝐸 ∼ 𝐹 → ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) ) )
98 18 97 mpd ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) )
99 nfv ⊢ Ⅎ 𝑦 ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑧 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑧 ) )
100 nfv ⊢ Ⅎ 𝑧 ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) )
101 99 100 95 cbvralw ⊢ ( ∀ 𝑧 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑧 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑧 ) ) ↔ ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) )
102 98 101 sylibr ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑧 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑧 ) ) )
103 102 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ∀ 𝑧 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑧 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑧 ) ) )
104 95 103 56 rspcdva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) )
105 104 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) = ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) )
106 105 oveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐷 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 ↑ 𝑦 ) ) ) = ( 𝐷 ↑ ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) ) )
107 90 106 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐷 ↑ ( 𝐸 ↑ 𝑦 ) ) ) = ( 𝐷 ↑ ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) ) )
108 107 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐷 ↑ ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐷 ↑ ( 𝐸 ↑ 𝑦 ) ) ) )
109 27 31 38 3jca ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ∧ 𝑦 ∈ ( Base ‘ 𝑉 ) ) )
110 50 7 mulgnn0ass ⊢ ( ( 𝑉 ∈ Mnd ∧ ( 𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ∧ 𝑦 ∈ ( Base ‘ 𝑉 ) ) ) → ( ( 𝐷 · 𝐸 ) ↑ 𝑦 ) = ( 𝐷 ↑ ( 𝐸 ↑ 𝑦 ) ) )
111 110 eqcomd ⊢ ( ( 𝑉 ∈ Mnd ∧ ( 𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ∧ 𝑦 ∈ ( Base ‘ 𝑉 ) ) ) → ( 𝐷 ↑ ( 𝐸 ↑ 𝑦 ) ) = ( ( 𝐷 · 𝐸 ) ↑ 𝑦 ) )
112 23 109 111 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐷 ↑ ( 𝐸 ↑ 𝑦 ) ) = ( ( 𝐷 · 𝐸 ) ↑ 𝑦 ) )
113 112 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐷 ↑ ( 𝐸 ↑ 𝑦 ) ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( ( 𝐷 · 𝐸 ) ↑ 𝑦 ) ) )
114 52 108 113 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝐷 · 𝐸 ) ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( ( 𝐷 · 𝐸 ) ↑ 𝑦 ) ) )
115 114 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( ( 𝐷 · 𝐸 ) ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( ( 𝐷 · 𝐸 ) ↑ 𝑦 ) ) )
116 25 29 nnmulcld ⊢ ( 𝜑 → ( 𝐷 · 𝐸 ) ∈ ℕ )
117 1 44 116 aks6d1c1p1 ⊢ ( 𝜑 → ( ( 𝐷 · 𝐸 ) ∼ 𝐹 ↔ ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( ( 𝐷 · 𝐸 ) ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( ( 𝐷 · 𝐸 ) ↑ 𝑦 ) ) ) )
118 115 117 mpbird ⊢ ( 𝜑 → ( 𝐷 · 𝐸 ) ∼ 𝐹 )