Theorem deg1pwle

Description: Limiting degree of a variable power. (Contributed by Stefan O'Rear, 1-Apr-2015)

	Ref	Expression
Hypotheses	deg1pw.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	deg1pw.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	deg1pw.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	deg1pw.n	$$⊢N={\mathrm{mulGrp}}_P$$
	deg1pw.e	$$⊢\underset{\dot{}}{\times }={\cdot }_N$$
Assertion	deg1pwle	$$⊢\left(R\in \mathrm{Ring}\wedge F\in {\mathbb{N}}_0\right)\to D\left(F\underset{\dot{}}{\times }X\right)\le F$$

Proof

Step	Hyp	Ref	Expression
1		deg1pw.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
2		deg1pw.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
3		deg1pw.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
4		deg1pw.n	$$⊢N={\mathrm{mulGrp}}_P$$
5		deg1pw.e	$$⊢\underset{\dot{}}{\times }={\cdot }_N$$
6	2	ply1lmod	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{LMod}$$
7		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
8	2 3 4 5 7	ply1moncl	$$⊢\left(R\in \mathrm{Ring}\wedge F\in {\mathbb{N}}_0\right)\to F\underset{\dot{}}{\times }X\in {\mathrm{Base}}_P$$
9		eqid	$$⊢\mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left(P\right)$$
10		eqid	$$⊢{\cdot }_P={\cdot }_P$$
11		eqid	$$⊢1_{\mathrm{Scalar}\left(P\right)}=1_{\mathrm{Scalar}\left(P\right)}$$
12	7 9 10 11	lmodvs1	$$⊢\left(P\in \mathrm{LMod}\wedge F\underset{\dot{}}{\times }X\in {\mathrm{Base}}_P\right)\to 1_{\mathrm{Scalar}\left(P\right)}{\cdot }_P\left(F\underset{\dot{}}{\times }X\right)=F\underset{\dot{}}{\times }X$$
13	6 8 12	syl2an2r	$$⊢\left(R\in \mathrm{Ring}\wedge F\in {\mathbb{N}}_0\right)\to 1_{\mathrm{Scalar}\left(P\right)}{\cdot }_P\left(F\underset{\dot{}}{\times }X\right)=F\underset{\dot{}}{\times }X$$
14	13	fveq2d	$$⊢\left(R\in \mathrm{Ring}\wedge F\in {\mathbb{N}}_0\right)\to D\left(1_{\mathrm{Scalar}\left(P\right)}{\cdot }_P\left(F\underset{\dot{}}{\times }X\right)\right)=D\left(F\underset{\dot{}}{\times }X\right)$$
15		simpl	$$⊢\left(R\in \mathrm{Ring}\wedge F\in {\mathbb{N}}_0\right)\to R\in \mathrm{Ring}$$
16	2	ply1sca	$$⊢R\in \mathrm{Ring}\to R=\mathrm{Scalar}\left(P\right)$$
17	16	fveq2d	$$⊢R\in \mathrm{Ring}\to 1_R=1_{\mathrm{Scalar}\left(P\right)}$$
18		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
19		eqid	$$⊢1_R=1_R$$
20	18 19	ringidcl	$$⊢R\in \mathrm{Ring}\to 1_R\in {\mathrm{Base}}_R$$
21	17 20	eqeltrrd	$$⊢R\in \mathrm{Ring}\to 1_{\mathrm{Scalar}\left(P\right)}\in {\mathrm{Base}}_R$$
22	21	adantr	$$⊢\left(R\in \mathrm{Ring}\wedge F\in {\mathbb{N}}_0\right)\to 1_{\mathrm{Scalar}\left(P\right)}\in {\mathrm{Base}}_R$$
23		simpr	$$⊢\left(R\in \mathrm{Ring}\wedge F\in {\mathbb{N}}_0\right)\to F\in {\mathbb{N}}_0$$
24	1 18 2 3 10 4 5	deg1tmle	$$⊢\left(R\in \mathrm{Ring}\wedge 1_{\mathrm{Scalar}\left(P\right)}\in {\mathrm{Base}}_R\wedge F\in {\mathbb{N}}_0\right)\to D\left(1_{\mathrm{Scalar}\left(P\right)}{\cdot }_P\left(F\underset{\dot{}}{\times }X\right)\right)\le F$$
25	15 22 23 24	syl3anc	$$⊢\left(R\in \mathrm{Ring}\wedge F\in {\mathbb{N}}_0\right)\to D\left(1_{\mathrm{Scalar}\left(P\right)}{\cdot }_P\left(F\underset{\dot{}}{\times }X\right)\right)\le F$$
26	14 25	eqbrtrrd	$$⊢\left(R\in \mathrm{Ring}\wedge F\in {\mathbb{N}}_0\right)\to D\left(F\underset{\dot{}}{\times }X\right)\le F$$