Step | Hyp | Ref
| Expression |
1 | | pl1cn.k |
. 2
⊢ 𝐾 = (Base‘𝑅) |
2 | | eqid 2610 |
. 2
⊢
(+g‘𝑅) = (+g‘𝑅) |
3 | | eqid 2610 |
. 2
⊢
(.r‘𝑅) = (.r‘𝑅) |
4 | | eqid 2610 |
. 2
⊢ ran
(eval1‘𝑅)
= ran (eval1‘𝑅) |
5 | | fvex 6113 |
. . . . . . . . 9
⊢
(Base‘𝑅)
∈ V |
6 | 1, 5 | eqeltri 2684 |
. . . . . . . 8
⊢ 𝐾 ∈ V |
7 | 6 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → 𝐾 ∈ V) |
8 | | fvex 6113 |
. . . . . . . 8
⊢ (𝑓‘𝑥) ∈ V |
9 | 8 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) ∧ 𝑥 ∈ 𝐾) → (𝑓‘𝑥) ∈ V) |
10 | | fvex 6113 |
. . . . . . . 8
⊢ (𝑔‘𝑥) ∈ V |
11 | 10 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) ∧ 𝑥 ∈ 𝐾) → (𝑔‘𝑥) ∈ V) |
12 | | simp1 1054 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → 𝜑) |
13 | | eqid 2610 |
. . . . . . . . . . 11
⊢ ∪ 𝐽 =
∪ 𝐽 |
14 | 13, 13 | cnf 20860 |
. . . . . . . . . 10
⊢ (𝑓 ∈ (𝐽 Cn 𝐽) → 𝑓:∪ 𝐽⟶∪ 𝐽) |
15 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝑓:∪
𝐽⟶∪ 𝐽
→ 𝑓 Fn ∪ 𝐽) |
16 | 14, 15 | syl 17 |
. . . . . . . . 9
⊢ (𝑓 ∈ (𝐽 Cn 𝐽) → 𝑓 Fn ∪ 𝐽) |
17 | 16 | 3ad2ant2 1076 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → 𝑓 Fn ∪ 𝐽) |
18 | | dffn5 6151 |
. . . . . . . . . 10
⊢ (𝑓 Fn 𝐾 ↔ 𝑓 = (𝑥 ∈ 𝐾 ↦ (𝑓‘𝑥))) |
19 | | pl1cn.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ∈ TopRing) |
20 | | trgtgp 21781 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ TopRing → 𝑅 ∈ TopGrp) |
21 | | pl1cn.j |
. . . . . . . . . . . . . 14
⊢ 𝐽 = (TopOpen‘𝑅) |
22 | 21, 1 | tgptopon 21696 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝐾)) |
23 | 19, 20, 22 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝐾)) |
24 | | toponuni 20542 |
. . . . . . . . . . . 12
⊢ (𝐽 ∈ (TopOn‘𝐾) → 𝐾 = ∪ 𝐽) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 = ∪ 𝐽) |
26 | 25 | fneq2d 5896 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑓 Fn 𝐾 ↔ 𝑓 Fn ∪ 𝐽)) |
27 | 18, 26 | syl5rbbr 274 |
. . . . . . . . 9
⊢ (𝜑 → (𝑓 Fn ∪ 𝐽 ↔ 𝑓 = (𝑥 ∈ 𝐾 ↦ (𝑓‘𝑥)))) |
28 | 27 | biimpa 500 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 Fn ∪ 𝐽) → 𝑓 = (𝑥 ∈ 𝐾 ↦ (𝑓‘𝑥))) |
29 | 12, 17, 28 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → 𝑓 = (𝑥 ∈ 𝐾 ↦ (𝑓‘𝑥))) |
30 | 13, 13 | cnf 20860 |
. . . . . . . . . 10
⊢ (𝑔 ∈ (𝐽 Cn 𝐽) → 𝑔:∪ 𝐽⟶∪ 𝐽) |
31 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝑔:∪
𝐽⟶∪ 𝐽
→ 𝑔 Fn ∪ 𝐽) |
32 | 30, 31 | syl 17 |
. . . . . . . . 9
⊢ (𝑔 ∈ (𝐽 Cn 𝐽) → 𝑔 Fn ∪ 𝐽) |
33 | 32 | 3ad2ant3 1077 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → 𝑔 Fn ∪ 𝐽) |
34 | | dffn5 6151 |
. . . . . . . . . 10
⊢ (𝑔 Fn 𝐾 ↔ 𝑔 = (𝑥 ∈ 𝐾 ↦ (𝑔‘𝑥))) |
35 | 25 | fneq2d 5896 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑔 Fn 𝐾 ↔ 𝑔 Fn ∪ 𝐽)) |
36 | 34, 35 | syl5rbbr 274 |
. . . . . . . . 9
⊢ (𝜑 → (𝑔 Fn ∪ 𝐽 ↔ 𝑔 = (𝑥 ∈ 𝐾 ↦ (𝑔‘𝑥)))) |
37 | 36 | biimpa 500 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 Fn ∪ 𝐽) → 𝑔 = (𝑥 ∈ 𝐾 ↦ (𝑔‘𝑥))) |
38 | 12, 33, 37 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → 𝑔 = (𝑥 ∈ 𝐾 ↦ (𝑔‘𝑥))) |
39 | 7, 9, 11, 29, 38 | offval2 6812 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → (𝑓 ∘𝑓
(+g‘𝑅)𝑔) = (𝑥 ∈ 𝐾 ↦ ((𝑓‘𝑥)(+g‘𝑅)(𝑔‘𝑥)))) |
40 | 23 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → 𝐽 ∈ (TopOn‘𝐾)) |
41 | | simp2 1055 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → 𝑓 ∈ (𝐽 Cn 𝐽)) |
42 | 29, 41 | eqeltrrd 2689 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → (𝑥 ∈ 𝐾 ↦ (𝑓‘𝑥)) ∈ (𝐽 Cn 𝐽)) |
43 | | simp3 1056 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → 𝑔 ∈ (𝐽 Cn 𝐽)) |
44 | 38, 43 | eqeltrrd 2689 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → (𝑥 ∈ 𝐾 ↦ (𝑔‘𝑥)) ∈ (𝐽 Cn 𝐽)) |
45 | | eqid 2610 |
. . . . . . . . . 10
⊢
(+𝑓‘𝑅) = (+𝑓‘𝑅) |
46 | 1, 2, 45 | plusffval 17070 |
. . . . . . . . 9
⊢
(+𝑓‘𝑅) = (𝑦 ∈ 𝐾, 𝑧 ∈ 𝐾 ↦ (𝑦(+g‘𝑅)𝑧)) |
47 | 21, 45 | tgpcn 21698 |
. . . . . . . . . 10
⊢ (𝑅 ∈ TopGrp →
(+𝑓‘𝑅) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
48 | 19, 20, 47 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 →
(+𝑓‘𝑅) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
49 | 46, 48 | syl5eqelr 2693 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ 𝐾, 𝑧 ∈ 𝐾 ↦ (𝑦(+g‘𝑅)𝑧)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
50 | 49 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → (𝑦 ∈ 𝐾, 𝑧 ∈ 𝐾 ↦ (𝑦(+g‘𝑅)𝑧)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
51 | | oveq12 6558 |
. . . . . . 7
⊢ ((𝑦 = (𝑓‘𝑥) ∧ 𝑧 = (𝑔‘𝑥)) → (𝑦(+g‘𝑅)𝑧) = ((𝑓‘𝑥)(+g‘𝑅)(𝑔‘𝑥))) |
52 | 40, 42, 44, 40, 40, 50, 51 | cnmpt12 21280 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → (𝑥 ∈ 𝐾 ↦ ((𝑓‘𝑥)(+g‘𝑅)(𝑔‘𝑥))) ∈ (𝐽 Cn 𝐽)) |
53 | 39, 52 | eqeltrd 2688 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → (𝑓 ∘𝑓
(+g‘𝑅)𝑔) ∈ (𝐽 Cn 𝐽)) |
54 | 53 | 3adant2l 1312 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ ran (eval1‘𝑅) ∧ 𝑓 ∈ (𝐽 Cn 𝐽)) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → (𝑓 ∘𝑓
(+g‘𝑅)𝑔) ∈ (𝐽 Cn 𝐽)) |
55 | 54 | 3adant3l 1314 |
. . 3
⊢ ((𝜑 ∧ (𝑓 ∈ ran (eval1‘𝑅) ∧ 𝑓 ∈ (𝐽 Cn 𝐽)) ∧ (𝑔 ∈ ran (eval1‘𝑅) ∧ 𝑔 ∈ (𝐽 Cn 𝐽))) → (𝑓 ∘𝑓
(+g‘𝑅)𝑔) ∈ (𝐽 Cn 𝐽)) |
56 | 55 | 3expb 1258 |
. 2
⊢ ((𝜑 ∧ ((𝑓 ∈ ran (eval1‘𝑅) ∧ 𝑓 ∈ (𝐽 Cn 𝐽)) ∧ (𝑔 ∈ ran (eval1‘𝑅) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)))) → (𝑓 ∘𝑓
(+g‘𝑅)𝑔) ∈ (𝐽 Cn 𝐽)) |
57 | 7, 9, 11, 29, 38 | offval2 6812 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → (𝑓 ∘𝑓
(.r‘𝑅)𝑔) = (𝑥 ∈ 𝐾 ↦ ((𝑓‘𝑥)(.r‘𝑅)(𝑔‘𝑥)))) |
58 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
59 | 58, 1 | mgpbas 18318 |
. . . . . . . . . 10
⊢ 𝐾 =
(Base‘(mulGrp‘𝑅)) |
60 | 58, 3 | mgpplusg 18316 |
. . . . . . . . . 10
⊢
(.r‘𝑅) = (+g‘(mulGrp‘𝑅)) |
61 | | eqid 2610 |
. . . . . . . . . 10
⊢
(+𝑓‘(mulGrp‘𝑅)) =
(+𝑓‘(mulGrp‘𝑅)) |
62 | 59, 60, 61 | plusffval 17070 |
. . . . . . . . 9
⊢
(+𝑓‘(mulGrp‘𝑅)) = (𝑦 ∈ 𝐾, 𝑧 ∈ 𝐾 ↦ (𝑦(.r‘𝑅)𝑧)) |
63 | 21, 61 | mulrcn 21792 |
. . . . . . . . . 10
⊢ (𝑅 ∈ TopRing →
(+𝑓‘(mulGrp‘𝑅)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
64 | 19, 63 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 →
(+𝑓‘(mulGrp‘𝑅)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
65 | 62, 64 | syl5eqelr 2693 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ 𝐾, 𝑧 ∈ 𝐾 ↦ (𝑦(.r‘𝑅)𝑧)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
66 | 65 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → (𝑦 ∈ 𝐾, 𝑧 ∈ 𝐾 ↦ (𝑦(.r‘𝑅)𝑧)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
67 | | oveq12 6558 |
. . . . . . 7
⊢ ((𝑦 = (𝑓‘𝑥) ∧ 𝑧 = (𝑔‘𝑥)) → (𝑦(.r‘𝑅)𝑧) = ((𝑓‘𝑥)(.r‘𝑅)(𝑔‘𝑥))) |
68 | 40, 42, 44, 40, 40, 66, 67 | cnmpt12 21280 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → (𝑥 ∈ 𝐾 ↦ ((𝑓‘𝑥)(.r‘𝑅)(𝑔‘𝑥))) ∈ (𝐽 Cn 𝐽)) |
69 | 57, 68 | eqeltrd 2688 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → (𝑓 ∘𝑓
(.r‘𝑅)𝑔) ∈ (𝐽 Cn 𝐽)) |
70 | 69 | 3adant2l 1312 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ ran (eval1‘𝑅) ∧ 𝑓 ∈ (𝐽 Cn 𝐽)) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → (𝑓 ∘𝑓
(.r‘𝑅)𝑔) ∈ (𝐽 Cn 𝐽)) |
71 | 70 | 3adant3l 1314 |
. . 3
⊢ ((𝜑 ∧ (𝑓 ∈ ran (eval1‘𝑅) ∧ 𝑓 ∈ (𝐽 Cn 𝐽)) ∧ (𝑔 ∈ ran (eval1‘𝑅) ∧ 𝑔 ∈ (𝐽 Cn 𝐽))) → (𝑓 ∘𝑓
(.r‘𝑅)𝑔) ∈ (𝐽 Cn 𝐽)) |
72 | 71 | 3expb 1258 |
. 2
⊢ ((𝜑 ∧ ((𝑓 ∈ ran (eval1‘𝑅) ∧ 𝑓 ∈ (𝐽 Cn 𝐽)) ∧ (𝑔 ∈ ran (eval1‘𝑅) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)))) → (𝑓 ∘𝑓
(.r‘𝑅)𝑔) ∈ (𝐽 Cn 𝐽)) |
73 | | eleq1 2676 |
. 2
⊢ (ℎ = (𝐾 × {𝑓}) → (ℎ ∈ (𝐽 Cn 𝐽) ↔ (𝐾 × {𝑓}) ∈ (𝐽 Cn 𝐽))) |
74 | | eleq1 2676 |
. 2
⊢ (ℎ = ( I ↾ 𝐾) → (ℎ ∈ (𝐽 Cn 𝐽) ↔ ( I ↾ 𝐾) ∈ (𝐽 Cn 𝐽))) |
75 | | eleq1 2676 |
. 2
⊢ (ℎ = 𝑓 → (ℎ ∈ (𝐽 Cn 𝐽) ↔ 𝑓 ∈ (𝐽 Cn 𝐽))) |
76 | | eleq1 2676 |
. 2
⊢ (ℎ = 𝑔 → (ℎ ∈ (𝐽 Cn 𝐽) ↔ 𝑔 ∈ (𝐽 Cn 𝐽))) |
77 | | eleq1 2676 |
. 2
⊢ (ℎ = (𝑓 ∘𝑓
(+g‘𝑅)𝑔) → (ℎ ∈ (𝐽 Cn 𝐽) ↔ (𝑓 ∘𝑓
(+g‘𝑅)𝑔) ∈ (𝐽 Cn 𝐽))) |
78 | | eleq1 2676 |
. 2
⊢ (ℎ = (𝑓 ∘𝑓
(.r‘𝑅)𝑔) → (ℎ ∈ (𝐽 Cn 𝐽) ↔ (𝑓 ∘𝑓
(.r‘𝑅)𝑔) ∈ (𝐽 Cn 𝐽))) |
79 | | eleq1 2676 |
. 2
⊢ (ℎ = (𝐸‘𝐹) → (ℎ ∈ (𝐽 Cn 𝐽) ↔ (𝐸‘𝐹) ∈ (𝐽 Cn 𝐽))) |
80 | 23 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐾) → 𝐽 ∈ (TopOn‘𝐾)) |
81 | | simpr 476 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐾) → 𝑓 ∈ 𝐾) |
82 | | cnconst2 20897 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝐾) ∧ 𝐽 ∈ (TopOn‘𝐾) ∧ 𝑓 ∈ 𝐾) → (𝐾 × {𝑓}) ∈ (𝐽 Cn 𝐽)) |
83 | 80, 80, 81, 82 | syl3anc 1318 |
. 2
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐾) → (𝐾 × {𝑓}) ∈ (𝐽 Cn 𝐽)) |
84 | | idcn 20871 |
. . 3
⊢ (𝐽 ∈ (TopOn‘𝐾) → ( I ↾ 𝐾) ∈ (𝐽 Cn 𝐽)) |
85 | 23, 84 | syl 17 |
. 2
⊢ (𝜑 → ( I ↾ 𝐾) ∈ (𝐽 Cn 𝐽)) |
86 | | pl1cn.1 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ CRing) |
87 | | pl1cn.e |
. . . . . . 7
⊢ 𝐸 = (eval1‘𝑅) |
88 | | pl1cn.p |
. . . . . . 7
⊢ 𝑃 = (Poly1‘𝑅) |
89 | | eqid 2610 |
. . . . . . 7
⊢ (𝑅 ↑s 𝐾) = (𝑅 ↑s 𝐾) |
90 | 87, 88, 89, 1 | evl1rhm 19517 |
. . . . . 6
⊢ (𝑅 ∈ CRing → 𝐸 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾))) |
91 | | pl1cn.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑃) |
92 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘(𝑅
↑s 𝐾)) = (Base‘(𝑅 ↑s 𝐾)) |
93 | 91, 92 | rhmf 18549 |
. . . . . 6
⊢ (𝐸 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾)) → 𝐸:𝐵⟶(Base‘(𝑅 ↑s 𝐾))) |
94 | | ffn 5958 |
. . . . . 6
⊢ (𝐸:𝐵⟶(Base‘(𝑅 ↑s 𝐾)) → 𝐸 Fn 𝐵) |
95 | | dffn3 5967 |
. . . . . . 7
⊢ (𝐸 Fn 𝐵 ↔ 𝐸:𝐵⟶ran 𝐸) |
96 | 95 | biimpi 205 |
. . . . . 6
⊢ (𝐸 Fn 𝐵 → 𝐸:𝐵⟶ran 𝐸) |
97 | 90, 93, 94, 96 | 4syl 19 |
. . . . 5
⊢ (𝑅 ∈ CRing → 𝐸:𝐵⟶ran 𝐸) |
98 | 86, 97 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐸:𝐵⟶ran 𝐸) |
99 | | pl1cn.3 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ 𝐵) |
100 | 98, 99 | ffvelrnd 6268 |
. . 3
⊢ (𝜑 → (𝐸‘𝐹) ∈ ran 𝐸) |
101 | 87 | rneqi 5273 |
. . 3
⊢ ran 𝐸 = ran
(eval1‘𝑅) |
102 | 100, 101 | syl6eleq 2698 |
. 2
⊢ (𝜑 → (𝐸‘𝐹) ∈ ran (eval1‘𝑅)) |
103 | 1, 2, 3, 4, 56, 72, 73, 74, 75, 76, 77, 78, 79, 83, 85, 102 | pf1ind 19540 |
1
⊢ (𝜑 → (𝐸‘𝐹) ∈ (𝐽 Cn 𝐽)) |