aks6d1c6isolem2

Description: Lemma to construct the group homomorphism for the AKS Theorem. (Contributed by metakunt, 14-May-2025)

	Ref	Expression
Hypotheses	aks6d1c6isolem1.1	$⊢ φ \to R \in CMnd$
	aks6d1c6isolem1.2	$⊢ φ \to K \in ℕ$
	aks6d1c6isolem1.3	$⊢ U = \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
	aks6d1c6isolem1.4	$⊢ F = (x \in ℤ ⟼ x \cdot_{(R ↾_{𝑠} U)} M)$
	aks6d1c6isolem1.5	$⊢ φ \to M \in (R PrimRoots K)$
Assertion	aks6d1c6isolem2	$⊢ φ \to F \in (ℤ_{ring} GrpHom ((R ↾_{𝑠} U) ↾_{𝑠} ran F))$

Proof

Step	Hyp	Ref	Expression
1		aks6d1c6isolem1.1	$⊢ φ \to R \in CMnd$
2		aks6d1c6isolem1.2	$⊢ φ \to K \in ℕ$
3		aks6d1c6isolem1.3	$⊢ U = \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
4		aks6d1c6isolem1.4	$⊢ F = (x \in ℤ ⟼ x \cdot_{(R ↾_{𝑠} U)} M)$
5		aks6d1c6isolem1.5	$⊢ φ \to M \in (R PrimRoots K)$
6		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
7		eqid	$⊢ {Base}_{((R ↾_{𝑠} U) ↾_{𝑠} ran F)} = {Base}_{((R ↾_{𝑠} U) ↾_{𝑠} ran F)}$
8		zringplusg	$⊢ + = +_{ℤ_{ring}}$
9		zex	$⊢ ℤ \in V$
10	9	mptex	$⊢ (x \in ℤ ⟼ x \cdot_{(R ↾_{𝑠} U)} M) \in V$
11	4 10	eqeltri	$⊢ F \in V$
12	11	rnex	$⊢ ran F \in V$
13		eqid	$⊢ (R ↾_{𝑠} U) ↾_{𝑠} ran F = (R ↾_{𝑠} U) ↾_{𝑠} ran F$
14		eqid	$⊢ +_{(R ↾_{𝑠} U)} = +_{(R ↾_{𝑠} U)}$
15	13 14	ressplusg	$⊢ ran F \in V \to +_{(R ↾_{𝑠} U)} = +_{((R ↾_{𝑠} U) ↾_{𝑠} ran F)}$
16	12 15	ax-mp	$⊢ +_{(R ↾_{𝑠} U)} = +_{((R ↾_{𝑠} U) ↾_{𝑠} ran F)}$
17		zringring	$⊢ ℤ_{ring} \in Ring$
18	17	a1i	$⊢ φ \to ℤ_{ring} \in Ring$
19		ringgrp	$⊢ ℤ_{ring} \in Ring \to ℤ_{ring} \in Grp$
20	18 19	syl	$⊢ φ \to ℤ_{ring} \in Grp$
21	1 2 3 4 5	aks6d1c6isolem1	$⊢ φ \to (R ↾_{𝑠} U) ↾_{𝑠} ran F \in Grp$
22		ovexd	$⊢ (φ \land x \in ℤ) \to x \cdot_{(R ↾_{𝑠} U)} M \in V$
23	22 4	fmptd	$⊢ φ \to F : ℤ ⟶ V$
24		ffn	$⊢ F : ℤ ⟶ V \to F Fn ℤ$
25	23 24	syl	$⊢ φ \to F Fn ℤ$
26		dffn3	$⊢ F Fn ℤ \leftrightarrow F : ℤ ⟶ ran F$
27	25 26	sylib	$⊢ φ \to F : ℤ ⟶ ran F$
28		fvelrnb	$⊢ F Fn ℤ \to (w \in ran F \leftrightarrow \exists v \in ℤ F (v) = w)$
29	25 28	syl	$⊢ φ \to (w \in ran F \leftrightarrow \exists v \in ℤ F (v) = w)$
30	29	biimpd	$⊢ φ \to (w \in ran F \to \exists v \in ℤ F (v) = w)$
31	30	imp	$⊢ (φ \land w \in ran F) \to \exists v \in ℤ F (v) = w$
32		simpr	$⊢ (((φ \land \exists v \in ℤ F (v) = w) \land z \in ℤ) \land F (z) = w) \to F (z) = w$
33	32	eqcomd	$⊢ (((φ \land \exists v \in ℤ F (v) = w) \land z \in ℤ) \land F (z) = w) \to w = F (z)$
34		simplll	$⊢ (((φ \land \exists v \in ℤ F (v) = w) \land z \in ℤ) \land F (z) = w) \to φ$
35		simplr	$⊢ (((φ \land \exists v \in ℤ F (v) = w) \land z \in ℤ) \land F (z) = w) \to z \in ℤ$
36	34 35	jca	$⊢ (((φ \land \exists v \in ℤ F (v) = w) \land z \in ℤ) \land F (z) = w) \to (φ \land z \in ℤ)$
37	4	a1i	$⊢ (φ \land z \in ℤ) \to F = (x \in ℤ ⟼ x \cdot_{(R ↾_{𝑠} U)} M)$
38		simpr	$⊢ ((φ \land z \in ℤ) \land x = z) \to x = z$
39	38	oveq1d	$⊢ ((φ \land z \in ℤ) \land x = z) \to x \cdot_{(R ↾_{𝑠} U)} M = z \cdot_{(R ↾_{𝑠} U)} M$
40		simpr	$⊢ (φ \land z \in ℤ) \to z \in ℤ$
41		ovexd	$⊢ (φ \land z \in ℤ) \to z \cdot_{(R ↾_{𝑠} U)} M \in V$
42	37 39 40 41	fvmptd	$⊢ (φ \land z \in ℤ) \to F (z) = z \cdot_{(R ↾_{𝑠} U)} M$
43		eqid	$⊢ {Base}_{(R ↾_{𝑠} U)} = {Base}_{(R ↾_{𝑠} U)}$
44		eqid	$⊢ \cdot_{(R ↾_{𝑠} U)} = \cdot_{(R ↾_{𝑠} U)}$
45	1 2 3	primrootsunit	$⊢ φ \to (R PrimRoots K = (R ↾_{𝑠} U) PrimRoots K \land R ↾_{𝑠} U \in Abel)$
46	45	simprd	$⊢ φ \to R ↾_{𝑠} U \in Abel$
47	46	ablgrpd	$⊢ φ \to R ↾_{𝑠} U \in Grp$
48	47	adantr	$⊢ (φ \land z \in ℤ) \to R ↾_{𝑠} U \in Grp$
49	45	simpld	$⊢ φ \to R PrimRoots K = (R ↾_{𝑠} U) PrimRoots K$
50	5 49	eleqtrd	$⊢ φ \to M \in ((R ↾_{𝑠} U) PrimRoots K)$
51	46	ablcmnd	$⊢ φ \to R ↾_{𝑠} U \in CMnd$
52	2	nnnn0d	$⊢ φ \to K \in ℕ_{0}$
53	51 52 44	isprimroot	$⊢ φ \to (M \in ((R ↾_{𝑠} U) PrimRoots K) \leftrightarrow (M \in {Base}_{(R ↾_{𝑠} U)} \land K \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \land \forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)))$
54	53	biimpd	$⊢ φ \to (M \in ((R ↾_{𝑠} U) PrimRoots K) \to (M \in {Base}_{(R ↾_{𝑠} U)} \land K \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \land \forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)))$
55	50 54	mpd	$⊢ φ \to (M \in {Base}_{(R ↾_{𝑠} U)} \land K \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \land \forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l))$
56	55	simp1d	$⊢ φ \to M \in {Base}_{(R ↾_{𝑠} U)}$
57	56	adantr	$⊢ (φ \land z \in ℤ) \to M \in {Base}_{(R ↾_{𝑠} U)}$
58	43 44 48 40 57	mulgcld	$⊢ (φ \land z \in ℤ) \to z \cdot_{(R ↾_{𝑠} U)} M \in {Base}_{(R ↾_{𝑠} U)}$
59	42 58	eqeltrd	$⊢ (φ \land z \in ℤ) \to F (z) \in {Base}_{(R ↾_{𝑠} U)}$
60	36 59	syl	$⊢ (((φ \land \exists v \in ℤ F (v) = w) \land z \in ℤ) \land F (z) = w) \to F (z) \in {Base}_{(R ↾_{𝑠} U)}$
61	33 60	eqeltrd	$⊢ (((φ \land \exists v \in ℤ F (v) = w) \land z \in ℤ) \land F (z) = w) \to w \in {Base}_{(R ↾_{𝑠} U)}$
62		nfv	$⊢ Ⅎ z F (v) = w$
63		nfv	$⊢ Ⅎ v F (z) = w$
64		fveqeq2	$⊢ v = z \to (F (v) = w \leftrightarrow F (z) = w)$
65	62 63 64	cbvrexw	$⊢ \exists v \in ℤ F (v) = w \leftrightarrow \exists z \in ℤ F (z) = w$
66	65	bilani	$⊢ (φ \land \exists v \in ℤ F (v) = w) \to \exists z \in ℤ F (z) = w$
67	61 66	r19.29a	$⊢ (φ \land \exists v \in ℤ F (v) = w) \to w \in {Base}_{(R ↾_{𝑠} U)}$
68	67	ex	$⊢ φ \to (\exists v \in ℤ F (v) = w \to w \in {Base}_{(R ↾_{𝑠} U)})$
69	68	adantr	$⊢ (φ \land w \in ran F) \to (\exists v \in ℤ F (v) = w \to w \in {Base}_{(R ↾_{𝑠} U)})$
70	69	imp	$⊢ ((φ \land w \in ran F) \land \exists v \in ℤ F (v) = w) \to w \in {Base}_{(R ↾_{𝑠} U)}$
71	31 70	mpdan	$⊢ (φ \land w \in ran F) \to w \in {Base}_{(R ↾_{𝑠} U)}$
72	71	ex	$⊢ φ \to (w \in ran F \to w \in {Base}_{(R ↾_{𝑠} U)})$
73	72	ssrdv	$⊢ φ \to ran F \subseteq {Base}_{(R ↾_{𝑠} U)}$
74	13 43	ressbas2	$⊢ ran F \subseteq {Base}_{(R ↾_{𝑠} U)} \to ran F = {Base}_{((R ↾_{𝑠} U) ↾_{𝑠} ran F)}$
75	73 74	syl	$⊢ φ \to ran F = {Base}_{((R ↾_{𝑠} U) ↾_{𝑠} ran F)}$
76	75	feq3d	$⊢ φ \to (F : ℤ ⟶ ran F \leftrightarrow F : ℤ ⟶ {Base}_{((R ↾_{𝑠} U) ↾_{𝑠} ran F)})$
77	27 76	mpbid	$⊢ φ \to F : ℤ ⟶ {Base}_{((R ↾_{𝑠} U) ↾_{𝑠} ran F)}$
78	4	a1i	$⊢ (φ \land (y \in ℤ \land z \in ℤ)) \to F = (x \in ℤ ⟼ x \cdot_{(R ↾_{𝑠} U)} M)$
79		simpr	$⊢ ((φ \land (y \in ℤ \land z \in ℤ)) \land x = y + z) \to x = y + z$
80	79	oveq1d	$⊢ ((φ \land (y \in ℤ \land z \in ℤ)) \land x = y + z) \to x \cdot_{(R ↾_{𝑠} U)} M = (y + z) \cdot_{(R ↾_{𝑠} U)} M$
81		simprl	$⊢ (φ \land (y \in ℤ \land z \in ℤ)) \to y \in ℤ$
82		simprr	$⊢ (φ \land (y \in ℤ \land z \in ℤ)) \to z \in ℤ$
83	81 82	zaddcld	$⊢ (φ \land (y \in ℤ \land z \in ℤ)) \to y + z \in ℤ$
84		ovexd	$⊢ (φ \land (y \in ℤ \land z \in ℤ)) \to (y + z) \cdot_{(R ↾_{𝑠} U)} M \in V$
85	78 80 83 84	fvmptd	$⊢ (φ \land (y \in ℤ \land z \in ℤ)) \to F (y + z) = (y + z) \cdot_{(R ↾_{𝑠} U)} M$
86	47	adantr	$⊢ (φ \land (y \in ℤ \land z \in ℤ)) \to R ↾_{𝑠} U \in Grp$
87	56	adantr	$⊢ (φ \land (y \in ℤ \land z \in ℤ)) \to M \in {Base}_{(R ↾_{𝑠} U)}$
88	81 82 87	3jca	$⊢ (φ \land (y \in ℤ \land z \in ℤ)) \to (y \in ℤ \land z \in ℤ \land M \in {Base}_{(R ↾_{𝑠} U)})$
89	43 44 14	mulgdir	$⊢ (R ↾_{𝑠} U \in Grp \land (y \in ℤ \land z \in ℤ \land M \in {Base}_{(R ↾_{𝑠} U)})) \to (y + z) \cdot_{(R ↾_{𝑠} U)} M = (y \cdot_{(R ↾_{𝑠} U)} M) +_{(R ↾_{𝑠} U)} (z \cdot_{(R ↾_{𝑠} U)} M)$
90	86 88 89	syl2anc	$⊢ (φ \land (y \in ℤ \land z \in ℤ)) \to (y + z) \cdot_{(R ↾_{𝑠} U)} M = (y \cdot_{(R ↾_{𝑠} U)} M) +_{(R ↾_{𝑠} U)} (z \cdot_{(R ↾_{𝑠} U)} M)$
91		simpr	$⊢ ((φ \land (y \in ℤ \land z \in ℤ)) \land x = y) \to x = y$
92	91	oveq1d	$⊢ ((φ \land (y \in ℤ \land z \in ℤ)) \land x = y) \to x \cdot_{(R ↾_{𝑠} U)} M = y \cdot_{(R ↾_{𝑠} U)} M$
93		ovexd	$⊢ (φ \land (y \in ℤ \land z \in ℤ)) \to y \cdot_{(R ↾_{𝑠} U)} M \in V$
94	78 92 81 93	fvmptd	$⊢ (φ \land (y \in ℤ \land z \in ℤ)) \to F (y) = y \cdot_{(R ↾_{𝑠} U)} M$
95		simpr	$⊢ ((φ \land (y \in ℤ \land z \in ℤ)) \land x = z) \to x = z$
96	95	oveq1d	$⊢ ((φ \land (y \in ℤ \land z \in ℤ)) \land x = z) \to x \cdot_{(R ↾_{𝑠} U)} M = z \cdot_{(R ↾_{𝑠} U)} M$
97		ovexd	$⊢ (φ \land (y \in ℤ \land z \in ℤ)) \to z \cdot_{(R ↾_{𝑠} U)} M \in V$
98	78 96 82 97	fvmptd	$⊢ (φ \land (y \in ℤ \land z \in ℤ)) \to F (z) = z \cdot_{(R ↾_{𝑠} U)} M$
99	94 98	oveq12d	$⊢ (φ \land (y \in ℤ \land z \in ℤ)) \to F (y) +_{(R ↾_{𝑠} U)} F (z) = (y \cdot_{(R ↾_{𝑠} U)} M) +_{(R ↾_{𝑠} U)} (z \cdot_{(R ↾_{𝑠} U)} M)$
100	99	eqcomd	$⊢ (φ \land (y \in ℤ \land z \in ℤ)) \to (y \cdot_{(R ↾_{𝑠} U)} M) +_{(R ↾_{𝑠} U)} (z \cdot_{(R ↾_{𝑠} U)} M) = F (y) +_{(R ↾_{𝑠} U)} F (z)$
101	90 100	eqtrd	$⊢ (φ \land (y \in ℤ \land z \in ℤ)) \to (y + z) \cdot_{(R ↾_{𝑠} U)} M = F (y) +_{(R ↾_{𝑠} U)} F (z)$
102	85 101	eqtrd	$⊢ (φ \land (y \in ℤ \land z \in ℤ)) \to F (y + z) = F (y) +_{(R ↾_{𝑠} U)} F (z)$
103	6 7 8 16 20 21 77 102	isghmd	$⊢ φ \to F \in (ℤ_{ring} GrpHom ((R ↾_{𝑠} U) ↾_{𝑠} ran F))$

Metamath Proof Explorer

Theorem aks6d1c6isolem2

Proof