Metamath Proof Explorer

Theorem elmnc

Description: Property of a monic polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014)

Ref Expression
Assertion elmnc ⊢ P ∈ Monic ⁡ S ↔ P ∈ Poly ⁡ S ∧ coeff ⁡ P ⁡ deg ⁡ P = 1

Proof

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