Step | Hyp | Ref
| Expression |
1 | | pf1rcl.q |
. . 3
⊢ 𝑄 = ran
(eval1‘𝑅) |
2 | 1 | pf1rcl 19534 |
. 2
⊢ (𝐹 ∈ 𝑄 → 𝑅 ∈ CRing) |
3 | | id 22 |
. . . 4
⊢ (𝐹 ∈ 𝑄 → 𝐹 ∈ 𝑄) |
4 | 3, 1 | syl6eleq 2698 |
. . 3
⊢ (𝐹 ∈ 𝑄 → 𝐹 ∈ ran (eval1‘𝑅)) |
5 | | eqid 2610 |
. . . . . 6
⊢
(eval1‘𝑅) = (eval1‘𝑅) |
6 | | eqid 2610 |
. . . . . 6
⊢
(Poly1‘𝑅) = (Poly1‘𝑅) |
7 | | eqid 2610 |
. . . . . 6
⊢ (𝑅 ↑s 𝐵) = (𝑅 ↑s 𝐵) |
8 | | pf1f.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
9 | 5, 6, 7, 8 | evl1rhm 19517 |
. . . . 5
⊢ (𝑅 ∈ CRing →
(eval1‘𝑅)
∈ ((Poly1‘𝑅) RingHom (𝑅 ↑s 𝐵))) |
10 | 2, 9 | syl 17 |
. . . 4
⊢ (𝐹 ∈ 𝑄 → (eval1‘𝑅) ∈
((Poly1‘𝑅)
RingHom (𝑅
↑s 𝐵))) |
11 | | eqid 2610 |
. . . . 5
⊢
(Base‘(Poly1‘𝑅)) =
(Base‘(Poly1‘𝑅)) |
12 | | eqid 2610 |
. . . . 5
⊢
(Base‘(𝑅
↑s 𝐵)) = (Base‘(𝑅 ↑s 𝐵)) |
13 | 11, 12 | rhmf 18549 |
. . . 4
⊢
((eval1‘𝑅) ∈ ((Poly1‘𝑅) RingHom (𝑅 ↑s 𝐵)) → (eval1‘𝑅):(Base‘(Poly1‘𝑅))⟶(Base‘(𝑅 ↑s 𝐵))) |
14 | | ffn 5958 |
. . . 4
⊢
((eval1‘𝑅):(Base‘(Poly1‘𝑅))⟶(Base‘(𝑅 ↑s 𝐵)) →
(eval1‘𝑅)
Fn (Base‘(Poly1‘𝑅))) |
15 | | fvelrnb 6153 |
. . . 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 221 |
. 2
⊢ (𝐹 ∈ 𝑄 → ∃𝑦 ∈
(Base‘(Poly1‘𝑅))((eval1‘𝑅)‘𝑦) = 𝐹) |
18 | | eqid 2610 |
. . . . . . . 8
⊢
(1𝑜 eval 𝑅) = (1𝑜 eval 𝑅) |
19 | | eqid 2610 |
. . . . . . . 8
⊢
(1𝑜 mPoly 𝑅) = (1𝑜 mPoly 𝑅) |
20 | | eqid 2610 |
. . . . . . . . 9
⊢
(PwSer1‘𝑅) = (PwSer1‘𝑅) |
21 | 6, 20, 11 | ply1bas 19386 |
. . . . . . . 8
⊢
(Base‘(Poly1‘𝑅)) = (Base‘(1𝑜
mPoly 𝑅)) |
22 | 5, 18, 8, 19, 21 | evl1val 19514 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → ((eval1‘𝑅)‘𝑦) = (((1𝑜 eval 𝑅)‘𝑦) ∘ (𝑧 ∈ 𝐵 ↦ (1𝑜 ×
{𝑧})))) |
23 | 22 | coeq1d 5205 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → (((eval1‘𝑅)‘𝑦) ∘ (𝑥 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑥‘∅))) = ((((1𝑜
eval 𝑅)‘𝑦) ∘ (𝑧 ∈ 𝐵 ↦ (1𝑜 ×
{𝑧}))) ∘ (𝑥 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑥‘∅)))) |
24 | | coass 5571 |
. . . . . . 7
⊢
((((1𝑜 eval 𝑅)‘𝑦) ∘ (𝑧 ∈ 𝐵 ↦ (1𝑜 ×
{𝑧}))) ∘ (𝑥 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑥‘∅))) = (((1𝑜
eval 𝑅)‘𝑦) ∘ ((𝑧 ∈ 𝐵 ↦ (1𝑜 ×
{𝑧})) ∘ (𝑥 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑥‘∅)))) |
25 | | df1o2 7459 |
. . . . . . . . . . 11
⊢
1𝑜 = {∅} |
26 | | fvex 6113 |
. . . . . . . . . . . 12
⊢
(Base‘𝑅)
∈ V |
27 | 8, 26 | eqeltri 2684 |
. . . . . . . . . . 11
⊢ 𝐵 ∈ V |
28 | | 0ex 4718 |
. . . . . . . . . . 11
⊢ ∅
∈ V |
29 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑥‘∅)) = (𝑥 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑥‘∅)) |
30 | 25, 27, 28, 29 | mapsncnv 7790 |
. . . . . . . . . 10
⊢ ◡(𝑥 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑥‘∅)) = (𝑧 ∈ 𝐵 ↦ (1𝑜 ×
{𝑧})) |
31 | 30 | coeq1i 5203 |
. . . . . . . . 9
⊢ (◡(𝑥 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑥‘∅)) ∘ (𝑥 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑥‘∅))) = ((𝑧 ∈ 𝐵 ↦ (1𝑜 ×
{𝑧})) ∘ (𝑥 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑥‘∅))) |
32 | 25, 27, 28, 29 | mapsnf1o2 7791 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑥‘∅)):(𝐵 ↑𝑚
1𝑜)–1-1-onto→𝐵 |
33 | | f1ococnv1 6078 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑥‘∅)):(𝐵 ↑𝑚
1𝑜)–1-1-onto→𝐵 → (◡(𝑥 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑥‘∅)) ∘ (𝑥 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑥‘∅))) = ( I ↾ (𝐵 ↑𝑚
1𝑜))) |
34 | 32, 33 | mp1i 13 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → (◡(𝑥 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑥‘∅)) ∘ (𝑥 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑥‘∅))) = ( I ↾ (𝐵 ↑𝑚
1𝑜))) |
35 | 31, 34 | syl5eqr 2658 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → ((𝑧 ∈ 𝐵 ↦ (1𝑜 ×
{𝑧})) ∘ (𝑥 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑥‘∅))) = ( I ↾ (𝐵 ↑𝑚
1𝑜))) |
36 | 35 | coeq2d 5206 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → (((1𝑜 eval
𝑅)‘𝑦) ∘ ((𝑧 ∈ 𝐵 ↦ (1𝑜 ×
{𝑧})) ∘ (𝑥 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑥‘∅)))) = (((1𝑜
eval 𝑅)‘𝑦) ∘ ( I ↾ (𝐵 ↑𝑚
1𝑜)))) |
37 | 24, 36 | syl5eq 2656 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → ((((1𝑜 eval
𝑅)‘𝑦) ∘ (𝑧 ∈ 𝐵 ↦ (1𝑜 ×
{𝑧}))) ∘ (𝑥 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑥‘∅))) = (((1𝑜
eval 𝑅)‘𝑦) ∘ ( I ↾ (𝐵 ↑𝑚
1𝑜)))) |
38 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑅 ↑s
(𝐵
↑𝑚 1𝑜)) = (𝑅 ↑s (𝐵 ↑𝑚
1𝑜)) |
39 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘(𝑅
↑s (𝐵 ↑𝑚
1𝑜))) = (Base‘(𝑅 ↑s (𝐵 ↑𝑚
1𝑜))) |
40 | | simpl 472 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → 𝑅 ∈ CRing) |
41 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝐵 ↑𝑚
1𝑜) ∈ V |
42 | 41 | a1i 11 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → (𝐵 ↑𝑚
1𝑜) ∈ V) |
43 | | 1on 7454 |
. . . . . . . . . . 11
⊢
1𝑜 ∈ On |
44 | 18, 8, 19, 38 | evlrhm 19346 |
. . . . . . . . . . 11
⊢
((1𝑜 ∈ On ∧ 𝑅 ∈ CRing) → (1𝑜
eval 𝑅) ∈
((1𝑜 mPoly 𝑅) RingHom (𝑅 ↑s (𝐵 ↑𝑚
1𝑜)))) |
45 | 43, 44 | mpan 702 |
. . . . . . . . . 10
⊢ (𝑅 ∈ CRing →
(1𝑜 eval 𝑅) ∈ ((1𝑜 mPoly 𝑅) RingHom (𝑅 ↑s (𝐵 ↑𝑚
1𝑜)))) |
46 | 21, 39 | rhmf 18549 |
. . . . . . . . . 10
⊢
((1𝑜 eval 𝑅) ∈ ((1𝑜 mPoly 𝑅) RingHom (𝑅 ↑s (𝐵 ↑𝑚
1𝑜))) → (1𝑜 eval 𝑅):(Base‘(Poly1‘𝑅))⟶(Base‘(𝑅 ↑s
(𝐵
↑𝑚 1𝑜)))) |
47 | 45, 46 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing →
(1𝑜 eval 𝑅):(Base‘(Poly1‘𝑅))⟶(Base‘(𝑅 ↑s
(𝐵
↑𝑚 1𝑜)))) |
48 | 47 | ffvelrnda 6267 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → ((1𝑜 eval
𝑅)‘𝑦) ∈ (Base‘(𝑅 ↑s (𝐵 ↑𝑚
1𝑜)))) |
49 | 38, 8, 39, 40, 42, 48 | pwselbas 15972 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → ((1𝑜 eval
𝑅)‘𝑦):(𝐵 ↑𝑚
1𝑜)⟶𝐵) |
50 | | fcoi1 5991 |
. . . . . . 7
⊢
(((1𝑜 eval 𝑅)‘𝑦):(𝐵 ↑𝑚
1𝑜)⟶𝐵 → (((1𝑜 eval 𝑅)‘𝑦) ∘ ( I ↾ (𝐵 ↑𝑚
1𝑜))) = ((1𝑜 eval 𝑅)‘𝑦)) |
51 | 49, 50 | syl 17 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → (((1𝑜 eval
𝑅)‘𝑦) ∘ ( I ↾ (𝐵 ↑𝑚
1𝑜))) = ((1𝑜 eval 𝑅)‘𝑦)) |
52 | 23, 37, 51 | 3eqtrd 2648 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → (((eval1‘𝑅)‘𝑦) ∘ (𝑥 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑥‘∅))) = ((1𝑜
eval 𝑅)‘𝑦)) |
53 | | ffn 5958 |
. . . . . . . 8
⊢
((1𝑜 eval 𝑅):(Base‘(Poly1‘𝑅))⟶(Base‘(𝑅 ↑s
(𝐵
↑𝑚 1𝑜))) →
(1𝑜 eval 𝑅) Fn
(Base‘(Poly1‘𝑅))) |
54 | 47, 53 | syl 17 |
. . . . . . 7
⊢ (𝑅 ∈ CRing →
(1𝑜 eval 𝑅) Fn
(Base‘(Poly1‘𝑅))) |
55 | | fnfvelrn 6264 |
. . . . . . 7
⊢
(((1𝑜 eval 𝑅) Fn
(Base‘(Poly1‘𝑅)) ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → ((1𝑜 eval
𝑅)‘𝑦) ∈ ran (1𝑜 eval
𝑅)) |
56 | 54, 55 | sylan 487 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → ((1𝑜 eval
𝑅)‘𝑦) ∈ ran (1𝑜 eval
𝑅)) |
57 | | mpfpf1.q |
. . . . . 6
⊢ 𝐸 = ran (1𝑜
eval 𝑅) |
58 | 56, 57 | syl6eleqr 2699 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → ((1𝑜 eval
𝑅)‘𝑦) ∈ 𝐸) |
59 | 52, 58 | eqeltrd 2688 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → (((eval1‘𝑅)‘𝑦) ∘ (𝑥 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑥‘∅))) ∈ 𝐸) |
60 | | coeq1 5201 |
. . . . 5
⊢
(((eval1‘𝑅)‘𝑦) = 𝐹 → (((eval1‘𝑅)‘𝑦) ∘ (𝑥 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑥‘∅))) = (𝐹 ∘ (𝑥 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑥‘∅)))) |
61 | 60 | eleq1d 2672 |
. . . 4
⊢
(((eval1‘𝑅)‘𝑦) = 𝐹 → ((((eval1‘𝑅)‘𝑦) ∘ (𝑥 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑥‘∅))) ∈ 𝐸 ↔ (𝐹 ∘ (𝑥 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑥‘∅))) ∈ 𝐸)) |
62 | 59, 61 | syl5ibcom 234 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈
(Base‘(Poly1‘𝑅))) → (((eval1‘𝑅)‘𝑦) = 𝐹 → (𝐹 ∘ (𝑥 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑥‘∅))) ∈ 𝐸)) |
63 | 62 | rexlimdva 3013 |
. 2
⊢ (𝑅 ∈ CRing →
(∃𝑦 ∈
(Base‘(Poly1‘𝑅))((eval1‘𝑅)‘𝑦) = 𝐹 → (𝐹 ∘ (𝑥 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑥‘∅))) ∈ 𝐸)) |
64 | 2, 17, 63 | sylc 63 |
1
⊢ (𝐹 ∈ 𝑄 → (𝐹 ∘ (𝑥 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑥‘∅))) ∈ 𝐸) |