This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ressply1evl

Description: Evaluation of a univariate subring polynomial is the same as the evaluation in the bigger ring. (Contributed by Thierry Arnoux, 23-Jan-2025)

Ref Expression
Hypotheses ressply1evl2.q 
|- Q = ( S evalSub1 R )
ressply1evl2.k 
|- K = ( Base ` S )
ressply1evl2.w 
|- W = ( Poly1 ` U )
ressply1evl2.u 
|- U = ( S |`s R )
ressply1evl2.b 
|- B = ( Base ` W )
ressply1evl.e 
|- E = ( eval1 ` S )
ressply1evl.s 
|- ( ph -> S e. CRing )
ressply1evl.r 
|- ( ph -> R e. ( SubRing ` S ) )
Assertion ressply1evl 
|- ( ph -> Q = ( E |` B ) )

Proof

Step Hyp Ref Expression
1 ressply1evl2.q 
 |-  Q = ( S evalSub1 R )
2 ressply1evl2.k 
 |-  K = ( Base ` S )
3 ressply1evl2.w 
 |-  W = ( Poly1 ` U )
4 ressply1evl2.u 
 |-  U = ( S |`s R )
5 ressply1evl2.b 
 |-  B = ( Base ` W )
6 ressply1evl.e 
 |-  E = ( eval1 ` S )
7 ressply1evl.s 
 |-  ( ph -> S e. CRing )
8 ressply1evl.r 
 |-  ( ph -> R e. ( SubRing ` S ) )
9 6 2 evl1fval1 
 |-  E = ( S evalSub1 K )
10 eqid 
 |-  ( Poly1 ` ( S |`s K ) ) = ( Poly1 ` ( S |`s K ) )
11 eqid 
 |-  ( S |`s K ) = ( S |`s K )
12 eqid 
 |-  ( Base ` ( Poly1 ` ( S |`s K ) ) ) = ( Base ` ( Poly1 ` ( S |`s K ) ) )
13 7 adantr 
 |-  ( ( ph /\ m e. B ) -> S e. CRing )
14 7 crngringd 
 |-  ( ph -> S e. Ring )
15 2 subrgid 
 |-  ( S e. Ring -> K e. ( SubRing ` S ) )
16 14 15 syl 
 |-  ( ph -> K e. ( SubRing ` S ) )
17 16 adantr 
 |-  ( ( ph /\ m e. B ) -> K e. ( SubRing ` S ) )
18 eqid 
 |-  ( Poly1 ` S ) = ( Poly1 ` S )
19 eqid 
 |-  ( PwSer1 ` U ) = ( PwSer1 ` U )
20 eqid 
 |-  ( Base ` ( PwSer1 ` U ) ) = ( Base ` ( PwSer1 ` U ) )
21 eqid 
 |-  ( Base ` ( Poly1 ` S ) ) = ( Base ` ( Poly1 ` S ) )
22 18 4 3 5 8 19 20 21 ressply1bas2 
 |-  ( ph -> B = ( ( Base ` ( PwSer1 ` U ) ) i^i ( Base ` ( Poly1 ` S ) ) ) )
23 inss2 
 |-  ( ( Base ` ( PwSer1 ` U ) ) i^i ( Base ` ( Poly1 ` S ) ) ) C_ ( Base ` ( Poly1 ` S ) )
24 22 23 eqsstrdi 
 |-  ( ph -> B C_ ( Base ` ( Poly1 ` S ) ) )
25 2 ressid 
 |-  ( S e. CRing -> ( S |`s K ) = S )
26 7 25 syl 
 |-  ( ph -> ( S |`s K ) = S )
27 26 fveq2d 
 |-  ( ph -> ( Poly1 ` ( S |`s K ) ) = ( Poly1 ` S ) )
28 27 fveq2d 
 |-  ( ph -> ( Base ` ( Poly1 ` ( S |`s K ) ) ) = ( Base ` ( Poly1 ` S ) ) )
29 24 28 sseqtrrd 
 |-  ( ph -> B C_ ( Base ` ( Poly1 ` ( S |`s K ) ) ) )
30 29 sselda 
 |-  ( ( ph /\ m e. B ) -> m e. ( Base ` ( Poly1 ` ( S |`s K ) ) ) )
31 eqid 
 |-  ( .r ` S ) = ( .r ` S )
32 eqid 
 |-  ( .g ` ( mulGrp ` S ) ) = ( .g ` ( mulGrp ` S ) )
33 eqid 
 |-  ( coe1 ` m ) = ( coe1 ` m )
34 9 2 10 11 12 13 17 30 31 32 33 evls1fpws 
 |-  ( ( ph /\ m e. B ) -> ( E ` m ) = ( x e. K |-> ( S gsum ( k e. NN0 |-> ( ( ( coe1 ` m ) ` k ) ( .r ` S ) ( k ( .g ` ( mulGrp ` S ) ) x ) ) ) ) ) )
35 8 adantr 
 |-  ( ( ph /\ m e. B ) -> R e. ( SubRing ` S ) )
36 simpr 
 |-  ( ( ph /\ m e. B ) -> m e. B )
37 1 2 3 4 5 13 35 36 31 32 33 evls1fpws 
 |-  ( ( ph /\ m e. B ) -> ( Q ` m ) = ( x e. K |-> ( S gsum ( k e. NN0 |-> ( ( ( coe1 ` m ) ` k ) ( .r ` S ) ( k ( .g ` ( mulGrp ` S ) ) x ) ) ) ) ) )
38 34 37 eqtr4d 
 |-  ( ( ph /\ m e. B ) -> ( E ` m ) = ( Q ` m ) )
39 38 ralrimiva 
 |-  ( ph -> A. m e. B ( E ` m ) = ( Q ` m ) )
40 eqid 
 |-  ( S ^s K ) = ( S ^s K )
41 6 18 40 2 evl1rhm 
 |-  ( S e. CRing -> E e. ( ( Poly1 ` S ) RingHom ( S ^s K ) ) )
42 eqid 
 |-  ( Base ` ( S ^s K ) ) = ( Base ` ( S ^s K ) )
43 21 42 rhmf 
 |-  ( E e. ( ( Poly1 ` S ) RingHom ( S ^s K ) ) -> E : ( Base ` ( Poly1 ` S ) ) --> ( Base ` ( S ^s K ) ) )
44 7 41 43 3syl 
 |-  ( ph -> E : ( Base ` ( Poly1 ` S ) ) --> ( Base ` ( S ^s K ) ) )
45 44 ffnd 
 |-  ( ph -> E Fn ( Base ` ( Poly1 ` S ) ) )
46 1 2 40 4 3 evls1rhm 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( W RingHom ( S ^s K ) ) )
47 7 8 46 syl2anc 
 |-  ( ph -> Q e. ( W RingHom ( S ^s K ) ) )
48 5 42 rhmf 
 |-  ( Q e. ( W RingHom ( S ^s K ) ) -> Q : B --> ( Base ` ( S ^s K ) ) )
49 47 48 syl 
 |-  ( ph -> Q : B --> ( Base ` ( S ^s K ) ) )
50 49 ffnd 
 |-  ( ph -> Q Fn B )
51 fvreseq1 
 |-  ( ( ( E Fn ( Base ` ( Poly1 ` S ) ) /\ Q Fn B ) /\ B C_ ( Base ` ( Poly1 ` S ) ) ) -> ( ( E |` B ) = Q <-> A. m e. B ( E ` m ) = ( Q ` m ) ) )
52 45 50 24 51 syl21anc 
 |-  ( ph -> ( ( E |` B ) = Q <-> A. m e. B ( E ` m ) = ( Q ` m ) ) )
53 39 52 mpbird 
 |-  ( ph -> ( E |` B ) = Q )
54 53 eqcomd 
 |-  ( ph -> Q = ( E |` B ) )