This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )