Metamath Proof Explorer


Theorem ismon1p

Description: Being a monic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses uc1pval.p 𝑃 = ( Poly1𝑅 )
uc1pval.b 𝐵 = ( Base ‘ 𝑃 )
uc1pval.z 0 = ( 0g𝑃 )
uc1pval.d 𝐷 = ( deg1𝑅 )
mon1pval.m 𝑀 = ( Monic1p𝑅 )
mon1pval.o 1 = ( 1r𝑅 )
Assertion ismon1p ( 𝐹𝑀 ↔ ( 𝐹𝐵𝐹0 ∧ ( ( coe1𝐹 ) ‘ ( 𝐷𝐹 ) ) = 1 ) )

Proof

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 ) )