This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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