Step |
Hyp |
Ref |
Expression |
1 |
|
df-mnc |
⊢ Monic = ( 𝑠 ∈ 𝒫 ℂ ↦ { 𝑝 ∈ ( Poly ‘ 𝑠 ) ∣ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 } ) |
2 |
1
|
dmmptss |
⊢ dom Monic ⊆ 𝒫 ℂ |
3 |
|
elfvdm |
⊢ ( 𝑃 ∈ ( Monic ‘ 𝑆 ) → 𝑆 ∈ dom Monic ) |
4 |
2 3
|
sseldi |
⊢ ( 𝑃 ∈ ( Monic ‘ 𝑆 ) → 𝑆 ∈ 𝒫 ℂ ) |
5 |
4
|
elpwid |
⊢ ( 𝑃 ∈ ( Monic ‘ 𝑆 ) → 𝑆 ⊆ ℂ ) |
6 |
|
plybss |
⊢ ( 𝑃 ∈ ( Poly ‘ 𝑆 ) → 𝑆 ⊆ ℂ ) |
7 |
6
|
adantr |
⊢ ( ( 𝑃 ∈ ( Poly ‘ 𝑆 ) ∧ ( ( coeff ‘ 𝑃 ) ‘ ( deg ‘ 𝑃 ) ) = 1 ) → 𝑆 ⊆ ℂ ) |
8 |
|
cnex |
⊢ ℂ ∈ V |
9 |
8
|
elpw2 |
⊢ ( 𝑆 ∈ 𝒫 ℂ ↔ 𝑆 ⊆ ℂ ) |
10 |
|
fveq2 |
⊢ ( 𝑠 = 𝑆 → ( Poly ‘ 𝑠 ) = ( Poly ‘ 𝑆 ) ) |
11 |
|
rabeq |
⊢ ( ( Poly ‘ 𝑠 ) = ( Poly ‘ 𝑆 ) → { 𝑝 ∈ ( Poly ‘ 𝑠 ) ∣ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 } = { 𝑝 ∈ ( Poly ‘ 𝑆 ) ∣ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 } ) |
12 |
10 11
|
syl |
⊢ ( 𝑠 = 𝑆 → { 𝑝 ∈ ( Poly ‘ 𝑠 ) ∣ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 } = { 𝑝 ∈ ( Poly ‘ 𝑆 ) ∣ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 } ) |
13 |
|
fvex |
⊢ ( Poly ‘ 𝑆 ) ∈ V |
14 |
13
|
rabex |
⊢ { 𝑝 ∈ ( Poly ‘ 𝑆 ) ∣ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 } ∈ V |
15 |
12 1 14
|
fvmpt |
⊢ ( 𝑆 ∈ 𝒫 ℂ → ( Monic ‘ 𝑆 ) = { 𝑝 ∈ ( Poly ‘ 𝑆 ) ∣ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 } ) |
16 |
9 15
|
sylbir |
⊢ ( 𝑆 ⊆ ℂ → ( Monic ‘ 𝑆 ) = { 𝑝 ∈ ( Poly ‘ 𝑆 ) ∣ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 } ) |
17 |
16
|
eleq2d |
⊢ ( 𝑆 ⊆ ℂ → ( 𝑃 ∈ ( Monic ‘ 𝑆 ) ↔ 𝑃 ∈ { 𝑝 ∈ ( Poly ‘ 𝑆 ) ∣ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 } ) ) |
18 |
|
fveq2 |
⊢ ( 𝑝 = 𝑃 → ( coeff ‘ 𝑝 ) = ( coeff ‘ 𝑃 ) ) |
19 |
|
fveq2 |
⊢ ( 𝑝 = 𝑃 → ( deg ‘ 𝑝 ) = ( deg ‘ 𝑃 ) ) |
20 |
18 19
|
fveq12d |
⊢ ( 𝑝 = 𝑃 → ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = ( ( coeff ‘ 𝑃 ) ‘ ( deg ‘ 𝑃 ) ) ) |
21 |
20
|
eqeq1d |
⊢ ( 𝑝 = 𝑃 → ( ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 ↔ ( ( coeff ‘ 𝑃 ) ‘ ( deg ‘ 𝑃 ) ) = 1 ) ) |
22 |
21
|
elrab |
⊢ ( 𝑃 ∈ { 𝑝 ∈ ( Poly ‘ 𝑆 ) ∣ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 } ↔ ( 𝑃 ∈ ( Poly ‘ 𝑆 ) ∧ ( ( coeff ‘ 𝑃 ) ‘ ( deg ‘ 𝑃 ) ) = 1 ) ) |
23 |
17 22
|
bitrdi |
⊢ ( 𝑆 ⊆ ℂ → ( 𝑃 ∈ ( Monic ‘ 𝑆 ) ↔ ( 𝑃 ∈ ( Poly ‘ 𝑆 ) ∧ ( ( coeff ‘ 𝑃 ) ‘ ( deg ‘ 𝑃 ) ) = 1 ) ) ) |
24 |
5 7 23
|
pm5.21nii |
⊢ ( 𝑃 ∈ ( Monic ‘ 𝑆 ) ↔ ( 𝑃 ∈ ( Poly ‘ 𝑆 ) ∧ ( ( coeff ‘ 𝑃 ) ‘ ( deg ‘ 𝑃 ) ) = 1 ) ) |