Metamath Proof Explorer

Theorem pl1cn

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

Ref Expression
Hypotheses pl1cn.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
pl1cn.e ⊢ 𝐸 = ( eval1 ‘ 𝑅 )
pl1cn.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
pl1cn.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
pl1cn.j ⊢ 𝐽 = ( TopOpen ‘ 𝑅 )
pl1cn.1 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
pl1cn.2 ⊢ ( 𝜑 → 𝑅 ∈ TopRing )
pl1cn.3 ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
Assertion pl1cn ( 𝜑 → ( 𝐸 ‘ 𝐹 ) ∈ ( 𝐽 Cn 𝐽 ) )

Proof

Step Hyp Ref Expression
1 pl1cn.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 pl1cn.e ⊢ 𝐸 = ( eval1 ‘ 𝑅 )
3 pl1cn.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
4 pl1cn.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
5 pl1cn.j ⊢ 𝐽 = ( TopOpen ‘ 𝑅 )
6 pl1cn.1 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
7 pl1cn.2 ⊢ ( 𝜑 → 𝑅 ∈ TopRing )
8 pl1cn.3 ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
9 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
10 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
11 eqid ⊢ ran ( eval1 ‘ 𝑅 ) = ran ( eval1 ‘ 𝑅 )
12 4 fvexi ⊢ 𝐾 ∈ V
13 12 a1i ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐽 Cn 𝐽 ) ∧ 𝑔 ∈ ( 𝐽 Cn 𝐽 ) ) → 𝐾 ∈ V )
14 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐽 Cn 𝐽 ) ∧ 𝑔 ∈ ( 𝐽 Cn 𝐽 ) ) ∧ 𝑥 ∈ 𝐾 ) → ( 𝑓 ‘ 𝑥 ) ∈ V )
15 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐽 Cn 𝐽 ) ∧ 𝑔 ∈ ( 𝐽 Cn 𝐽 ) ) ∧ 𝑥 ∈ 𝐾 ) → ( 𝑔 ‘ 𝑥 ) ∈ V )
16 simp1 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐽 Cn 𝐽 ) ∧ 𝑔 ∈ ( 𝐽 Cn 𝐽 ) ) → 𝜑 )
17 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
18 17 17 cnf ⊢ ( 𝑓 ∈ ( 𝐽 Cn 𝐽 ) → 𝑓 : ∪ 𝐽 ⟶ ∪ 𝐽 )
19 18 ffnd ⊢ ( 𝑓 ∈ ( 𝐽 Cn 𝐽 ) → 𝑓 Fn ∪ 𝐽 )
20 19 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐽 Cn 𝐽 ) ∧ 𝑔 ∈ ( 𝐽 Cn 𝐽 ) ) → 𝑓 Fn ∪ 𝐽 )
21 trgtgp ⊢ ( 𝑅 ∈ TopRing → 𝑅 ∈ TopGrp )
22 5 4 tgptopon ⊢ ( 𝑅 ∈ TopGrp → 𝐽 ∈ ( TopOn ‘ 𝐾 ) )
23 7 21 22 3syl ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝐾 ) )
24 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐾 ) → 𝐾 = ∪ 𝐽 )
25 23 24 syl ⊢ ( 𝜑 → 𝐾 = ∪ 𝐽 )
26 25 fneq2d ⊢ ( 𝜑 → ( 𝑓 Fn 𝐾 ↔ 𝑓 Fn ∪ 𝐽 ) )
27 dffn5 ⊢ ( 𝑓 Fn 𝐾 ↔ 𝑓 = ( 𝑥 ∈ 𝐾 ↦ ( 𝑓 ‘ 𝑥 ) ) )
28 26 27 bitr3di ⊢ ( 𝜑 → ( 𝑓 Fn ∪ 𝐽 ↔ 𝑓 = ( 𝑥 ∈ 𝐾 ↦ ( 𝑓 ‘ 𝑥 ) ) ) )
29 28 biimpa ⊢ ( ( 𝜑 ∧ 𝑓 Fn ∪ 𝐽 ) → 𝑓 = ( 𝑥 ∈ 𝐾 ↦ ( 𝑓 ‘ 𝑥 ) ) )
30 16 20 29 syl2anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐽 Cn 𝐽 ) ∧ 𝑔 ∈ ( 𝐽 Cn 𝐽 ) ) → 𝑓 = ( 𝑥 ∈ 𝐾 ↦ ( 𝑓 ‘ 𝑥 ) ) )
31 17 17 cnf ⊢ ( 𝑔 ∈ ( 𝐽 Cn 𝐽 ) → 𝑔 : ∪ 𝐽 ⟶ ∪ 𝐽 )
32 31 ffnd ⊢ ( 𝑔 ∈ ( 𝐽 Cn 𝐽 ) → 𝑔 Fn ∪ 𝐽 )
33 32 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐽 Cn 𝐽 ) ∧ 𝑔 ∈ ( 𝐽 Cn 𝐽 ) ) → 𝑔 Fn ∪ 𝐽 )
34 25 fneq2d ⊢ ( 𝜑 → ( 𝑔 Fn 𝐾 ↔ 𝑔 Fn ∪ 𝐽 ) )
35 dffn5 ⊢ ( 𝑔 Fn 𝐾 ↔ 𝑔 = ( 𝑥 ∈ 𝐾 ↦ ( 𝑔 ‘ 𝑥 ) ) )
36 34 35 bitr3di ⊢ ( 𝜑 → ( 𝑔 Fn ∪ 𝐽 ↔ 𝑔 = ( 𝑥 ∈ 𝐾 ↦ ( 𝑔 ‘ 𝑥 ) ) ) )
37 36 biimpa ⊢ ( ( 𝜑 ∧ 𝑔 Fn ∪ 𝐽 ) → 𝑔 = ( 𝑥 ∈ 𝐾 ↦ ( 𝑔 ‘ 𝑥 ) ) )
38 16 33 37 syl2anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐽 Cn 𝐽 ) ∧ 𝑔 ∈ ( 𝐽 Cn 𝐽 ) ) → 𝑔 = ( 𝑥 ∈ 𝐾 ↦ ( 𝑔 ‘ 𝑥 ) ) )
39 13 14 15 30 38 offval2 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐽 Cn 𝐽 ) ∧ 𝑔 ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑓 ∘f ( +g ‘ 𝑅 ) 𝑔 ) = ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( 𝑔 ‘ 𝑥 ) ) ) )
40 23 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐽 Cn 𝐽 ) ∧ 𝑔 ∈ ( 𝐽 Cn 𝐽 ) ) → 𝐽 ∈ ( TopOn ‘ 𝐾 ) )
41 simp2 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐽 Cn 𝐽 ) ∧ 𝑔 ∈ ( 𝐽 Cn 𝐽 ) ) → 𝑓 ∈ ( 𝐽 Cn 𝐽 ) )
42 30 41 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐽 Cn 𝐽 ) ∧ 𝑔 ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑥 ∈ 𝐾 ↦ ( 𝑓 ‘ 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
43 simp3 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐽 Cn 𝐽 ) ∧ 𝑔 ∈ ( 𝐽 Cn 𝐽 ) ) → 𝑔 ∈ ( 𝐽 Cn 𝐽 ) )
44 38 43 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐽 Cn 𝐽 ) ∧ 𝑔 ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑥 ∈ 𝐾 ↦ ( 𝑔 ‘ 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
45 eqid ⊢ ( +𝑓 ‘ 𝑅 ) = ( +𝑓 ‘ 𝑅 )
46 4 9 45 plusffval ⊢ ( +𝑓 ‘ 𝑅 ) = ( 𝑦 ∈ 𝐾 , 𝑧 ∈ 𝐾 ↦ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) )
47 5 45 tgpcn ⊢ ( 𝑅 ∈ TopGrp → ( +𝑓 ‘ 𝑅 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
48 7 21 47 3syl ⊢ ( 𝜑 → ( +𝑓 ‘ 𝑅 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
49 46 48 eqeltrrid ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐾 , 𝑧 ∈ 𝐾 ↦ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
50 49 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐽 Cn 𝐽 ) ∧ 𝑔 ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑦 ∈ 𝐾 , 𝑧 ∈ 𝐾 ↦ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
51 oveq12 ⊢ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) ∧ 𝑧 = ( 𝑔 ‘ 𝑥 ) ) → ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( 𝑔 ‘ 𝑥 ) ) )
52 40 42 44 40 40 50 51 cnmpt12 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐽 Cn 𝐽 ) ∧ 𝑔 ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( 𝑔 ‘ 𝑥 ) ) ) ∈ ( 𝐽 Cn 𝐽 ) )
53 39 52 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐽 Cn 𝐽 ) ∧ 𝑔 ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑓 ∘f ( +g ‘ 𝑅 ) 𝑔 ) ∈ ( 𝐽 Cn 𝐽 ) )
54 53 3adant2l ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ran ( eval1 ‘ 𝑅 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐽 ) ) ∧ 𝑔 ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑓 ∘f ( +g ‘ 𝑅 ) 𝑔 ) ∈ ( 𝐽 Cn 𝐽 ) )
55 54 3adant3l ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ran ( eval1 ‘ 𝑅 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐽 ) ) ∧ ( 𝑔 ∈ ran ( eval1 ‘ 𝑅 ) ∧ 𝑔 ∈ ( 𝐽 Cn 𝐽 ) ) ) → ( 𝑓 ∘f ( +g ‘ 𝑅 ) 𝑔 ) ∈ ( 𝐽 Cn 𝐽 ) )
56 55 3expb ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ ran ( eval1 ‘ 𝑅 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐽 ) ) ∧ ( 𝑔 ∈ ran ( eval1 ‘ 𝑅 ) ∧ 𝑔 ∈ ( 𝐽 Cn 𝐽 ) ) ) ) → ( 𝑓 ∘f ( +g ‘ 𝑅 ) 𝑔 ) ∈ ( 𝐽 Cn 𝐽 ) )
57 13 14 15 30 38 offval2 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐽 Cn 𝐽 ) ∧ 𝑔 ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑓 ∘f ( .r ‘ 𝑅 ) 𝑔 ) = ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ 𝑥 ) ) ) )
58 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
59 58 4 mgpbas ⊢ 𝐾 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
60 58 10 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
61 eqid ⊢ ( +𝑓 ‘ ( mulGrp ‘ 𝑅 ) ) = ( +𝑓 ‘ ( mulGrp ‘ 𝑅 ) )
62 59 60 61 plusffval ⊢ ( +𝑓 ‘ ( mulGrp ‘ 𝑅 ) ) = ( 𝑦 ∈ 𝐾 , 𝑧 ∈ 𝐾 ↦ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) )
63 5 61 mulrcn ⊢ ( 𝑅 ∈ TopRing → ( +𝑓 ‘ ( mulGrp ‘ 𝑅 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
64 7 63 syl ⊢ ( 𝜑 → ( +𝑓 ‘ ( mulGrp ‘ 𝑅 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
65 62 64 eqeltrrid ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐾 , 𝑧 ∈ 𝐾 ↦ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
66 65 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐽 Cn 𝐽 ) ∧ 𝑔 ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑦 ∈ 𝐾 , 𝑧 ∈ 𝐾 ↦ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
67 oveq12 ⊢ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) ∧ 𝑧 = ( 𝑔 ‘ 𝑥 ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ 𝑥 ) ) )
68 40 42 44 40 40 66 67 cnmpt12 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐽 Cn 𝐽 ) ∧ 𝑔 ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ 𝑥 ) ) ) ∈ ( 𝐽 Cn 𝐽 ) )
69 57 68 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐽 Cn 𝐽 ) ∧ 𝑔 ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑓 ∘f ( .r ‘ 𝑅 ) 𝑔 ) ∈ ( 𝐽 Cn 𝐽 ) )
70 69 3adant2l ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ran ( eval1 ‘ 𝑅 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐽 ) ) ∧ 𝑔 ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑓 ∘f ( .r ‘ 𝑅 ) 𝑔 ) ∈ ( 𝐽 Cn 𝐽 ) )
71 70 3adant3l ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ran ( eval1 ‘ 𝑅 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐽 ) ) ∧ ( 𝑔 ∈ ran ( eval1 ‘ 𝑅 ) ∧ 𝑔 ∈ ( 𝐽 Cn 𝐽 ) ) ) → ( 𝑓 ∘f ( .r ‘ 𝑅 ) 𝑔 ) ∈ ( 𝐽 Cn 𝐽 ) )
72 71 3expb ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ ran ( eval1 ‘ 𝑅 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐽 ) ) ∧ ( 𝑔 ∈ ran ( eval1 ‘ 𝑅 ) ∧ 𝑔 ∈ ( 𝐽 Cn 𝐽 ) ) ) ) → ( 𝑓 ∘f ( .r ‘ 𝑅 ) 𝑔 ) ∈ ( 𝐽 Cn 𝐽 ) )
73 eleq1 ⊢ ( ℎ = ( 𝐾 × { 𝑓 } ) → ( ℎ ∈ ( 𝐽 Cn 𝐽 ) ↔ ( 𝐾 × { 𝑓 } ) ∈ ( 𝐽 Cn 𝐽 ) ) )
74 eleq1 ⊢ ( ℎ = ( I ↾ 𝐾 ) → ( ℎ ∈ ( 𝐽 Cn 𝐽 ) ↔ ( I ↾ 𝐾 ) ∈ ( 𝐽 Cn 𝐽 ) ) )
75 eleq1 ⊢ ( ℎ = 𝑓 → ( ℎ ∈ ( 𝐽 Cn 𝐽 ) ↔ 𝑓 ∈ ( 𝐽 Cn 𝐽 ) ) )
76 eleq1 ⊢ ( ℎ = 𝑔 → ( ℎ ∈ ( 𝐽 Cn 𝐽 ) ↔ 𝑔 ∈ ( 𝐽 Cn 𝐽 ) ) )
77 eleq1 ⊢ ( ℎ = ( 𝑓 ∘f ( +g ‘ 𝑅 ) 𝑔 ) → ( ℎ ∈ ( 𝐽 Cn 𝐽 ) ↔ ( 𝑓 ∘f ( +g ‘ 𝑅 ) 𝑔 ) ∈ ( 𝐽 Cn 𝐽 ) ) )
78 eleq1 ⊢ ( ℎ = ( 𝑓 ∘f ( .r ‘ 𝑅 ) 𝑔 ) → ( ℎ ∈ ( 𝐽 Cn 𝐽 ) ↔ ( 𝑓 ∘f ( .r ‘ 𝑅 ) 𝑔 ) ∈ ( 𝐽 Cn 𝐽 ) ) )
79 eleq1 ⊢ ( ℎ = ( 𝐸 ‘ 𝐹 ) → ( ℎ ∈ ( 𝐽 Cn 𝐽 ) ↔ ( 𝐸 ‘ 𝐹 ) ∈ ( 𝐽 Cn 𝐽 ) ) )
80 23 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐾 ) → 𝐽 ∈ ( TopOn ‘ 𝐾 ) )
81 simpr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐾 ) → 𝑓 ∈ 𝐾 )
82 cnconst2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝐾 ) ∧ 𝐽 ∈ ( TopOn ‘ 𝐾 ) ∧ 𝑓 ∈ 𝐾 ) → ( 𝐾 × { 𝑓 } ) ∈ ( 𝐽 Cn 𝐽 ) )
83 80 80 81 82 syl3anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐾 ) → ( 𝐾 × { 𝑓 } ) ∈ ( 𝐽 Cn 𝐽 ) )
84 idcn ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐾 ) → ( I ↾ 𝐾 ) ∈ ( 𝐽 Cn 𝐽 ) )
85 23 84 syl ⊢ ( 𝜑 → ( I ↾ 𝐾 ) ∈ ( 𝐽 Cn 𝐽 ) )
86 eqid ⊢ ( 𝑅 ↑s 𝐾 ) = ( 𝑅 ↑s 𝐾 )
87 2 1 86 4 evl1rhm ⊢ ( 𝑅 ∈ CRing → 𝐸 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐾 ) ) )
88 eqid ⊢ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) = ( Base ‘ ( 𝑅 ↑s 𝐾 ) )
89 3 88 rhmf ⊢ ( 𝐸 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐾 ) ) → 𝐸 : 𝐵 ⟶ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) )
90 ffn ⊢ ( 𝐸 : 𝐵 ⟶ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) → 𝐸 Fn 𝐵 )
91 dffn3 ⊢ ( 𝐸 Fn 𝐵 ↔ 𝐸 : 𝐵 ⟶ ran 𝐸 )
92 91 biimpi ⊢ ( 𝐸 Fn 𝐵 → 𝐸 : 𝐵 ⟶ ran 𝐸 )
93 87 89 90 92 4syl ⊢ ( 𝑅 ∈ CRing → 𝐸 : 𝐵 ⟶ ran 𝐸 )
94 6 93 syl ⊢ ( 𝜑 → 𝐸 : 𝐵 ⟶ ran 𝐸 )
95 94 8 ffvelcdmd ⊢ ( 𝜑 → ( 𝐸 ‘ 𝐹 ) ∈ ran 𝐸 )
96 2 rneqi ⊢ ran 𝐸 = ran ( eval1 ‘ 𝑅 )
97 95 96 eleqtrdi ⊢ ( 𝜑 → ( 𝐸 ‘ 𝐹 ) ∈ ran ( eval1 ‘ 𝑅 ) )
98 4 9 10 11 56 72 73 74 75 76 77 78 79 83 85 97 pf1ind ⊢ ( 𝜑 → ( 𝐸 ‘ 𝐹 ) ∈ ( 𝐽 Cn 𝐽 ) )