Metamath Proof Explorer

Theorem aks5lem6

Description: Connect results of section 5 and Theorem 6.1 AKS. (Contributed by metakunt, 25-Jun-2025)

Ref Expression
Hypotheses aks5lem6.1 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) }
aks5lem6.2 ⊢ 𝑃 = ( chr ‘ 𝐾 )
aks5lem6.3 ⊢ ( 𝜑 → 𝐾 ∈ Field )
aks5lem6.4 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
aks5lem6.5 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
aks5lem6.6 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
aks5lem6.7 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
aks5lem6.8 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
aks5lem6.9 ⊢ 𝐴 = ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) )
aks5lem6.10 ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
aks5lem6.11 ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
aks5lem6.12 ⊢ ( 𝜑 → 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
aks5lem6.13 ⊢ ( 𝜑 → ∀ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝑏 gcd 𝑁 ) = 1 )
aks5lem6.14 ⊢ 𝑆 = ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) )
aks5lem6.15 ⊢ 𝐿 = ( ( RSpan ‘ 𝑆 ) ‘ { ( ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( -g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) } )
aks5lem6.16 ⊢ 𝑋 = ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) )
aks5lem6.17 ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( 𝑋 ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) )
Assertion aks5lem6 ( 𝜑 → 𝑁 = ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 aks5lem6.1 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) }
2 aks5lem6.2 ⊢ 𝑃 = ( chr ‘ 𝐾 )
3 aks5lem6.3 ⊢ ( 𝜑 → 𝐾 ∈ Field )
4 aks5lem6.4 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5 aks5lem6.5 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
6 aks5lem6.6 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
7 aks5lem6.7 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
8 aks5lem6.8 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
9 aks5lem6.9 ⊢ 𝐴 = ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) )
10 aks5lem6.10 ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
11 aks5lem6.11 ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
12 aks5lem6.12 ⊢ ( 𝜑 → 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
13 aks5lem6.13 ⊢ ( 𝜑 → ∀ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝑏 gcd 𝑁 ) = 1 )
14 aks5lem6.14 ⊢ 𝑆 = ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) )
15 aks5lem6.15 ⊢ 𝐿 = ( ( RSpan ‘ 𝑆 ) ‘ { ( ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( -g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) } )
16 aks5lem6.16 ⊢ 𝑋 = ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) )
17 aks5lem6.17 ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( 𝑋 ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) )
18 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℤ )
19 6 18 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
20 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
21 3re ⊢ 3 ∈ ℝ
22 21 a1i ⊢ ( 𝜑 → 3 ∈ ℝ )
23 19 zred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
24 3pos ⊢ 0 < 3
25 24 a1i ⊢ ( 𝜑 → 0 < 3 )
26 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 3 ≤ 𝑁 )
27 6 26 syl ⊢ ( 𝜑 → 3 ≤ 𝑁 )
28 20 22 23 25 27 ltletrd ⊢ ( 𝜑 → 0 < 𝑁 )
29 19 28 jca ⊢ ( 𝜑 → ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) )
30 elnnz ⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) )
31 29 30 sylibr ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
32 4 31 7 3jca ⊢ ( 𝜑 → ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ∧ 𝑃 ∥ 𝑁 ) )
33 eqid ⊢ ( 𝑆 /s ( 𝑆 ~QG 𝐿 ) ) = ( 𝑆 /s ( 𝑆 ~QG 𝐿 ) )
34 16 eqcomi ⊢ ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = 𝑋
35 34 a1i ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) ∧ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( 𝑋 ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) → ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = 𝑋 )
36 35 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) ∧ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( 𝑋 ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) → ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) = ( 𝑋 ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) )
37 36 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) ∧ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( 𝑋 ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) → ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( 𝑋 ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) )
38 37 eceq1d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) ∧ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( 𝑋 ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) → [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( 𝑋 ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) )
39 simpr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) ∧ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( 𝑋 ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) → [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( 𝑋 ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) )
40 eqcom ⊢ ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = 𝑋 ↔ 𝑋 = ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
41 40 imbi2i ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) ∧ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( 𝑋 ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) → ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = 𝑋 ) ↔ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) ∧ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( 𝑋 ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) → 𝑋 = ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
42 35 41 mpbi ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) ∧ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( 𝑋 ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) → 𝑋 = ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
43 42 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) ∧ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( 𝑋 ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) → ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
44 43 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) ∧ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( 𝑋 ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) → ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) = ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) )
45 44 eceq1d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) ∧ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( 𝑋 ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) → [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) )
46 38 39 45 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) ∧ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( 𝑋 ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) → [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) )
47 46 ex ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝐴 ) ) → ( [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( 𝑋 ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) → [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) )
48 47 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑎 ∈ ( 1 ... 𝐴 ) [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( 𝑋 ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) ) )
49 17 48 mpd ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) )
50 3 2 32 33 15 5 1 14 49 aks5lem5a ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) 𝑁 ∼ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) )
51 1 2 3 4 5 6 7 8 9 10 11 12 13 50 aks6d1c7 ⊢ ( 𝜑 → 𝑁 = ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) )