Theorem ismon1p

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

	Ref	Expression
Hypotheses	uc1pval.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	uc1pval.b	$$⊢B={\mathrm{Base}}_P$$
	uc1pval.z	$$⊢\underset{\dot{}}{0}=0_P$$
	uc1pval.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	mon1pval.m	$$⊢M={Monic}_{\mathrm{1p}}\left(R\right)$$
	mon1pval.o	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	ismon1p	$$⊢F\in M\leftrightarrow \left(F\in B\wedge F\ne \underset{\dot{}}{0}\wedge {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)=\underset{\dot{}}{1}\right)$$

Proof

Step	Hyp	Ref	Expression
1		uc1pval.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		uc1pval.b	$$⊢B={\mathrm{Base}}_P$$
3		uc1pval.z	$$⊢\underset{\dot{}}{0}=0_P$$
4		uc1pval.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
5		mon1pval.m	$$⊢M={Monic}_{\mathrm{1p}}\left(R\right)$$
6		mon1pval.o	$$⊢\underset{\dot{}}{1}=1_R$$
7		neeq1	$$⊢f=F\to \left(f\ne \underset{\dot{}}{0}\leftrightarrow F\ne \underset{\dot{}}{0}\right)$$
8		fveq2	$$⊢f=F\to {\mathrm{coe}}_1\left(f\right)={\mathrm{coe}}_1\left(F\right)$$
9		fveq2	$$⊢f=F\to D\left(f\right)=D\left(F\right)$$
10	8 9	fveq12d	$$⊢f=F\to {\mathrm{coe}}_1\left(f\right)\left(D\left(f\right)\right)={\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)$$
11	10	eqeq1d	$$⊢f=F\to \left({\mathrm{coe}}_1\left(f\right)\left(D\left(f\right)\right)=\underset{\dot{}}{1}\leftrightarrow {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)=\underset{\dot{}}{1}\right)$$
12	7 11	anbi12d	$$⊢f=F\to \left(\left(f\ne \underset{\dot{}}{0}\wedge {\mathrm{coe}}_1\left(f\right)\left(D\left(f\right)\right)=\underset{\dot{}}{1}\right)\leftrightarrow \left(F\ne \underset{\dot{}}{0}\wedge {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)=\underset{\dot{}}{1}\right)\right)$$
13	1 2 3 4 5 6	mon1pval	$$⊢M=\left\{f\in B|\left(f\ne \underset{\dot{}}{0}\wedge {\mathrm{coe}}_1\left(f\right)\left(D\left(f\right)\right)=\underset{\dot{}}{1}\right)\right\}$$
14	12 13	elrab2	$$⊢F\in M\leftrightarrow \left(F\in B\wedge \left(F\ne \underset{\dot{}}{0}\wedge {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)=\underset{\dot{}}{1}\right)\right)$$
15		3anass	$$⊢\left(F\in B\wedge F\ne \underset{\dot{}}{0}\wedge {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)=\underset{\dot{}}{1}\right)\leftrightarrow \left(F\in B\wedge \left(F\ne \underset{\dot{}}{0}\wedge {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)=\underset{\dot{}}{1}\right)\right)$$
16	14 15	bitr4i	$$⊢F\in M\leftrightarrow \left(F\in B\wedge F\ne \underset{\dot{}}{0}\wedge {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)=\underset{\dot{}}{1}\right)$$