Metamath Proof Explorer

Theorem aks5lem5a

Description: Lemma for AKS, section 5, connect to Theorem 6.1. (Contributed by metakunt, 17-Jun-2025)

Ref Expression
Hypotheses aks5lema.1 ⊢ ( 𝜑 → 𝐾 ∈ Field )
aks5lema.2 ⊢ 𝑃 = ( chr ‘ 𝐾 )
aks5lema.3 ⊢ ( 𝜑 → ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ∧ 𝑃 ∥ 𝑁 ) )
aks5lema.9 ⊢ 𝐵 = ( 𝑆 /s ( 𝑆 ~QG 𝐿 ) )
aks5lema.10 ⊢ 𝐿 = ( ( RSpan ‘ 𝑆 ) ‘ { ( ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( -g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) } )
aks5lema.11 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
aks5lema.14 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) }
aks5lema.15 ⊢ 𝑆 = ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) )
aks5lem5a.13 ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) )
Assertion aks5lem5a ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) 𝑁 ∼ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) )

Proof

Step Hyp Ref Expression
1 aks5lema.1 ⊢ ( 𝜑 → 𝐾 ∈ Field )
2 aks5lema.2 ⊢ 𝑃 = ( chr ‘ 𝐾 )
3 aks5lema.3 ⊢ ( 𝜑 → ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ∧ 𝑃 ∥ 𝑁 ) )
4 aks5lema.9 ⊢ 𝐵 = ( 𝑆 /s ( 𝑆 ~QG 𝐿 ) )
5 aks5lema.10 ⊢ 𝐿 = ( ( RSpan ‘ 𝑆 ) ‘ { ( ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( -g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) } )
6 aks5lema.11 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
7 aks5lema.14 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) }
8 aks5lema.15 ⊢ 𝑆 = ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) )
9 aks5lem5a.13 ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) )
10 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) ∧ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) ∧ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ) → 𝐾 ∈ Field )
11 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) ∧ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) ∧ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ) → ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ∧ 𝑃 ∥ 𝑁 ) )
12 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) ∧ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) ∧ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ) → 𝑅 ∈ ℕ )
13 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) ∧ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) ∧ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ) → 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
14 elfzelz ⊢ ( 𝑎 ∈ ( 1 ... 𝐴 ) → 𝑎 ∈ ℤ )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) → 𝑎 ∈ ℤ )
16 15 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) ∧ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) → 𝑎 ∈ ℤ )
17 16 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) ∧ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) ∧ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ) → 𝑎 ∈ ℤ )
18 eqid ⊢ ( algSc ‘ 𝑆 ) = ( algSc ‘ 𝑆 )
19 eqid ⊢ ( ℤRHom ‘ 𝑆 ) = ( ℤRHom ‘ 𝑆 )
20 eqid ⊢ ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) )
21 3 simp2d ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) → 𝑁 ∈ ℕ )
23 22 nnnn0d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) → 𝑁 ∈ ℕ0 )
24 eqid ⊢ ( ℤ/nℤ ‘ 𝑁 ) = ( ℤ/nℤ ‘ 𝑁 )
25 24 zncrng ⊢ ( 𝑁 ∈ ℕ0 → ( ℤ/nℤ ‘ 𝑁 ) ∈ CRing )
26 23 25 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) → ( ℤ/nℤ ‘ 𝑁 ) ∈ CRing )
27 8 18 19 20 26 15 ply1asclzrhval ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) → ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝑎 ) ) = ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) )
28 27 oveq2d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) → ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝑎 ) ) ) = ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) )
29 28 oveq2d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) → ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝑎 ) ) ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) )
30 29 eceq1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) → [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝑎 ) ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) )
31 30 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) ∧ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) → [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝑎 ) ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) )
32 simpr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) ∧ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) → [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) )
33 27 eqcomd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) → ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) = ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝑎 ) ) )
34 33 oveq2d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) → ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) = ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝑎 ) ) ) )
35 34 eceq1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) → [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) )
36 35 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) ∧ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) → [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) )
37 31 32 36 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) ∧ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) → [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝑎 ) ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) )
38 37 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) ∧ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) ∧ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ) → [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝑎 ) ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) )
39 10 2 11 4 5 12 7 8 13 17 38 aks5lem4a ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) ∧ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) ∧ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ) → ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) ) ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) )
40 39 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) ∧ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) → ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) ) ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) )
41 eqid ⊢ ( Poly1 ‘ 𝐾 ) = ( Poly1 ‘ 𝐾 )
42 eqid ⊢ ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) = ( algSc ‘ ( Poly1 ‘ 𝐾 ) )
43 eqid ⊢ ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) = ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) )
44 eqid ⊢ ( ℤRHom ‘ 𝐾 ) = ( ℤRHom ‘ 𝐾 )
45 1 fldcrngd ⊢ ( 𝜑 → 𝐾 ∈ CRing )
46 45 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) → 𝐾 ∈ CRing )
47 41 42 43 44 46 15 ply1asclzrhval ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) → ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) = ( ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ‘ 𝑎 ) )
48 47 oveq2d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) → ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) = ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ‘ 𝑎 ) ) )
49 eqid ⊢ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) = ( Base ‘ ( Poly1 ‘ 𝐾 ) )
50 eqid ⊢ ( +g ‘ ( Poly1 ‘ 𝐾 ) ) = ( +g ‘ ( Poly1 ‘ 𝐾 ) )
51 41 ply1crng ⊢ ( 𝐾 ∈ CRing → ( Poly1 ‘ 𝐾 ) ∈ CRing )
52 45 51 syl ⊢ ( 𝜑 → ( Poly1 ‘ 𝐾 ) ∈ CRing )
53 52 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) → ( Poly1 ‘ 𝐾 ) ∈ CRing )
54 crngring ⊢ ( ( Poly1 ‘ 𝐾 ) ∈ CRing → ( Poly1 ‘ 𝐾 ) ∈ Ring )
55 53 54 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) → ( Poly1 ‘ 𝐾 ) ∈ Ring )
56 55 ringgrpd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) → ( Poly1 ‘ 𝐾 ) ∈ Grp )
57 46 crngringd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) → 𝐾 ∈ Ring )
58 eqid ⊢ ( var1 ‘ 𝐾 ) = ( var1 ‘ 𝐾 )
59 58 41 49 vr1cl ⊢ ( 𝐾 ∈ Ring → ( var1 ‘ 𝐾 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
60 57 59 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) → ( var1 ‘ 𝐾 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
61 43 zrhrhm ⊢ ( ( Poly1 ‘ 𝐾 ) ∈ Ring → ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ∈ ( ℤring RingHom ( Poly1 ‘ 𝐾 ) ) )
62 55 61 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) → ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ∈ ( ℤring RingHom ( Poly1 ‘ 𝐾 ) ) )
63 zringbas ⊢ ℤ = ( Base ‘ ℤring )
64 63 49 rhmf ⊢ ( ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ∈ ( ℤring RingHom ( Poly1 ‘ 𝐾 ) ) → ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) : ℤ ⟶ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
65 62 64 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) → ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) : ℤ ⟶ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
66 65 15 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) → ( ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ‘ 𝑎 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
67 49 50 56 60 66 grpcld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) → ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ‘ 𝑎 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
68 48 67 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) → ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
69 68 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) ∧ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) → ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
70 22 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) ∧ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) → 𝑁 ∈ ℕ )
71 7 69 70 aks6d1c1p1 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) ∧ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) → ( 𝑁 ∼ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) ↔ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) ) ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) )
72 40 71 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) ∧ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) → 𝑁 ∼ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) )
73 72 ex ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) → ( [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) → 𝑁 ∼ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) ) )
74 73 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑎 ∈ ( 1 ... 𝐴 ) [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) 𝑁 ∼ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) ) )
75 9 74 mpd ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) 𝑁 ∼ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) )