Theorem isuc1p

Description: Being a unitic 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)$$
	uc1pval.c	$$⊢C={Unic}_{\mathrm{1p}}\left(R\right)$$
	uc1pval.u	$$⊢U=\mathrm{Unit}\left(R\right)$$
Assertion	isuc1p	$$⊢F\in C\leftrightarrow \left(F\in B\wedge F\ne \underset{\dot{}}{0}\wedge {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)\in U\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		uc1pval.c	$$⊢C={Unic}_{\mathrm{1p}}\left(R\right)$$
6		uc1pval.u	$$⊢U=\mathrm{Unit}\left(R\right)$$
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	eleq1d	$$⊢f=F\to \left({\mathrm{coe}}_1\left(f\right)\left(D\left(f\right)\right)\in U\leftrightarrow {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)\in U\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)\in U\right)\leftrightarrow \left(F\ne \underset{\dot{}}{0}\wedge {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)\in U\right)\right)$$
13	1 2 3 4 5 6	uc1pval	$$⊢C=\left\{f\in B|\left(f\ne \underset{\dot{}}{0}\wedge {\mathrm{coe}}_1\left(f\right)\left(D\left(f\right)\right)\in U\right)\right\}$$
14	12 13	elrab2	$$⊢F\in C\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)\in U\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)\in U\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)\in U\right)\right)$$
16	14 15	bitr4i	$$⊢F\in C\leftrightarrow \left(F\in B\wedge F\ne \underset{\dot{}}{0}\wedge {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)\in U\right)$$