Metamath Proof Explorer

Theorem evls1rgspncl

Description: Closure of the subring polynomial evaluation in a generated ring. Generic version of cnsrplycl . See also evls1fldgencl . (Contributed by Thierry Arnoux, 8-Nov-2026)

Ref Expression
Hypotheses rngunsnply1.b 
|- B = ( Base ` R )
rngunsnply1.p 
|- P = ( Poly1 ` ( R |`s S ) )
rngunsnply1.u 
|- U = ( Base ` P )
rngunsnply1.q 
|- Q = ( R evalSub1 S )
rngunsnply1.r 
|- ( ph -> R e. CRing )
rngunsnply1.s 
|- ( ph -> S e. ( SubRing ` R ) )
rngunsnply1.x 
|- ( ph -> X e. B )
rngunsnply1.n 
|- N = ( RingSpan ` R )
evls1rgspncl.f 
|- ( ph -> F e. U )
Assertion evls1rgspncl 
|- ( ph -> ( ( Q ` F ) ` X ) e. ( N ` ( S u. { X } ) ) )

Proof

Step Hyp Ref Expression
1 rngunsnply1.b 
 |-  B = ( Base ` R )
2 rngunsnply1.p 
 |-  P = ( Poly1 ` ( R |`s S ) )
3 rngunsnply1.u 
 |-  U = ( Base ` P )
4 rngunsnply1.q 
 |-  Q = ( R evalSub1 S )
5 rngunsnply1.r 
 |-  ( ph -> R e. CRing )
6 rngunsnply1.s 
 |-  ( ph -> S e. ( SubRing ` R ) )
7 rngunsnply1.x 
 |-  ( ph -> X e. B )
8 rngunsnply1.n 
 |-  N = ( RingSpan ` R )
9 evls1rgspncl.f 
 |-  ( ph -> F e. U )
10 oveq2 
 |-  ( x = X -> ( i ( .g ` ( mulGrp ` R ) ) x ) = ( i ( .g ` ( mulGrp ` R ) ) X ) )
11 10 oveq2d 
 |-  ( x = X -> ( ( ( coe1 ` F ) ` i ) ( .r ` R ) ( i ( .g ` ( mulGrp ` R ) ) x ) ) = ( ( ( coe1 ` F ) ` i ) ( .r ` R ) ( i ( .g ` ( mulGrp ` R ) ) X ) ) )
12 11 mpteq2dv 
 |-  ( x = X -> ( i e. NN0 |-> ( ( ( coe1 ` F ) ` i ) ( .r ` R ) ( i ( .g ` ( mulGrp ` R ) ) x ) ) ) = ( i e. NN0 |-> ( ( ( coe1 ` F ) ` i ) ( .r ` R ) ( i ( .g ` ( mulGrp ` R ) ) X ) ) ) )
13 12 oveq2d 
 |-  ( x = X -> ( R gsum ( i e. NN0 |-> ( ( ( coe1 ` F ) ` i ) ( .r ` R ) ( i ( .g ` ( mulGrp ` R ) ) x ) ) ) ) = ( R gsum ( i e. NN0 |-> ( ( ( coe1 ` F ) ` i ) ( .r ` R ) ( i ( .g ` ( mulGrp ` R ) ) X ) ) ) ) )
14 eqid 
 |-  ( R |`s S ) = ( R |`s S )
15 eqid 
 |-  ( .r ` R ) = ( .r ` R )
16 eqid 
 |-  ( .g ` ( mulGrp ` R ) ) = ( .g ` ( mulGrp ` R ) )
17 eqid 
 |-  ( coe1 ` F ) = ( coe1 ` F )
18 4 1 2 14 3 5 6 9 15 16 17 evls1fpws 
 |-  ( ph -> ( Q ` F ) = ( x e. B |-> ( R gsum ( i e. NN0 |-> ( ( ( coe1 ` F ) ` i ) ( .r ` R ) ( i ( .g ` ( mulGrp ` R ) ) x ) ) ) ) ) )
19 ovexd 
 |-  ( ph -> ( R gsum ( i e. NN0 |-> ( ( ( coe1 ` F ) ` i ) ( .r ` R ) ( i ( .g ` ( mulGrp ` R ) ) X ) ) ) ) e. _V )
20 13 18 7 19 fvmptd4 
 |-  ( ph -> ( ( Q ` F ) ` X ) = ( R gsum ( i e. NN0 |-> ( ( ( coe1 ` F ) ` i ) ( .r ` R ) ( i ( .g ` ( mulGrp ` R ) ) X ) ) ) ) )
21 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
22 5 crngringd 
 |-  ( ph -> R e. Ring )
23 22 ringabld 
 |-  ( ph -> R e. Abel )
24 nn0ex 
 |-  NN0 e. _V
25 24 a1i 
 |-  ( ph -> NN0 e. _V )
26 1 a1i 
 |-  ( ph -> B = ( Base ` R ) )
27 1 subrgss 
 |-  ( S e. ( SubRing ` R ) -> S C_ B )
28 6 27 syl 
 |-  ( ph -> S C_ B )
29 7 snssd 
 |-  ( ph -> { X } C_ B )
30 28 29 unssd 
 |-  ( ph -> ( S u. { X } ) C_ B )
31 8 a1i 
 |-  ( ph -> N = ( RingSpan ` R ) )
32 eqidd 
 |-  ( ph -> ( N ` ( S u. { X } ) ) = ( N ` ( S u. { X } ) ) )
33 22 26 30 31 32 rgspncl 
 |-  ( ph -> ( N ` ( S u. { X } ) ) e. ( SubRing ` R ) )
34 subrgsubg 
 |-  ( ( N ` ( S u. { X } ) ) e. ( SubRing ` R ) -> ( N ` ( S u. { X } ) ) e. ( SubGrp ` R ) )
35 33 34 syl 
 |-  ( ph -> ( N ` ( S u. { X } ) ) e. ( SubGrp ` R ) )
36 33 adantr 
 |-  ( ( ph /\ i e. NN0 ) -> ( N ` ( S u. { X } ) ) e. ( SubRing ` R ) )
37 22 26 30 31 32 rgspnssid 
 |-  ( ph -> ( S u. { X } ) C_ ( N ` ( S u. { X } ) ) )
38 37 adantr 
 |-  ( ( ph /\ i e. NN0 ) -> ( S u. { X } ) C_ ( N ` ( S u. { X } ) ) )
39 38 unssad 
 |-  ( ( ph /\ i e. NN0 ) -> S C_ ( N ` ( S u. { X } ) ) )
40 eqid 
 |-  ( Base ` ( R |`s S ) ) = ( Base ` ( R |`s S ) )
41 17 3 2 40 coe1fvalcl 
 |-  ( ( F e. U /\ i e. NN0 ) -> ( ( coe1 ` F ) ` i ) e. ( Base ` ( R |`s S ) ) )
42 9 41 sylan 
 |-  ( ( ph /\ i e. NN0 ) -> ( ( coe1 ` F ) ` i ) e. ( Base ` ( R |`s S ) ) )
43 14 1 ressbas2 
 |-  ( S C_ B -> S = ( Base ` ( R |`s S ) ) )
44 28 43 syl 
 |-  ( ph -> S = ( Base ` ( R |`s S ) ) )
45 44 adantr 
 |-  ( ( ph /\ i e. NN0 ) -> S = ( Base ` ( R |`s S ) ) )
46 42 45 eleqtrrd 
 |-  ( ( ph /\ i e. NN0 ) -> ( ( coe1 ` F ) ` i ) e. S )
47 39 46 sseldd 
 |-  ( ( ph /\ i e. NN0 ) -> ( ( coe1 ` F ) ` i ) e. ( N ` ( S u. { X } ) ) )
48 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
49 48 subrgsubm 
 |-  ( ( N ` ( S u. { X } ) ) e. ( SubRing ` R ) -> ( N ` ( S u. { X } ) ) e. ( SubMnd ` ( mulGrp ` R ) ) )
50 33 49 syl 
 |-  ( ph -> ( N ` ( S u. { X } ) ) e. ( SubMnd ` ( mulGrp ` R ) ) )
51 50 adantr 
 |-  ( ( ph /\ i e. NN0 ) -> ( N ` ( S u. { X } ) ) e. ( SubMnd ` ( mulGrp ` R ) ) )
52 simpr 
 |-  ( ( ph /\ i e. NN0 ) -> i e. NN0 )
53 ssun2 
 |-  { X } C_ ( S u. { X } )
54 snidg 
 |-  ( X e. B -> X e. { X } )
55 7 54 syl 
 |-  ( ph -> X e. { X } )
56 53 55 sselid 
 |-  ( ph -> X e. ( S u. { X } ) )
57 37 56 sseldd 
 |-  ( ph -> X e. ( N ` ( S u. { X } ) ) )
58 57 adantr 
 |-  ( ( ph /\ i e. NN0 ) -> X e. ( N ` ( S u. { X } ) ) )
59 16 submmulgcl 
 |-  ( ( ( N ` ( S u. { X } ) ) e. ( SubMnd ` ( mulGrp ` R ) ) /\ i e. NN0 /\ X e. ( N ` ( S u. { X } ) ) ) -> ( i ( .g ` ( mulGrp ` R ) ) X ) e. ( N ` ( S u. { X } ) ) )
60 51 52 58 59 syl3anc 
 |-  ( ( ph /\ i e. NN0 ) -> ( i ( .g ` ( mulGrp ` R ) ) X ) e. ( N ` ( S u. { X } ) ) )
61 15 36 47 60 subrgmcld 
 |-  ( ( ph /\ i e. NN0 ) -> ( ( ( coe1 ` F ) ` i ) ( .r ` R ) ( i ( .g ` ( mulGrp ` R ) ) X ) ) e. ( N ` ( S u. { X } ) ) )
62 61 fmpttd 
 |-  ( ph -> ( i e. NN0 |-> ( ( ( coe1 ` F ) ` i ) ( .r ` R ) ( i ( .g ` ( mulGrp ` R ) ) X ) ) ) : NN0 --> ( N ` ( S u. { X } ) ) )
63 14 subrgring 
 |-  ( S e. ( SubRing ` R ) -> ( R |`s S ) e. Ring )
64 6 63 syl 
 |-  ( ph -> ( R |`s S ) e. Ring )
65 eqid 
 |-  ( 0g ` ( R |`s S ) ) = ( 0g ` ( R |`s S ) )
66 2 3 65 mptcoe1fsupp 
 |-  ( ( ( R |`s S ) e. Ring /\ F e. U ) -> ( i e. NN0 |-> ( ( coe1 ` F ) ` i ) ) finSupp ( 0g ` ( R |`s S ) ) )
67 64 9 66 syl2anc 
 |-  ( ph -> ( i e. NN0 |-> ( ( coe1 ` F ) ` i ) ) finSupp ( 0g ` ( R |`s S ) ) )
68 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
69 22 68 syl 
 |-  ( ph -> R e. Mnd )
70 subrgsubg 
 |-  ( S e. ( SubRing ` R ) -> S e. ( SubGrp ` R ) )
71 6 70 syl 
 |-  ( ph -> S e. ( SubGrp ` R ) )
72 subgsubm 
 |-  ( S e. ( SubGrp ` R ) -> S e. ( SubMnd ` R ) )
73 21 subm0cl 
 |-  ( S e. ( SubMnd ` R ) -> ( 0g ` R ) e. S )
74 71 72 73 3syl 
 |-  ( ph -> ( 0g ` R ) e. S )
75 14 1 21 ress0g 
 |-  ( ( R e. Mnd /\ ( 0g ` R ) e. S /\ S C_ B ) -> ( 0g ` R ) = ( 0g ` ( R |`s S ) ) )
76 69 74 28 75 syl3anc 
 |-  ( ph -> ( 0g ` R ) = ( 0g ` ( R |`s S ) ) )
77 67 76 breqtrrd 
 |-  ( ph -> ( i e. NN0 |-> ( ( coe1 ` F ) ` i ) ) finSupp ( 0g ` R ) )
78 22 adantr 
 |-  ( ( ph /\ x e. B ) -> R e. Ring )
79 simpr 
 |-  ( ( ph /\ x e. B ) -> x e. B )
80 1 15 21 78 79 ringlzd 
 |-  ( ( ph /\ x e. B ) -> ( ( 0g ` R ) ( .r ` R ) x ) = ( 0g ` R ) )
81 1 subrgss 
 |-  ( ( N ` ( S u. { X } ) ) e. ( SubRing ` R ) -> ( N ` ( S u. { X } ) ) C_ B )
82 33 81 syl 
 |-  ( ph -> ( N ` ( S u. { X } ) ) C_ B )
83 82 adantr 
 |-  ( ( ph /\ i e. NN0 ) -> ( N ` ( S u. { X } ) ) C_ B )
84 83 60 sseldd 
 |-  ( ( ph /\ i e. NN0 ) -> ( i ( .g ` ( mulGrp ` R ) ) X ) e. B )
85 77 80 42 84 74 fsuppssov1 
 |-  ( ph -> ( i e. NN0 |-> ( ( ( coe1 ` F ) ` i ) ( .r ` R ) ( i ( .g ` ( mulGrp ` R ) ) X ) ) ) finSupp ( 0g ` R ) )
86 21 23 25 35 62 85 gsumsubgcl 
 |-  ( ph -> ( R gsum ( i e. NN0 |-> ( ( ( coe1 ` F ) ` i ) ( .r ` R ) ( i ( .g ` ( mulGrp ` R ) ) X ) ) ) ) e. ( N ` ( S u. { X } ) ) )
87 20 86 eqeltrd 
 |-  ( ph -> ( ( Q ` F ) ` X ) e. ( N ` ( S u. { X } ) ) )