Step | Hyp | Ref
| Expression |
1 | | pl1cn.k |
. 2
⊢ 𝐾 = (Base‘𝑅) |
2 | | eqid 2622 |
. 2
⊢
(+g‘𝑅) = (+g‘𝑅) |
3 | | eqid 2622 |
. 2
⊢
(.r‘𝑅) = (.r‘𝑅) |
4 | | eqid 2622 |
. 2
⊢ ran
(eval1‘𝑅)
= ran (eval1‘𝑅) |
5 | | fvex 6201 |
. . . . . . . . 9
⊢
(Base‘𝑅)
∈ V |
6 | 1, 5 | eqeltri 2697 |
. . . . . . . 8
⊢ 𝐾 ∈ V |
7 | 6 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → 𝐾 ∈ V) |
8 | | fvexd 6203 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) ∧ 𝑥 ∈ 𝐾) → (𝑓‘𝑥) ∈ V) |
9 | | fvexd 6203 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) ∧ 𝑥 ∈ 𝐾) → (𝑔‘𝑥) ∈ V) |
10 | | simp1 1061 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → 𝜑) |
11 | | eqid 2622 |
. . . . . . . . . . 11
⊢ ∪ 𝐽 =
∪ 𝐽 |
12 | 11, 11 | cnf 21050 |
. . . . . . . . . 10
⊢ (𝑓 ∈ (𝐽 Cn 𝐽) → 𝑓:∪ 𝐽⟶∪ 𝐽) |
13 | | ffn 6045 |
. . . . . . . . . 10
⊢ (𝑓:∪
𝐽⟶∪ 𝐽
→ 𝑓 Fn ∪ 𝐽) |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
⊢ (𝑓 ∈ (𝐽 Cn 𝐽) → 𝑓 Fn ∪ 𝐽) |
15 | 14 | 3ad2ant2 1083 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → 𝑓 Fn ∪ 𝐽) |
16 | | dffn5 6241 |
. . . . . . . . . 10
⊢ (𝑓 Fn 𝐾 ↔ 𝑓 = (𝑥 ∈ 𝐾 ↦ (𝑓‘𝑥))) |
17 | | pl1cn.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ∈ TopRing) |
18 | | trgtgp 21971 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ TopRing → 𝑅 ∈ TopGrp) |
19 | | pl1cn.j |
. . . . . . . . . . . . . 14
⊢ 𝐽 = (TopOpen‘𝑅) |
20 | 19, 1 | tgptopon 21886 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝐾)) |
21 | 17, 18, 20 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝐾)) |
22 | | toponuni 20719 |
. . . . . . . . . . . 12
⊢ (𝐽 ∈ (TopOn‘𝐾) → 𝐾 = ∪ 𝐽) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 = ∪ 𝐽) |
24 | 23 | fneq2d 5982 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑓 Fn 𝐾 ↔ 𝑓 Fn ∪ 𝐽)) |
25 | 16, 24 | syl5rbbr 275 |
. . . . . . . . 9
⊢ (𝜑 → (𝑓 Fn ∪ 𝐽 ↔ 𝑓 = (𝑥 ∈ 𝐾 ↦ (𝑓‘𝑥)))) |
26 | 25 | biimpa 501 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 Fn ∪ 𝐽) → 𝑓 = (𝑥 ∈ 𝐾 ↦ (𝑓‘𝑥))) |
27 | 10, 15, 26 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → 𝑓 = (𝑥 ∈ 𝐾 ↦ (𝑓‘𝑥))) |
28 | 11, 11 | cnf 21050 |
. . . . . . . . . 10
⊢ (𝑔 ∈ (𝐽 Cn 𝐽) → 𝑔:∪ 𝐽⟶∪ 𝐽) |
29 | | ffn 6045 |
. . . . . . . . . 10
⊢ (𝑔:∪
𝐽⟶∪ 𝐽
→ 𝑔 Fn ∪ 𝐽) |
30 | 28, 29 | syl 17 |
. . . . . . . . 9
⊢ (𝑔 ∈ (𝐽 Cn 𝐽) → 𝑔 Fn ∪ 𝐽) |
31 | 30 | 3ad2ant3 1084 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → 𝑔 Fn ∪ 𝐽) |
32 | | dffn5 6241 |
. . . . . . . . . 10
⊢ (𝑔 Fn 𝐾 ↔ 𝑔 = (𝑥 ∈ 𝐾 ↦ (𝑔‘𝑥))) |
33 | 23 | fneq2d 5982 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑔 Fn 𝐾 ↔ 𝑔 Fn ∪ 𝐽)) |
34 | 32, 33 | syl5rbbr 275 |
. . . . . . . . 9
⊢ (𝜑 → (𝑔 Fn ∪ 𝐽 ↔ 𝑔 = (𝑥 ∈ 𝐾 ↦ (𝑔‘𝑥)))) |
35 | 34 | biimpa 501 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 Fn ∪ 𝐽) → 𝑔 = (𝑥 ∈ 𝐾 ↦ (𝑔‘𝑥))) |
36 | 10, 31, 35 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → 𝑔 = (𝑥 ∈ 𝐾 ↦ (𝑔‘𝑥))) |
37 | 7, 8, 9, 27, 36 | offval2 6914 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → (𝑓 ∘𝑓
(+g‘𝑅)𝑔) = (𝑥 ∈ 𝐾 ↦ ((𝑓‘𝑥)(+g‘𝑅)(𝑔‘𝑥)))) |
38 | 21 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → 𝐽 ∈ (TopOn‘𝐾)) |
39 | | simp2 1062 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → 𝑓 ∈ (𝐽 Cn 𝐽)) |
40 | 27, 39 | eqeltrrd 2702 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → (𝑥 ∈ 𝐾 ↦ (𝑓‘𝑥)) ∈ (𝐽 Cn 𝐽)) |
41 | | simp3 1063 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → 𝑔 ∈ (𝐽 Cn 𝐽)) |
42 | 36, 41 | eqeltrrd 2702 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → (𝑥 ∈ 𝐾 ↦ (𝑔‘𝑥)) ∈ (𝐽 Cn 𝐽)) |
43 | | eqid 2622 |
. . . . . . . . . 10
⊢
(+𝑓‘𝑅) = (+𝑓‘𝑅) |
44 | 1, 2, 43 | plusffval 17247 |
. . . . . . . . 9
⊢
(+𝑓‘𝑅) = (𝑦 ∈ 𝐾, 𝑧 ∈ 𝐾 ↦ (𝑦(+g‘𝑅)𝑧)) |
45 | 19, 43 | tgpcn 21888 |
. . . . . . . . . 10
⊢ (𝑅 ∈ TopGrp →
(+𝑓‘𝑅) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
46 | 17, 18, 45 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 →
(+𝑓‘𝑅) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
47 | 44, 46 | syl5eqelr 2706 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ 𝐾, 𝑧 ∈ 𝐾 ↦ (𝑦(+g‘𝑅)𝑧)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
48 | 47 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → (𝑦 ∈ 𝐾, 𝑧 ∈ 𝐾 ↦ (𝑦(+g‘𝑅)𝑧)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
49 | | oveq12 6659 |
. . . . . . 7
⊢ ((𝑦 = (𝑓‘𝑥) ∧ 𝑧 = (𝑔‘𝑥)) → (𝑦(+g‘𝑅)𝑧) = ((𝑓‘𝑥)(+g‘𝑅)(𝑔‘𝑥))) |
50 | 38, 40, 42, 38, 38, 48, 49 | cnmpt12 21470 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → (𝑥 ∈ 𝐾 ↦ ((𝑓‘𝑥)(+g‘𝑅)(𝑔‘𝑥))) ∈ (𝐽 Cn 𝐽)) |
51 | 37, 50 | eqeltrd 2701 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → (𝑓 ∘𝑓
(+g‘𝑅)𝑔) ∈ (𝐽 Cn 𝐽)) |
52 | 51 | 3adant2l 1320 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ ran (eval1‘𝑅) ∧ 𝑓 ∈ (𝐽 Cn 𝐽)) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → (𝑓 ∘𝑓
(+g‘𝑅)𝑔) ∈ (𝐽 Cn 𝐽)) |
53 | 52 | 3adant3l 1322 |
. . 3
⊢ ((𝜑 ∧ (𝑓 ∈ ran (eval1‘𝑅) ∧ 𝑓 ∈ (𝐽 Cn 𝐽)) ∧ (𝑔 ∈ ran (eval1‘𝑅) ∧ 𝑔 ∈ (𝐽 Cn 𝐽))) → (𝑓 ∘𝑓
(+g‘𝑅)𝑔) ∈ (𝐽 Cn 𝐽)) |
54 | 53 | 3expb 1266 |
. 2
⊢ ((𝜑 ∧ ((𝑓 ∈ ran (eval1‘𝑅) ∧ 𝑓 ∈ (𝐽 Cn 𝐽)) ∧ (𝑔 ∈ ran (eval1‘𝑅) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)))) → (𝑓 ∘𝑓
(+g‘𝑅)𝑔) ∈ (𝐽 Cn 𝐽)) |
55 | 7, 8, 9, 27, 36 | offval2 6914 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → (𝑓 ∘𝑓
(.r‘𝑅)𝑔) = (𝑥 ∈ 𝐾 ↦ ((𝑓‘𝑥)(.r‘𝑅)(𝑔‘𝑥)))) |
56 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
57 | 56, 1 | mgpbas 18495 |
. . . . . . . . . 10
⊢ 𝐾 =
(Base‘(mulGrp‘𝑅)) |
58 | 56, 3 | mgpplusg 18493 |
. . . . . . . . . 10
⊢
(.r‘𝑅) = (+g‘(mulGrp‘𝑅)) |
59 | | eqid 2622 |
. . . . . . . . . 10
⊢
(+𝑓‘(mulGrp‘𝑅)) =
(+𝑓‘(mulGrp‘𝑅)) |
60 | 57, 58, 59 | plusffval 17247 |
. . . . . . . . 9
⊢
(+𝑓‘(mulGrp‘𝑅)) = (𝑦 ∈ 𝐾, 𝑧 ∈ 𝐾 ↦ (𝑦(.r‘𝑅)𝑧)) |
61 | 19, 59 | mulrcn 21982 |
. . . . . . . . . 10
⊢ (𝑅 ∈ TopRing →
(+𝑓‘(mulGrp‘𝑅)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
62 | 17, 61 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 →
(+𝑓‘(mulGrp‘𝑅)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
63 | 60, 62 | syl5eqelr 2706 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ 𝐾, 𝑧 ∈ 𝐾 ↦ (𝑦(.r‘𝑅)𝑧)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
64 | 63 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → (𝑦 ∈ 𝐾, 𝑧 ∈ 𝐾 ↦ (𝑦(.r‘𝑅)𝑧)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
65 | | oveq12 6659 |
. . . . . . 7
⊢ ((𝑦 = (𝑓‘𝑥) ∧ 𝑧 = (𝑔‘𝑥)) → (𝑦(.r‘𝑅)𝑧) = ((𝑓‘𝑥)(.r‘𝑅)(𝑔‘𝑥))) |
66 | 38, 40, 42, 38, 38, 64, 65 | cnmpt12 21470 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → (𝑥 ∈ 𝐾 ↦ ((𝑓‘𝑥)(.r‘𝑅)(𝑔‘𝑥))) ∈ (𝐽 Cn 𝐽)) |
67 | 55, 66 | eqeltrd 2701 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐽 Cn 𝐽) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → (𝑓 ∘𝑓
(.r‘𝑅)𝑔) ∈ (𝐽 Cn 𝐽)) |
68 | 67 | 3adant2l 1320 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ ran (eval1‘𝑅) ∧ 𝑓 ∈ (𝐽 Cn 𝐽)) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)) → (𝑓 ∘𝑓
(.r‘𝑅)𝑔) ∈ (𝐽 Cn 𝐽)) |
69 | 68 | 3adant3l 1322 |
. . 3
⊢ ((𝜑 ∧ (𝑓 ∈ ran (eval1‘𝑅) ∧ 𝑓 ∈ (𝐽 Cn 𝐽)) ∧ (𝑔 ∈ ran (eval1‘𝑅) ∧ 𝑔 ∈ (𝐽 Cn 𝐽))) → (𝑓 ∘𝑓
(.r‘𝑅)𝑔) ∈ (𝐽 Cn 𝐽)) |
70 | 69 | 3expb 1266 |
. 2
⊢ ((𝜑 ∧ ((𝑓 ∈ ran (eval1‘𝑅) ∧ 𝑓 ∈ (𝐽 Cn 𝐽)) ∧ (𝑔 ∈ ran (eval1‘𝑅) ∧ 𝑔 ∈ (𝐽 Cn 𝐽)))) → (𝑓 ∘𝑓
(.r‘𝑅)𝑔) ∈ (𝐽 Cn 𝐽)) |
71 | | eleq1 2689 |
. 2
⊢ (ℎ = (𝐾 × {𝑓}) → (ℎ ∈ (𝐽 Cn 𝐽) ↔ (𝐾 × {𝑓}) ∈ (𝐽 Cn 𝐽))) |
72 | | eleq1 2689 |
. 2
⊢ (ℎ = ( I ↾ 𝐾) → (ℎ ∈ (𝐽 Cn 𝐽) ↔ ( I ↾ 𝐾) ∈ (𝐽 Cn 𝐽))) |
73 | | eleq1 2689 |
. 2
⊢ (ℎ = 𝑓 → (ℎ ∈ (𝐽 Cn 𝐽) ↔ 𝑓 ∈ (𝐽 Cn 𝐽))) |
74 | | eleq1 2689 |
. 2
⊢ (ℎ = 𝑔 → (ℎ ∈ (𝐽 Cn 𝐽) ↔ 𝑔 ∈ (𝐽 Cn 𝐽))) |
75 | | eleq1 2689 |
. 2
⊢ (ℎ = (𝑓 ∘𝑓
(+g‘𝑅)𝑔) → (ℎ ∈ (𝐽 Cn 𝐽) ↔ (𝑓 ∘𝑓
(+g‘𝑅)𝑔) ∈ (𝐽 Cn 𝐽))) |
76 | | eleq1 2689 |
. 2
⊢ (ℎ = (𝑓 ∘𝑓
(.r‘𝑅)𝑔) → (ℎ ∈ (𝐽 Cn 𝐽) ↔ (𝑓 ∘𝑓
(.r‘𝑅)𝑔) ∈ (𝐽 Cn 𝐽))) |
77 | | eleq1 2689 |
. 2
⊢ (ℎ = (𝐸‘𝐹) → (ℎ ∈ (𝐽 Cn 𝐽) ↔ (𝐸‘𝐹) ∈ (𝐽 Cn 𝐽))) |
78 | 21 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐾) → 𝐽 ∈ (TopOn‘𝐾)) |
79 | | simpr 477 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐾) → 𝑓 ∈ 𝐾) |
80 | | cnconst2 21087 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝐾) ∧ 𝐽 ∈ (TopOn‘𝐾) ∧ 𝑓 ∈ 𝐾) → (𝐾 × {𝑓}) ∈ (𝐽 Cn 𝐽)) |
81 | 78, 78, 79, 80 | syl3anc 1326 |
. 2
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐾) → (𝐾 × {𝑓}) ∈ (𝐽 Cn 𝐽)) |
82 | | idcn 21061 |
. . 3
⊢ (𝐽 ∈ (TopOn‘𝐾) → ( I ↾ 𝐾) ∈ (𝐽 Cn 𝐽)) |
83 | 21, 82 | syl 17 |
. 2
⊢ (𝜑 → ( I ↾ 𝐾) ∈ (𝐽 Cn 𝐽)) |
84 | | pl1cn.1 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ CRing) |
85 | | pl1cn.e |
. . . . . . 7
⊢ 𝐸 = (eval1‘𝑅) |
86 | | pl1cn.p |
. . . . . . 7
⊢ 𝑃 = (Poly1‘𝑅) |
87 | | eqid 2622 |
. . . . . . 7
⊢ (𝑅 ↑s 𝐾) = (𝑅 ↑s 𝐾) |
88 | 85, 86, 87, 1 | evl1rhm 19696 |
. . . . . 6
⊢ (𝑅 ∈ CRing → 𝐸 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾))) |
89 | | pl1cn.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑃) |
90 | | eqid 2622 |
. . . . . . 7
⊢
(Base‘(𝑅
↑s 𝐾)) = (Base‘(𝑅 ↑s 𝐾)) |
91 | 89, 90 | rhmf 18726 |
. . . . . 6
⊢ (𝐸 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾)) → 𝐸:𝐵⟶(Base‘(𝑅 ↑s 𝐾))) |
92 | | ffn 6045 |
. . . . . 6
⊢ (𝐸:𝐵⟶(Base‘(𝑅 ↑s 𝐾)) → 𝐸 Fn 𝐵) |
93 | | dffn3 6054 |
. . . . . . 7
⊢ (𝐸 Fn 𝐵 ↔ 𝐸:𝐵⟶ran 𝐸) |
94 | 93 | biimpi 206 |
. . . . . 6
⊢ (𝐸 Fn 𝐵 → 𝐸:𝐵⟶ran 𝐸) |
95 | 88, 91, 92, 94 | 4syl 19 |
. . . . 5
⊢ (𝑅 ∈ CRing → 𝐸:𝐵⟶ran 𝐸) |
96 | 84, 95 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐸:𝐵⟶ran 𝐸) |
97 | | pl1cn.3 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ 𝐵) |
98 | 96, 97 | ffvelrnd 6360 |
. . 3
⊢ (𝜑 → (𝐸‘𝐹) ∈ ran 𝐸) |
99 | 85 | rneqi 5352 |
. . 3
⊢ ran 𝐸 = ran
(eval1‘𝑅) |
100 | 98, 99 | syl6eleq 2711 |
. 2
⊢ (𝜑 → (𝐸‘𝐹) ∈ ran (eval1‘𝑅)) |
101 | 1, 2, 3, 4, 54, 70, 71, 72, 73, 74, 75, 76, 77, 81, 83, 100 | pf1ind 19719 |
1
⊢ (𝜑 → (𝐸‘𝐹) ∈ (𝐽 Cn 𝐽)) |