Step | Hyp | Ref
| Expression |
1 | | mon1pval.m |
. 2
⊢ 𝑀 =
(Monic1p‘𝑅) |
2 | | fveq2 6774 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (Poly1‘𝑟) =
(Poly1‘𝑅)) |
3 | | uc1pval.p |
. . . . . . . 8
⊢ 𝑃 = (Poly1‘𝑅) |
4 | 2, 3 | eqtr4di 2796 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (Poly1‘𝑟) = 𝑃) |
5 | 4 | fveq2d 6778 |
. . . . . 6
⊢ (𝑟 = 𝑅 →
(Base‘(Poly1‘𝑟)) = (Base‘𝑃)) |
6 | | uc1pval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑃) |
7 | 5, 6 | eqtr4di 2796 |
. . . . 5
⊢ (𝑟 = 𝑅 →
(Base‘(Poly1‘𝑟)) = 𝐵) |
8 | 4 | fveq2d 6778 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 →
(0g‘(Poly1‘𝑟)) = (0g‘𝑃)) |
9 | | uc1pval.z |
. . . . . . . 8
⊢ 0 =
(0g‘𝑃) |
10 | 8, 9 | eqtr4di 2796 |
. . . . . . 7
⊢ (𝑟 = 𝑅 →
(0g‘(Poly1‘𝑟)) = 0 ) |
11 | 10 | neeq2d 3004 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (𝑓 ≠
(0g‘(Poly1‘𝑟)) ↔ 𝑓 ≠ 0 )) |
12 | | fveq2 6774 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → ( deg1 ‘𝑟) = ( deg1
‘𝑅)) |
13 | | uc1pval.d |
. . . . . . . . . 10
⊢ 𝐷 = ( deg1
‘𝑅) |
14 | 12, 13 | eqtr4di 2796 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → ( deg1 ‘𝑟) = 𝐷) |
15 | 14 | fveq1d 6776 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (( deg1 ‘𝑟)‘𝑓) = (𝐷‘𝑓)) |
16 | 15 | fveq2d 6778 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → ((coe1‘𝑓)‘(( deg1
‘𝑟)‘𝑓)) =
((coe1‘𝑓)‘(𝐷‘𝑓))) |
17 | | fveq2 6774 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (1r‘𝑟) = (1r‘𝑅)) |
18 | | mon1pval.o |
. . . . . . . 8
⊢ 1 =
(1r‘𝑅) |
19 | 17, 18 | eqtr4di 2796 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (1r‘𝑟) = 1 ) |
20 | 16, 19 | eqeq12d 2754 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (((coe1‘𝑓)‘(( deg1
‘𝑟)‘𝑓)) = (1r‘𝑟) ↔
((coe1‘𝑓)‘(𝐷‘𝑓)) = 1 )) |
21 | 11, 20 | anbi12d 631 |
. . . . 5
⊢ (𝑟 = 𝑅 → ((𝑓 ≠
(0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1
‘𝑟)‘𝑓)) = (1r‘𝑟)) ↔ (𝑓 ≠ 0 ∧
((coe1‘𝑓)‘(𝐷‘𝑓)) = 1 ))) |
22 | 7, 21 | rabeqbidv 3420 |
. . . 4
⊢ (𝑟 = 𝑅 → {𝑓 ∈
(Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠
(0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1
‘𝑟)‘𝑓)) = (1r‘𝑟))} = {𝑓 ∈ 𝐵 ∣ (𝑓 ≠ 0 ∧
((coe1‘𝑓)‘(𝐷‘𝑓)) = 1 )}) |
23 | | df-mon1 25295 |
. . . 4
⊢
Monic1p = (𝑟 ∈ V ↦ {𝑓 ∈
(Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠
(0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1
‘𝑟)‘𝑓)) = (1r‘𝑟))}) |
24 | 6 | fvexi 6788 |
. . . . 5
⊢ 𝐵 ∈ V |
25 | 24 | rabex 5256 |
. . . 4
⊢ {𝑓 ∈ 𝐵 ∣ (𝑓 ≠ 0 ∧
((coe1‘𝑓)‘(𝐷‘𝑓)) = 1 )} ∈
V |
26 | 22, 23, 25 | fvmpt 6875 |
. . 3
⊢ (𝑅 ∈ V →
(Monic1p‘𝑅) = {𝑓 ∈ 𝐵 ∣ (𝑓 ≠ 0 ∧
((coe1‘𝑓)‘(𝐷‘𝑓)) = 1 )}) |
27 | | fvprc 6766 |
. . . 4
⊢ (¬
𝑅 ∈ V →
(Monic1p‘𝑅) = ∅) |
28 | | ssrab2 4013 |
. . . . . 6
⊢ {𝑓 ∈ 𝐵 ∣ (𝑓 ≠ 0 ∧
((coe1‘𝑓)‘(𝐷‘𝑓)) = 1 )} ⊆ 𝐵 |
29 | | fvprc 6766 |
. . . . . . . . . 10
⊢ (¬
𝑅 ∈ V →
(Poly1‘𝑅)
= ∅) |
30 | 3, 29 | eqtrid 2790 |
. . . . . . . . 9
⊢ (¬
𝑅 ∈ V → 𝑃 = ∅) |
31 | 30 | fveq2d 6778 |
. . . . . . . 8
⊢ (¬
𝑅 ∈ V →
(Base‘𝑃) =
(Base‘∅)) |
32 | 6, 31 | eqtrid 2790 |
. . . . . . 7
⊢ (¬
𝑅 ∈ V → 𝐵 =
(Base‘∅)) |
33 | | base0 16917 |
. . . . . . 7
⊢ ∅ =
(Base‘∅) |
34 | 32, 33 | eqtr4di 2796 |
. . . . . 6
⊢ (¬
𝑅 ∈ V → 𝐵 = ∅) |
35 | 28, 34 | sseqtrid 3973 |
. . . . 5
⊢ (¬
𝑅 ∈ V → {𝑓 ∈ 𝐵 ∣ (𝑓 ≠ 0 ∧
((coe1‘𝑓)‘(𝐷‘𝑓)) = 1 )} ⊆
∅) |
36 | | ss0 4332 |
. . . . 5
⊢ ({𝑓 ∈ 𝐵 ∣ (𝑓 ≠ 0 ∧
((coe1‘𝑓)‘(𝐷‘𝑓)) = 1 )} ⊆ ∅ →
{𝑓 ∈ 𝐵 ∣ (𝑓 ≠ 0 ∧
((coe1‘𝑓)‘(𝐷‘𝑓)) = 1 )} =
∅) |
37 | 35, 36 | syl 17 |
. . . 4
⊢ (¬
𝑅 ∈ V → {𝑓 ∈ 𝐵 ∣ (𝑓 ≠ 0 ∧
((coe1‘𝑓)‘(𝐷‘𝑓)) = 1 )} =
∅) |
38 | 27, 37 | eqtr4d 2781 |
. . 3
⊢ (¬
𝑅 ∈ V →
(Monic1p‘𝑅) = {𝑓 ∈ 𝐵 ∣ (𝑓 ≠ 0 ∧
((coe1‘𝑓)‘(𝐷‘𝑓)) = 1 )}) |
39 | 26, 38 | pm2.61i 182 |
. 2
⊢
(Monic1p‘𝑅) = {𝑓 ∈ 𝐵 ∣ (𝑓 ≠ 0 ∧
((coe1‘𝑓)‘(𝐷‘𝑓)) = 1 )} |
40 | 1, 39 | eqtri 2766 |
1
⊢ 𝑀 = {𝑓 ∈ 𝐵 ∣ (𝑓 ≠ 0 ∧
((coe1‘𝑓)‘(𝐷‘𝑓)) = 1 )} |