Metamath Proof Explorer

Theorem aks6d1c1rh

Description: Claim 1 of AKS primality proof with collapsed definitions since their ease of use is no longer needed. (Contributed by metakunt, 1-May-2025)

Ref Expression
Hypotheses aks6d1c1rh.1 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) }
aks6d1c1rh.2 ⊢ 𝑃 = ( chr ‘ 𝐾 )
aks6d1c1rh.3 ⊢ ( 𝜑 → 𝐾 ∈ Field )
aks6d1c1rh.4 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
aks6d1c1rh.5 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
aks6d1c1rh.6 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
aks6d1c1rh.7 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
aks6d1c1rh.8 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
aks6d1c1rh.9 ⊢ ( 𝜑 → 𝐹 : ( 0 ... 𝐴 ) ⟶ ℕ0 )
aks6d1c1rh.10 ⊢ 𝐺 = ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
aks6d1c1rh.11 ⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
aks6d1c1rh.12 ⊢ ( 𝜑 → 𝑈 ∈ ℕ0 )
aks6d1c1rh.13 ⊢ ( 𝜑 → 𝐿 ∈ ℕ0 )
aks6d1c1rh.14 ⊢ 𝐸 = ( ( 𝑃 ↑ 𝑈 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝐿 ) )
aks6d1c1rh.15 ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) 𝑁 ∼ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) )
aks6d1c1rh.16 ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
Assertion aks6d1c1rh ( 𝜑 → 𝐸 ∼ ( 𝐺 ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 aks6d1c1rh.1 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) }
2 aks6d1c1rh.2 ⊢ 𝑃 = ( chr ‘ 𝐾 )
3 aks6d1c1rh.3 ⊢ ( 𝜑 → 𝐾 ∈ Field )
4 aks6d1c1rh.4 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5 aks6d1c1rh.5 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
6 aks6d1c1rh.6 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
7 aks6d1c1rh.7 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
8 aks6d1c1rh.8 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
9 aks6d1c1rh.9 ⊢ ( 𝜑 → 𝐹 : ( 0 ... 𝐴 ) ⟶ ℕ0 )
10 aks6d1c1rh.10 ⊢ 𝐺 = ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
11 aks6d1c1rh.11 ⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
12 aks6d1c1rh.12 ⊢ ( 𝜑 → 𝑈 ∈ ℕ0 )
13 aks6d1c1rh.13 ⊢ ( 𝜑 → 𝐿 ∈ ℕ0 )
14 aks6d1c1rh.14 ⊢ 𝐸 = ( ( 𝑃 ↑ 𝑈 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝐿 ) )
15 aks6d1c1rh.15 ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) 𝑁 ∼ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) )
16 aks6d1c1rh.16 ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
17 nfv ⊢ Ⅎ 𝑧 ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) )
18 nfv ⊢ Ⅎ 𝑦 ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑧 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑧 ) )
19 fveq2 ⊢ ( 𝑦 = 𝑧 → ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑧 ) )
20 19 oveq2d ⊢ ( 𝑦 = 𝑧 → ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑧 ) ) )
21 oveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) = ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑧 ) )
22 21 fveq2d ⊢ ( 𝑦 = 𝑧 → ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑧 ) ) )
23 20 22 eqeq12d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ↔ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑧 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑧 ) ) ) )
24 17 18 23 cbvralw ⊢ ( ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ↔ ∀ 𝑧 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑧 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑧 ) ) )
25 24 3anbi3i ⊢ ( ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) ↔ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑧 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑧 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑧 ) ) ) )
26 25 opabbii ⊢ { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) } = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑧 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑧 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑧 ) ) ) }
27 1 26 eqtri ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑧 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑧 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑧 ) ) ) }
28 eqid ⊢ ( Poly1 ‘ 𝐾 ) = ( Poly1 ‘ 𝐾 )
29 eqid ⊢ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) = ( Base ‘ ( Poly1 ‘ 𝐾 ) )
30 eqid ⊢ ( var1 ‘ 𝐾 ) = ( var1 ‘ 𝐾 )
31 eqid ⊢ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) = ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) )
32 eqid ⊢ ( mulGrp ‘ 𝐾 ) = ( mulGrp ‘ 𝐾 )
33 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝐾 ) ) = ( .g ‘ ( mulGrp ‘ 𝐾 ) )
34 eqid ⊢ ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) = ( algSc ‘ ( Poly1 ‘ 𝐾 ) )
35 eqid ⊢ ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) )
36 eqid ⊢ ( eval1 ‘ 𝐾 ) = ( eval1 ‘ 𝐾 )
37 eqid ⊢ ( +g ‘ ( Poly1 ‘ 𝐾 ) ) = ( +g ‘ ( Poly1 ‘ 𝐾 ) )
38 27 28 29 30 31 32 33 34 35 2 36 37 3 4 5 6 7 8 9 10 11 12 13 14 15 16 aks6d1c1 ⊢ ( 𝜑 → 𝐸 ∼ ( 𝐺 ‘ 𝐹 ) )