Metamath Proof Explorer

Theorem rngunsnply1

Description: Adjoining one element to a ring results in a set of polynomial evaluations. Generalization of rngunsnply . (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 )
Assertion rngunsnply1 
|- ( ph -> ( V e. ( N ` ( S u. { X } ) ) <-> E. p e. U V = ( ( Q ` p ) ` 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 5 crngringd 
 |-  ( ph -> R e. Ring )
10 1 a1i 
 |-  ( ph -> B = ( Base ` R ) )
11 1 subrgss 
 |-  ( S e. ( SubRing ` R ) -> S C_ B )
12 6 11 syl 
 |-  ( ph -> S C_ B )
13 7 snssd 
 |-  ( ph -> { X } C_ B )
14 12 13 unssd 
 |-  ( ph -> ( S u. { X } ) C_ B )
15 8 a1i 
 |-  ( ph -> N = ( RingSpan ` R ) )
16 eqidd 
 |-  ( ph -> ( N ` ( S u. { X } ) ) = ( N ` ( S u. { X } ) ) )
17 eqid 
 |-  ( p e. U |-> ( ( Q ` p ) ` X ) ) = ( p e. U |-> ( ( Q ` p ) ` X ) )
18 4 2 1 3 5 6 7 17 evls1maprhm 
 |-  ( ph -> ( p e. U |-> ( ( Q ` p ) ` X ) ) e. ( P RingHom R ) )
19 rnrhmsubrg 
 |-  ( ( p e. U |-> ( ( Q ` p ) ` X ) ) e. ( P RingHom R ) -> ran ( p e. U |-> ( ( Q ` p ) ` X ) ) e. ( SubRing ` R ) )
20 18 19 syl 
 |-  ( ph -> ran ( p e. U |-> ( ( Q ` p ) ` X ) ) e. ( SubRing ` R ) )
21 4 2 1 3 5 6 7 17 evls1maprnss 
 |-  ( ph -> S C_ ran ( p e. U |-> ( ( Q ` p ) ` X ) ) )
22 eqid 
 |-  ( var1 ` R ) = ( var1 ` R )
23 eqid 
 |-  ( R |`s S ) = ( R |`s S )
24 22 6 23 2 3 subrgvr1cl 
 |-  ( ph -> ( var1 ` R ) e. U )
25 22 6 23 subrgvr1 
 |-  ( ph -> ( var1 ` R ) = ( var1 ` ( R |`s S ) ) )
26 25 fveq2d 
 |-  ( ph -> ( Q ` ( var1 ` R ) ) = ( Q ` ( var1 ` ( R |`s S ) ) ) )
27 26 fveq1d 
 |-  ( ph -> ( ( Q ` ( var1 ` R ) ) ` X ) = ( ( Q ` ( var1 ` ( R |`s S ) ) ) ` X ) )
28 eqid 
 |-  ( var1 ` ( R |`s S ) ) = ( var1 ` ( R |`s S ) )
29 4 28 23 1 5 6 evls1var 
 |-  ( ph -> ( Q ` ( var1 ` ( R |`s S ) ) ) = ( _I |` B ) )
30 29 fveq1d 
 |-  ( ph -> ( ( Q ` ( var1 ` ( R |`s S ) ) ) ` X ) = ( ( _I |` B ) ` X ) )
31 fvresi 
 |-  ( X e. B -> ( ( _I |` B ) ` X ) = X )
32 7 31 syl 
 |-  ( ph -> ( ( _I |` B ) ` X ) = X )
33 27 30 32 3eqtrrd 
 |-  ( ph -> X = ( ( Q ` ( var1 ` R ) ) ` X ) )
34 33 adantr 
 |-  ( ( ph /\ p = ( var1 ` R ) ) -> X = ( ( Q ` ( var1 ` R ) ) ` X ) )
35 fveq2 
 |-  ( p = ( var1 ` R ) -> ( Q ` p ) = ( Q ` ( var1 ` R ) ) )
36 35 fveq1d 
 |-  ( p = ( var1 ` R ) -> ( ( Q ` p ) ` X ) = ( ( Q ` ( var1 ` R ) ) ` X ) )
37 36 adantl 
 |-  ( ( ph /\ p = ( var1 ` R ) ) -> ( ( Q ` p ) ` X ) = ( ( Q ` ( var1 ` R ) ) ` X ) )
38 34 37 eqtr4d 
 |-  ( ( ph /\ p = ( var1 ` R ) ) -> X = ( ( Q ` p ) ` X ) )
39 17 24 7 38 elrnmptdv 
 |-  ( ph -> X e. ran ( p e. U |-> ( ( Q ` p ) ` X ) ) )
40 39 snssd 
 |-  ( ph -> { X } C_ ran ( p e. U |-> ( ( Q ` p ) ` X ) ) )
41 21 40 unssd 
 |-  ( ph -> ( S u. { X } ) C_ ran ( p e. U |-> ( ( Q ` p ) ` X ) ) )
42 9 10 14 15 16 20 41 rgspnmin 
 |-  ( ph -> ( N ` ( S u. { X } ) ) C_ ran ( p e. U |-> ( ( Q ` p ) ` X ) ) )
43 42 sseld 
 |-  ( ph -> ( V e. ( N ` ( S u. { X } ) ) -> V e. ran ( p e. U |-> ( ( Q ` p ) ` X ) ) ) )
44 fvex 
 |-  ( ( Q ` p ) ` X ) e. _V
45 17 44 elrnmpti 
 |-  ( V e. ran ( p e. U |-> ( ( Q ` p ) ` X ) ) <-> E. p e. U V = ( ( Q ` p ) ` X ) )
46 43 45 imbitrdi 
 |-  ( ph -> ( V e. ( N ` ( S u. { X } ) ) -> E. p e. U V = ( ( Q ` p ) ` X ) ) )
47 5 adantr 
 |-  ( ( ph /\ p e. U ) -> R e. CRing )
48 6 adantr 
 |-  ( ( ph /\ p e. U ) -> S e. ( SubRing ` R ) )
49 7 adantr 
 |-  ( ( ph /\ p e. U ) -> X e. B )
50 simpr 
 |-  ( ( ph /\ p e. U ) -> p e. U )
51 1 2 3 4 47 48 49 8 50 evls1rgspncl 
 |-  ( ( ph /\ p e. U ) -> ( ( Q ` p ) ` X ) e. ( N ` ( S u. { X } ) ) )
52 eleq1 
 |-  ( V = ( ( Q ` p ) ` X ) -> ( V e. ( N ` ( S u. { X } ) ) <-> ( ( Q ` p ) ` X ) e. ( N ` ( S u. { X } ) ) ) )
53 51 52 syl5ibrcom 
 |-  ( ( ph /\ p e. U ) -> ( V = ( ( Q ` p ) ` X ) -> V e. ( N ` ( S u. { X } ) ) ) )
54 53 rexlimdva 
 |-  ( ph -> ( E. p e. U V = ( ( Q ` p ) ` X ) -> V e. ( N ` ( S u. { X } ) ) ) )
55 46 54 impbid 
 |-  ( ph -> ( V e. ( N ` ( S u. { X } ) ) <-> E. p e. U V = ( ( Q ` p ) ` X ) ) )