Theorem mon1pval

Description: Value of the set of monic 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)$$
	mon1pval.m	$$⊢M={Monic}_{\mathrm{1p}}\left(R\right)$$
	mon1pval.o	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	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\}$$

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		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 1_r=1_R$$
19	18 6	eqtr4di	$$⊢r=R\to 1_r=\underset{\dot{}}{1}$$
20	17 19	eqeq12d	$$⊢r=R\to \left({\mathrm{coe}}_1\left(f\right)\left({\mathrm{deg}}_1\left(r\right)\left(f\right)\right)=1_r\leftrightarrow {\mathrm{coe}}_1\left(f\right)\left(D\left(f\right)\right)=\underset{\dot{}}{1}\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)=1_r\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)$$
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)=1_r\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)=\underset{\dot{}}{1}\right)\right\}$$
23		df-mon1	$$⊢{Monic}_{\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)=1_r\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)=\underset{\dot{}}{1}\right)\right\}\in \mathrm{V}$$
26	22 23 25	fvmpt	$$⊢R\in \mathrm{V}\to {Monic}_{\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)=\underset{\dot{}}{1}\right)\right\}$$
27		fvprc	$$⊢\neg R\in \mathrm{V}\to {Monic}_{\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)=\underset{\dot{}}{1}\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	2 31	syl5eq	$$⊢\neg R\in \mathrm{V}\to B={\mathrm{Base}}_{\varnothing }$$
33		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
34	32 33	eqtr4di	$$⊢\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)=\underset{\dot{}}{1}\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)=\underset{\dot{}}{1}\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)=\underset{\dot{}}{1}\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)=\underset{\dot{}}{1}\right)\right\}=\varnothing$$
38	27 37	eqtr4d	$$⊢\neg R\in \mathrm{V}\to {Monic}_{\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)=\underset{\dot{}}{1}\right)\right\}$$
39	26 38	pm2.61i	$$⊢{Monic}_{\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)=\underset{\dot{}}{1}\right)\right\}$$
40	5 39	eqtri	$$⊢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\}$$