aks6d1c7lem3

Description: Remove lots of hypotheses now that we have the AKS contradiction. (Contributed by metakunt, 16-May-2025)

	Ref	Expression
Hypotheses	aks6d1c7.1	⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly₁ ‘ 𝐾 ) ) ∧ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( ._g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval₁ ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval₁ ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( ._g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) }
	aks6d1c7.2	⊢ 𝑃 = ( chr ‘ 𝐾 )
	aks6d1c7.3	⊢ ( 𝜑 → 𝐾 ∈ Field )
	aks6d1c7.4	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	aks6d1c7.5	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
	aks6d1c7.6	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ_≥ ‘ 3 ) )
	aks6d1c7.7	⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
	aks6d1c7.8	⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
	aks6d1c7.9	⊢ 𝐴 = ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 log_b 𝑁 ) ) )
	aks6d1c7.10	⊢ ( 𝜑 → ( ( 2 log_b 𝑁 ) ↑ 2 ) < ( ( od_ℤ ‘ 𝑅 ) ‘ 𝑁 ) )
	aks6d1c7.11	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( ._g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
	aks6d1c7.12	⊢ ( 𝜑 → 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
	aks6d1c7.13	⊢ ( 𝜑 → ∀ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝑏 gcd 𝑁 ) = 1 )
	aks6d1c7.14	⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) 𝑁 ∼ ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) )
	aks6d1c7lem3.1	⊢ ( 𝜑 → ( 𝑄 ∈ ℙ ∧ 𝑄 ∥ 𝑁 ) )
Assertion	aks6d1c7lem3	⊢ ( 𝜑 → 𝑃 = 𝑄 )

Proof

Step	Hyp	Ref	Expression
1		aks6d1c7.1	⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly₁ ‘ 𝐾 ) ) ∧ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( ._g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval₁ ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval₁ ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( ._g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) }
2		aks6d1c7.2	⊢ 𝑃 = ( chr ‘ 𝐾 )
3		aks6d1c7.3	⊢ ( 𝜑 → 𝐾 ∈ Field )
4		aks6d1c7.4	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5		aks6d1c7.5	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
6		aks6d1c7.6	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ_≥ ‘ 3 ) )
7		aks6d1c7.7	⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
8		aks6d1c7.8	⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
9		aks6d1c7.9	⊢ 𝐴 = ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 log_b 𝑁 ) ) )
10		aks6d1c7.10	⊢ ( 𝜑 → ( ( 2 log_b 𝑁 ) ↑ 2 ) < ( ( od_ℤ ‘ 𝑅 ) ‘ 𝑁 ) )
11		aks6d1c7.11	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( ._g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
12		aks6d1c7.12	⊢ ( 𝜑 → 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
13		aks6d1c7.13	⊢ ( 𝜑 → ∀ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝑏 gcd 𝑁 ) = 1 )
14		aks6d1c7.14	⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) 𝑁 ∼ ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) )
15		aks6d1c7lem3.1	⊢ ( 𝜑 → ( 𝑄 ∈ ℙ ∧ 𝑄 ∥ 𝑁 ) )
16		nfcv	⊢ Ⅎ 𝑘 ( ( 𝑃 ↑ 𝑖 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑗 ) )
17		nfcv	⊢ Ⅎ 𝑙 ( ( 𝑃 ↑ 𝑖 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑗 ) )
18		nfcv	⊢ Ⅎ 𝑖 ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) )
19		nfcv	⊢ Ⅎ 𝑗 ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) )
20		simpl	⊢ ( ( 𝑖 = 𝑘 ∧ 𝑗 = 𝑙 ) → 𝑖 = 𝑘 )
21	20	oveq2d	⊢ ( ( 𝑖 = 𝑘 ∧ 𝑗 = 𝑙 ) → ( 𝑃 ↑ 𝑖 ) = ( 𝑃 ↑ 𝑘 ) )
22		simpr	⊢ ( ( 𝑖 = 𝑘 ∧ 𝑗 = 𝑙 ) → 𝑗 = 𝑙 )
23	22	oveq2d	⊢ ( ( 𝑖 = 𝑘 ∧ 𝑗 = 𝑙 ) → ( ( 𝑁 / 𝑃 ) ↑ 𝑗 ) = ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) )
24	21 23	oveq12d	⊢ ( ( 𝑖 = 𝑘 ∧ 𝑗 = 𝑙 ) → ( ( 𝑃 ↑ 𝑖 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑗 ) ) = ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
25	16 17 18 19 24	cbvmpo	⊢ ( 𝑖 ∈ ℕ₀ , 𝑗 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑖 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑗 ) ) ) = ( 𝑘 ∈ ℕ₀ , 𝑙 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
26		eqid	⊢ ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) ) = ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) )
27		eqid	⊢ ( ♯ ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) ) “ ( ( 𝑖 ∈ ℕ₀ , 𝑗 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑖 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑗 ) ) ) “ ( ℕ₀ × ℕ₀ ) ) ) ) = ( ♯ ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) ) “ ( ( 𝑖 ∈ ℕ₀ , 𝑗 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑖 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑗 ) ) ) “ ( ℕ₀ × ℕ₀ ) ) ) )
28		nfcv	⊢ Ⅎ 𝑣 ( ( ( eval₁ ‘ 𝐾 ) ‘ ( ( 𝑚 ∈ ( ℕ₀ ↑_m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) Σ_g ( 𝑛 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑚 ‘ 𝑛 ) ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) ) ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑛 ) ) ) ) ) ) ) ‘ 𝑤 ) ) ‘ 𝑀 )
29		nfcv	⊢ Ⅎ 𝑤 ( ( ( eval₁ ‘ 𝐾 ) ‘ ( ( 𝑚 ∈ ( ℕ₀ ↑_m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) Σ_g ( 𝑛 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑚 ‘ 𝑛 ) ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) ) ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑛 ) ) ) ) ) ) ) ‘ 𝑣 ) ) ‘ 𝑀 )
30		2fveq3	⊢ ( 𝑤 = 𝑣 → ( ( eval₁ ‘ 𝐾 ) ‘ ( ( 𝑚 ∈ ( ℕ₀ ↑_m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) Σ_g ( 𝑛 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑚 ‘ 𝑛 ) ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) ) ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑛 ) ) ) ) ) ) ) ‘ 𝑤 ) ) = ( ( eval₁ ‘ 𝐾 ) ‘ ( ( 𝑚 ∈ ( ℕ₀ ↑_m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) Σ_g ( 𝑛 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑚 ‘ 𝑛 ) ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) ) ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑛 ) ) ) ) ) ) ) ‘ 𝑣 ) ) )
31	30	fveq1d	⊢ ( 𝑤 = 𝑣 → ( ( ( eval₁ ‘ 𝐾 ) ‘ ( ( 𝑚 ∈ ( ℕ₀ ↑_m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) Σ_g ( 𝑛 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑚 ‘ 𝑛 ) ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) ) ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑛 ) ) ) ) ) ) ) ‘ 𝑤 ) ) ‘ 𝑀 ) = ( ( ( eval₁ ‘ 𝐾 ) ‘ ( ( 𝑚 ∈ ( ℕ₀ ↑_m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) Σ_g ( 𝑛 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑚 ‘ 𝑛 ) ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) ) ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑛 ) ) ) ) ) ) ) ‘ 𝑣 ) ) ‘ 𝑀 ) )
32	28 29 31	cbvmpt	⊢ ( 𝑤 ∈ ( ℕ₀ ↑_m ( 0 ... 𝐴 ) ) ↦ ( ( ( eval₁ ‘ 𝐾 ) ‘ ( ( 𝑚 ∈ ( ℕ₀ ↑_m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) Σ_g ( 𝑛 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑚 ‘ 𝑛 ) ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) ) ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑛 ) ) ) ) ) ) ) ‘ 𝑤 ) ) ‘ 𝑀 ) ) = ( 𝑣 ∈ ( ℕ₀ ↑_m ( 0 ... 𝐴 ) ) ↦ ( ( ( eval₁ ‘ 𝐾 ) ‘ ( ( 𝑚 ∈ ( ℕ₀ ↑_m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) Σ_g ( 𝑛 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑚 ‘ 𝑛 ) ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) ) ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑛 ) ) ) ) ) ) ) ‘ 𝑣 ) ) ‘ 𝑀 ) )
33		eqid	⊢ ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) ) “ ( ( 𝑖 ∈ ℕ₀ , 𝑗 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑖 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑗 ) ) ) “ ( ℕ₀ × ℕ₀ ) ) ) ) ) ) = ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) ) “ ( ( 𝑖 ∈ ℕ₀ , 𝑗 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑖 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑗 ) ) ) “ ( ℕ₀ × ℕ₀ ) ) ) ) ) )
34		eqid	⊢ ( ( 𝑖 ∈ ℕ₀ , 𝑗 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑖 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑗 ) ) ) “ ( ( 0 ... ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) ) “ ( ( 𝑖 ∈ ℕ₀ , 𝑗 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑖 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑗 ) ) ) “ ( ℕ₀ × ℕ₀ ) ) ) ) ) ) ) × ( 0 ... ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) ) “ ( ( 𝑖 ∈ ℕ₀ , 𝑗 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑖 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑗 ) ) ) “ ( ℕ₀ × ℕ₀ ) ) ) ) ) ) ) ) ) = ( ( 𝑖 ∈ ℕ₀ , 𝑗 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑖 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑗 ) ) ) “ ( ( 0 ... ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) ) “ ( ( 𝑖 ∈ ℕ₀ , 𝑗 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑖 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑗 ) ) ) “ ( ℕ₀ × ℕ₀ ) ) ) ) ) ) ) × ( 0 ... ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) ) “ ( ( 𝑖 ∈ ℕ₀ , 𝑗 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑖 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑗 ) ) ) “ ( ℕ₀ × ℕ₀ ) ) ) ) ) ) ) ) )
35		nfcv	⊢ Ⅎ 𝑔 ( ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) Σ_g ( 𝑛 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑚 ‘ 𝑛 ) ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) ) ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑛 ) ) ) ) ) )
36		nfcv	⊢ Ⅎ 𝑚 ( ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) Σ_g ( ℎ ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ ℎ ) ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) ) ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ℎ ) ) ) ) ) )
37		nfcv	⊢ Ⅎ ℎ ( ( 𝑚 ‘ 𝑛 ) ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) ) ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑛 ) ) ) )
38		nfcv	⊢ Ⅎ 𝑛 ( ( 𝑚 ‘ ℎ ) ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) ) ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ℎ ) ) ) )
39		fveq2	⊢ ( 𝑛 = ℎ → ( 𝑚 ‘ 𝑛 ) = ( 𝑚 ‘ ℎ ) )
40		2fveq3	⊢ ( 𝑛 = ℎ → ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑛 ) ) = ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ℎ ) ) )
41	40	oveq2d	⊢ ( 𝑛 = ℎ → ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑛 ) ) ) = ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ℎ ) ) ) )
42	39 41	oveq12d	⊢ ( 𝑛 = ℎ → ( ( 𝑚 ‘ 𝑛 ) ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) ) ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑛 ) ) ) ) = ( ( 𝑚 ‘ ℎ ) ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) ) ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ℎ ) ) ) ) )
43	37 38 42	cbvmpt	⊢ ( 𝑛 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑚 ‘ 𝑛 ) ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) ) ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑛 ) ) ) ) ) = ( ℎ ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑚 ‘ ℎ ) ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) ) ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ℎ ) ) ) ) )
44	43	a1i	⊢ ( 𝑚 = 𝑔 → ( 𝑛 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑚 ‘ 𝑛 ) ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) ) ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑛 ) ) ) ) ) = ( ℎ ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑚 ‘ ℎ ) ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) ) ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ℎ ) ) ) ) ) )
45		simpl	⊢ ( ( 𝑚 = 𝑔 ∧ ℎ ∈ ( 0 ... 𝐴 ) ) → 𝑚 = 𝑔 )
46	45	fveq1d	⊢ ( ( 𝑚 = 𝑔 ∧ ℎ ∈ ( 0 ... 𝐴 ) ) → ( 𝑚 ‘ ℎ ) = ( 𝑔 ‘ ℎ ) )
47	46	oveq1d	⊢ ( ( 𝑚 = 𝑔 ∧ ℎ ∈ ( 0 ... 𝐴 ) ) → ( ( 𝑚 ‘ ℎ ) ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) ) ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ℎ ) ) ) ) = ( ( 𝑔 ‘ ℎ ) ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) ) ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ℎ ) ) ) ) )
48	47	mpteq2dva	⊢ ( 𝑚 = 𝑔 → ( ℎ ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑚 ‘ ℎ ) ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) ) ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ℎ ) ) ) ) ) = ( ℎ ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ ℎ ) ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) ) ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ℎ ) ) ) ) ) )
49	44 48	eqtrd	⊢ ( 𝑚 = 𝑔 → ( 𝑛 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑚 ‘ 𝑛 ) ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) ) ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑛 ) ) ) ) ) = ( ℎ ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ ℎ ) ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) ) ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ℎ ) ) ) ) ) )
50	49	oveq2d	⊢ ( 𝑚 = 𝑔 → ( ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) Σ_g ( 𝑛 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑚 ‘ 𝑛 ) ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) ) ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑛 ) ) ) ) ) ) = ( ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) Σ_g ( ℎ ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ ℎ ) ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) ) ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ℎ ) ) ) ) ) ) )
51	35 36 50	cbvmpt	⊢ ( 𝑚 ∈ ( ℕ₀ ↑_m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) Σ_g ( 𝑛 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑚 ‘ 𝑛 ) ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) ) ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑛 ) ) ) ) ) ) ) = ( 𝑔 ∈ ( ℕ₀ ↑_m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) Σ_g ( ℎ ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ ℎ ) ( ._g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝐾 ) ) ) ( ( var₁ ‘ 𝐾 ) ( +_g ‘ ( Poly₁ ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ℎ ) ) ) ) ) ) )
52		nfcv	⊢ Ⅎ 𝑢 ( ℕ₀ ↑_m ( 0 ... 𝐴 ) )
53		nfcv	⊢ Ⅎ 𝑜 ( ℕ₀ ↑_m ( 0 ... 𝐴 ) )
54		nfv	⊢ Ⅎ 𝑜 Σ 𝑞 ∈ ( 0 ... 𝐴 ) ( 𝑢 ‘ 𝑞 ) ≤ ( ( ♯ ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) ) “ ( ( 𝑘 ∈ ℕ₀ , 𝑙 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) ) “ ( ℕ₀ × ℕ₀ ) ) ) ) − 1 )
55		nfv	⊢ Ⅎ 𝑢 Σ 𝑝 ∈ ( 0 ... 𝐴 ) ( 𝑜 ‘ 𝑝 ) ≤ ( ( ♯ ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) ) “ ( ( 𝑖 ∈ ℕ₀ , 𝑗 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑖 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑗 ) ) ) “ ( ℕ₀ × ℕ₀ ) ) ) ) − 1 )
56		simpl	⊢ ( ( 𝑢 = 𝑜 ∧ 𝑞 ∈ ( 0 ... 𝐴 ) ) → 𝑢 = 𝑜 )
57	56	fveq1d	⊢ ( ( 𝑢 = 𝑜 ∧ 𝑞 ∈ ( 0 ... 𝐴 ) ) → ( 𝑢 ‘ 𝑞 ) = ( 𝑜 ‘ 𝑞 ) )
58	57	sumeq2dv	⊢ ( 𝑢 = 𝑜 → Σ 𝑞 ∈ ( 0 ... 𝐴 ) ( 𝑢 ‘ 𝑞 ) = Σ 𝑞 ∈ ( 0 ... 𝐴 ) ( 𝑜 ‘ 𝑞 ) )
59		fveq2	⊢ ( 𝑞 = 𝑝 → ( 𝑜 ‘ 𝑞 ) = ( 𝑜 ‘ 𝑝 ) )
60		nfcv	⊢ Ⅎ 𝑝 ( 𝑜 ‘ 𝑞 )
61		nfcv	⊢ Ⅎ 𝑞 ( 𝑜 ‘ 𝑝 )
62	59 60 61	cbvsum	⊢ Σ 𝑞 ∈ ( 0 ... 𝐴 ) ( 𝑜 ‘ 𝑞 ) = Σ 𝑝 ∈ ( 0 ... 𝐴 ) ( 𝑜 ‘ 𝑝 )
63	62	a1i	⊢ ( 𝑢 = 𝑜 → Σ 𝑞 ∈ ( 0 ... 𝐴 ) ( 𝑜 ‘ 𝑞 ) = Σ 𝑝 ∈ ( 0 ... 𝐴 ) ( 𝑜 ‘ 𝑝 ) )
64	58 63	eqtrd	⊢ ( 𝑢 = 𝑜 → Σ 𝑞 ∈ ( 0 ... 𝐴 ) ( 𝑢 ‘ 𝑞 ) = Σ 𝑝 ∈ ( 0 ... 𝐴 ) ( 𝑜 ‘ 𝑝 ) )
65	25	eqcomi	⊢ ( 𝑘 ∈ ℕ₀ , 𝑙 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) ) = ( 𝑖 ∈ ℕ₀ , 𝑗 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑖 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑗 ) ) )
66	65	a1i	⊢ ( 𝑢 = 𝑜 → ( 𝑘 ∈ ℕ₀ , 𝑙 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) ) = ( 𝑖 ∈ ℕ₀ , 𝑗 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑖 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑗 ) ) ) )
67	66	imaeq1d	⊢ ( 𝑢 = 𝑜 → ( ( 𝑘 ∈ ℕ₀ , 𝑙 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) ) “ ( ℕ₀ × ℕ₀ ) ) = ( ( 𝑖 ∈ ℕ₀ , 𝑗 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑖 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑗 ) ) ) “ ( ℕ₀ × ℕ₀ ) ) )
68	67	imaeq2d	⊢ ( 𝑢 = 𝑜 → ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) ) “ ( ( 𝑘 ∈ ℕ₀ , 𝑙 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) ) “ ( ℕ₀ × ℕ₀ ) ) ) = ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) ) “ ( ( 𝑖 ∈ ℕ₀ , 𝑗 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑖 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑗 ) ) ) “ ( ℕ₀ × ℕ₀ ) ) ) )
69	68	fveq2d	⊢ ( 𝑢 = 𝑜 → ( ♯ ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) ) “ ( ( 𝑘 ∈ ℕ₀ , 𝑙 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) ) “ ( ℕ₀ × ℕ₀ ) ) ) ) = ( ♯ ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) ) “ ( ( 𝑖 ∈ ℕ₀ , 𝑗 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑖 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑗 ) ) ) “ ( ℕ₀ × ℕ₀ ) ) ) ) )
70	69	oveq1d	⊢ ( 𝑢 = 𝑜 → ( ( ♯ ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) ) “ ( ( 𝑘 ∈ ℕ₀ , 𝑙 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) ) “ ( ℕ₀ × ℕ₀ ) ) ) ) − 1 ) = ( ( ♯ ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) ) “ ( ( 𝑖 ∈ ℕ₀ , 𝑗 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑖 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑗 ) ) ) “ ( ℕ₀ × ℕ₀ ) ) ) ) − 1 ) )
71	64 70	breq12d	⊢ ( 𝑢 = 𝑜 → ( Σ 𝑞 ∈ ( 0 ... 𝐴 ) ( 𝑢 ‘ 𝑞 ) ≤ ( ( ♯ ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) ) “ ( ( 𝑘 ∈ ℕ₀ , 𝑙 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) ) “ ( ℕ₀ × ℕ₀ ) ) ) ) − 1 ) ↔ Σ 𝑝 ∈ ( 0 ... 𝐴 ) ( 𝑜 ‘ 𝑝 ) ≤ ( ( ♯ ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) ) “ ( ( 𝑖 ∈ ℕ₀ , 𝑗 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑖 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑗 ) ) ) “ ( ℕ₀ × ℕ₀ ) ) ) ) − 1 ) ) )
72	52 53 54 55 71	cbvrabw	⊢ { 𝑢 ∈ ( ℕ₀ ↑_m ( 0 ... 𝐴 ) ) ∣ Σ 𝑞 ∈ ( 0 ... 𝐴 ) ( 𝑢 ‘ 𝑞 ) ≤ ( ( ♯ ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) ) “ ( ( 𝑘 ∈ ℕ₀ , 𝑙 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) ) “ ( ℕ₀ × ℕ₀ ) ) ) ) − 1 ) } = { 𝑜 ∈ ( ℕ₀ ↑_m ( 0 ... 𝐴 ) ) ∣ Σ 𝑝 ∈ ( 0 ... 𝐴 ) ( 𝑜 ‘ 𝑝 ) ≤ ( ( ♯ ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) ) “ ( ( 𝑖 ∈ ℕ₀ , 𝑗 ∈ ℕ₀ ↦ ( ( 𝑃 ↑ 𝑖 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑗 ) ) ) “ ( ℕ₀ × ℕ₀ ) ) ) ) − 1 ) }
73	1 2 3 4 5 6 7 8 25 26 27 9 10 11 12 32 33 34 15 13 51 14 72	aks6d1c7lem2	⊢ ( 𝜑 → 𝑃 = 𝑄 )

Metamath Proof Explorer

Theorem aks6d1c7lem3

Proof