aks6d1c5lem1

Description: Lemma for claim 5, evaluate the linear factor at -c to get a root. (Contributed by metakunt, 5-May-2025)

	Ref	Expression
Hypotheses	aks6d1p5.1	$⊢ φ \to K \in Field$
	aks6d1p5.2	$⊢ φ \to P \in ℙ$
	aks6d1c5.3	$⊢ P = chr (K)$
	aks6d1c5.4	$⊢ φ \to A \in ℕ_{0}$
	aks6d1c5.5	$⊢ φ \to A < P$
	aks6d1c5.6	$⊢ X = {var}_{1} (K)$
	aks6d1c5.7	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{{Poly}_{1} (K)}}$
	aks6d1c5.8	$⊢ G = (g \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {\sum_{{mulGrp}_{{Poly}_{1} (K)}}}_{i = 0}^{A} (g (i) \underset{˙}{\times} (X +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (i)))))$
	aks6d1c5p1.1	$⊢ φ \to B \in (0 \dots A)$
	aks6d1c5p1.2	$⊢ φ \to C \in (0 \dots A)$
Assertion	aks6d1c5lem1	$⊢ φ \to (B = C \leftrightarrow {eval}_{1} (K) (X +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (B))) (ℤRHom (K) (0 - C)) = 0_{K})$

Proof

Step	Hyp	Ref	Expression
1		aks6d1p5.1	$⊢ φ \to K \in Field$
2		aks6d1p5.2	$⊢ φ \to P \in ℙ$
3		aks6d1c5.3	$⊢ P = chr (K)$
4		aks6d1c5.4	$⊢ φ \to A \in ℕ_{0}$
5		aks6d1c5.5	$⊢ φ \to A < P$
6		aks6d1c5.6	$⊢ X = {var}_{1} (K)$
7		aks6d1c5.7	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{{Poly}_{1} (K)}}$
8		aks6d1c5.8	$⊢ G = (g \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {\sum_{{mulGrp}_{{Poly}_{1} (K)}}}_{i = 0}^{A} (g (i) \underset{˙}{\times} (X +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (i)))))$
9		aks6d1c5p1.1	$⊢ φ \to B \in (0 \dots A)$
10		aks6d1c5p1.2	$⊢ φ \to C \in (0 \dots A)$
11		zringplusg	$⊢ + = +_{ℤ_{ring}}$
12	11	eqcomi	$⊢ +_{ℤ_{ring}} = +$
13	12	a1i	$⊢ φ \to +_{ℤ_{ring}} = +$
14	13	oveqd	$⊢ φ \to (0 - C) +_{ℤ_{ring}} B = 0 - C + B$
15		0cnd	$⊢ φ \to 0 \in ℂ$
16	10	elfzelzd	$⊢ φ \to C \in ℤ$
17	16	zcnd	$⊢ φ \to C \in ℂ$
18	9	elfzelzd	$⊢ φ \to B \in ℤ$
19	18	zcnd	$⊢ φ \to B \in ℂ$
20	15 17 19	subadd23d	$⊢ φ \to 0 - C + B = 0 + B - C$
21	19 17	subcld	$⊢ φ \to B - C \in ℂ$
22	21	addlidd	$⊢ φ \to 0 + B - C = B - C$
23	20 22	eqtrd	$⊢ φ \to 0 - C + B = B - C$
24	14 23	eqtrd	$⊢ φ \to (0 - C) +_{ℤ_{ring}} B = B - C$
25	24	fveq2d	$⊢ φ \to ℤRHom (K) ((0 - C) +_{ℤ_{ring}} B) = ℤRHom (K) (B - C)$
26	25	eqeq1d	$⊢ φ \to (ℤRHom (K) ((0 - C) +_{ℤ_{ring}} B) = 0_{K} \leftrightarrow ℤRHom (K) (B - C) = 0_{K})$
27	2	adantr	$⊢ (φ \land B = C) \to P \in ℙ$
28		prmnn	$⊢ P \in ℙ \to P \in ℕ$
29	27 28	syl	$⊢ (φ \land B = C) \to P \in ℕ$
30	29	nnzd	$⊢ (φ \land B = C) \to P \in ℤ$
31		dvds0	$⊢ P \in ℤ \to P ∥ 0$
32	30 31	syl	$⊢ (φ \land B = C) \to P ∥ 0$
33	19	adantr	$⊢ (φ \land B = C) \to B \in ℂ$
34	33	subidd	$⊢ (φ \land B = C) \to B - B = 0$
35	34	eqcomd	$⊢ (φ \land B = C) \to 0 = B - B$
36		simpr	$⊢ (φ \land B = C) \to B = C$
37	36	oveq2d	$⊢ (φ \land B = C) \to B - B = B - C$
38	35 37	eqtrd	$⊢ (φ \land B = C) \to 0 = B - C$
39	32 38	breqtrd	$⊢ (φ \land B = C) \to P ∥ (B - C)$
40	39	ex	$⊢ φ \to (B = C \to P ∥ (B - C))$
41	2 28	syl	$⊢ φ \to P \in ℕ$
42	41	adantr	$⊢ (φ \land \neg B = C) \to P \in ℕ$
43	42	adantr	$⊢ ((φ \land \neg B = C) \land C < B) \to P \in ℕ$
44		1zzd	$⊢ ((φ \land \neg B = C) \land C < B) \to 1 \in ℤ$
45	43	nnzd	$⊢ ((φ \land \neg B = C) \land C < B) \to P \in ℤ$
46	45 44	zsubcld	$⊢ ((φ \land \neg B = C) \land C < B) \to P - 1 \in ℤ$
47	18 16	zsubcld	$⊢ φ \to B - C \in ℤ$
48	47	ad2antrr	$⊢ ((φ \land \neg B = C) \land C < B) \to B - C \in ℤ$
49		1e0p1	$⊢ 1 = 0 + 1$
50	49	a1i	$⊢ ((φ \land \neg B = C) \land C < B) \to 1 = 0 + 1$
51		simpr	$⊢ ((φ \land \neg B = C) \land C < B) \to C < B$
52	16	zred	$⊢ φ \to C \in ℝ$
53	52	adantr	$⊢ (φ \land \neg B = C) \to C \in ℝ$
54	53	adantr	$⊢ ((φ \land \neg B = C) \land C < B) \to C \in ℝ$
55	18	zred	$⊢ φ \to B \in ℝ$
56	55	adantr	$⊢ (φ \land \neg B = C) \to B \in ℝ$
57	56	adantr	$⊢ ((φ \land \neg B = C) \land C < B) \to B \in ℝ$
58	54 57	posdifd	$⊢ ((φ \land \neg B = C) \land C < B) \to (C < B \leftrightarrow 0 < B - C)$
59	51 58	mpbid	$⊢ ((φ \land \neg B = C) \land C < B) \to 0 < B - C$
60		0zd	$⊢ ((φ \land \neg B = C) \land C < B) \to 0 \in ℤ$
61	60 48	zltp1led	$⊢ ((φ \land \neg B = C) \land C < B) \to (0 < B - C \leftrightarrow 0 + 1 \leq B - C)$
62	59 61	mpbid	$⊢ ((φ \land \neg B = C) \land C < B) \to 0 + 1 \leq B - C$
63	50 62	eqbrtrd	$⊢ ((φ \land \neg B = C) \land C < B) \to 1 \leq B - C$
64	48	zred	$⊢ ((φ \land \neg B = C) \land C < B) \to B - C \in ℝ$
65	43	nnred	$⊢ ((φ \land \neg B = C) \land C < B) \to P \in ℝ$
66		elfzle1	$⊢ C \in (0 \dots A) \to 0 \leq C$
67	10 66	syl	$⊢ φ \to 0 \leq C$
68	67	adantr	$⊢ (φ \land \neg B = C) \to 0 \leq C$
69	68	adantr	$⊢ ((φ \land \neg B = C) \land C < B) \to 0 \leq C$
70	57 54	subge02d	$⊢ ((φ \land \neg B = C) \land C < B) \to (0 \leq C \leftrightarrow B - C \leq B)$
71	69 70	mpbid	$⊢ ((φ \land \neg B = C) \land C < B) \to B - C \leq B$
72	4	nn0red	$⊢ φ \to A \in ℝ$
73	41	nnred	$⊢ φ \to P \in ℝ$
74		elfzle2	$⊢ B \in (0 \dots A) \to B \leq A$
75	9 74	syl	$⊢ φ \to B \leq A$
76	55 72 73 75 5	lelttrd	$⊢ φ \to B < P$
77	76	adantr	$⊢ (φ \land \neg B = C) \to B < P$
78	77	adantr	$⊢ ((φ \land \neg B = C) \land C < B) \to B < P$
79	64 57 65 71 78	lelttrd	$⊢ ((φ \land \neg B = C) \land C < B) \to B - C < P$
80	48 45	zltlem1d	$⊢ ((φ \land \neg B = C) \land C < B) \to (B - C < P \leftrightarrow B - C \leq P - 1)$
81	79 80	mpbid	$⊢ ((φ \land \neg B = C) \land C < B) \to B - C \leq P - 1$
82	44 46 48 63 81	elfzd	$⊢ ((φ \land \neg B = C) \land C < B) \to B - C \in (1 \dots P - 1)$
83		fzm1ndvds	$⊢ (P \in ℕ \land B - C \in (1 \dots P - 1)) \to \neg P ∥ (B - C)$
84	43 82 83	syl2anc	$⊢ ((φ \land \neg B = C) \land C < B) \to \neg P ∥ (B - C)$
85		simpll	$⊢ ((φ \land \neg B = C) \land \neg C < B) \to φ$
86		axlttri	$⊢ (B \in ℝ \land C \in ℝ) \to (B < C \leftrightarrow \neg (B = C \lor C < B))$
87	55 52 86	syl2anc	$⊢ φ \to (B < C \leftrightarrow \neg (B = C \lor C < B))$
88		ioran	$⊢ \neg (B = C \lor C < B) \leftrightarrow (\neg B = C \land \neg C < B)$
89	88	a1i	$⊢ φ \to (\neg (B = C \lor C < B) \leftrightarrow (\neg B = C \land \neg C < B))$
90	87 89	bitr2d	$⊢ φ \to ((\neg B = C \land \neg C < B) \leftrightarrow B < C)$
91	90	biimpd	$⊢ φ \to ((\neg B = C \land \neg C < B) \to B < C)$
92	91	imp	$⊢ (φ \land (\neg B = C \land \neg C < B)) \to B < C$
93	92	anassrs	$⊢ ((φ \land \neg B = C) \land \neg C < B) \to B < C$
94	85 93	jca	$⊢ ((φ \land \neg B = C) \land \neg C < B) \to (φ \land B < C)$
95	41	adantr	$⊢ (φ \land B < C) \to P \in ℕ$
96		1zzd	$⊢ (φ \land B < C) \to 1 \in ℤ$
97	41	nnzd	$⊢ φ \to P \in ℤ$
98	97	adantr	$⊢ (φ \land B < C) \to P \in ℤ$
99	98 96	zsubcld	$⊢ (φ \land B < C) \to P - 1 \in ℤ$
100	16	adantr	$⊢ (φ \land B < C) \to C \in ℤ$
101	18	adantr	$⊢ (φ \land B < C) \to B \in ℤ$
102	100 101	zsubcld	$⊢ (φ \land B < C) \to C - B \in ℤ$
103	49	a1i	$⊢ (φ \land B < C) \to 1 = 0 + 1$
104	55 52	posdifd	$⊢ φ \to (B < C \leftrightarrow 0 < C - B)$
105	104	biimpd	$⊢ φ \to (B < C \to 0 < C - B)$
106	105	imp	$⊢ (φ \land B < C) \to 0 < C - B$
107		0zd	$⊢ (φ \land B < C) \to 0 \in ℤ$
108	107 102	zltp1led	$⊢ (φ \land B < C) \to (0 < C - B \leftrightarrow 0 + 1 \leq C - B)$
109	106 108	mpbid	$⊢ (φ \land B < C) \to 0 + 1 \leq C - B$
110	103 109	eqbrtrd	$⊢ (φ \land B < C) \to 1 \leq C - B$
111	102	zred	$⊢ (φ \land B < C) \to C - B \in ℝ$
112	52	adantr	$⊢ (φ \land B < C) \to C \in ℝ$
113	73	adantr	$⊢ (φ \land B < C) \to P \in ℝ$
114	9	adantr	$⊢ (φ \land B < C) \to B \in (0 \dots A)$
115		elfzle1	$⊢ B \in (0 \dots A) \to 0 \leq B$
116	114 115	syl	$⊢ (φ \land B < C) \to 0 \leq B$
117	55	adantr	$⊢ (φ \land B < C) \to B \in ℝ$
118	112 117	subge02d	$⊢ (φ \land B < C) \to (0 \leq B \leftrightarrow C - B \leq C)$
119	116 118	mpbid	$⊢ (φ \land B < C) \to C - B \leq C$
120	72	adantr	$⊢ (φ \land B < C) \to A \in ℝ$
121		elfzle2	$⊢ C \in (0 \dots A) \to C \leq A$
122	10 121	syl	$⊢ φ \to C \leq A$
123	122	adantr	$⊢ (φ \land B < C) \to C \leq A$
124	5	adantr	$⊢ (φ \land B < C) \to A < P$
125	112 120 113 123 124	lelttrd	$⊢ (φ \land B < C) \to C < P$
126	111 112 113 119 125	lelttrd	$⊢ (φ \land B < C) \to C - B < P$
127	102 98	zltlem1d	$⊢ (φ \land B < C) \to (C - B < P \leftrightarrow C - B \leq P - 1)$
128	126 127	mpbid	$⊢ (φ \land B < C) \to C - B \leq P - 1$
129	96 99 102 110 128	elfzd	$⊢ (φ \land B < C) \to C - B \in (1 \dots P - 1)$
130		fzm1ndvds	$⊢ (P \in ℕ \land C - B \in (1 \dots P - 1)) \to \neg P ∥ (C - B)$
131	95 129 130	syl2anc	$⊢ (φ \land B < C) \to \neg P ∥ (C - B)$
132		dvdsnegb	$⊢ (P \in ℤ \land B - C \in ℤ) \to (P ∥ (B - C) \leftrightarrow P ∥ (- (B - C)))$
133	97 47 132	syl2anc	$⊢ φ \to (P ∥ (B - C) \leftrightarrow P ∥ (- (B - C)))$
134	19 17	negsubdi2d	$⊢ φ \to - (B - C) = C - B$
135	134	breq2d	$⊢ φ \to (P ∥ (- (B - C)) \leftrightarrow P ∥ (C - B))$
136	133 135	bitrd	$⊢ φ \to (P ∥ (B - C) \leftrightarrow P ∥ (C - B))$
137	136	adantr	$⊢ (φ \land B < C) \to (P ∥ (B - C) \leftrightarrow P ∥ (C - B))$
138	131 137	mtbird	$⊢ (φ \land B < C) \to \neg P ∥ (B - C)$
139	94 138	syl	$⊢ ((φ \land \neg B = C) \land \neg C < B) \to \neg P ∥ (B - C)$
140	84 139	pm2.61dan	$⊢ (φ \land \neg B = C) \to \neg P ∥ (B - C)$
141	140	ex	$⊢ φ \to (\neg B = C \to \neg P ∥ (B - C))$
142	141	con4d	$⊢ φ \to (P ∥ (B - C) \to B = C)$
143	40 142	impbid	$⊢ φ \to (B = C \leftrightarrow P ∥ (B - C))$
144	1	fldcrngd	$⊢ φ \to K \in CRing$
145		crngring	$⊢ K \in CRing \to K \in Ring$
146	144 145	syl	$⊢ φ \to K \in Ring$
147		eqid	$⊢ ℤRHom (K) = ℤRHom (K)$
148		eqid	$⊢ 0_{K} = 0_{K}$
149	3 147 148	chrdvds	$⊢ (K \in Ring \land B - C \in ℤ) \to (P ∥ (B - C) \leftrightarrow ℤRHom (K) (B - C) = 0_{K})$
150	146 47 149	syl2anc	$⊢ φ \to (P ∥ (B - C) \leftrightarrow ℤRHom (K) (B - C) = 0_{K})$
151	143 150	bitr2d	$⊢ φ \to (ℤRHom (K) (B - C) = 0_{K} \leftrightarrow B = C)$
152	26 151	bitrd	$⊢ φ \to (ℤRHom (K) ((0 - C) +_{ℤ_{ring}} B) = 0_{K} \leftrightarrow B = C)$
153	152	bicomd	$⊢ φ \to (B = C \leftrightarrow ℤRHom (K) ((0 - C) +_{ℤ_{ring}} B) = 0_{K})$
154	147	zrhrhm	$⊢ K \in Ring \to ℤRHom (K) \in (ℤ_{ring} RingHom K)$
155		rhmghm	$⊢ ℤRHom (K) \in (ℤ_{ring} RingHom K) \to ℤRHom (K) \in (ℤ_{ring} GrpHom K)$
156	154 155	syl	$⊢ K \in Ring \to ℤRHom (K) \in (ℤ_{ring} GrpHom K)$
157	146 156	syl	$⊢ φ \to ℤRHom (K) \in (ℤ_{ring} GrpHom K)$
158		0zd	$⊢ φ \to 0 \in ℤ$
159	158 16	zsubcld	$⊢ φ \to 0 - C \in ℤ$
160		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
161	159 160	eleqtrdi	$⊢ φ \to 0 - C \in {Base}_{ℤ_{ring}}$
162	18 160	eleqtrdi	$⊢ φ \to B \in {Base}_{ℤ_{ring}}$
163		eqid	$⊢ {Base}_{ℤ_{ring}} = {Base}_{ℤ_{ring}}$
164		eqid	$⊢ +_{ℤ_{ring}} = +_{ℤ_{ring}}$
165		eqid	$⊢ +_{K} = +_{K}$
166	163 164 165	ghmlin	$⊢ (ℤRHom (K) \in (ℤ_{ring} GrpHom K) \land 0 - C \in {Base}_{ℤ_{ring}} \land B \in {Base}_{ℤ_{ring}}) \to ℤRHom (K) ((0 - C) +_{ℤ_{ring}} B) = ℤRHom (K) (0 - C) +_{K} ℤRHom (K) (B)$
167	157 161 162 166	syl3anc	$⊢ φ \to ℤRHom (K) ((0 - C) +_{ℤ_{ring}} B) = ℤRHom (K) (0 - C) +_{K} ℤRHom (K) (B)$
168	167	eqeq1d	$⊢ φ \to (ℤRHom (K) ((0 - C) +_{ℤ_{ring}} B) = 0_{K} \leftrightarrow ℤRHom (K) (0 - C) +_{K} ℤRHom (K) (B) = 0_{K})$
169	153 168	bitrd	$⊢ φ \to (B = C \leftrightarrow ℤRHom (K) (0 - C) +_{K} ℤRHom (K) (B) = 0_{K})$
170		eqid	$⊢ {eval}_{1} (K) = {eval}_{1} (K)$
171		eqid	$⊢ {Poly}_{1} (K) = {Poly}_{1} (K)$
172		eqid	$⊢ {Base}_{K} = {Base}_{K}$
173		eqid	$⊢ {Base}_{{Poly}_{1} (K)} = {Base}_{{Poly}_{1} (K)}$
174	160 172	ghmf	$⊢ ℤRHom (K) \in (ℤ_{ring} GrpHom K) \to ℤRHom (K) : ℤ ⟶ {Base}_{K}$
175	157 174	syl	$⊢ φ \to ℤRHom (K) : ℤ ⟶ {Base}_{K}$
176	175 159	ffvelcdmd	$⊢ φ \to ℤRHom (K) (0 - C) \in {Base}_{K}$
177	170 6 172 171 173 144 176	evl1vard	$⊢ φ \to (X \in {Base}_{{Poly}_{1} (K)} \land {eval}_{1} (K) (X) (ℤRHom (K) (0 - C)) = ℤRHom (K) (0 - C))$
178		eqid	$⊢ algSc ({Poly}_{1} (K)) = algSc ({Poly}_{1} (K))$
179	175 18	ffvelcdmd	$⊢ φ \to ℤRHom (K) (B) \in {Base}_{K}$
180	170 171 172 178 173 144 179 176	evl1scad	$⊢ φ \to (algSc ({Poly}_{1} (K)) (ℤRHom (K) (B)) \in {Base}_{{Poly}_{1} (K)} \land {eval}_{1} (K) (algSc ({Poly}_{1} (K)) (ℤRHom (K) (B))) (ℤRHom (K) (0 - C)) = ℤRHom (K) (B))$
181		eqid	$⊢ +_{{Poly}_{1} (K)} = +_{{Poly}_{1} (K)}$
182	170 171 172 173 144 176 177 180 181 165	evl1addd	$⊢ φ \to (X +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (B)) \in {Base}_{{Poly}_{1} (K)} \land {eval}_{1} (K) (X +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (B))) (ℤRHom (K) (0 - C)) = ℤRHom (K) (0 - C) +_{K} ℤRHom (K) (B))$
183	182	simprd	$⊢ φ \to {eval}_{1} (K) (X +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (B))) (ℤRHom (K) (0 - C)) = ℤRHom (K) (0 - C) +_{K} ℤRHom (K) (B)$
184	183	eqcomd	$⊢ φ \to ℤRHom (K) (0 - C) +_{K} ℤRHom (K) (B) = {eval}_{1} (K) (X +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (B))) (ℤRHom (K) (0 - C))$
185	184	eqeq1d	$⊢ φ \to (ℤRHom (K) (0 - C) +_{K} ℤRHom (K) (B) = 0_{K} \leftrightarrow {eval}_{1} (K) (X +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (B))) (ℤRHom (K) (0 - C)) = 0_{K})$
186	169 185	bitrd	$⊢ φ \to (B = C \leftrightarrow {eval}_{1} (K) (X +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (B))) (ℤRHom (K) (0 - C)) = 0_{K})$

Metamath Proof Explorer

Theorem aks6d1c5lem1

Proof