isuc1p

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

	Ref	Expression
Hypotheses	uc1pval.p	$⊢ P = {Poly}_{1} (R)$
	uc1pval.b	$⊢ B = {Base}_{P}$
	uc1pval.z	$⊢ \underset{˙}{0} = 0_{P}$
	uc1pval.d	$⊢ D = \deg_{1} (R)$
	uc1pval.c	$⊢ C = {Unic}_{1p} (R)$
	uc1pval.u	$⊢ U = Unit (R)$
Assertion	isuc1p	$⊢ F \in C \leftrightarrow (F \in B \land F \neq \underset{˙}{0} \land {coe}_{1} (F) (D (F)) \in U)$

Step	Hyp	Ref	Expression
1		uc1pval.p	$⊢ P = {Poly}_{1} (R)$
2		uc1pval.b	$⊢ B = {Base}_{P}$
3		uc1pval.z	$⊢ \underset{˙}{0} = 0_{P}$
4		uc1pval.d	$⊢ D = \deg_{1} (R)$
5		uc1pval.c	$⊢ C = {Unic}_{1p} (R)$
6		uc1pval.u	$⊢ U = Unit (R)$
7		neeq1	$⊢ f = F \to (f \neq \underset{˙}{0} \leftrightarrow F \neq \underset{˙}{0})$
8		fveq2	$⊢ f = F \to {coe}_{1} (f) = {coe}_{1} (F)$
9		fveq2	$⊢ f = F \to D (f) = D (F)$
10	8 9	fveq12d	$⊢ f = F \to {coe}_{1} (f) (D (f)) = {coe}_{1} (F) (D (F))$
11	10	eleq1d	$⊢ f = F \to ({coe}_{1} (f) (D (f)) \in U \leftrightarrow {coe}_{1} (F) (D (F)) \in U)$
12	7 11	anbi12d	$⊢ f = F \to ((f \neq \underset{˙}{0} \land {coe}_{1} (f) (D (f)) \in U) \leftrightarrow (F \neq \underset{˙}{0} \land {coe}_{1} (F) (D (F)) \in U))$
13	1 2 3 4 5 6	uc1pval	$⊢ C = \{f \in B \| (f \neq \underset{˙}{0} \land {coe}_{1} (f) (D (f)) \in U)\}$
14	12 13	elrab2	$⊢ F \in C \leftrightarrow (F \in B \land (F \neq \underset{˙}{0} \land {coe}_{1} (F) (D (F)) \in U))$
15		3anass	$⊢ (F \in B \land F \neq \underset{˙}{0} \land {coe}_{1} (F) (D (F)) \in U) \leftrightarrow (F \in B \land (F \neq \underset{˙}{0} \land {coe}_{1} (F) (D (F)) \in U))$
16	14 15	bitr4i	$⊢ F \in C \leftrightarrow (F \in B \land F \neq \underset{˙}{0} \land {coe}_{1} (F) (D (F)) \in U)$

Metamath Proof Explorer