Metamath Proof Explorer

Theorem elmnc

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

Ref Expression
Assertion elmnc ( 𝑃 ∈ ( Monic ‘ 𝑆 ) ↔ ( 𝑃 ∈ ( Poly ‘ 𝑆 ) ∧ ( ( coeff ‘ 𝑃 ) ‘ ( deg ‘ 𝑃 ) ) = 1 ) )

Proof

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 sselid ⊢ ( 𝑃 ∈ ( 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 ) )