pl1cn

Description: A univariate polynomial is continuous. (Contributed by Thierry Arnoux, 17-Sep-2018)

	Ref	Expression
Hypotheses	pl1cn.p	$⊢ P = {Poly}_{1} (R)$
	pl1cn.e	$⊢ E = {eval}_{1} (R)$
	pl1cn.b	$⊢ B = {Base}_{P}$
	pl1cn.k	$⊢ K = {Base}_{R}$
	pl1cn.j	$⊢ J = TopOpen (R)$
	pl1cn.1	$⊢ φ \to R \in CRing$
	pl1cn.2	$⊢ φ \to R \in TopRing$
	pl1cn.3	$⊢ φ \to F \in B$
Assertion	pl1cn	$⊢ φ \to E (F) \in (J Cn J)$

Proof

Step	Hyp	Ref	Expression
1		pl1cn.p	$⊢ P = {Poly}_{1} (R)$
2		pl1cn.e	$⊢ E = {eval}_{1} (R)$
3		pl1cn.b	$⊢ B = {Base}_{P}$
4		pl1cn.k	$⊢ K = {Base}_{R}$
5		pl1cn.j	$⊢ J = TopOpen (R)$
6		pl1cn.1	$⊢ φ \to R \in CRing$
7		pl1cn.2	$⊢ φ \to R \in TopRing$
8		pl1cn.3	$⊢ φ \to F \in B$
9		eqid	$⊢ +_{R} = +_{R}$
10		eqid	$⊢ \cdot_{R} = \cdot_{R}$
11		eqid	$⊢ ran {eval}_{1} (R) = ran {eval}_{1} (R)$
12	4	fvexi	$⊢ K \in V$
13	12	a1i	$⊢ (φ \land f \in (J Cn J) \land g \in (J Cn J)) \to K \in V$
14		fvexd	$⊢ ((φ \land f \in (J Cn J) \land g \in (J Cn J)) \land x \in K) \to f (x) \in V$
15		fvexd	$⊢ ((φ \land f \in (J Cn J) \land g \in (J Cn J)) \land x \in K) \to g (x) \in V$
16		simp1	$⊢ (φ \land f \in (J Cn J) \land g \in (J Cn J)) \to φ$
17		eqid	$⊢ ⋃ J = ⋃ J$
18	17 17	cnf	$⊢ f \in (J Cn J) \to f : ⋃ J ⟶ ⋃ J$
19	18	ffnd	$⊢ f \in (J Cn J) \to f Fn ⋃ J$
20	19	3ad2ant2	$⊢ (φ \land f \in (J Cn J) \land g \in (J Cn J)) \to f Fn ⋃ J$
21		trgtgp	$⊢ R \in TopRing \to R \in TopGrp$
22	5 4	tgptopon	$⊢ R \in TopGrp \to J \in TopOn (K)$
23	7 21 22	3syl	$⊢ φ \to J \in TopOn (K)$
24		toponuni	$⊢ J \in TopOn (K) \to K = ⋃ J$
25	23 24	syl	$⊢ φ \to K = ⋃ J$
26	25	fneq2d	$⊢ φ \to (f Fn K \leftrightarrow f Fn ⋃ J)$
27		dffn5	$⊢ f Fn K \leftrightarrow f = (x \in K ⟼ f (x))$
28	26 27	bitr3di	$⊢ φ \to (f Fn ⋃ J \leftrightarrow f = (x \in K ⟼ f (x)))$
29	28	biimpa	$⊢ (φ \land f Fn ⋃ J) \to f = (x \in K ⟼ f (x))$
30	16 20 29	syl2anc	$⊢ (φ \land f \in (J Cn J) \land g \in (J Cn J)) \to f = (x \in K ⟼ f (x))$
31	17 17	cnf	$⊢ g \in (J Cn J) \to g : ⋃ J ⟶ ⋃ J$
32	31	ffnd	$⊢ g \in (J Cn J) \to g Fn ⋃ J$
33	32	3ad2ant3	$⊢ (φ \land f \in (J Cn J) \land g \in (J Cn J)) \to g Fn ⋃ J$
34	25	fneq2d	$⊢ φ \to (g Fn K \leftrightarrow g Fn ⋃ J)$
35		dffn5	$⊢ g Fn K \leftrightarrow g = (x \in K ⟼ g (x))$
36	34 35	bitr3di	$⊢ φ \to (g Fn ⋃ J \leftrightarrow g = (x \in K ⟼ g (x)))$
37	36	biimpa	$⊢ (φ \land g Fn ⋃ J) \to g = (x \in K ⟼ g (x))$
38	16 33 37	syl2anc	$⊢ (φ \land f \in (J Cn J) \land g \in (J Cn J)) \to g = (x \in K ⟼ g (x))$
39	13 14 15 30 38	offval2	$⊢ (φ \land f \in (J Cn J) \land g \in (J Cn J)) \to f {+_{R}}_{f} g = (x \in K ⟼ f (x) +_{R} g (x))$
40	23	3ad2ant1	$⊢ (φ \land f \in (J Cn J) \land g \in (J Cn J)) \to J \in TopOn (K)$
41		simp2	$⊢ (φ \land f \in (J Cn J) \land g \in (J Cn J)) \to f \in (J Cn J)$
42	30 41	eqeltrrd	$⊢ (φ \land f \in (J Cn J) \land g \in (J Cn J)) \to (x \in K ⟼ f (x)) \in (J Cn J)$
43		simp3	$⊢ (φ \land f \in (J Cn J) \land g \in (J Cn J)) \to g \in (J Cn J)$
44	38 43	eqeltrrd	$⊢ (φ \land f \in (J Cn J) \land g \in (J Cn J)) \to (x \in K ⟼ g (x)) \in (J Cn J)$
45		eqid	$⊢ +_{𝑓} (R) = +_{𝑓} (R)$
46	4 9 45	plusffval	$⊢ +_{𝑓} (R) = (y \in K, z \in K ⟼ y +_{R} z)$
47	5 45	tgpcn	$⊢ R \in TopGrp \to +_{𝑓} (R) \in ((J \times_{t} J) Cn J)$
48	7 21 47	3syl	$⊢ φ \to +_{𝑓} (R) \in ((J \times_{t} J) Cn J)$
49	46 48	eqeltrrid	$⊢ φ \to (y \in K, z \in K ⟼ y +_{R} z) \in ((J \times_{t} J) Cn J)$
50	49	3ad2ant1	$⊢ (φ \land f \in (J Cn J) \land g \in (J Cn J)) \to (y \in K, z \in K ⟼ y +_{R} z) \in ((J \times_{t} J) Cn J)$
51		oveq12	$⊢ (y = f (x) \land z = g (x)) \to y +_{R} z = f (x) +_{R} g (x)$
52	40 42 44 40 40 50 51	cnmpt12	$⊢ (φ \land f \in (J Cn J) \land g \in (J Cn J)) \to (x \in K ⟼ f (x) +_{R} g (x)) \in (J Cn J)$
53	39 52	eqeltrd	$⊢ (φ \land f \in (J Cn J) \land g \in (J Cn J)) \to f {+_{R}}_{f} g \in (J Cn J)$
54	53	3adant2l	$⊢ (φ \land (f \in ran {eval}_{1} (R) \land f \in (J Cn J)) \land g \in (J Cn J)) \to f {+_{R}}_{f} g \in (J Cn J)$
55	54	3adant3l	$⊢ (φ \land (f \in ran {eval}_{1} (R) \land f \in (J Cn J)) \land (g \in ran {eval}_{1} (R) \land g \in (J Cn J))) \to f {+_{R}}_{f} g \in (J Cn J)$
56	55	3expb	$⊢ (φ \land ((f \in ran {eval}_{1} (R) \land f \in (J Cn J)) \land (g \in ran {eval}_{1} (R) \land g \in (J Cn J)))) \to f {+_{R}}_{f} g \in (J Cn J)$
57	13 14 15 30 38	offval2	$⊢ (φ \land f \in (J Cn J) \land g \in (J Cn J)) \to f {\cdot_{R}}_{f} g = (x \in K ⟼ f (x) \cdot_{R} g (x))$
58		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
59	58 4	mgpbas	$⊢ K = {Base}_{{mulGrp}_{R}}$
60	58 10	mgpplusg	$⊢ \cdot_{R} = +_{{mulGrp}_{R}}$
61		eqid	$⊢ +_{𝑓} ({mulGrp}_{R}) = +_{𝑓} ({mulGrp}_{R})$
62	59 60 61	plusffval	$⊢ +_{𝑓} ({mulGrp}_{R}) = (y \in K, z \in K ⟼ y \cdot_{R} z)$
63	5 61	mulrcn	$⊢ R \in TopRing \to +_{𝑓} ({mulGrp}_{R}) \in ((J \times_{t} J) Cn J)$
64	7 63	syl	$⊢ φ \to +_{𝑓} ({mulGrp}_{R}) \in ((J \times_{t} J) Cn J)$
65	62 64	eqeltrrid	$⊢ φ \to (y \in K, z \in K ⟼ y \cdot_{R} z) \in ((J \times_{t} J) Cn J)$
66	65	3ad2ant1	$⊢ (φ \land f \in (J Cn J) \land g \in (J Cn J)) \to (y \in K, z \in K ⟼ y \cdot_{R} z) \in ((J \times_{t} J) Cn J)$
67		oveq12	$⊢ (y = f (x) \land z = g (x)) \to y \cdot_{R} z = f (x) \cdot_{R} g (x)$
68	40 42 44 40 40 66 67	cnmpt12	$⊢ (φ \land f \in (J Cn J) \land g \in (J Cn J)) \to (x \in K ⟼ f (x) \cdot_{R} g (x)) \in (J Cn J)$
69	57 68	eqeltrd	$⊢ (φ \land f \in (J Cn J) \land g \in (J Cn J)) \to f {\cdot_{R}}_{f} g \in (J Cn J)$
70	69	3adant2l	$⊢ (φ \land (f \in ran {eval}_{1} (R) \land f \in (J Cn J)) \land g \in (J Cn J)) \to f {\cdot_{R}}_{f} g \in (J Cn J)$
71	70	3adant3l	$⊢ (φ \land (f \in ran {eval}_{1} (R) \land f \in (J Cn J)) \land (g \in ran {eval}_{1} (R) \land g \in (J Cn J))) \to f {\cdot_{R}}_{f} g \in (J Cn J)$
72	71	3expb	$⊢ (φ \land ((f \in ran {eval}_{1} (R) \land f \in (J Cn J)) \land (g \in ran {eval}_{1} (R) \land g \in (J Cn J)))) \to f {\cdot_{R}}_{f} g \in (J Cn J)$
73		eleq1	$⊢ h = K \times \{f\} \to (h \in (J Cn J) \leftrightarrow K \times \{f\} \in (J Cn J))$
74		eleq1	$⊢ h = {I ↾}_{K} \to (h \in (J Cn J) \leftrightarrow {I ↾}_{K} \in (J Cn J))$
75		eleq1	$⊢ h = f \to (h \in (J Cn J) \leftrightarrow f \in (J Cn J))$
76		eleq1	$⊢ h = g \to (h \in (J Cn J) \leftrightarrow g \in (J Cn J))$
77		eleq1	$⊢ h = f {+_{R}}_{f} g \to (h \in (J Cn J) \leftrightarrow f {+_{R}}_{f} g \in (J Cn J))$
78		eleq1	$⊢ h = f {\cdot_{R}}_{f} g \to (h \in (J Cn J) \leftrightarrow f {\cdot_{R}}_{f} g \in (J Cn J))$
79		eleq1	$⊢ h = E (F) \to (h \in (J Cn J) \leftrightarrow E (F) \in (J Cn J))$
80	23	adantr	$⊢ (φ \land f \in K) \to J \in TopOn (K)$
81		simpr	$⊢ (φ \land f \in K) \to f \in K$
82		cnconst2	$⊢ (J \in TopOn (K) \land J \in TopOn (K) \land f \in K) \to K \times \{f\} \in (J Cn J)$
83	80 80 81 82	syl3anc	$⊢ (φ \land f \in K) \to K \times \{f\} \in (J Cn J)$
84		idcn	$⊢ J \in TopOn (K) \to {I ↾}_{K} \in (J Cn J)$
85	23 84	syl	$⊢ φ \to {I ↾}_{K} \in (J Cn J)$
86		eqid	$⊢ R ↑_{𝑠} K = R ↑_{𝑠} K$
87	2 1 86 4	evl1rhm	$⊢ R \in CRing \to E \in (P RingHom (R ↑_{𝑠} K))$
88		eqid	$⊢ {Base}_{(R ↑_{𝑠} K)} = {Base}_{(R ↑_{𝑠} K)}$
89	3 88	rhmf	$⊢ E \in (P RingHom (R ↑_{𝑠} K)) \to E : B ⟶ {Base}_{(R ↑_{𝑠} K)}$
90		ffn	$⊢ E : B ⟶ {Base}_{(R ↑_{𝑠} K)} \to E Fn B$
91		dffn3	$⊢ E Fn B \leftrightarrow E : B ⟶ ran E$
92	91	biimpi	$⊢ E Fn B \to E : B ⟶ ran E$
93	87 89 90 92	4syl	$⊢ R \in CRing \to E : B ⟶ ran E$
94	6 93	syl	$⊢ φ \to E : B ⟶ ran E$
95	94 8	ffvelcdmd	$⊢ φ \to E (F) \in ran E$
96	2	rneqi	$⊢ ran E = ran {eval}_{1} (R)$
97	95 96	eleqtrdi	$⊢ φ \to E (F) \in ran {eval}_{1} (R)$
98	4 9 10 11 56 72 73 74 75 76 77 78 79 83 85 97	pf1ind	$⊢ φ \to E (F) \in (J Cn J)$

Metamath Proof Explorer

Theorem pl1cn

Proof