aks5lem5a

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

	Ref	Expression
Hypotheses	aks5lema.1	$⊢ φ \to K \in Field$
	aks5lema.2	$⊢ P = chr (K)$
	aks5lema.3	$⊢ φ \to (P \in ℙ \land N \in ℕ \land P ∥ N)$
	aks5lema.9	$⊢ B = S /_{𝑠} (S ~_{QG} L)$
	aks5lema.10	$⊢ L = RSpan (S) (\{(R \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) -_{S} 1_{S}\})$
	aks5lema.11	$⊢ φ \to R \in ℕ$
	aks5lema.14	$⊢ \underset{˙}{\sim} = \{⟨e, f⟩ \| (e \in ℕ \land f \in {Base}_{{Poly}_{1} (K)} \land \forall y \in ({mulGrp}_{K} PrimRoots R) e \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (f) (y) = {eval}_{1} (K) (f) (e \cdot_{{mulGrp}_{K}} y))\}$
	aks5lema.15	$⊢ S = {Poly}_{1} (ℤ / N ℤ)$
	aks5lem5a.13	$⊢ φ \to \forall a \in (1 \dots A) [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)$
Assertion	aks5lem5a	$⊢ φ \to \forall a \in (1 \dots A) N \underset{˙}{\sim} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a)))$

Proof

Step	Hyp	Ref	Expression
1		aks5lema.1	$⊢ φ \to K \in Field$
2		aks5lema.2	$⊢ P = chr (K)$
3		aks5lema.3	$⊢ φ \to (P \in ℙ \land N \in ℕ \land P ∥ N)$
4		aks5lema.9	$⊢ B = S /_{𝑠} (S ~_{QG} L)$
5		aks5lema.10	$⊢ L = RSpan (S) (\{(R \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) -_{S} 1_{S}\})$
6		aks5lema.11	$⊢ φ \to R \in ℕ$
7		aks5lema.14	$⊢ \underset{˙}{\sim} = \{⟨e, f⟩ \| (e \in ℕ \land f \in {Base}_{{Poly}_{1} (K)} \land \forall y \in ({mulGrp}_{K} PrimRoots R) e \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (f) (y) = {eval}_{1} (K) (f) (e \cdot_{{mulGrp}_{K}} y))\}$
8		aks5lema.15	$⊢ S = {Poly}_{1} (ℤ / N ℤ)$
9		aks5lem5a.13	$⊢ φ \to \forall a \in (1 \dots A) [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)$
10	1	ad3antrrr	$⊢ (((φ \land a \in (1 \dots A)) \land [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)) \land y \in ({mulGrp}_{K} PrimRoots R)) \to K \in Field$
11	3	ad3antrrr	$⊢ (((φ \land a \in (1 \dots A)) \land [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)) \land y \in ({mulGrp}_{K} PrimRoots R)) \to (P \in ℙ \land N \in ℕ \land P ∥ N)$
12	6	ad3antrrr	$⊢ (((φ \land a \in (1 \dots A)) \land [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)) \land y \in ({mulGrp}_{K} PrimRoots R)) \to R \in ℕ$
13		simpr	$⊢ (((φ \land a \in (1 \dots A)) \land [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)) \land y \in ({mulGrp}_{K} PrimRoots R)) \to y \in ({mulGrp}_{K} PrimRoots R)$
14		elfzelz	$⊢ a \in (1 \dots A) \to a \in ℤ$
15	14	adantl	$⊢ (φ \land a \in (1 \dots A)) \to a \in ℤ$
16	15	adantr	$⊢ ((φ \land a \in (1 \dots A)) \land [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)) \to a \in ℤ$
17	16	adantr	$⊢ (((φ \land a \in (1 \dots A)) \land [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)) \land y \in ({mulGrp}_{K} PrimRoots R)) \to a \in ℤ$
18		eqid	$⊢ algSc (S) = algSc (S)$
19		eqid	$⊢ ℤRHom (S) = ℤRHom (S)$
20		eqid	$⊢ ℤRHom (ℤ / N ℤ) = ℤRHom (ℤ / N ℤ)$
21	3	simp2d	$⊢ φ \to N \in ℕ$
22	21	adantr	$⊢ (φ \land a \in (1 \dots A)) \to N \in ℕ$
23	22	nnnn0d	$⊢ (φ \land a \in (1 \dots A)) \to N \in ℕ_{0}$
24		eqid	$⊢ ℤ / N ℤ = ℤ / N ℤ$
25	24	zncrng	$⊢ N \in ℕ_{0} \to ℤ / N ℤ \in CRing$
26	23 25	syl	$⊢ (φ \land a \in (1 \dots A)) \to ℤ / N ℤ \in CRing$
27	8 18 19 20 26 15	ply1asclzrhval	$⊢ (φ \land a \in (1 \dots A)) \to algSc (S) (ℤRHom (ℤ / N ℤ) (a)) = ℤRHom (S) (a)$
28	27	oveq2d	$⊢ (φ \land a \in (1 \dots A)) \to {var}_{1} (ℤ / N ℤ) +_{S} algSc (S) (ℤRHom (ℤ / N ℤ) (a)) = {var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)$
29	28	oveq2d	$⊢ (φ \land a \in (1 \dots A)) \to N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} algSc (S) (ℤRHom (ℤ / N ℤ) (a))) = N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a))$
30	29	eceq1d	$⊢ (φ \land a \in (1 \dots A)) \to [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} algSc (S) (ℤRHom (ℤ / N ℤ) (a))))] (S ~_{QG} L) = [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)))] (S ~_{QG} L)$
31	30	adantr	$⊢ ((φ \land a \in (1 \dots A)) \land [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)) \to [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} algSc (S) (ℤRHom (ℤ / N ℤ) (a))))] (S ~_{QG} L) = [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)))] (S ~_{QG} L)$
32		simpr	$⊢ ((φ \land a \in (1 \dots A)) \land [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)) \to [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)$
33	27	eqcomd	$⊢ (φ \land a \in (1 \dots A)) \to ℤRHom (S) (a) = algSc (S) (ℤRHom (ℤ / N ℤ) (a))$
34	33	oveq2d	$⊢ (φ \land a \in (1 \dots A)) \to (N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a) = (N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} algSc (S) (ℤRHom (ℤ / N ℤ) (a))$
35	34	eceq1d	$⊢ (φ \land a \in (1 \dots A)) \to [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} algSc (S) (ℤRHom (ℤ / N ℤ) (a)))] (S ~_{QG} L)$
36	35	adantr	$⊢ ((φ \land a \in (1 \dots A)) \land [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)) \to [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} algSc (S) (ℤRHom (ℤ / N ℤ) (a)))] (S ~_{QG} L)$
37	31 32 36	3eqtrd	$⊢ ((φ \land a \in (1 \dots A)) \land [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)) \to [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} algSc (S) (ℤRHom (ℤ / N ℤ) (a))))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} algSc (S) (ℤRHom (ℤ / N ℤ) (a)))] (S ~_{QG} L)$
38	37	adantr	$⊢ (((φ \land a \in (1 \dots A)) \land [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)) \land y \in ({mulGrp}_{K} PrimRoots R)) \to [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} algSc (S) (ℤRHom (ℤ / N ℤ) (a))))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} algSc (S) (ℤRHom (ℤ / N ℤ) (a)))] (S ~_{QG} L)$
39	10 2 11 4 5 12 7 8 13 17 38	aks5lem4a	$⊢ (((φ \land a \in (1 \dots A)) \land [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)) \land y \in ({mulGrp}_{K} PrimRoots R)) \to N \cdot_{{mulGrp}_{K}} {eval}_{1} (K) ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a))) (y) = {eval}_{1} (K) ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a))) (N \cdot_{{mulGrp}_{K}} y)$
40	39	ralrimiva	$⊢ ((φ \land a \in (1 \dots A)) \land [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)) \to \forall y \in ({mulGrp}_{K} PrimRoots R) N \cdot_{{mulGrp}_{K}} {eval}_{1} (K) ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a))) (y) = {eval}_{1} (K) ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a))) (N \cdot_{{mulGrp}_{K}} y)$
41		eqid	$⊢ {Poly}_{1} (K) = {Poly}_{1} (K)$
42		eqid	$⊢ algSc ({Poly}_{1} (K)) = algSc ({Poly}_{1} (K))$
43		eqid	$⊢ ℤRHom ({Poly}_{1} (K)) = ℤRHom ({Poly}_{1} (K))$
44		eqid	$⊢ ℤRHom (K) = ℤRHom (K)$
45	1	fldcrngd	$⊢ φ \to K \in CRing$
46	45	adantr	$⊢ (φ \land a \in (1 \dots A)) \to K \in CRing$
47	41 42 43 44 46 15	ply1asclzrhval	$⊢ (φ \land a \in (1 \dots A)) \to algSc ({Poly}_{1} (K)) (ℤRHom (K) (a)) = ℤRHom ({Poly}_{1} (K)) (a)$
48	47	oveq2d	$⊢ (φ \land a \in (1 \dots A)) \to {var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a)) = {var}_{1} (K) +_{{Poly}_{1} (K)} ℤRHom ({Poly}_{1} (K)) (a)$
49		eqid	$⊢ {Base}_{{Poly}_{1} (K)} = {Base}_{{Poly}_{1} (K)}$
50		eqid	$⊢ +_{{Poly}_{1} (K)} = +_{{Poly}_{1} (K)}$
51	41	ply1crng	$⊢ K \in CRing \to {Poly}_{1} (K) \in CRing$
52	45 51	syl	$⊢ φ \to {Poly}_{1} (K) \in CRing$
53	52	adantr	$⊢ (φ \land a \in (1 \dots A)) \to {Poly}_{1} (K) \in CRing$
54		crngring	$⊢ {Poly}_{1} (K) \in CRing \to {Poly}_{1} (K) \in Ring$
55	53 54	syl	$⊢ (φ \land a \in (1 \dots A)) \to {Poly}_{1} (K) \in Ring$
56	55	ringgrpd	$⊢ (φ \land a \in (1 \dots A)) \to {Poly}_{1} (K) \in Grp$
57	46	crngringd	$⊢ (φ \land a \in (1 \dots A)) \to K \in Ring$
58		eqid	$⊢ {var}_{1} (K) = {var}_{1} (K)$
59	58 41 49	vr1cl	$⊢ K \in Ring \to {var}_{1} (K) \in {Base}_{{Poly}_{1} (K)}$
60	57 59	syl	$⊢ (φ \land a \in (1 \dots A)) \to {var}_{1} (K) \in {Base}_{{Poly}_{1} (K)}$
61	43	zrhrhm	$⊢ {Poly}_{1} (K) \in Ring \to ℤRHom ({Poly}_{1} (K)) \in (ℤ_{ring} RingHom {Poly}_{1} (K))$
62	55 61	syl	$⊢ (φ \land a \in (1 \dots A)) \to ℤRHom ({Poly}_{1} (K)) \in (ℤ_{ring} RingHom {Poly}_{1} (K))$
63		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
64	63 49	rhmf	$⊢ ℤRHom ({Poly}_{1} (K)) \in (ℤ_{ring} RingHom {Poly}_{1} (K)) \to ℤRHom ({Poly}_{1} (K)) : ℤ ⟶ {Base}_{{Poly}_{1} (K)}$
65	62 64	syl	$⊢ (φ \land a \in (1 \dots A)) \to ℤRHom ({Poly}_{1} (K)) : ℤ ⟶ {Base}_{{Poly}_{1} (K)}$
66	65 15	ffvelcdmd	$⊢ (φ \land a \in (1 \dots A)) \to ℤRHom ({Poly}_{1} (K)) (a) \in {Base}_{{Poly}_{1} (K)}$
67	49 50 56 60 66	grpcld	$⊢ (φ \land a \in (1 \dots A)) \to {var}_{1} (K) +_{{Poly}_{1} (K)} ℤRHom ({Poly}_{1} (K)) (a) \in {Base}_{{Poly}_{1} (K)}$
68	48 67	eqeltrd	$⊢ (φ \land a \in (1 \dots A)) \to {var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a)) \in {Base}_{{Poly}_{1} (K)}$
69	68	adantr	$⊢ ((φ \land a \in (1 \dots A)) \land [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)) \to {var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a)) \in {Base}_{{Poly}_{1} (K)}$
70	22	adantr	$⊢ ((φ \land a \in (1 \dots A)) \land [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)) \to N \in ℕ$
71	7 69 70	aks6d1c1p1	$⊢ ((φ \land a \in (1 \dots A)) \land [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)) \to (N \underset{˙}{\sim} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a))) \leftrightarrow \forall y \in ({mulGrp}_{K} PrimRoots R) N \cdot_{{mulGrp}_{K}} {eval}_{1} (K) ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a))) (y) = {eval}_{1} (K) ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a))) (N \cdot_{{mulGrp}_{K}} y))$
72	40 71	mpbird	$⊢ ((φ \land a \in (1 \dots A)) \land [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)) \to N \underset{˙}{\sim} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a)))$
73	72	ex	$⊢ (φ \land a \in (1 \dots A)) \to ([(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a))] (S ~_{QG} L) \to N \underset{˙}{\sim} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a))))$
74	73	ralimdva	$⊢ φ \to (\forall a \in (1 \dots A) [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a))] (S ~_{QG} L) \to \forall a \in (1 \dots A) N \underset{˙}{\sim} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a))))$
75	9 74	mpd	$⊢ φ \to \forall a \in (1 \dots A) N \underset{˙}{\sim} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a)))$

Metamath Proof Explorer

Theorem aks5lem5a

Proof