ply1remlem

Description: A term of the form x - N is linear, monic, and has exactly one zero. (Contributed by Mario Carneiro, 12-Jun-2015)

	Ref	Expression
Hypotheses	ply1rem.p	$⊢ P = {Poly}_{1} (R)$
	ply1rem.b	$⊢ B = {Base}_{P}$
	ply1rem.k	$⊢ K = {Base}_{R}$
	ply1rem.x	$⊢ X = {var}_{1} (R)$
	ply1rem.m	$⊢ \underset{˙}{-} = -_{P}$
	ply1rem.a	$⊢ A = algSc (P)$
	ply1rem.g	$⊢ G = X \underset{˙}{-} A (N)$
	ply1rem.o	$⊢ O = {eval}_{1} (R)$
	ply1rem.1	$⊢ φ \to R \in NzRing$
	ply1rem.2	$⊢ φ \to R \in CRing$
	ply1rem.3	$⊢ φ \to N \in K$
	ply1rem.u	$⊢ U = {Monic}_{1p} (R)$
	ply1rem.d	$⊢ D = \deg_{1} (R)$
	ply1rem.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	ply1remlem	$⊢ φ \to (G \in U \land D (G) = 1 \land {O (G)}^{-1} [\{\underset{˙}{0}\}] = \{N\})$

Proof

Step	Hyp	Ref	Expression
1		ply1rem.p	$⊢ P = {Poly}_{1} (R)$
2		ply1rem.b	$⊢ B = {Base}_{P}$
3		ply1rem.k	$⊢ K = {Base}_{R}$
4		ply1rem.x	$⊢ X = {var}_{1} (R)$
5		ply1rem.m	$⊢ \underset{˙}{-} = -_{P}$
6		ply1rem.a	$⊢ A = algSc (P)$
7		ply1rem.g	$⊢ G = X \underset{˙}{-} A (N)$
8		ply1rem.o	$⊢ O = {eval}_{1} (R)$
9		ply1rem.1	$⊢ φ \to R \in NzRing$
10		ply1rem.2	$⊢ φ \to R \in CRing$
11		ply1rem.3	$⊢ φ \to N \in K$
12		ply1rem.u	$⊢ U = {Monic}_{1p} (R)$
13		ply1rem.d	$⊢ D = \deg_{1} (R)$
14		ply1rem.z	$⊢ \underset{˙}{0} = 0_{R}$
15		nzrring	$⊢ R \in NzRing \to R \in Ring$
16	9 15	syl	$⊢ φ \to R \in Ring$
17	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
18	16 17	syl	$⊢ φ \to P \in Ring$
19		ringgrp	$⊢ P \in Ring \to P \in Grp$
20	18 19	syl	$⊢ φ \to P \in Grp$
21	4 1 2	vr1cl	$⊢ R \in Ring \to X \in B$
22	16 21	syl	$⊢ φ \to X \in B$
23	1 6 3 2	ply1sclf	$⊢ R \in Ring \to A : K ⟶ B$
24	16 23	syl	$⊢ φ \to A : K ⟶ B$
25	24 11	ffvelrnd	$⊢ φ \to A (N) \in B$
26	2 5	grpsubcl	$⊢ (P \in Grp \land X \in B \land A (N) \in B) \to X \underset{˙}{-} A (N) \in B$
27	20 22 25 26	syl3anc	$⊢ φ \to X \underset{˙}{-} A (N) \in B$
28	7 27	eqeltrid	$⊢ φ \to G \in B$
29	7	fveq2i	$⊢ D (G) = D (X \underset{˙}{-} A (N))$
30	13 1 2	deg1xrcl	$⊢ A (N) \in B \to D (A (N)) \in ℝ^{*}$
31	25 30	syl	$⊢ φ \to D (A (N)) \in ℝ^{*}$
32		0xr	$⊢ 0 \in ℝ^{*}$
33	32	a1i	$⊢ φ \to 0 \in ℝ^{*}$
34		1re	$⊢ 1 \in ℝ$
35		rexr	$⊢ 1 \in ℝ \to 1 \in ℝ^{*}$
36	34 35	mp1i	$⊢ φ \to 1 \in ℝ^{*}$
37	13 1 3 6	deg1sclle	$⊢ (R \in Ring \land N \in K) \to D (A (N)) \leq 0$
38	16 11 37	syl2anc	$⊢ φ \to D (A (N)) \leq 0$
39		0lt1	$⊢ 0 < 1$
40	39	a1i	$⊢ φ \to 0 < 1$
41	31 33 36 38 40	xrlelttrd	$⊢ φ \to D (A (N)) < 1$
42		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
43	42 2	mgpbas	$⊢ B = {Base}_{{mulGrp}_{P}}$
44		eqid	$⊢ \cdot_{{mulGrp}_{P}} = \cdot_{{mulGrp}_{P}}$
45	43 44	mulg1	$⊢ X \in B \to 1 \cdot_{{mulGrp}_{P}} X = X$
46	22 45	syl	$⊢ φ \to 1 \cdot_{{mulGrp}_{P}} X = X$
47	46	fveq2d	$⊢ φ \to D (1 \cdot_{{mulGrp}_{P}} X) = D (X)$
48		1nn0	$⊢ 1 \in ℕ_{0}$
49	13 1 4 42 44	deg1pw	$⊢ (R \in NzRing \land 1 \in ℕ_{0}) \to D (1 \cdot_{{mulGrp}_{P}} X) = 1$
50	9 48 49	sylancl	$⊢ φ \to D (1 \cdot_{{mulGrp}_{P}} X) = 1$
51	47 50	eqtr3d	$⊢ φ \to D (X) = 1$
52	41 51	breqtrrd	$⊢ φ \to D (A (N)) < D (X)$
53	1 13 16 2 5 22 25 52	deg1sub	$⊢ φ \to D (X \underset{˙}{-} A (N)) = D (X)$
54	29 53	eqtrid	$⊢ φ \to D (G) = D (X)$
55	54 51	eqtrd	$⊢ φ \to D (G) = 1$
56	55 48	eqeltrdi	$⊢ φ \to D (G) \in ℕ_{0}$
57		eqid	$⊢ 0_{P} = 0_{P}$
58	13 1 57 2	deg1nn0clb	$⊢ (R \in Ring \land G \in B) \to (G \neq 0_{P} \leftrightarrow D (G) \in ℕ_{0})$
59	16 28 58	syl2anc	$⊢ φ \to (G \neq 0_{P} \leftrightarrow D (G) \in ℕ_{0})$
60	56 59	mpbird	$⊢ φ \to G \neq 0_{P}$
61	55	fveq2d	$⊢ φ \to {coe}_{1} (G) (D (G)) = {coe}_{1} (G) (1)$
62	7	fveq2i	$⊢ {coe}_{1} (G) = {coe}_{1} (X \underset{˙}{-} A (N))$
63	62	fveq1i	$⊢ {coe}_{1} (G) (1) = {coe}_{1} (X \underset{˙}{-} A (N)) (1)$
64	48	a1i	$⊢ φ \to 1 \in ℕ_{0}$
65		eqid	$⊢ -_{R} = -_{R}$
66	1 2 5 65	coe1subfv	$⊢ ((R \in Ring \land X \in B \land A (N) \in B) \land 1 \in ℕ_{0}) \to {coe}_{1} (X \underset{˙}{-} A (N)) (1) = {coe}_{1} (X) (1) -_{R} {coe}_{1} (A (N)) (1)$
67	16 22 25 64 66	syl31anc	$⊢ φ \to {coe}_{1} (X \underset{˙}{-} A (N)) (1) = {coe}_{1} (X) (1) -_{R} {coe}_{1} (A (N)) (1)$
68	63 67	eqtrid	$⊢ φ \to {coe}_{1} (G) (1) = {coe}_{1} (X) (1) -_{R} {coe}_{1} (A (N)) (1)$
69	46	oveq2d	$⊢ φ \to 1_{R} \cdot_{P} (1 \cdot_{{mulGrp}_{P}} X) = 1_{R} \cdot_{P} X$
70	1	ply1sca	$⊢ R \in NzRing \to R = Scalar (P)$
71	9 70	syl	$⊢ φ \to R = Scalar (P)$
72	71	fveq2d	$⊢ φ \to 1_{R} = 1_{Scalar (P)}$
73	72	oveq1d	$⊢ φ \to 1_{R} \cdot_{P} X = 1_{Scalar (P)} \cdot_{P} X$
74	1	ply1lmod	$⊢ R \in Ring \to P \in LMod$
75	16 74	syl	$⊢ φ \to P \in LMod$
76		eqid	$⊢ Scalar (P) = Scalar (P)$
77		eqid	$⊢ \cdot_{P} = \cdot_{P}$
78		eqid	$⊢ 1_{Scalar (P)} = 1_{Scalar (P)}$
79	2 76 77 78	lmodvs1	$⊢ (P \in LMod \land X \in B) \to 1_{Scalar (P)} \cdot_{P} X = X$
80	75 22 79	syl2anc	$⊢ φ \to 1_{Scalar (P)} \cdot_{P} X = X$
81	69 73 80	3eqtrd	$⊢ φ \to 1_{R} \cdot_{P} (1 \cdot_{{mulGrp}_{P}} X) = X$
82	81	fveq2d	$⊢ φ \to {coe}_{1} (1_{R} \cdot_{P} (1 \cdot_{{mulGrp}_{P}} X)) = {coe}_{1} (X)$
83	82	fveq1d	$⊢ φ \to {coe}_{1} (1_{R} \cdot_{P} (1 \cdot_{{mulGrp}_{P}} X)) (1) = {coe}_{1} (X) (1)$
84		eqid	$⊢ 1_{R} = 1_{R}$
85	3 84	ringidcl	$⊢ R \in Ring \to 1_{R} \in K$
86	16 85	syl	$⊢ φ \to 1_{R} \in K$
87	14 3 1 4 77 42 44	coe1tmfv1	$⊢ (R \in Ring \land 1_{R} \in K \land 1 \in ℕ_{0}) \to {coe}_{1} (1_{R} \cdot_{P} (1 \cdot_{{mulGrp}_{P}} X)) (1) = 1_{R}$
88	16 86 64 87	syl3anc	$⊢ φ \to {coe}_{1} (1_{R} \cdot_{P} (1 \cdot_{{mulGrp}_{P}} X)) (1) = 1_{R}$
89	83 88	eqtr3d	$⊢ φ \to {coe}_{1} (X) (1) = 1_{R}$
90		eqid	$⊢ 0_{R} = 0_{R}$
91	1 6 3 90	coe1scl	$⊢ (R \in Ring \land N \in K) \to {coe}_{1} (A (N)) = (x \in ℕ_{0} ⟼ if (x = 0, N, 0_{R}))$
92	16 11 91	syl2anc	$⊢ φ \to {coe}_{1} (A (N)) = (x \in ℕ_{0} ⟼ if (x = 0, N, 0_{R}))$
93	92	fveq1d	$⊢ φ \to {coe}_{1} (A (N)) (1) = (x \in ℕ_{0} ⟼ if (x = 0, N, 0_{R})) (1)$
94		ax-1ne0	$⊢ 1 \neq 0$
95		neeq1	$⊢ x = 1 \to (x \neq 0 \leftrightarrow 1 \neq 0)$
96	94 95	mpbiri	$⊢ x = 1 \to x \neq 0$
97		ifnefalse	$⊢ x \neq 0 \to if (x = 0, N, 0_{R}) = 0_{R}$
98	96 97	syl	$⊢ x = 1 \to if (x = 0, N, 0_{R}) = 0_{R}$
99		eqid	$⊢ (x \in ℕ_{0} ⟼ if (x = 0, N, 0_{R})) = (x \in ℕ_{0} ⟼ if (x = 0, N, 0_{R}))$
100		fvex	$⊢ 0_{R} \in V$
101	98 99 100	fvmpt	$⊢ 1 \in ℕ_{0} \to (x \in ℕ_{0} ⟼ if (x = 0, N, 0_{R})) (1) = 0_{R}$
102	48 101	ax-mp	$⊢ (x \in ℕ_{0} ⟼ if (x = 0, N, 0_{R})) (1) = 0_{R}$
103	93 102	eqtrdi	$⊢ φ \to {coe}_{1} (A (N)) (1) = 0_{R}$
104	89 103	oveq12d	$⊢ φ \to {coe}_{1} (X) (1) -_{R} {coe}_{1} (A (N)) (1) = 1_{R} -_{R} 0_{R}$
105		ringgrp	$⊢ R \in Ring \to R \in Grp$
106	16 105	syl	$⊢ φ \to R \in Grp$
107	3 90 65	grpsubid1	$⊢ (R \in Grp \land 1_{R} \in K) \to 1_{R} -_{R} 0_{R} = 1_{R}$
108	106 86 107	syl2anc	$⊢ φ \to 1_{R} -_{R} 0_{R} = 1_{R}$
109	104 108	eqtrd	$⊢ φ \to {coe}_{1} (X) (1) -_{R} {coe}_{1} (A (N)) (1) = 1_{R}$
110	61 68 109	3eqtrd	$⊢ φ \to {coe}_{1} (G) (D (G)) = 1_{R}$
111	1 2 57 13 12 84	ismon1p	$⊢ G \in U \leftrightarrow (G \in B \land G \neq 0_{P} \land {coe}_{1} (G) (D (G)) = 1_{R})$
112	28 60 110 111	syl3anbrc	$⊢ φ \to G \in U$
113	7	fveq2i	$⊢ O (G) = O (X \underset{˙}{-} A (N))$
114	113	fveq1i	$⊢ O (G) (x) = O (X \underset{˙}{-} A (N)) (x)$
115	10	adantr	$⊢ (φ \land x \in K) \to R \in CRing$
116		simpr	$⊢ (φ \land x \in K) \to x \in K$
117	8 4 3 1 2 115 116	evl1vard	$⊢ (φ \land x \in K) \to (X \in B \land O (X) (x) = x)$
118	11	adantr	$⊢ (φ \land x \in K) \to N \in K$
119	8 1 3 6 2 115 118 116	evl1scad	$⊢ (φ \land x \in K) \to (A (N) \in B \land O (A (N)) (x) = N)$
120	8 1 3 2 115 116 117 119 5 65	evl1subd	$⊢ (φ \land x \in K) \to (X \underset{˙}{-} A (N) \in B \land O (X \underset{˙}{-} A (N)) (x) = x -_{R} N)$
121	120	simprd	$⊢ (φ \land x \in K) \to O (X \underset{˙}{-} A (N)) (x) = x -_{R} N$
122	114 121	eqtrid	$⊢ (φ \land x \in K) \to O (G) (x) = x -_{R} N$
123	122	eqeq1d	$⊢ (φ \land x \in K) \to (O (G) (x) = \underset{˙}{0} \leftrightarrow x -_{R} N = \underset{˙}{0})$
124	106	adantr	$⊢ (φ \land x \in K) \to R \in Grp$
125	3 14 65	grpsubeq0	$⊢ (R \in Grp \land x \in K \land N \in K) \to (x -_{R} N = \underset{˙}{0} \leftrightarrow x = N)$
126	124 116 118 125	syl3anc	$⊢ (φ \land x \in K) \to (x -_{R} N = \underset{˙}{0} \leftrightarrow x = N)$
127	123 126	bitrd	$⊢ (φ \land x \in K) \to (O (G) (x) = \underset{˙}{0} \leftrightarrow x = N)$
128		velsn	$⊢ x \in \{N\} \leftrightarrow x = N$
129	127 128	bitr4di	$⊢ (φ \land x \in K) \to (O (G) (x) = \underset{˙}{0} \leftrightarrow x \in \{N\})$
130	129	pm5.32da	$⊢ φ \to ((x \in K \land O (G) (x) = \underset{˙}{0}) \leftrightarrow (x \in K \land x \in \{N\}))$
131		eqid	$⊢ R ↑_{𝑠} K = R ↑_{𝑠} K$
132		eqid	$⊢ {Base}_{(R ↑_{𝑠} K)} = {Base}_{(R ↑_{𝑠} K)}$
133	3	fvexi	$⊢ K \in V$
134	133	a1i	$⊢ φ \to K \in V$
135	8 1 131 3	evl1rhm	$⊢ R \in CRing \to O \in (P RingHom (R ↑_{𝑠} K))$
136	10 135	syl	$⊢ φ \to O \in (P RingHom (R ↑_{𝑠} K))$
137	2 132	rhmf	$⊢ O \in (P RingHom (R ↑_{𝑠} K)) \to O : B ⟶ {Base}_{(R ↑_{𝑠} K)}$
138	136 137	syl	$⊢ φ \to O : B ⟶ {Base}_{(R ↑_{𝑠} K)}$
139	138 28	ffvelrnd	$⊢ φ \to O (G) \in {Base}_{(R ↑_{𝑠} K)}$
140	131 3 132 9 134 139	pwselbas	$⊢ φ \to O (G) : K ⟶ K$
141	140	ffnd	$⊢ φ \to O (G) Fn K$
142		fniniseg	$⊢ O (G) Fn K \to (x \in {O (G)}^{-1} [\{\underset{˙}{0}\}] \leftrightarrow (x \in K \land O (G) (x) = \underset{˙}{0}))$
143	141 142	syl	$⊢ φ \to (x \in {O (G)}^{-1} [\{\underset{˙}{0}\}] \leftrightarrow (x \in K \land O (G) (x) = \underset{˙}{0}))$
144	11	snssd	$⊢ φ \to \{N\} \subseteq K$
145	144	sseld	$⊢ φ \to (x \in \{N\} \to x \in K)$
146	145	pm4.71rd	$⊢ φ \to (x \in \{N\} \leftrightarrow (x \in K \land x \in \{N\}))$
147	130 143 146	3bitr4d	$⊢ φ \to (x \in {O (G)}^{-1} [\{\underset{˙}{0}\}] \leftrightarrow x \in \{N\})$
148	147	eqrdv	$⊢ φ \to {O (G)}^{-1} [\{\underset{˙}{0}\}] = \{N\}$
149	112 55 148	3jca	$⊢ φ \to (G \in U \land D (G) = 1 \land {O (G)}^{-1} [\{\underset{˙}{0}\}] = \{N\})$

Metamath Proof Explorer

Theorem ply1remlem

Proof