Metamath Proof Explorer

Theorem evls1var

Description: Univariate polynomial evaluation for subrings maps the variable to the identity function. (Contributed by AV, 13-Sep-2019)

Ref Expression
Hypotheses evls1var.q 
|- Q = ( S evalSub1 R )
evls1var.x 
|- X = ( var1 ` U )
evls1var.u 
|- U = ( S |`s R )
evls1var.b 
|- B = ( Base ` S )
evls1var.s 
|- ( ph -> S e. CRing )
evls1var.r 
|- ( ph -> R e. ( SubRing ` S ) )
Assertion evls1var 
|- ( ph -> ( Q ` X ) = ( _I |` B ) )

Proof

Step Hyp Ref Expression
1 evls1var.q 
 |-  Q = ( S evalSub1 R )
2 evls1var.x 
 |-  X = ( var1 ` U )
3 evls1var.u 
 |-  U = ( S |`s R )
4 evls1var.b 
 |-  B = ( Base ` S )
5 evls1var.s 
 |-  ( ph -> S e. CRing )
6 evls1var.r 
 |-  ( ph -> R e. ( SubRing ` S ) )
7 eqid 
 |-  ( var1 ` S ) = ( var1 ` S )
8 7 6 3 subrgvr1 
 |-  ( ph -> ( var1 ` S ) = ( var1 ` U ) )
9 2 8 eqtr4id 
 |-  ( ph -> X = ( var1 ` S ) )
10 9 fveq2d 
 |-  ( ph -> ( Q ` X ) = ( Q ` ( var1 ` S ) ) )
11 eqid 
 |-  ( ( 1o evalSub S ) ` R ) = ( ( 1o evalSub S ) ` R )
12 eqid 
 |-  ( 1o eval S ) = ( 1o eval S )
13 eqid 
 |-  ( 1o mVar U ) = ( 1o mVar U )
14 1on 
 |-  1o e. On
15 14 a1i 
 |-  ( ph -> 1o e. On )
16 0lt1o 
 |-  (/) e. 1o
17 16 a1i 
 |-  ( ph -> (/) e. 1o )
18 11 12 13 3 4 15 5 6 17 evlsvarsrng 
 |-  ( ph -> ( ( ( 1o evalSub S ) ` R ) ` ( ( 1o mVar U ) ` (/) ) ) = ( ( 1o eval S ) ` ( ( 1o mVar U ) ` (/) ) ) )
19 7 vr1val 
 |-  ( var1 ` S ) = ( ( 1o mVar S ) ` (/) )
20 eqid 
 |-  ( 1o mVar S ) = ( 1o mVar S )
21 20 15 6 3 subrgmvr 
 |-  ( ph -> ( 1o mVar S ) = ( 1o mVar U ) )
22 21 fveq1d 
 |-  ( ph -> ( ( 1o mVar S ) ` (/) ) = ( ( 1o mVar U ) ` (/) ) )
23 19 22 syl5eq 
 |-  ( ph -> ( var1 ` S ) = ( ( 1o mVar U ) ` (/) ) )
24 23 fveq2d 
 |-  ( ph -> ( ( ( 1o evalSub S ) ` R ) ` ( var1 ` S ) ) = ( ( ( 1o evalSub S ) ` R ) ` ( ( 1o mVar U ) ` (/) ) ) )
25 23 fveq2d 
 |-  ( ph -> ( ( 1o eval S ) ` ( var1 ` S ) ) = ( ( 1o eval S ) ` ( ( 1o mVar U ) ` (/) ) ) )
26 18 24 25 3eqtr4d 
 |-  ( ph -> ( ( ( 1o evalSub S ) ` R ) ` ( var1 ` S ) ) = ( ( 1o eval S ) ` ( var1 ` S ) ) )
27 26 coeq1d 
 |-  ( ph -> ( ( ( ( 1o evalSub S ) ` R ) ` ( var1 ` S ) ) o. ( y e. B |-> ( 1o X. { y } ) ) ) = ( ( ( 1o eval S ) ` ( var1 ` S ) ) o. ( y e. B |-> ( 1o X. { y } ) ) ) )
28 eqid 
 |-  ( Poly1 ` U ) = ( Poly1 ` U )
29 eqid 
 |-  ( Poly1 ` ( S |`s R ) ) = ( Poly1 ` ( S |`s R ) )
30 eqid 
 |-  ( PwSer1 ` ( S |`s R ) ) = ( PwSer1 ` ( S |`s R ) )
31 3 fveq2i 
 |-  ( Poly1 ` U ) = ( Poly1 ` ( S |`s R ) )
32 31 fveq2i 
 |-  ( Base ` ( Poly1 ` U ) ) = ( Base ` ( Poly1 ` ( S |`s R ) ) )
33 29 30 32 ply1bas 
 |-  ( Base ` ( Poly1 ` U ) ) = ( Base ` ( 1o mPoly ( S |`s R ) ) )
34 33 eqcomi 
 |-  ( Base ` ( 1o mPoly ( S |`s R ) ) ) = ( Base ` ( Poly1 ` U ) )
35 7 6 3 28 34 subrgvr1cl 
 |-  ( ph -> ( var1 ` S ) e. ( Base ` ( 1o mPoly ( S |`s R ) ) ) )
36 eqid 
 |-  ( 1o evalSub S ) = ( 1o evalSub S )
37 eqid 
 |-  ( 1o mPoly ( S |`s R ) ) = ( 1o mPoly ( S |`s R ) )
38 eqid 
 |-  ( Base ` ( 1o mPoly ( S |`s R ) ) ) = ( Base ` ( 1o mPoly ( S |`s R ) ) )
39 1 36 4 37 38 evls1val 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) /\ ( var1 ` S ) e. ( Base ` ( 1o mPoly ( S |`s R ) ) ) ) -> ( Q ` ( var1 ` S ) ) = ( ( ( ( 1o evalSub S ) ` R ) ` ( var1 ` S ) ) o. ( y e. B |-> ( 1o X. { y } ) ) ) )
40 5 6 35 39 syl3anc 
 |-  ( ph -> ( Q ` ( var1 ` S ) ) = ( ( ( ( 1o evalSub S ) ` R ) ` ( var1 ` S ) ) o. ( y e. B |-> ( 1o X. { y } ) ) ) )
41 crngring 
 |-  ( S e. CRing -> S e. Ring )
42 eqid 
 |-  ( Poly1 ` S ) = ( Poly1 ` S )
43 eqid 
 |-  ( PwSer1 ` S ) = ( PwSer1 ` S )
44 eqid 
 |-  ( Base ` ( Poly1 ` S ) ) = ( Base ` ( Poly1 ` S ) )
45 42 43 44 ply1bas 
 |-  ( Base ` ( Poly1 ` S ) ) = ( Base ` ( 1o mPoly S ) )
46 45 eqcomi 
 |-  ( Base ` ( 1o mPoly S ) ) = ( Base ` ( Poly1 ` S ) )
47 7 42 46 vr1cl 
 |-  ( S e. Ring -> ( var1 ` S ) e. ( Base ` ( 1o mPoly S ) ) )
48 5 41 47 3syl 
 |-  ( ph -> ( var1 ` S ) e. ( Base ` ( 1o mPoly S ) ) )
49 eqid 
 |-  ( eval1 ` S ) = ( eval1 ` S )
50 eqid 
 |-  ( 1o mPoly S ) = ( 1o mPoly S )
51 eqid 
 |-  ( Base ` ( 1o mPoly S ) ) = ( Base ` ( 1o mPoly S ) )
52 49 12 4 50 51 evl1val 
 |-  ( ( S e. CRing /\ ( var1 ` S ) e. ( Base ` ( 1o mPoly S ) ) ) -> ( ( eval1 ` S ) ` ( var1 ` S ) ) = ( ( ( 1o eval S ) ` ( var1 ` S ) ) o. ( y e. B |-> ( 1o X. { y } ) ) ) )
53 5 48 52 syl2anc 
 |-  ( ph -> ( ( eval1 ` S ) ` ( var1 ` S ) ) = ( ( ( 1o eval S ) ` ( var1 ` S ) ) o. ( y e. B |-> ( 1o X. { y } ) ) ) )
54 27 40 53 3eqtr4d 
 |-  ( ph -> ( Q ` ( var1 ` S ) ) = ( ( eval1 ` S ) ` ( var1 ` S ) ) )
55 49 7 4 evl1var 
 |-  ( S e. CRing -> ( ( eval1 ` S ) ` ( var1 ` S ) ) = ( _I |` B ) )
56 5 55 syl 
 |-  ( ph -> ( ( eval1 ` S ) ` ( var1 ` S ) ) = ( _I |` B ) )
57 10 54 56 3eqtrd 
 |-  ( ph -> ( Q ` X ) = ( _I |` B ) )