| Step | Hyp | Ref
| Expression |
| 1 | | pf1rcl.q |
. . 3
⊢ 𝑄 = ran
(eval1‘𝑅) |
| 2 | 1 | pf1rcl 22353 |
. 2
⊢ (𝐹 ∈ 𝑄 → 𝑅 ∈ CRing) |
| 3 | | id 22 |
. . . 4
⊢ (𝐹 ∈ 𝑄 → 𝐹 ∈ 𝑄) |
| 4 | 3, 1 | eleqtrdi 2851 |
. . 3
⊢ (𝐹 ∈ 𝑄 → 𝐹 ∈ ran (eval1‘𝑅)) |
| 5 | | eqid 2737 |
. . . . . 6
⊢
(eval1‘𝑅) = (eval1‘𝑅) |
| 6 | | eqid 2737 |
. . . . . 6
⊢
(Poly1‘𝑅) = (Poly1‘𝑅) |
| 7 | | eqid 2737 |
. . . . . 6
⊢ (𝑅 ↑s 𝐵) = (𝑅 ↑s 𝐵) |
| 8 | | pf1f.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
| 9 | 5, 6, 7, 8 | evl1rhm 22336 |
. . . . 5
⊢ (𝑅 ∈ CRing →
(eval1‘𝑅)
∈ ((Poly1‘𝑅) RingHom (𝑅 ↑s 𝐵))) |
| 10 | 2, 9 | syl 17 |
. . . 4
⊢ (𝐹 ∈ 𝑄 → (eval1‘𝑅) ∈
((Poly1‘𝑅)
RingHom (𝑅
↑s 𝐵))) |
| 11 | | eqid 2737 |
. . . . 5
⊢
(Base‘(Poly1‘𝑅)) =
(Base‘(Poly1‘𝑅)) |
| 12 | | eqid 2737 |
. . . . 5
⊢
(Base‘(𝑅
↑s 𝐵)) = (Base‘(𝑅 ↑s 𝐵)) |
| 13 | 11, 12 | rhmf 20485 |
. . . 4
⊢
((eval1‘𝑅) ∈ ((Poly1‘𝑅) RingHom (𝑅 ↑s 𝐵)) → (eval1‘𝑅):(Base‘(Poly1‘𝑅))⟶(Base‘(𝑅 ↑s 𝐵))) |
| 14 | | ffn 6736 |
. . . 4
⊢
((eval1‘𝑅):(Base‘(Poly1‘𝑅))⟶(Base‘(𝑅 ↑s 𝐵)) →
(eval1‘𝑅)
Fn (Base‘(Poly1‘𝑅))) |
| 15 | | fvelrnb 6969 |
. . . 4
⊢
((eval1‘𝑅) Fn
(Base‘(Poly1‘𝑅)) → (𝐹 ∈ ran (eval1‘𝑅) ↔ ∃𝑦 ∈
(Base‘(Poly1‘𝑅))((eval1‘𝑅)‘𝑦) = 𝐹)) |
| 16 | 10, 13, 14, 15 | 4syl 19 |
. . 3
⊢ (𝐹 ∈ 𝑄 → (𝐹 ∈ ran (eval1‘𝑅) ↔ ∃𝑦 ∈
(Base‘(Poly1‘𝑅))((eval1‘𝑅)‘𝑦) = 𝐹)) |
| 17 | 4, 16 | mpbid 232 |
. 2
⊢ (𝐹 ∈ 𝑄 → ∃𝑦 ∈
(Base‘(Poly1‘𝑅))((eval1‘𝑅)‘𝑦) = 𝐹) |
| 18 | | eqid 2737 |
. . . . . . . 8
⊢
(1o eval 𝑅) = (1o eval 𝑅) |
| 19 | | eqid 2737 |
. . . . . . . 8
⊢
(1o mPoly 𝑅) = (1o mPoly 𝑅) |
| 20 | 6, 11 | ply1bas 22196 |
. . . . . . . 8
⊢
(Base‘(Poly1‘𝑅)) = (Base‘(1o mPoly 𝑅)) |
| 21 | 5, 18, 8, 19, 20 | evl1val 22333 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → ((eval1‘𝑅)‘𝑦) = (((1o eval 𝑅)‘𝑦) ∘ (𝑧 ∈ 𝐵 ↦ (1o × {𝑧})))) |
| 22 | 21 | coeq1d 5872 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → (((eval1‘𝑅)‘𝑦) ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅))) =
((((1o eval 𝑅)‘𝑦) ∘ (𝑧 ∈ 𝐵 ↦ (1o × {𝑧}))) ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅)))) |
| 23 | | coass 6285 |
. . . . . . 7
⊢
((((1o eval 𝑅)‘𝑦) ∘ (𝑧 ∈ 𝐵 ↦ (1o × {𝑧}))) ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅))) =
(((1o eval 𝑅)‘𝑦) ∘ ((𝑧 ∈ 𝐵 ↦ (1o × {𝑧})) ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅)))) |
| 24 | | df1o2 8513 |
. . . . . . . . . . 11
⊢
1o = {∅} |
| 25 | 8 | fvexi 6920 |
. . . . . . . . . . 11
⊢ 𝐵 ∈ V |
| 26 | | 0ex 5307 |
. . . . . . . . . . 11
⊢ ∅
∈ V |
| 27 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅)) = (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅)) |
| 28 | 24, 25, 26, 27 | mapsncnv 8933 |
. . . . . . . . . 10
⊢ ◡(𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅)) = (𝑧 ∈ 𝐵 ↦ (1o × {𝑧})) |
| 29 | 28 | coeq1i 5870 |
. . . . . . . . 9
⊢ (◡(𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅)) ∘
(𝑥 ∈ (𝐵 ↑m
1o) ↦ (𝑥‘∅))) = ((𝑧 ∈ 𝐵 ↦ (1o × {𝑧})) ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅))) |
| 30 | 24, 25, 26, 27 | mapsnf1o2 8934 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅)):(𝐵 ↑m
1o)–1-1-onto→𝐵 |
| 31 | | f1ococnv1 6877 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅)):(𝐵 ↑m
1o)–1-1-onto→𝐵 → (◡(𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅)) ∘
(𝑥 ∈ (𝐵 ↑m
1o) ↦ (𝑥‘∅))) = ( I ↾ (𝐵 ↑m
1o))) |
| 32 | 30, 31 | mp1i 13 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → (◡(𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅)) ∘
(𝑥 ∈ (𝐵 ↑m
1o) ↦ (𝑥‘∅))) = ( I ↾ (𝐵 ↑m
1o))) |
| 33 | 29, 32 | eqtr3id 2791 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → ((𝑧 ∈ 𝐵 ↦ (1o × {𝑧})) ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅))) = ( I
↾ (𝐵
↑m 1o))) |
| 34 | 33 | coeq2d 5873 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → (((1o eval 𝑅)‘𝑦) ∘ ((𝑧 ∈ 𝐵 ↦ (1o × {𝑧})) ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅)))) =
(((1o eval 𝑅)‘𝑦) ∘ ( I ↾ (𝐵 ↑m
1o)))) |
| 35 | 23, 34 | eqtrid 2789 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → ((((1o eval 𝑅)‘𝑦) ∘ (𝑧 ∈ 𝐵 ↦ (1o × {𝑧}))) ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅))) =
(((1o eval 𝑅)‘𝑦) ∘ ( I ↾ (𝐵 ↑m
1o)))) |
| 36 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑅 ↑s
(𝐵 ↑m
1o)) = (𝑅
↑s (𝐵 ↑m
1o)) |
| 37 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘(𝑅
↑s (𝐵 ↑m 1o))) =
(Base‘(𝑅
↑s (𝐵 ↑m
1o))) |
| 38 | | simpl 482 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → 𝑅 ∈ CRing) |
| 39 | | ovexd 7466 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → (𝐵 ↑m 1o) ∈
V) |
| 40 | | 1on 8518 |
. . . . . . . . . . 11
⊢
1o ∈ On |
| 41 | 18, 8, 19, 36 | evlrhm 22120 |
. . . . . . . . . . 11
⊢
((1o ∈ On ∧ 𝑅 ∈ CRing) → (1o eval
𝑅) ∈ ((1o
mPoly 𝑅) RingHom (𝑅 ↑s
(𝐵 ↑m
1o)))) |
| 42 | 40, 41 | mpan 690 |
. . . . . . . . . 10
⊢ (𝑅 ∈ CRing →
(1o eval 𝑅)
∈ ((1o mPoly 𝑅) RingHom (𝑅 ↑s (𝐵 ↑m
1o)))) |
| 43 | 20, 37 | rhmf 20485 |
. . . . . . . . . 10
⊢
((1o eval 𝑅) ∈ ((1o mPoly 𝑅) RingHom (𝑅 ↑s (𝐵 ↑m
1o))) → (1o eval 𝑅):(Base‘(Poly1‘𝑅))⟶(Base‘(𝑅 ↑s
(𝐵 ↑m
1o)))) |
| 44 | 42, 43 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing →
(1o eval 𝑅):(Base‘(Poly1‘𝑅))⟶(Base‘(𝑅 ↑s
(𝐵 ↑m
1o)))) |
| 45 | 44 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → ((1o eval 𝑅)‘𝑦) ∈ (Base‘(𝑅 ↑s (𝐵 ↑m
1o)))) |
| 46 | 36, 8, 37, 38, 39, 45 | pwselbas 17534 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → ((1o eval 𝑅)‘𝑦):(𝐵 ↑m
1o)⟶𝐵) |
| 47 | | fcoi1 6782 |
. . . . . . 7
⊢
(((1o eval 𝑅)‘𝑦):(𝐵 ↑m
1o)⟶𝐵
→ (((1o eval 𝑅)‘𝑦) ∘ ( I ↾ (𝐵 ↑m 1o))) =
((1o eval 𝑅)‘𝑦)) |
| 48 | 46, 47 | syl 17 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → (((1o eval 𝑅)‘𝑦) ∘ ( I ↾ (𝐵 ↑m 1o))) =
((1o eval 𝑅)‘𝑦)) |
| 49 | 22, 35, 48 | 3eqtrd 2781 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → (((eval1‘𝑅)‘𝑦) ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅))) =
((1o eval 𝑅)‘𝑦)) |
| 50 | 44 | ffnd 6737 |
. . . . . . 7
⊢ (𝑅 ∈ CRing →
(1o eval 𝑅) Fn
(Base‘(Poly1‘𝑅))) |
| 51 | | fnfvelrn 7100 |
. . . . . . 7
⊢
(((1o eval 𝑅) Fn
(Base‘(Poly1‘𝑅)) ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → ((1o eval 𝑅)‘𝑦) ∈ ran (1o eval 𝑅)) |
| 52 | 50, 51 | sylan 580 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → ((1o eval 𝑅)‘𝑦) ∈ ran (1o eval 𝑅)) |
| 53 | | mpfpf1.q |
. . . . . 6
⊢ 𝐸 = ran (1o eval 𝑅) |
| 54 | 52, 53 | eleqtrrdi 2852 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → ((1o eval 𝑅)‘𝑦) ∈ 𝐸) |
| 55 | 49, 54 | eqeltrd 2841 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → (((eval1‘𝑅)‘𝑦) ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅))) ∈
𝐸) |
| 56 | | coeq1 5868 |
. . . . 5
⊢
(((eval1‘𝑅)‘𝑦) = 𝐹 → (((eval1‘𝑅)‘𝑦) ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅))) =
(𝐹 ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅)))) |
| 57 | 56 | eleq1d 2826 |
. . . 4
⊢
(((eval1‘𝑅)‘𝑦) = 𝐹 → ((((eval1‘𝑅)‘𝑦) ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅))) ∈
𝐸 ↔ (𝐹 ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅))) ∈
𝐸)) |
| 58 | 55, 57 | syl5ibcom 245 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → (((eval1‘𝑅)‘𝑦) = 𝐹 → (𝐹 ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅))) ∈
𝐸)) |
| 59 | 58 | rexlimdva 3155 |
. 2
⊢ (𝑅 ∈ CRing →
(∃𝑦 ∈
(Base‘(Poly1‘𝑅))((eval1‘𝑅)‘𝑦) = 𝐹 → (𝐹 ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅))) ∈
𝐸)) |
| 60 | 2, 17, 59 | sylc 65 |
1
⊢ (𝐹 ∈ 𝑄 → (𝐹 ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅))) ∈
𝐸) |