Theorem aks5lem4a

Description: Lemma for AKS section 5, reduce hypotheses. (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ℤ ‘ 𝑁 ) )
	aks5lem4a.7	⊢ ( 𝜑 → 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
	aks5lem4a.12	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
	aks5lem4a.13	⊢ ( 𝜑 → [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ] ( 𝑆 ~QG 𝐿 ) )
Assertion	aks5lem4a	⊢ ( 𝜑 → ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ 𝑀 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )

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		aks5lem4a.7	⊢ ( 𝜑 → 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
10		aks5lem4a.12	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
11		aks5lem4a.13	⊢ ( 𝜑 → [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ] ( 𝑆 ~QG 𝐿 ) )
12		eqid	⊢ ( 𝑏 ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ↦ ( ( 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↦ ∪ ( ( ℤRHom ‘ 𝐾 ) “ 𝑎 ) ) ∘ 𝑏 ) ) = ( 𝑏 ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ↦ ( ( 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↦ ∪ ( ( ℤRHom ‘ 𝐾 ) “ 𝑎 ) ) ∘ 𝑏 ) )
13		eqid	⊢ ( 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↦ ∪ ( ( ℤRHom ‘ 𝐾 ) “ 𝑎 ) ) = ( 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↦ ∪ ( ( ℤRHom ‘ 𝐾 ) “ 𝑎 ) )
14		eqid	⊢ ( 𝑐 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑐 ) ‘ 𝑀 ) ) = ( 𝑐 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑐 ) ‘ 𝑀 ) )
15		nfcv	⊢ Ⅎ 𝑑 ∪ ( ( ( 𝑐 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑐 ) ‘ 𝑀 ) ) ∘ ( 𝑏 ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ↦ ( ( 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↦ ∪ ( ( ℤRHom ‘ 𝐾 ) “ 𝑎 ) ) ∘ 𝑏 ) ) ) “ 𝑒 )
16		nfcv	⊢ Ⅎ 𝑒 ∪ ( ( ( 𝑐 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑐 ) ‘ 𝑀 ) ) ∘ ( 𝑏 ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ↦ ( ( 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↦ ∪ ( ( ℤRHom ‘ 𝐾 ) “ 𝑎 ) ) ∘ 𝑏 ) ) ) “ 𝑑 )
17		imaeq2	⊢ ( 𝑒 = 𝑑 → ( ( ( 𝑐 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑐 ) ‘ 𝑀 ) ) ∘ ( 𝑏 ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ↦ ( ( 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↦ ∪ ( ( ℤRHom ‘ 𝐾 ) “ 𝑎 ) ) ∘ 𝑏 ) ) ) “ 𝑒 ) = ( ( ( 𝑐 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑐 ) ‘ 𝑀 ) ) ∘ ( 𝑏 ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ↦ ( ( 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↦ ∪ ( ( ℤRHom ‘ 𝐾 ) “ 𝑎 ) ) ∘ 𝑏 ) ) ) “ 𝑑 ) )
18	17	unieqd	⊢ ( 𝑒 = 𝑑 → ∪ ( ( ( 𝑐 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑐 ) ‘ 𝑀 ) ) ∘ ( 𝑏 ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ↦ ( ( 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↦ ∪ ( ( ℤRHom ‘ 𝐾 ) “ 𝑎 ) ) ∘ 𝑏 ) ) ) “ 𝑒 ) = ∪ ( ( ( 𝑐 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑐 ) ‘ 𝑀 ) ) ∘ ( 𝑏 ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ↦ ( ( 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↦ ∪ ( ( ℤRHom ‘ 𝐾 ) “ 𝑎 ) ) ∘ 𝑏 ) ) ) “ 𝑑 ) )
19	15 16 18	cbvmpt	⊢ ( 𝑒 ∈ ( Base ‘ 𝐵 ) ↦ ∪ ( ( ( 𝑐 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑐 ) ‘ 𝑀 ) ) ∘ ( 𝑏 ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ↦ ( ( 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↦ ∪ ( ( ℤRHom ‘ 𝐾 ) “ 𝑎 ) ) ∘ 𝑏 ) ) ) “ 𝑒 ) ) = ( 𝑑 ∈ ( Base ‘ 𝐵 ) ↦ ∪ ( ( ( 𝑐 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑐 ) ‘ 𝑀 ) ) ∘ ( 𝑏 ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ↦ ( ( 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↦ ∪ ( ( ℤRHom ‘ 𝐾 ) “ 𝑎 ) ) ∘ 𝑏 ) ) ) “ 𝑑 ) )
20	1 2 3 4 5 6 7 8 12 13 14 9 19 10 11	aks5lem3a	⊢ ( 𝜑 → ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ 𝑀 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )