Step | Hyp | Ref
| Expression |
1 | | mon1pval.m |
. 2
⊢ 𝑀 =
(Monic1p‘𝑅) |
2 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (Poly1‘𝑟) =
(Poly1‘𝑅)) |
3 | | uc1pval.p |
. . . . . . . 8
⊢ 𝑃 = (Poly1‘𝑅) |
4 | 2, 3 | syl6eqr 2674 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (Poly1‘𝑟) = 𝑃) |
5 | 4 | fveq2d 6195 |
. . . . . 6
⊢ (𝑟 = 𝑅 →
(Base‘(Poly1‘𝑟)) = (Base‘𝑃)) |
6 | | uc1pval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑃) |
7 | 5, 6 | syl6eqr 2674 |
. . . . 5
⊢ (𝑟 = 𝑅 →
(Base‘(Poly1‘𝑟)) = 𝐵) |
8 | 4 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 →
(0g‘(Poly1‘𝑟)) = (0g‘𝑃)) |
9 | | uc1pval.z |
. . . . . . . 8
⊢ 0 =
(0g‘𝑃) |
10 | 8, 9 | syl6eqr 2674 |
. . . . . . 7
⊢ (𝑟 = 𝑅 →
(0g‘(Poly1‘𝑟)) = 0 ) |
11 | 10 | neeq2d 2854 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (𝑓 ≠
(0g‘(Poly1‘𝑟)) ↔ 𝑓 ≠ 0 )) |
12 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → ( deg1 ‘𝑟) = ( deg1
‘𝑅)) |
13 | | uc1pval.d |
. . . . . . . . . 10
⊢ 𝐷 = ( deg1
‘𝑅) |
14 | 12, 13 | syl6eqr 2674 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → ( deg1 ‘𝑟) = 𝐷) |
15 | 14 | fveq1d 6193 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (( deg1 ‘𝑟)‘𝑓) = (𝐷‘𝑓)) |
16 | 15 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → ((coe1‘𝑓)‘(( deg1
‘𝑟)‘𝑓)) =
((coe1‘𝑓)‘(𝐷‘𝑓))) |
17 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (1r‘𝑟) = (1r‘𝑅)) |
18 | | mon1pval.o |
. . . . . . . 8
⊢ 1 =
(1r‘𝑅) |
19 | 17, 18 | syl6eqr 2674 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (1r‘𝑟) = 1 ) |
20 | 16, 19 | eqeq12d 2637 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (((coe1‘𝑓)‘(( deg1
‘𝑟)‘𝑓)) = (1r‘𝑟) ↔
((coe1‘𝑓)‘(𝐷‘𝑓)) = 1 )) |
21 | 11, 20 | anbi12d 747 |
. . . . 5
⊢ (𝑟 = 𝑅 → ((𝑓 ≠
(0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1
‘𝑟)‘𝑓)) = (1r‘𝑟)) ↔ (𝑓 ≠ 0 ∧
((coe1‘𝑓)‘(𝐷‘𝑓)) = 1 ))) |
22 | 7, 21 | rabeqbidv 3195 |
. . . 4
⊢ (𝑟 = 𝑅 → {𝑓 ∈
(Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠
(0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1
‘𝑟)‘𝑓)) = (1r‘𝑟))} = {𝑓 ∈ 𝐵 ∣ (𝑓 ≠ 0 ∧
((coe1‘𝑓)‘(𝐷‘𝑓)) = 1 )}) |
23 | | df-mon1 23890 |
. . . 4
⊢
Monic1p = (𝑟 ∈ V ↦ {𝑓 ∈
(Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠
(0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1
‘𝑟)‘𝑓)) = (1r‘𝑟))}) |
24 | | fvex 6201 |
. . . . . 6
⊢
(Base‘𝑃)
∈ V |
25 | 6, 24 | eqeltri 2697 |
. . . . 5
⊢ 𝐵 ∈ V |
26 | 25 | rabex 4813 |
. . . 4
⊢ {𝑓 ∈ 𝐵 ∣ (𝑓 ≠ 0 ∧
((coe1‘𝑓)‘(𝐷‘𝑓)) = 1 )} ∈
V |
27 | 22, 23, 26 | fvmpt 6282 |
. . 3
⊢ (𝑅 ∈ V →
(Monic1p‘𝑅) = {𝑓 ∈ 𝐵 ∣ (𝑓 ≠ 0 ∧
((coe1‘𝑓)‘(𝐷‘𝑓)) = 1 )}) |
28 | | fvprc 6185 |
. . . 4
⊢ (¬
𝑅 ∈ V →
(Monic1p‘𝑅) = ∅) |
29 | | ssrab2 3687 |
. . . . . 6
⊢ {𝑓 ∈ 𝐵 ∣ (𝑓 ≠ 0 ∧
((coe1‘𝑓)‘(𝐷‘𝑓)) = 1 )} ⊆ 𝐵 |
30 | | fvprc 6185 |
. . . . . . . . . 10
⊢ (¬
𝑅 ∈ V →
(Poly1‘𝑅)
= ∅) |
31 | 3, 30 | syl5eq 2668 |
. . . . . . . . 9
⊢ (¬
𝑅 ∈ V → 𝑃 = ∅) |
32 | 31 | fveq2d 6195 |
. . . . . . . 8
⊢ (¬
𝑅 ∈ V →
(Base‘𝑃) =
(Base‘∅)) |
33 | 6, 32 | syl5eq 2668 |
. . . . . . 7
⊢ (¬
𝑅 ∈ V → 𝐵 =
(Base‘∅)) |
34 | | base0 15912 |
. . . . . . 7
⊢ ∅ =
(Base‘∅) |
35 | 33, 34 | syl6eqr 2674 |
. . . . . 6
⊢ (¬
𝑅 ∈ V → 𝐵 = ∅) |
36 | 29, 35 | syl5sseq 3653 |
. . . . 5
⊢ (¬
𝑅 ∈ V → {𝑓 ∈ 𝐵 ∣ (𝑓 ≠ 0 ∧
((coe1‘𝑓)‘(𝐷‘𝑓)) = 1 )} ⊆
∅) |
37 | | ss0 3974 |
. . . . 5
⊢ ({𝑓 ∈ 𝐵 ∣ (𝑓 ≠ 0 ∧
((coe1‘𝑓)‘(𝐷‘𝑓)) = 1 )} ⊆ ∅ →
{𝑓 ∈ 𝐵 ∣ (𝑓 ≠ 0 ∧
((coe1‘𝑓)‘(𝐷‘𝑓)) = 1 )} =
∅) |
38 | 36, 37 | syl 17 |
. . . 4
⊢ (¬
𝑅 ∈ V → {𝑓 ∈ 𝐵 ∣ (𝑓 ≠ 0 ∧
((coe1‘𝑓)‘(𝐷‘𝑓)) = 1 )} =
∅) |
39 | 28, 38 | eqtr4d 2659 |
. . 3
⊢ (¬
𝑅 ∈ V →
(Monic1p‘𝑅) = {𝑓 ∈ 𝐵 ∣ (𝑓 ≠ 0 ∧
((coe1‘𝑓)‘(𝐷‘𝑓)) = 1 )}) |
40 | 27, 39 | pm2.61i 176 |
. 2
⊢
(Monic1p‘𝑅) = {𝑓 ∈ 𝐵 ∣ (𝑓 ≠ 0 ∧
((coe1‘𝑓)‘(𝐷‘𝑓)) = 1 )} |
41 | 1, 40 | eqtri 2644 |
1
⊢ 𝑀 = {𝑓 ∈ 𝐵 ∣ (𝑓 ≠ 0 ∧
((coe1‘𝑓)‘(𝐷‘𝑓)) = 1 )} |