Step | Hyp | Ref
| Expression |
1 | | pf1rcl.q |
. . 3
⊢ 𝑄 = ran
(eval1‘𝑅) |
2 | 1 | pf1rcl 21515 |
. 2
⊢ (𝐹 ∈ 𝑄 → 𝑅 ∈ CRing) |
3 | | id 22 |
. . . 4
⊢ (𝐹 ∈ 𝑄 → 𝐹 ∈ 𝑄) |
4 | 3, 1 | eleqtrdi 2849 |
. . 3
⊢ (𝐹 ∈ 𝑄 → 𝐹 ∈ ran (eval1‘𝑅)) |
5 | | eqid 2738 |
. . . . . 6
⊢
(eval1‘𝑅) = (eval1‘𝑅) |
6 | | eqid 2738 |
. . . . . 6
⊢
(Poly1‘𝑅) = (Poly1‘𝑅) |
7 | | eqid 2738 |
. . . . . 6
⊢ (𝑅 ↑s 𝐵) = (𝑅 ↑s 𝐵) |
8 | | pf1f.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
9 | 5, 6, 7, 8 | evl1rhm 21498 |
. . . . 5
⊢ (𝑅 ∈ CRing →
(eval1‘𝑅)
∈ ((Poly1‘𝑅) RingHom (𝑅 ↑s 𝐵))) |
10 | 2, 9 | syl 17 |
. . . 4
⊢ (𝐹 ∈ 𝑄 → (eval1‘𝑅) ∈
((Poly1‘𝑅)
RingHom (𝑅
↑s 𝐵))) |
11 | | eqid 2738 |
. . . . 5
⊢
(Base‘(Poly1‘𝑅)) =
(Base‘(Poly1‘𝑅)) |
12 | | eqid 2738 |
. . . . 5
⊢
(Base‘(𝑅
↑s 𝐵)) = (Base‘(𝑅 ↑s 𝐵)) |
13 | 11, 12 | rhmf 19970 |
. . . 4
⊢
((eval1‘𝑅) ∈ ((Poly1‘𝑅) RingHom (𝑅 ↑s 𝐵)) → (eval1‘𝑅):(Base‘(Poly1‘𝑅))⟶(Base‘(𝑅 ↑s 𝐵))) |
14 | | ffn 6600 |
. . . 4
⊢
((eval1‘𝑅):(Base‘(Poly1‘𝑅))⟶(Base‘(𝑅 ↑s 𝐵)) →
(eval1‘𝑅)
Fn (Base‘(Poly1‘𝑅))) |
15 | | fvelrnb 6830 |
. . . 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 231 |
. 2
⊢ (𝐹 ∈ 𝑄 → ∃𝑦 ∈
(Base‘(Poly1‘𝑅))((eval1‘𝑅)‘𝑦) = 𝐹) |
18 | | eqid 2738 |
. . . . . . . 8
⊢
(1o eval 𝑅) = (1o eval 𝑅) |
19 | | eqid 2738 |
. . . . . . . 8
⊢
(1o mPoly 𝑅) = (1o mPoly 𝑅) |
20 | | eqid 2738 |
. . . . . . . . 9
⊢
(PwSer1‘𝑅) = (PwSer1‘𝑅) |
21 | 6, 20, 11 | ply1bas 21366 |
. . . . . . . 8
⊢
(Base‘(Poly1‘𝑅)) = (Base‘(1o mPoly 𝑅)) |
22 | 5, 18, 8, 19, 21 | evl1val 21495 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → ((eval1‘𝑅)‘𝑦) = (((1o eval 𝑅)‘𝑦) ∘ (𝑧 ∈ 𝐵 ↦ (1o × {𝑧})))) |
23 | 22 | coeq1d 5770 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → (((eval1‘𝑅)‘𝑦) ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅))) =
((((1o eval 𝑅)‘𝑦) ∘ (𝑧 ∈ 𝐵 ↦ (1o × {𝑧}))) ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅)))) |
24 | | coass 6169 |
. . . . . . 7
⊢
((((1o eval 𝑅)‘𝑦) ∘ (𝑧 ∈ 𝐵 ↦ (1o × {𝑧}))) ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅))) =
(((1o eval 𝑅)‘𝑦) ∘ ((𝑧 ∈ 𝐵 ↦ (1o × {𝑧})) ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅)))) |
25 | | df1o2 8304 |
. . . . . . . . . . 11
⊢
1o = {∅} |
26 | 8 | fvexi 6788 |
. . . . . . . . . . 11
⊢ 𝐵 ∈ V |
27 | | 0ex 5231 |
. . . . . . . . . . 11
⊢ ∅
∈ V |
28 | | eqid 2738 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅)) = (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅)) |
29 | 25, 26, 27, 28 | mapsncnv 8681 |
. . . . . . . . . 10
⊢ ◡(𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅)) = (𝑧 ∈ 𝐵 ↦ (1o × {𝑧})) |
30 | 29 | coeq1i 5768 |
. . . . . . . . 9
⊢ (◡(𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅)) ∘
(𝑥 ∈ (𝐵 ↑m
1o) ↦ (𝑥‘∅))) = ((𝑧 ∈ 𝐵 ↦ (1o × {𝑧})) ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅))) |
31 | 25, 26, 27, 28 | mapsnf1o2 8682 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅)):(𝐵 ↑m
1o)–1-1-onto→𝐵 |
32 | | f1ococnv1 6745 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅)):(𝐵 ↑m
1o)–1-1-onto→𝐵 → (◡(𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅)) ∘
(𝑥 ∈ (𝐵 ↑m
1o) ↦ (𝑥‘∅))) = ( I ↾ (𝐵 ↑m
1o))) |
33 | 31, 32 | mp1i 13 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → (◡(𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅)) ∘
(𝑥 ∈ (𝐵 ↑m
1o) ↦ (𝑥‘∅))) = ( I ↾ (𝐵 ↑m
1o))) |
34 | 30, 33 | eqtr3id 2792 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → ((𝑧 ∈ 𝐵 ↦ (1o × {𝑧})) ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅))) = ( I
↾ (𝐵
↑m 1o))) |
35 | 34 | coeq2d 5771 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → (((1o eval 𝑅)‘𝑦) ∘ ((𝑧 ∈ 𝐵 ↦ (1o × {𝑧})) ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅)))) =
(((1o eval 𝑅)‘𝑦) ∘ ( I ↾ (𝐵 ↑m
1o)))) |
36 | 24, 35 | eqtrid 2790 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → ((((1o eval 𝑅)‘𝑦) ∘ (𝑧 ∈ 𝐵 ↦ (1o × {𝑧}))) ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅))) =
(((1o eval 𝑅)‘𝑦) ∘ ( I ↾ (𝐵 ↑m
1o)))) |
37 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑅 ↑s
(𝐵 ↑m
1o)) = (𝑅
↑s (𝐵 ↑m
1o)) |
38 | | eqid 2738 |
. . . . . . . 8
⊢
(Base‘(𝑅
↑s (𝐵 ↑m 1o))) =
(Base‘(𝑅
↑s (𝐵 ↑m
1o))) |
39 | | simpl 483 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → 𝑅 ∈ CRing) |
40 | | ovexd 7310 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → (𝐵 ↑m 1o) ∈
V) |
41 | | 1on 8309 |
. . . . . . . . . . 11
⊢
1o ∈ On |
42 | 18, 8, 19, 37 | evlrhm 21306 |
. . . . . . . . . . 11
⊢
((1o ∈ On ∧ 𝑅 ∈ CRing) → (1o eval
𝑅) ∈ ((1o
mPoly 𝑅) RingHom (𝑅 ↑s
(𝐵 ↑m
1o)))) |
43 | 41, 42 | mpan 687 |
. . . . . . . . . 10
⊢ (𝑅 ∈ CRing →
(1o eval 𝑅)
∈ ((1o mPoly 𝑅) RingHom (𝑅 ↑s (𝐵 ↑m
1o)))) |
44 | 21, 38 | rhmf 19970 |
. . . . . . . . . 10
⊢
((1o eval 𝑅) ∈ ((1o mPoly 𝑅) RingHom (𝑅 ↑s (𝐵 ↑m
1o))) → (1o eval 𝑅):(Base‘(Poly1‘𝑅))⟶(Base‘(𝑅 ↑s
(𝐵 ↑m
1o)))) |
45 | 43, 44 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing →
(1o eval 𝑅):(Base‘(Poly1‘𝑅))⟶(Base‘(𝑅 ↑s
(𝐵 ↑m
1o)))) |
46 | 45 | ffvelrnda 6961 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → ((1o eval 𝑅)‘𝑦) ∈ (Base‘(𝑅 ↑s (𝐵 ↑m
1o)))) |
47 | 37, 8, 38, 39, 40, 46 | pwselbas 17200 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → ((1o eval 𝑅)‘𝑦):(𝐵 ↑m
1o)⟶𝐵) |
48 | | fcoi1 6648 |
. . . . . . 7
⊢
(((1o eval 𝑅)‘𝑦):(𝐵 ↑m
1o)⟶𝐵
→ (((1o eval 𝑅)‘𝑦) ∘ ( I ↾ (𝐵 ↑m 1o))) =
((1o eval 𝑅)‘𝑦)) |
49 | 47, 48 | syl 17 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → (((1o eval 𝑅)‘𝑦) ∘ ( I ↾ (𝐵 ↑m 1o))) =
((1o eval 𝑅)‘𝑦)) |
50 | 23, 36, 49 | 3eqtrd 2782 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → (((eval1‘𝑅)‘𝑦) ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅))) =
((1o eval 𝑅)‘𝑦)) |
51 | 45 | ffnd 6601 |
. . . . . . 7
⊢ (𝑅 ∈ CRing →
(1o eval 𝑅) Fn
(Base‘(Poly1‘𝑅))) |
52 | | fnfvelrn 6958 |
. . . . . . 7
⊢
(((1o eval 𝑅) Fn
(Base‘(Poly1‘𝑅)) ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → ((1o eval 𝑅)‘𝑦) ∈ ran (1o eval 𝑅)) |
53 | 51, 52 | sylan 580 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → ((1o eval 𝑅)‘𝑦) ∈ ran (1o eval 𝑅)) |
54 | | mpfpf1.q |
. . . . . 6
⊢ 𝐸 = ran (1o eval 𝑅) |
55 | 53, 54 | eleqtrrdi 2850 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → ((1o eval 𝑅)‘𝑦) ∈ 𝐸) |
56 | 50, 55 | eqeltrd 2839 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → (((eval1‘𝑅)‘𝑦) ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅))) ∈
𝐸) |
57 | | coeq1 5766 |
. . . . 5
⊢
(((eval1‘𝑅)‘𝑦) = 𝐹 → (((eval1‘𝑅)‘𝑦) ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅))) =
(𝐹 ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅)))) |
58 | 57 | eleq1d 2823 |
. . . 4
⊢
(((eval1‘𝑅)‘𝑦) = 𝐹 → ((((eval1‘𝑅)‘𝑦) ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅))) ∈
𝐸 ↔ (𝐹 ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅))) ∈
𝐸)) |
59 | 56, 58 | syl5ibcom 244 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → (((eval1‘𝑅)‘𝑦) = 𝐹 → (𝐹 ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅))) ∈
𝐸)) |
60 | 59 | rexlimdva 3213 |
. 2
⊢ (𝑅 ∈ CRing →
(∃𝑦 ∈
(Base‘(Poly1‘𝑅))((eval1‘𝑅)‘𝑦) = 𝐹 → (𝐹 ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅))) ∈
𝐸)) |
61 | 2, 17, 60 | sylc 65 |
1
⊢ (𝐹 ∈ 𝑄 → (𝐹 ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦
(𝑥‘∅))) ∈
𝐸) |