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