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