Metamath Proof Explorer

Theorem rngunsnply1chr2lem3

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 rngunsnply1chr2lem3 
|- ( ph -> ( ( D ` H ) <_ 1 /\ ( ( Q ` H ) ` X ) = ( ( Q ` F ) ` X ) ) )

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 20 fveq2i 
 |-  ( D ` H ) = ( D ` ( F E G ) )
23 eqid 
 |-  ( R |`s S ) = ( R |`s S )
24 23 subrgring 
 |-  ( S e. ( SubRing ` R ) -> ( R |`s S ) e. Ring )
25 7 24 syl 
 |-  ( ph -> ( R |`s S ) e. Ring )
26 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 rngunsnply1chr2lem2 
 |-  ( ph -> G e. ( Unic1p ` ( R |`s S ) ) )
27 eqid 
 |-  ( Unic1p ` ( R |`s S ) ) = ( Unic1p ` ( R |`s S ) )
28 18 2 3 27 r1pcl 
 |-  ( ( ( R |`s S ) e. Ring /\ F e. U /\ G e. ( Unic1p ` ( R |`s S ) ) ) -> ( F E G ) e. U )
29 25 21 26 28 syl3anc 
 |-  ( ph -> ( F E G ) e. U )
30 23 17 2 3 29 7 ressdeg1 
 |-  ( ph -> ( D ` ( F E G ) ) = ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) )
31 22 30 eqtrid 
 |-  ( ph -> ( D ` H ) = ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) )
32 simpr 
 |-  ( ( ph /\ ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) e. NN0 ) -> ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) e. NN0 )
33 1nn0 
 |-  1 e. NN0
34 33 a1i 
 |-  ( ( ph /\ ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) e. NN0 ) -> 1 e. NN0 )
35 eqid 
 |-  ( deg1 ` ( R |`s S ) ) = ( deg1 ` ( R |`s S ) )
36 18 2 3 27 35 r1pdeglt 
 |-  ( ( ( R |`s S ) e. Ring /\ F e. U /\ G e. ( Unic1p ` ( R |`s S ) ) ) -> ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) < ( ( deg1 ` ( R |`s S ) ) ` G ) )
37 25 21 26 36 syl3anc 
 |-  ( ph -> ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) < ( ( deg1 ` ( R |`s S ) ) ` G ) )
38 37 adantr 
 |-  ( ( ph /\ ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) e. NN0 ) -> ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) < ( ( deg1 ` ( R |`s S ) ) ` G ) )
39 1p1e2 
 |-  ( 1 + 1 ) = 2
40 2 3 27 uc1pcl 
 |-  ( G e. ( Unic1p ` ( R |`s S ) ) -> G e. U )
41 26 40 syl 
 |-  ( ph -> G e. U )
42 23 17 2 3 41 7 ressdeg1 
 |-  ( ph -> ( D ` G ) = ( ( deg1 ` ( R |`s S ) ) ` G ) )
43 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 rngunsnply1chr2lem1 
 |-  ( ph -> ( D ` G ) = 2 )
44 42 43 eqtr3d 
 |-  ( ph -> ( ( deg1 ` ( R |`s S ) ) ` G ) = 2 )
45 39 44 eqtr4id 
 |-  ( ph -> ( 1 + 1 ) = ( ( deg1 ` ( R |`s S ) ) ` G ) )
46 45 adantr 
 |-  ( ( ph /\ ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) e. NN0 ) -> ( 1 + 1 ) = ( ( deg1 ` ( R |`s S ) ) ` G ) )
47 38 46 breqtrrd 
 |-  ( ( ph /\ ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) e. NN0 ) -> ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) < ( 1 + 1 ) )
48 nn0leltp1 
 |-  ( ( ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) e. NN0 /\ 1 e. NN0 ) -> ( ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) <_ 1 <-> ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) < ( 1 + 1 ) ) )
49 48 biimpar 
 |-  ( ( ( ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) e. NN0 /\ 1 e. NN0 ) /\ ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) < ( 1 + 1 ) ) -> ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) <_ 1 )
50 32 34 47 49 syl21anc 
 |-  ( ( ph /\ ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) e. NN0 ) -> ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) <_ 1 )
51 simpr 
 |-  ( ( ph /\ ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) = -oo ) -> ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) = -oo )
52 1xr 
 |-  1 e. RR*
53 mnfle 
 |-  ( 1 e. RR* -> -oo <_ 1 )
54 52 53 ax-mp 
 |-  -oo <_ 1
55 51 54 eqbrtrdi 
 |-  ( ( ph /\ ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) = -oo ) -> ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) <_ 1 )
56 35 2 3 deg1cl 
 |-  ( ( F E G ) e. U -> ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) e. ( NN0 u. { -oo } ) )
57 29 56 syl 
 |-  ( ph -> ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) e. ( NN0 u. { -oo } ) )
58 fvex 
 |-  ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) e. _V
59 elunsn 
 |-  ( ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) e. _V -> ( ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) e. ( NN0 u. { -oo } ) <-> ( ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) e. NN0 \/ ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) = -oo ) ) )
60 58 59 ax-mp 
 |-  ( ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) e. ( NN0 u. { -oo } ) <-> ( ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) e. NN0 \/ ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) = -oo ) )
61 57 60 sylib 
 |-  ( ph -> ( ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) e. NN0 \/ ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) = -oo ) )
62 50 55 61 mpjaodan 
 |-  ( ph -> ( ( deg1 ` ( R |`s S ) ) ` ( F E G ) ) <_ 1 )
63 31 62 eqbrtrd 
 |-  ( ph -> ( D ` H ) <_ 1 )
64 eqid 
 |-  ( +g ` P ) = ( +g ` P )
65 eqid 
 |-  ( .r ` P ) = ( .r ` P )
66 2 ply1ring 
 |-  ( ( R |`s S ) e. Ring -> P e. Ring )
67 25 66 syl 
 |-  ( ph -> P e. Ring )
68 eqid 
 |-  ( quot1p ` ( R |`s S ) ) = ( quot1p ` ( R |`s S ) )
69 68 2 3 27 q1pcl 
 |-  ( ( ( R |`s S ) e. Ring /\ F e. U /\ G e. ( Unic1p ` ( R |`s S ) ) ) -> ( F ( quot1p ` ( R |`s S ) ) G ) e. U )
70 25 21 26 69 syl3anc 
 |-  ( ph -> ( F ( quot1p ` ( R |`s S ) ) G ) e. U )
71 3 65 67 70 41 ringcld 
 |-  ( ph -> ( ( F ( quot1p ` ( R |`s S ) ) G ) ( .r ` P ) G ) e. U )
72 4 1 2 23 3 64 11 5 7 71 29 8 evls1addd 
 |-  ( ph -> ( ( Q ` ( ( ( F ( quot1p ` ( R |`s S ) ) G ) ( .r ` P ) G ) ( +g ` P ) ( F E G ) ) ) ` X ) = ( ( ( Q ` ( ( F ( quot1p ` ( R |`s S ) ) G ) ( .r ` P ) G ) ) ` X ) .+ ( ( Q ` ( F E G ) ) ` X ) ) )
73 4 1 2 23 3 65 12 5 7 70 41 8 evls1muld 
 |-  ( ph -> ( ( Q ` ( ( F ( quot1p ` ( R |`s S ) ) G ) ( .r ` P ) G ) ) ` X ) = ( ( ( Q ` ( F ( quot1p ` ( R |`s S ) ) G ) ) ` X ) .x. ( ( Q ` G ) ` X ) ) )
74 19 fveq2i 
 |-  ( Q ` G ) = ( Q ` ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) )
75 74 fveq1i 
 |-  ( ( Q ` G ) ` X ) = ( ( Q ` ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ` X )
76 75 a1i 
 |-  ( ph -> ( ( Q ` G ) ` X ) = ( ( Q ` ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ` X ) )
77 eqid 
 |-  ( -g ` P ) = ( -g ` P )
78 eqid 
 |-  ( -g ` R ) = ( -g ` R )
79 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
80 79 3 mgpbas 
 |-  U = ( Base ` ( mulGrp ` P ) )
81 eqid 
 |-  ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) )
82 79 ringmgp 
 |-  ( P e. Ring -> ( mulGrp ` P ) e. Mnd )
83 67 82 syl 
 |-  ( ph -> ( mulGrp ` P ) e. Mnd )
84 2nn0 
 |-  2 e. NN0
85 84 a1i 
 |-  ( ph -> 2 e. NN0 )
86 eqid 
 |-  ( var1 ` R ) = ( var1 ` R )
87 86 7 23 2 3 subrgvr1cl 
 |-  ( ph -> ( var1 ` R ) e. U )
88 80 81 83 85 87 mulgnn0cld 
 |-  ( ph -> ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. U )
89 67 ringgrpd 
 |-  ( ph -> P e. Grp )
90 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
91 eqid 
 |-  ( .s ` P ) = ( .s ` P )
92 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
93 2 ply1lmod 
 |-  ( ( R |`s S ) e. Ring -> P e. LMod )
94 25 93 syl 
 |-  ( ph -> P e. LMod )
95 23 subrgbas 
 |-  ( S e. ( SubRing ` R ) -> S = ( Base ` ( R |`s S ) ) )
96 7 95 syl 
 |-  ( ph -> S = ( Base ` ( R |`s S ) ) )
97 ovex 
 |-  ( R |`s S ) e. _V
98 2 ply1sca 
 |-  ( ( R |`s S ) e. _V -> ( R |`s S ) = ( Scalar ` P ) )
99 97 98 ax-mp 
 |-  ( R |`s S ) = ( Scalar ` P )
100 99 fveq2i 
 |-  ( Base ` ( R |`s S ) ) = ( Base ` ( Scalar ` P ) )
101 96 100 eqtrdi 
 |-  ( ph -> S = ( Base ` ( Scalar ` P ) ) )
102 14 101 eleqtrd 
 |-  ( ph -> A e. ( Base ` ( Scalar ` P ) ) )
103 3 90 91 92 94 102 87 lmodvscld 
 |-  ( ph -> ( A ( .s ` P ) ( var1 ` R ) ) e. U )
104 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
105 2 23 104 3 5 7 15 ressasclcl 
 |-  ( ph -> ( ( algSc ` P ) ` B ) e. U )
106 3 64 89 103 105 grpcld 
 |-  ( ph -> ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) e. U )
107 4 1 2 23 3 77 78 5 7 88 106 8 evls1subd 
 |-  ( ph -> ( ( Q ` ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ` X ) = ( ( ( Q ` ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ` X ) ( -g ` R ) ( ( Q ` ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ` X ) ) )
108 4 1 2 23 3 5 7 81 13 85 87 8 evls1expd 
 |-  ( ph -> ( ( Q ` ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ` X ) = ( 2 .^ ( ( Q ` ( var1 ` R ) ) ` X ) ) )
109 86 7 23 subrgvr1 
 |-  ( ph -> ( var1 ` R ) = ( var1 ` ( R |`s S ) ) )
110 109 fveq2d 
 |-  ( ph -> ( Q ` ( var1 ` R ) ) = ( Q ` ( var1 ` ( R |`s S ) ) ) )
111 110 fveq1d 
 |-  ( ph -> ( ( Q ` ( var1 ` R ) ) ` X ) = ( ( Q ` ( var1 ` ( R |`s S ) ) ) ` X ) )
112 eqid 
 |-  ( var1 ` ( R |`s S ) ) = ( var1 ` ( R |`s S ) )
113 4 112 23 1 5 7 evls1var 
 |-  ( ph -> ( Q ` ( var1 ` ( R |`s S ) ) ) = ( _I |` V ) )
114 113 fveq1d 
 |-  ( ph -> ( ( Q ` ( var1 ` ( R |`s S ) ) ) ` X ) = ( ( _I |` V ) ` X ) )
115 fvresi 
 |-  ( X e. V -> ( ( _I |` V ) ` X ) = X )
116 8 115 syl 
 |-  ( ph -> ( ( _I |` V ) ` X ) = X )
117 111 114 116 3eqtrd 
 |-  ( ph -> ( ( Q ` ( var1 ` R ) ) ` X ) = X )
118 117 oveq2d 
 |-  ( ph -> ( 2 .^ ( ( Q ` ( var1 ` R ) ) ` X ) ) = ( 2 .^ X ) )
119 108 118 eqtrd 
 |-  ( ph -> ( ( Q ` ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ` X ) = ( 2 .^ X ) )
120 4 1 2 23 3 64 11 5 7 103 105 8 evls1addd 
 |-  ( ph -> ( ( Q ` ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ` X ) = ( ( ( Q ` ( A ( .s ` P ) ( var1 ` R ) ) ) ` X ) .+ ( ( Q ` ( ( algSc ` P ) ` B ) ) ` X ) ) )
121 4 1 2 23 3 91 12 5 7 14 87 8 evls1vsca 
 |-  ( ph -> ( ( Q ` ( A ( .s ` P ) ( var1 ` R ) ) ) ` X ) = ( A .x. ( ( Q ` ( var1 ` R ) ) ` X ) ) )
122 117 oveq2d 
 |-  ( ph -> ( A .x. ( ( Q ` ( var1 ` R ) ) ` X ) ) = ( A .x. X ) )
123 121 122 eqtrd 
 |-  ( ph -> ( ( Q ` ( A ( .s ` P ) ( var1 ` R ) ) ) ` X ) = ( A .x. X ) )
124 4 2 23 1 104 5 7 15 8 evls1scafv 
 |-  ( ph -> ( ( Q ` ( ( algSc ` P ) ` B ) ) ` X ) = B )
125 123 124 oveq12d 
 |-  ( ph -> ( ( ( Q ` ( A ( .s ` P ) ( var1 ` R ) ) ) ` X ) .+ ( ( Q ` ( ( algSc ` P ) ` B ) ) ` X ) ) = ( ( A .x. X ) .+ B ) )
126 120 125 eqtrd 
 |-  ( ph -> ( ( Q ` ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ` X ) = ( ( A .x. X ) .+ B ) )
127 119 126 oveq12d 
 |-  ( ph -> ( ( ( Q ` ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ` X ) ( -g ` R ) ( ( Q ` ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ` X ) ) = ( ( 2 .^ X ) ( -g ` R ) ( ( A .x. X ) .+ B ) ) )
128 5 crnggrpd 
 |-  ( ph -> R e. Grp )
129 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
130 129 1 mgpbas 
 |-  V = ( Base ` ( mulGrp ` R ) )
131 5 crngringd 
 |-  ( ph -> R e. Ring )
132 129 ringmgp 
 |-  ( R e. Ring -> ( mulGrp ` R ) e. Mnd )
133 131 132 syl 
 |-  ( ph -> ( mulGrp ` R ) e. Mnd )
134 130 13 133 85 8 mulgnn0cld 
 |-  ( ph -> ( 2 .^ X ) e. V )
135 16 134 eqeltrrd 
 |-  ( ph -> ( ( A .x. X ) .+ B ) e. V )
136 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
137 1 136 78 grpsubeq0 
 |-  ( ( R e. Grp /\ ( 2 .^ X ) e. V /\ ( ( A .x. X ) .+ B ) e. V ) -> ( ( ( 2 .^ X ) ( -g ` R ) ( ( A .x. X ) .+ B ) ) = ( 0g ` R ) <-> ( 2 .^ X ) = ( ( A .x. X ) .+ B ) ) )
138 137 biimpar 
 |-  ( ( ( R e. Grp /\ ( 2 .^ X ) e. V /\ ( ( A .x. X ) .+ B ) e. V ) /\ ( 2 .^ X ) = ( ( A .x. X ) .+ B ) ) -> ( ( 2 .^ X ) ( -g ` R ) ( ( A .x. X ) .+ B ) ) = ( 0g ` R ) )
139 128 134 135 16 138 syl31anc 
 |-  ( ph -> ( ( 2 .^ X ) ( -g ` R ) ( ( A .x. X ) .+ B ) ) = ( 0g ` R ) )
140 127 139 eqtrd 
 |-  ( ph -> ( ( ( Q ` ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ` X ) ( -g ` R ) ( ( Q ` ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ` X ) ) = ( 0g ` R ) )
141 76 107 140 3eqtrd 
 |-  ( ph -> ( ( Q ` G ) ` X ) = ( 0g ` R ) )
142 141 oveq2d 
 |-  ( ph -> ( ( ( Q ` ( F ( quot1p ` ( R |`s S ) ) G ) ) ` X ) .x. ( ( Q ` G ) ` X ) ) = ( ( ( Q ` ( F ( quot1p ` ( R |`s S ) ) G ) ) ` X ) .x. ( 0g ` R ) ) )
143 4 2 1 3 5 7 8 70 evls1fvcl 
 |-  ( ph -> ( ( Q ` ( F ( quot1p ` ( R |`s S ) ) G ) ) ` X ) e. V )
144 1 12 136 131 143 ringrzd 
 |-  ( ph -> ( ( ( Q ` ( F ( quot1p ` ( R |`s S ) ) G ) ) ` X ) .x. ( 0g ` R ) ) = ( 0g ` R ) )
145 73 142 144 3eqtrd 
 |-  ( ph -> ( ( Q ` ( ( F ( quot1p ` ( R |`s S ) ) G ) ( .r ` P ) G ) ) ` X ) = ( 0g ` R ) )
146 145 oveq1d 
 |-  ( ph -> ( ( ( Q ` ( ( F ( quot1p ` ( R |`s S ) ) G ) ( .r ` P ) G ) ) ` X ) .+ ( ( Q ` ( F E G ) ) ` X ) ) = ( ( 0g ` R ) .+ ( ( Q ` ( F E G ) ) ` X ) ) )
147 4 2 1 3 5 7 8 29 evls1fvcl 
 |-  ( ph -> ( ( Q ` ( F E G ) ) ` X ) e. V )
148 1 11 136 128 147 grplidd 
 |-  ( ph -> ( ( 0g ` R ) .+ ( ( Q ` ( F E G ) ) ` X ) ) = ( ( Q ` ( F E G ) ) ` X ) )
149 72 146 148 3eqtrd 
 |-  ( ph -> ( ( Q ` ( ( ( F ( quot1p ` ( R |`s S ) ) G ) ( .r ` P ) G ) ( +g ` P ) ( F E G ) ) ) ` X ) = ( ( Q ` ( F E G ) ) ` X ) )
150 2 3 27 68 18 65 64 r1pid 
 |-  ( ( ( R |`s S ) e. Ring /\ F e. U /\ G e. ( Unic1p ` ( R |`s S ) ) ) -> F = ( ( ( F ( quot1p ` ( R |`s S ) ) G ) ( .r ` P ) G ) ( +g ` P ) ( F E G ) ) )
151 25 21 26 150 syl3anc 
 |-  ( ph -> F = ( ( ( F ( quot1p ` ( R |`s S ) ) G ) ( .r ` P ) G ) ( +g ` P ) ( F E G ) ) )
152 151 fveq2d 
 |-  ( ph -> ( Q ` F ) = ( Q ` ( ( ( F ( quot1p ` ( R |`s S ) ) G ) ( .r ` P ) G ) ( +g ` P ) ( F E G ) ) ) )
153 152 fveq1d 
 |-  ( ph -> ( ( Q ` F ) ` X ) = ( ( Q ` ( ( ( F ( quot1p ` ( R |`s S ) ) G ) ( .r ` P ) G ) ( +g ` P ) ( F E G ) ) ) ` X ) )
154 20 fveq2i 
 |-  ( Q ` H ) = ( Q ` ( F E G ) )
155 154 fveq1i 
 |-  ( ( Q ` H ) ` X ) = ( ( Q ` ( F E G ) ) ` X )
156 155 a1i 
 |-  ( ph -> ( ( Q ` H ) ` X ) = ( ( Q ` ( F E G ) ) ` X ) )
157 149 153 156 3eqtr4rd 
 |-  ( ph -> ( ( Q ` H ) ` X ) = ( ( Q ` F ) ` X ) )
158 63 157 jca 
 |-  ( ph -> ( ( D ` H ) <_ 1 /\ ( ( Q ` H ) ` X ) = ( ( Q ` F ) ` X ) ) )