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 
|- D = ( deg1 ` R )
deg1vr.2 
|- P = ( Poly1 ` R )
deg1vr.3 
|- X = ( var1 ` R )
deg1vr.4 
|- ( ph -> R e. NzRing )
Assertion deg1vr 
|- ( ph -> ( D ` X ) = 1 )

Proof

Step Hyp Ref Expression
1 deg1vr.1 
 |-  D = ( deg1 ` R )
2 deg1vr.2 
 |-  P = ( Poly1 ` R )
3 deg1vr.3 
 |-  X = ( var1 ` R )
4 deg1vr.4 
 |-  ( ph -> R e. NzRing )
5 nzrring 
 |-  ( R e. NzRing -> R e. Ring )
6 4 5 syl 
 |-  ( ph -> R e. Ring )
7 2 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
8 6 7 syl 
 |-  ( ph -> R = ( Scalar ` P ) )
9 8 fveq2d 
 |-  ( ph -> ( 1r ` R ) = ( 1r ` ( Scalar ` P ) ) )
10 9 oveq1d 
 |-  ( ph -> ( ( 1r ` R ) ( .s ` P ) ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) = ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) )
11 2 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
12 6 11 syl 
 |-  ( ph -> P e. LMod )
13 eqid 
 |-  ( Base ` P ) = ( Base ` P )
14 3 2 13 vr1cl 
 |-  ( R e. Ring -> X e. ( Base ` P ) )
15 6 14 syl 
 |-  ( ph -> X e. ( Base ` P ) )
16 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
17 16 13 mgpbas 
 |-  ( Base ` P ) = ( Base ` ( mulGrp ` P ) )
18 eqid 
 |-  ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) )
19 17 18 mulg1 
 |-  ( X e. ( Base ` P ) -> ( 1 ( .g ` ( mulGrp ` P ) ) X ) = X )
20 15 19 syl 
 |-  ( ph -> ( 1 ( .g ` ( mulGrp ` P ) ) X ) = X )
21 20 15 eqeltrd 
 |-  ( ph -> ( 1 ( .g ` ( mulGrp ` P ) ) X ) e. ( Base ` P ) )
22 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
23 eqid 
 |-  ( .s ` P ) = ( .s ` P )
24 eqid 
 |-  ( 1r ` ( Scalar ` P ) ) = ( 1r ` ( Scalar ` P ) )
25 13 22 23 24 lmodvs1 
 |-  ( ( P e. LMod /\ ( 1 ( .g ` ( mulGrp ` P ) ) X ) e. ( Base ` P ) ) -> ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) = ( 1 ( .g ` ( mulGrp ` P ) ) X ) )
26 12 21 25 syl2anc 
 |-  ( ph -> ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) = ( 1 ( .g ` ( mulGrp ` P ) ) X ) )
27 10 26 20 3eqtrd 
 |-  ( ph -> ( ( 1r ` R ) ( .s ` P ) ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) = X )
28 27 fveq2d 
 |-  ( ph -> ( D ` ( ( 1r ` R ) ( .s ` P ) ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) ) = ( D ` X ) )
29 eqid 
 |-  ( Base ` R ) = ( Base ` R )
30 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
31 29 30 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
32 6 31 syl 
 |-  ( ph -> ( 1r ` R ) e. ( Base ` R ) )
33 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
34 30 33 nzrnz 
 |-  ( R e. NzRing -> ( 1r ` R ) =/= ( 0g ` R ) )
35 4 34 syl 
 |-  ( ph -> ( 1r ` R ) =/= ( 0g ` R ) )
36 1nn0 
 |-  1 e. NN0
37 36 a1i 
 |-  ( ph -> 1 e. NN0 )
38 1 29 2 3 23 16 18 33 deg1tm 
 |-  ( ( R e. Ring /\ ( ( 1r ` R ) e. ( Base ` R ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) /\ 1 e. NN0 ) -> ( D ` ( ( 1r ` R ) ( .s ` P ) ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) ) = 1 )
39 6 32 35 37 38 syl121anc 
 |-  ( ph -> ( D ` ( ( 1r ` R ) ( .s ` P ) ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) ) = 1 )
40 28 39 eqtr3d 
 |-  ( ph -> ( D ` X ) = 1 )