Theorem deg1vr

Description: The degree of the variable polynomial is 1. (Contributed by Thierry Arnoux, 22-Jun-2025)

	Ref	Expression
Hypotheses	deg1vr.1	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	deg1vr.2	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	deg1vr.3	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	deg1vr.4	$$⊢\phi \to R\in \mathrm{NzRing}$$
Assertion	deg1vr	$$⊢\phi \to D\left(X\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		deg1vr.1	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
2		deg1vr.2	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
3		deg1vr.3	$$⊢X={\mathrm{var}}_1\left(R\right)$$
4		deg1vr.4	$$⊢\phi \to R\in \mathrm{NzRing}$$
5		nzrring	$$⊢R\in \mathrm{NzRing}\to R\in \mathrm{Ring}$$
6	4 5	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
7	2	ply1sca	$$⊢R\in \mathrm{Ring}\to R=\mathrm{Scalar}\left(P\right)$$
8	6 7	syl	$$⊢\phi \to R=\mathrm{Scalar}\left(P\right)$$
9	8	fveq2d	$$⊢\phi \to 1_R=1_{\mathrm{Scalar}\left(P\right)}$$
10	9	oveq1d	$$⊢\phi \to 1_R{\cdot }_P\left(1{\cdot }_{{\mathrm{mulGrp}}_P}X\right)=1_{\mathrm{Scalar}\left(P\right)}{\cdot }_P\left(1{\cdot }_{{\mathrm{mulGrp}}_P}X\right)$$
11	2	ply1lmod	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{LMod}$$
12	6 11	syl	$$⊢\phi \to P\in \mathrm{LMod}$$
13		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
14	3 2 13	vr1cl	$$⊢R\in \mathrm{Ring}\to X\in {\mathrm{Base}}_P$$
15	6 14	syl	$$⊢\phi \to X\in {\mathrm{Base}}_P$$
16		eqid	$$⊢{\mathrm{mulGrp}}_P={\mathrm{mulGrp}}_P$$
17	16 13	mgpbas	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_{{\mathrm{mulGrp}}_P}$$
18		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_P}={\cdot }_{{\mathrm{mulGrp}}_P}$$
19	17 18	mulg1	$$⊢X\in {\mathrm{Base}}_P\to 1{\cdot }_{{\mathrm{mulGrp}}_P}X=X$$
20	15 19	syl	$$⊢\phi \to 1{\cdot }_{{\mathrm{mulGrp}}_P}X=X$$
21	20 15	eqeltrd	$$⊢\phi \to 1{\cdot }_{{\mathrm{mulGrp}}_P}X\in {\mathrm{Base}}_P$$
22		eqid	$$⊢\mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left(P\right)$$
23		eqid	$$⊢{\cdot }_P={\cdot }_P$$
24		eqid	$$⊢1_{\mathrm{Scalar}\left(P\right)}=1_{\mathrm{Scalar}\left(P\right)}$$
25	13 22 23 24	lmodvs1	$$⊢\left(P\in \mathrm{LMod}\wedge 1{\cdot }_{{\mathrm{mulGrp}}_P}X\in {\mathrm{Base}}_P\right)\to 1_{\mathrm{Scalar}\left(P\right)}{\cdot }_P\left(1{\cdot }_{{\mathrm{mulGrp}}_P}X\right)=1{\cdot }_{{\mathrm{mulGrp}}_P}X$$
26	12 21 25	syl2anc	$$⊢\phi \to 1_{\mathrm{Scalar}\left(P\right)}{\cdot }_P\left(1{\cdot }_{{\mathrm{mulGrp}}_P}X\right)=1{\cdot }_{{\mathrm{mulGrp}}_P}X$$
27	10 26 20	3eqtrd	$$⊢\phi \to 1_R{\cdot }_P\left(1{\cdot }_{{\mathrm{mulGrp}}_P}X\right)=X$$
28	27	fveq2d	$$⊢\phi \to D\left(1_R{\cdot }_P\left(1{\cdot }_{{\mathrm{mulGrp}}_P}X\right)\right)=D\left(X\right)$$
29		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
30		eqid	$$⊢1_R=1_R$$
31	29 30	ringidcl	$$⊢R\in \mathrm{Ring}\to 1_R\in {\mathrm{Base}}_R$$
32	6 31	syl	$$⊢\phi \to 1_R\in {\mathrm{Base}}_R$$
33		eqid	$$⊢0_R=0_R$$
34	30 33	nzrnz	$$⊢R\in \mathrm{NzRing}\to 1_R\ne 0_R$$
35	4 34	syl	$$⊢\phi \to 1_R\ne 0_R$$
36		1nn0	$$⊢1\in {\mathbb{N}}_0$$
37	36	a1i	$$⊢\phi \to 1\in {\mathbb{N}}_0$$
38	1 29 2 3 23 16 18 33	deg1tm	$$⊢\left(R\in \mathrm{Ring}\wedge \left(1_R\in {\mathrm{Base}}_R\wedge 1_R\ne 0_R\right)\wedge 1\in {\mathbb{N}}_0\right)\to D\left(1_R{\cdot }_P\left(1{\cdot }_{{\mathrm{mulGrp}}_P}X\right)\right)=1$$
39	6 32 35 37 38	syl121anc	$$⊢\phi \to D\left(1_R{\cdot }_P\left(1{\cdot }_{{\mathrm{mulGrp}}_P}X\right)\right)=1$$
40	28 39	eqtr3d	$$⊢\phi \to D\left(X\right)=1$$