Metamath Proof Explorer

Theorem rngunsnply1chr2lem1

Description: Lemma for rngunsnply1chr2 . (Contributed by Thierry Arnoux, 8-Nov-2026)

Ref Expression
Hypotheses rngunsnply1chr2.v 
|- V = ( Base ` R )
rngunsnply1chr2.p 
|- P = ( Poly1 ` ( R |`s S ) )
rngunsnply1chr2.u 
|- U = ( Base ` P )
rngunsnply1chr2.q 
|- Q = ( R evalSub1 S )
rngunsnply1chr2.r 
|- ( ph -> R e. CRing )
rngunsnply1chr2.1 
|- ( ph -> R e. NzRing )
rngunsnply1chr2.s 
|- ( ph -> S e. ( SubRing ` R ) )
rngunsnply1chr2.x 
|- ( ph -> X e. V )
rngunsnply1chr2.y 
|- ( ph -> Y e. ( N ` ( S u. { X } ) ) )
rngunsnply1chr2.n 
|- N = ( RingSpan ` R )
rngunsnply1chr2.2 
|- .+ = ( +g ` R )
rngunsnply1chr2.3 
|- .x. = ( .r ` R )
rngunsnply1chr2.4 
|- .^ = ( .g ` ( mulGrp ` R ) )
rngunsnply1chr2.a 
|- ( ph -> A e. S )
rngunsnply1chr2.b 
|- ( ph -> B e. S )
rngunsnply1chr2.5 
|- ( ph -> ( 2 .^ X ) = ( ( A .x. X ) .+ B ) )
rngunsnply1chr2lem.d 
|- D = ( deg1 ` R )
rngunsnply1chr2lem.e 
|- E = ( rem1p ` ( R |`s S ) )
rngunsnply1chr2lem.g 
|- G = ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) )
rngunsnply1chr2lem.h 
|- H = ( F E G )
rngunsnply1chr2lem.f 
|- ( ph -> F e. U )
Assertion rngunsnply1chr2lem1 
|- ( ph -> ( D ` G ) = 2 )

Proof

Step Hyp Ref Expression
1 rngunsnply1chr2.v 
 |-  V = ( Base ` R )
2 rngunsnply1chr2.p 
 |-  P = ( Poly1 ` ( R |`s S ) )
3 rngunsnply1chr2.u 
 |-  U = ( Base ` P )
4 rngunsnply1chr2.q 
 |-  Q = ( R evalSub1 S )
5 rngunsnply1chr2.r 
 |-  ( ph -> R e. CRing )
6 rngunsnply1chr2.1 
 |-  ( ph -> R e. NzRing )
7 rngunsnply1chr2.s 
 |-  ( ph -> S e. ( SubRing ` R ) )
8 rngunsnply1chr2.x 
 |-  ( ph -> X e. V )
9 rngunsnply1chr2.y 
 |-  ( ph -> Y e. ( N ` ( S u. { X } ) ) )
10 rngunsnply1chr2.n 
 |-  N = ( RingSpan ` R )
11 rngunsnply1chr2.2 
 |-  .+ = ( +g ` R )
12 rngunsnply1chr2.3 
 |-  .x. = ( .r ` R )
13 rngunsnply1chr2.4 
 |-  .^ = ( .g ` ( mulGrp ` R ) )
14 rngunsnply1chr2.a 
 |-  ( ph -> A e. S )
15 rngunsnply1chr2.b 
 |-  ( ph -> B e. S )
16 rngunsnply1chr2.5 
 |-  ( ph -> ( 2 .^ X ) = ( ( A .x. X ) .+ B ) )
17 rngunsnply1chr2lem.d 
 |-  D = ( deg1 ` R )
18 rngunsnply1chr2lem.e 
 |-  E = ( rem1p ` ( R |`s S ) )
19 rngunsnply1chr2lem.g 
 |-  G = ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) )
20 rngunsnply1chr2lem.h 
 |-  H = ( F E G )
21 rngunsnply1chr2lem.f 
 |-  ( ph -> F e. U )
22 eqid 
 |-  ( R |`s S ) = ( R |`s S )
23 eqid 
 |-  ( -g ` P ) = ( -g ` P )
24 22 subrgring 
 |-  ( S e. ( SubRing ` R ) -> ( R |`s S ) e. Ring )
25 7 24 syl 
 |-  ( ph -> ( R |`s S ) e. Ring )
26 2 ply1ring 
 |-  ( ( R |`s S ) e. Ring -> P e. Ring )
27 25 26 syl 
 |-  ( ph -> P e. Ring )
28 27 ringgrpd 
 |-  ( ph -> P e. Grp )
29 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
30 29 3 mgpbas 
 |-  U = ( Base ` ( mulGrp ` P ) )
31 eqid 
 |-  ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) )
32 29 ringmgp 
 |-  ( P e. Ring -> ( mulGrp ` P ) e. Mnd )
33 27 32 syl 
 |-  ( ph -> ( mulGrp ` P ) e. Mnd )
34 2nn0 
 |-  2 e. NN0
35 34 a1i 
 |-  ( ph -> 2 e. NN0 )
36 eqid 
 |-  ( var1 ` R ) = ( var1 ` R )
37 36 7 22 2 3 subrgvr1cl 
 |-  ( ph -> ( var1 ` R ) e. U )
38 30 31 33 35 37 mulgnn0cld 
 |-  ( ph -> ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. U )
39 eqid 
 |-  ( +g ` P ) = ( +g ` P )
40 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
41 eqid 
 |-  ( .s ` P ) = ( .s ` P )
42 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
43 2 ply1lmod 
 |-  ( ( R |`s S ) e. Ring -> P e. LMod )
44 25 43 syl 
 |-  ( ph -> P e. LMod )
45 22 subrgbas 
 |-  ( S e. ( SubRing ` R ) -> S = ( Base ` ( R |`s S ) ) )
46 7 45 syl 
 |-  ( ph -> S = ( Base ` ( R |`s S ) ) )
47 ovex 
 |-  ( R |`s S ) e. _V
48 2 ply1sca 
 |-  ( ( R |`s S ) e. _V -> ( R |`s S ) = ( Scalar ` P ) )
49 47 48 ax-mp 
 |-  ( R |`s S ) = ( Scalar ` P )
50 49 fveq2i 
 |-  ( Base ` ( R |`s S ) ) = ( Base ` ( Scalar ` P ) )
51 46 50 eqtrdi 
 |-  ( ph -> S = ( Base ` ( Scalar ` P ) ) )
52 14 51 eleqtrd 
 |-  ( ph -> A e. ( Base ` ( Scalar ` P ) ) )
53 3 40 41 42 44 52 37 lmodvscld 
 |-  ( ph -> ( A ( .s ` P ) ( var1 ` R ) ) e. U )
54 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
55 2 22 54 3 5 7 15 ressasclcl 
 |-  ( ph -> ( ( algSc ` P ) ` B ) e. U )
56 3 39 28 53 55 grpcld 
 |-  ( ph -> ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) e. U )
57 3 23 28 38 56 grpsubcld 
 |-  ( ph -> ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) e. U )
58 19 57 eqeltrid 
 |-  ( ph -> G e. U )
59 22 17 2 3 58 7 ressdeg1 
 |-  ( ph -> ( D ` G ) = ( ( deg1 ` ( R |`s S ) ) ` G ) )
60 19 fveq2i 
 |-  ( ( deg1 ` ( R |`s S ) ) ` G ) = ( ( deg1 ` ( R |`s S ) ) ` ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) )
61 60 a1i 
 |-  ( ph -> ( ( deg1 ` ( R |`s S ) ) ` G ) = ( ( deg1 ` ( R |`s S ) ) ` ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) )
62 eqid 
 |-  ( deg1 ` ( R |`s S ) ) = ( deg1 ` ( R |`s S ) )
63 62 2 3 deg1xrcl 
 |-  ( ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) e. U -> ( ( deg1 ` ( R |`s S ) ) ` ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) e. RR* )
64 56 63 syl 
 |-  ( ph -> ( ( deg1 ` ( R |`s S ) ) ` ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) e. RR* )
65 1xr 
 |-  1 e. RR*
66 65 a1i 
 |-  ( ph -> 1 e. RR* )
67 62 2 3 deg1xrcl 
 |-  ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. U -> ( ( deg1 ` ( R |`s S ) ) ` ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) e. RR* )
68 38 67 syl 
 |-  ( ph -> ( ( deg1 ` ( R |`s S ) ) ` ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) e. RR* )
69 36 7 22 subrgvr1 
 |-  ( ph -> ( var1 ` R ) = ( var1 ` ( R |`s S ) ) )
70 69 37 eqeltrrd 
 |-  ( ph -> ( var1 ` ( R |`s S ) ) e. U )
71 30 31 mulg1 
 |-  ( ( var1 ` ( R |`s S ) ) e. U -> ( 1 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) = ( var1 ` ( R |`s S ) ) )
72 70 71 syl 
 |-  ( ph -> ( 1 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) = ( var1 ` ( R |`s S ) ) )
73 72 69 eqtr4d 
 |-  ( ph -> ( 1 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) = ( var1 ` R ) )
74 73 oveq2d 
 |-  ( ph -> ( A ( .s ` P ) ( 1 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) ) = ( A ( .s ` P ) ( var1 ` R ) ) )
75 74 fveq2d 
 |-  ( ph -> ( ( deg1 ` ( R |`s S ) ) ` ( A ( .s ` P ) ( 1 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) ) ) = ( ( deg1 ` ( R |`s S ) ) ` ( A ( .s ` P ) ( var1 ` R ) ) ) )
76 14 46 eleqtrd 
 |-  ( ph -> A e. ( Base ` ( R |`s S ) ) )
77 1nn0 
 |-  1 e. NN0
78 77 a1i 
 |-  ( ph -> 1 e. NN0 )
79 eqid 
 |-  ( Base ` ( R |`s S ) ) = ( Base ` ( R |`s S ) )
80 eqid 
 |-  ( var1 ` ( R |`s S ) ) = ( var1 ` ( R |`s S ) )
81 62 79 2 80 41 29 31 deg1tmle 
 |-  ( ( ( R |`s S ) e. Ring /\ A e. ( Base ` ( R |`s S ) ) /\ 1 e. NN0 ) -> ( ( deg1 ` ( R |`s S ) ) ` ( A ( .s ` P ) ( 1 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) ) ) <_ 1 )
82 25 76 78 81 syl3anc 
 |-  ( ph -> ( ( deg1 ` ( R |`s S ) ) ` ( A ( .s ` P ) ( 1 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) ) ) <_ 1 )
83 75 82 eqbrtrrd 
 |-  ( ph -> ( ( deg1 ` ( R |`s S ) ) ` ( A ( .s ` P ) ( var1 ` R ) ) ) <_ 1 )
84 62 2 3 deg1xrcl 
 |-  ( ( ( algSc ` P ) ` B ) e. U -> ( ( deg1 ` ( R |`s S ) ) ` ( ( algSc ` P ) ` B ) ) e. RR* )
85 55 84 syl 
 |-  ( ph -> ( ( deg1 ` ( R |`s S ) ) ` ( ( algSc ` P ) ` B ) ) e. RR* )
86 0xr 
 |-  0 e. RR*
87 86 a1i 
 |-  ( ph -> 0 e. RR* )
88 15 46 eleqtrd 
 |-  ( ph -> B e. ( Base ` ( R |`s S ) ) )
89 62 2 79 54 deg1sclle 
 |-  ( ( ( R |`s S ) e. Ring /\ B e. ( Base ` ( R |`s S ) ) ) -> ( ( deg1 ` ( R |`s S ) ) ` ( ( algSc ` P ) ` B ) ) <_ 0 )
90 25 88 89 syl2anc 
 |-  ( ph -> ( ( deg1 ` ( R |`s S ) ) ` ( ( algSc ` P ) ` B ) ) <_ 0 )
91 0lt1 
 |-  0 < 1
92 91 a1i 
 |-  ( ph -> 0 < 1 )
93 85 87 66 90 92 xrlelttrd 
 |-  ( ph -> ( ( deg1 ` ( R |`s S ) ) ` ( ( algSc ` P ) ` B ) ) < 1 )
94 85 66 93 xrltled 
 |-  ( ph -> ( ( deg1 ` ( R |`s S ) ) ` ( ( algSc ` P ) ` B ) ) <_ 1 )
95 2 62 25 3 39 53 55 66 83 94 deg1addle2 
 |-  ( ph -> ( ( deg1 ` ( R |`s S ) ) ` ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) <_ 1 )
96 1lt2 
 |-  1 < 2
97 69 oveq2d 
 |-  ( ph -> ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) )
98 97 fveq2d 
 |-  ( ph -> ( ( deg1 ` ( R |`s S ) ) ` ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( ( deg1 ` ( R |`s S ) ) ` ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) ) )
99 22 subrgnzr 
 |-  ( ( R e. NzRing /\ S e. ( SubRing ` R ) ) -> ( R |`s S ) e. NzRing )
100 6 7 99 syl2anc 
 |-  ( ph -> ( R |`s S ) e. NzRing )
101 62 2 80 29 31 deg1pw 
 |-  ( ( ( R |`s S ) e. NzRing /\ 2 e. NN0 ) -> ( ( deg1 ` ( R |`s S ) ) ` ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) ) = 2 )
102 100 35 101 syl2anc 
 |-  ( ph -> ( ( deg1 ` ( R |`s S ) ) ` ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) ) = 2 )
103 98 102 eqtrd 
 |-  ( ph -> ( ( deg1 ` ( R |`s S ) ) ` ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = 2 )
104 96 103 breqtrrid 
 |-  ( ph -> 1 < ( ( deg1 ` ( R |`s S ) ) ` ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
105 64 66 68 95 104 xrlelttrd 
 |-  ( ph -> ( ( deg1 ` ( R |`s S ) ) ` ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) < ( ( deg1 ` ( R |`s S ) ) ` ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
106 2 62 25 3 23 38 56 105 deg1sub 
 |-  ( ph -> ( ( deg1 ` ( R |`s S ) ) ` ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) = ( ( deg1 ` ( R |`s S ) ) ` ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
107 106 103 eqtrd 
 |-  ( ph -> ( ( deg1 ` ( R |`s S ) ) ` ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) = 2 )
108 59 61 107 3eqtrd 
 |-  ( ph -> ( D ` G ) = 2 )