Theorem uc1pval

Description: Value of the set of unitic polynomials. (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	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\}$$

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		fveq2	$$⊢r=R\to {\mathrm{Poly}}_1\left(r\right)={\mathrm{Poly}}_1\left(R\right)$$
8	7 1	eqtr4di	$$⊢r=R\to {\mathrm{Poly}}_1\left(r\right)=P$$
9	8	fveq2d	$$⊢r=R\to {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(r\right)}={\mathrm{Base}}_P$$
10	9 2	eqtr4di	$$⊢r=R\to {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(r\right)}=B$$
11	8	fveq2d	$$⊢r=R\to 0_{{\mathrm{Poly}}_1\left(r\right)}=0_P$$
12	11 3	eqtr4di	$$⊢r=R\to 0_{{\mathrm{Poly}}_1\left(r\right)}=\underset{\dot{}}{0}$$
13	12	neeq2d	$$⊢r=R\to \left(f\ne 0_{{\mathrm{Poly}}_1\left(r\right)}\leftrightarrow f\ne \underset{\dot{}}{0}\right)$$
14		fveq2	$$⊢r=R\to {\mathrm{deg}}_1\left(r\right)={\mathrm{deg}}_1\left(R\right)$$
15	14 4	eqtr4di	$$⊢r=R\to {\mathrm{deg}}_1\left(r\right)=D$$
16	15	fveq1d	$$⊢r=R\to {\mathrm{deg}}_1\left(r\right)\left(f\right)=D\left(f\right)$$
17	16	fveq2d	$$⊢r=R\to {\mathrm{coe}}_1\left(f\right)\left({\mathrm{deg}}_1\left(r\right)\left(f\right)\right)={\mathrm{coe}}_1\left(f\right)\left(D\left(f\right)\right)$$
18		fveq2	$$⊢r=R\to \mathrm{Unit}\left(r\right)=\mathrm{Unit}\left(R\right)$$
19	18 6	eqtr4di	$$⊢r=R\to \mathrm{Unit}\left(r\right)=U$$
20	17 19	eleq12d	$$⊢r=R\to \left({\mathrm{coe}}_1\left(f\right)\left({\mathrm{deg}}_1\left(r\right)\left(f\right)\right)\in \mathrm{Unit}\left(r\right)\leftrightarrow {\mathrm{coe}}_1\left(f\right)\left(D\left(f\right)\right)\in U\right)$$
21	13 20	anbi12d	$$⊢r=R\to \left(\left(f\ne 0_{{\mathrm{Poly}}_1\left(r\right)}\wedge {\mathrm{coe}}_1\left(f\right)\left({\mathrm{deg}}_1\left(r\right)\left(f\right)\right)\in \mathrm{Unit}\left(r\right)\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)$$
22	10 21	rabeqbidv	$$⊢r=R\to \left\{f\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(r\right)}|\left(f\ne 0_{{\mathrm{Poly}}_1\left(r\right)}\wedge {\mathrm{coe}}_1\left(f\right)\left({\mathrm{deg}}_1\left(r\right)\left(f\right)\right)\in \mathrm{Unit}\left(r\right)\right)\right\}=\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\}$$
23		df-uc1p	$$⊢{Unic}_{\mathrm{1p}}=\left(r\in \mathrm{V}⟼\left\{f\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(r\right)}|\left(f\ne 0_{{\mathrm{Poly}}_1\left(r\right)}\wedge {\mathrm{coe}}_1\left(f\right)\left({\mathrm{deg}}_1\left(r\right)\left(f\right)\right)\in \mathrm{Unit}\left(r\right)\right)\right\}\right)$$
24	2	fvexi	$$⊢B\in \mathrm{V}$$
25	24	rabex	$$⊢\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\}\in \mathrm{V}$$
26	22 23 25	fvmpt	$$⊢R\in \mathrm{V}\to {Unic}_{\mathrm{1p}}\left(R\right)=\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\}$$
27		fvprc	$$⊢\neg R\in \mathrm{V}\to {Unic}_{\mathrm{1p}}\left(R\right)=\varnothing$$
28		ssrab2	$$⊢\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\}\subseteq B$$
29		fvprc	$$⊢\neg R\in \mathrm{V}\to {\mathrm{Poly}}_1\left(R\right)=\varnothing$$
30	1 29	syl5eq	$$⊢\neg R\in \mathrm{V}\to P=\varnothing$$
31	30	fveq2d	$$⊢\neg R\in \mathrm{V}\to {\mathrm{Base}}_P={\mathrm{Base}}_{\varnothing }$$
32		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
33	31 32	eqtr4di	$$⊢\neg R\in \mathrm{V}\to {\mathrm{Base}}_P=\varnothing$$
34	2 33	syl5eq	$$⊢\neg R\in \mathrm{V}\to B=\varnothing$$
35	28 34	sseqtrid	$$⊢\neg R\in \mathrm{V}\to \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\}\subseteq \varnothing$$
36		ss0	$$⊢\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\}\subseteq \varnothing \to \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\}=\varnothing$$
37	35 36	syl	$$⊢\neg R\in \mathrm{V}\to \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\}=\varnothing$$
38	27 37	eqtr4d	$$⊢\neg R\in \mathrm{V}\to {Unic}_{\mathrm{1p}}\left(R\right)=\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\}$$
39	26 38	pm2.61i	$$⊢{Unic}_{\mathrm{1p}}\left(R\right)=\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\}$$
40	5 39	eqtri	$$⊢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\}$$