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 eqtrid 
 |-  ( 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 3 fveq2i 
 |-  ( Poly1 ` U ) = ( Poly1 ` ( S |`s R ) )
31 30 fveq2i 
 |-  ( Base ` ( Poly1 ` U ) ) = ( Base ` ( Poly1 ` ( S |`s R ) ) )
32 29 31 ply1bas 
 |-  ( Base ` ( Poly1 ` U ) ) = ( Base ` ( 1o mPoly ( S |`s R ) ) )
33 32 eqcomi 
 |-  ( Base ` ( 1o mPoly ( S |`s R ) ) ) = ( Base ` ( Poly1 ` U ) )
34 7 6 3 28 33 subrgvr1cl 
 |-  ( ph -> ( var1 ` S ) e. ( Base ` ( 1o mPoly ( S |`s R ) ) ) )
35 eqid 
 |-  ( 1o evalSub S ) = ( 1o evalSub S )
36 eqid 
 |-  ( 1o mPoly ( S |`s R ) ) = ( 1o mPoly ( S |`s R ) )
37 eqid 
 |-  ( Base ` ( 1o mPoly ( S |`s R ) ) ) = ( Base ` ( 1o mPoly ( S |`s R ) ) )
38 1 35 4 36 37 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 } ) ) ) )
39 5 6 34 38 syl3anc 
 |-  ( ph -> ( Q ` ( var1 ` S ) ) = ( ( ( ( 1o evalSub S ) ` R ) ` ( var1 ` S ) ) o. ( y e. B |-> ( 1o X. { y } ) ) ) )
40 crngring 
 |-  ( S e. CRing -> S e. Ring )
41 eqid 
 |-  ( Poly1 ` S ) = ( Poly1 ` S )
42 eqid 
 |-  ( Base ` ( Poly1 ` S ) ) = ( Base ` ( Poly1 ` S ) )
43 41 42 ply1bas 
 |-  ( Base ` ( Poly1 ` S ) ) = ( Base ` ( 1o mPoly S ) )
44 43 eqcomi 
 |-  ( Base ` ( 1o mPoly S ) ) = ( Base ` ( Poly1 ` S ) )
45 7 41 44 vr1cl 
 |-  ( S e. Ring -> ( var1 ` S ) e. ( Base ` ( 1o mPoly S ) ) )
46 5 40 45 3syl 
 |-  ( ph -> ( var1 ` S ) e. ( Base ` ( 1o mPoly S ) ) )
47 eqid 
 |-  ( eval1 ` S ) = ( eval1 ` S )
48 eqid 
 |-  ( 1o mPoly S ) = ( 1o mPoly S )
49 eqid 
 |-  ( Base ` ( 1o mPoly S ) ) = ( Base ` ( 1o mPoly S ) )
50 47 12 4 48 49 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 } ) ) ) )
51 5 46 50 syl2anc 
 |-  ( ph -> ( ( eval1 ` S ) ` ( var1 ` S ) ) = ( ( ( 1o eval S ) ` ( var1 ` S ) ) o. ( y e. B |-> ( 1o X. { y } ) ) ) )
52 27 39 51 3eqtr4d 
 |-  ( ph -> ( Q ` ( var1 ` S ) ) = ( ( eval1 ` S ) ` ( var1 ` S ) ) )
53 47 7 4 evl1var 
 |-  ( S e. CRing -> ( ( eval1 ` S ) ` ( var1 ` S ) ) = ( _I |` B ) )
54 5 53 syl 
 |-  ( ph -> ( ( eval1 ` S ) ` ( var1 ` S ) ) = ( _I |` B ) )
55 10 52 54 3eqtrd 
 |-  ( ph -> ( Q ` X ) = ( _I |` B ) )