Step |
Hyp |
Ref |
Expression |
1 |
|
uc1pval.p |
⊢ 𝑃 = ( Poly1 ‘ 𝑅 ) |
2 |
|
uc1pval.b |
⊢ 𝐵 = ( Base ‘ 𝑃 ) |
3 |
|
uc1pval.z |
⊢ 0 = ( 0g ‘ 𝑃 ) |
4 |
|
uc1pval.d |
⊢ 𝐷 = ( deg1 ‘ 𝑅 ) |
5 |
|
mon1pval.m |
⊢ 𝑀 = ( Monic1p ‘ 𝑅 ) |
6 |
|
mon1pval.o |
⊢ 1 = ( 1r ‘ 𝑅 ) |
7 |
|
neeq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 ≠ 0 ↔ 𝐹 ≠ 0 ) ) |
8 |
|
fveq2 |
⊢ ( 𝑓 = 𝐹 → ( coe1 ‘ 𝑓 ) = ( coe1 ‘ 𝐹 ) ) |
9 |
|
fveq2 |
⊢ ( 𝑓 = 𝐹 → ( 𝐷 ‘ 𝑓 ) = ( 𝐷 ‘ 𝐹 ) ) |
10 |
8 9
|
fveq12d |
⊢ ( 𝑓 = 𝐹 → ( ( coe1 ‘ 𝑓 ) ‘ ( 𝐷 ‘ 𝑓 ) ) = ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ) |
11 |
10
|
eqeq1d |
⊢ ( 𝑓 = 𝐹 → ( ( ( coe1 ‘ 𝑓 ) ‘ ( 𝐷 ‘ 𝑓 ) ) = 1 ↔ ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) = 1 ) ) |
12 |
7 11
|
anbi12d |
⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ≠ 0 ∧ ( ( coe1 ‘ 𝑓 ) ‘ ( 𝐷 ‘ 𝑓 ) ) = 1 ) ↔ ( 𝐹 ≠ 0 ∧ ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) = 1 ) ) ) |
13 |
1 2 3 4 5 6
|
mon1pval |
⊢ 𝑀 = { 𝑓 ∈ 𝐵 ∣ ( 𝑓 ≠ 0 ∧ ( ( coe1 ‘ 𝑓 ) ‘ ( 𝐷 ‘ 𝑓 ) ) = 1 ) } |
14 |
12 13
|
elrab2 |
⊢ ( 𝐹 ∈ 𝑀 ↔ ( 𝐹 ∈ 𝐵 ∧ ( 𝐹 ≠ 0 ∧ ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) = 1 ) ) ) |
15 |
|
3anass |
⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ∧ ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) = 1 ) ↔ ( 𝐹 ∈ 𝐵 ∧ ( 𝐹 ≠ 0 ∧ ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) = 1 ) ) ) |
16 |
14 15
|
bitr4i |
⊢ ( 𝐹 ∈ 𝑀 ↔ ( 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ∧ ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) = 1 ) ) |