Metamath Proof Explorer

Theorem pl1cn

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

Ref Expression
Hypotheses pl1cn.p 
|- P = ( Poly1 ` R )
pl1cn.e 
|- E = ( eval1 ` R )
pl1cn.b 
|- B = ( Base ` P )
pl1cn.k 
|- K = ( Base ` R )
pl1cn.j 
|- J = ( TopOpen ` R )
pl1cn.1 
|- ( ph -> R e. CRing )
pl1cn.2 
|- ( ph -> R e. TopRing )
pl1cn.3 
|- ( ph -> F e. B )
Assertion pl1cn 
|- ( ph -> ( E ` F ) e. ( J Cn J ) )

Proof

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