Theorem deg1vr

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

	Ref	Expression
Hypotheses	deg1vr.1	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	deg1vr.2	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	deg1vr.3	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	deg1vr.4	⊢ ( 𝜑 → 𝑅 ∈ NzRing )
Assertion	deg1vr	⊢ ( 𝜑 → ( 𝐷 ‘ 𝑋 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		deg1vr.1	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2		deg1vr.2	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		deg1vr.3	⊢ 𝑋 = ( var1 ‘ 𝑅 )
4		deg1vr.4	⊢ ( 𝜑 → 𝑅 ∈ NzRing )
5		nzrring	⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
6	4 5	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
7	2	ply1sca	⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
8	6 7	syl	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
9	8	fveq2d	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = ( 1r ‘ ( Scalar ‘ 𝑃 ) ) )
10	9	oveq1d	⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) = ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) )
11	2	ply1lmod	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
12	6 11	syl	⊢ ( 𝜑 → 𝑃 ∈ LMod )
13		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
14	3 2 13	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
15	6 14	syl	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑃 ) )
16		eqid	⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
17	16 13	mgpbas	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
18		eqid	⊢ ( .g ‘ ( mulGrp ‘ 𝑃 ) ) = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
19	17 18	mulg1	⊢ ( 𝑋 ∈ ( Base ‘ 𝑃 ) → ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) = 𝑋 )
20	15 19	syl	⊢ ( 𝜑 → ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) = 𝑋 )
21	20 15	eqeltrd	⊢ ( 𝜑 → ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
22		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
23		eqid	⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
24		eqid	⊢ ( 1r ‘ ( Scalar ‘ 𝑃 ) ) = ( 1r ‘ ( Scalar ‘ 𝑃 ) )
25	13 22 23 24	lmodvs1	⊢ ( ( 𝑃 ∈ LMod ∧ ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) = ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) )
26	12 21 25	syl2anc	⊢ ( 𝜑 → ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) = ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) )
27	10 26 20	3eqtrd	⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) = 𝑋 )
28	27	fveq2d	⊢ ( 𝜑 → ( 𝐷 ‘ ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) ) = ( 𝐷 ‘ 𝑋 ) )
29		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
30		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
31	29 30	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
32	6 31	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
33		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
34	30 33	nzrnz	⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
35	4 34	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
36		1nn0	⊢ 1 ∈ ℕ0
37	36	a1i	⊢ ( 𝜑 → 1 ∈ ℕ0 )
38	1 29 2 3 23 16 18 33	deg1tm	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) ∧ 1 ∈ ℕ0 ) → ( 𝐷 ‘ ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) ) = 1 )
39	6 32 35 37 38	syl121anc	⊢ ( 𝜑 → ( 𝐷 ‘ ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) ) = 1 )
40	28 39	eqtr3d	⊢ ( 𝜑 → ( 𝐷 ‘ 𝑋 ) = 1 )