Metamath Proof Explorer

Theorem evls1scasrng

Description: The evaluation of a scalar of a subring yields the same result as evaluated as a scalar over the ring itself. (Contributed by AV, 13-Sep-2019)

Ref Expression
Hypotheses evls1scasrng.q 
|- Q = ( S evalSub1 R )
evls1scasrng.o 
|- O = ( eval1 ` S )
evls1scasrng.w 
|- W = ( Poly1 ` U )
evls1scasrng.u 
|- U = ( S |`s R )
evls1scasrng.p 
|- P = ( Poly1 ` S )
evls1scasrng.b 
|- B = ( Base ` S )
evls1scasrng.a 
|- A = ( algSc ` W )
evls1scasrng.c 
|- C = ( algSc ` P )
evls1scasrng.s 
|- ( ph -> S e. CRing )
evls1scasrng.r 
|- ( ph -> R e. ( SubRing ` S ) )
evls1scasrng.x 
|- ( ph -> X e. R )
Assertion evls1scasrng 
|- ( ph -> ( Q ` ( A ` X ) ) = ( O ` ( C ` X ) ) )

Proof

Step Hyp Ref Expression
1 evls1scasrng.q 
 |-  Q = ( S evalSub1 R )
2 evls1scasrng.o 
 |-  O = ( eval1 ` S )
3 evls1scasrng.w 
 |-  W = ( Poly1 ` U )
4 evls1scasrng.u 
 |-  U = ( S |`s R )
5 evls1scasrng.p 
 |-  P = ( Poly1 ` S )
6 evls1scasrng.b 
 |-  B = ( Base ` S )
7 evls1scasrng.a 
 |-  A = ( algSc ` W )
8 evls1scasrng.c 
 |-  C = ( algSc ` P )
9 evls1scasrng.s 
 |-  ( ph -> S e. CRing )
10 evls1scasrng.r 
 |-  ( ph -> R e. ( SubRing ` S ) )
11 evls1scasrng.x 
 |-  ( ph -> X e. R )
12 6 ressid 
 |-  ( S e. CRing -> ( S |`s B ) = S )
13 12 eqcomd 
 |-  ( S e. CRing -> S = ( S |`s B ) )
14 9 13 syl 
 |-  ( ph -> S = ( S |`s B ) )
15 14 fveq2d 
 |-  ( ph -> ( Poly1 ` S ) = ( Poly1 ` ( S |`s B ) ) )
16 5 15 eqtrid 
 |-  ( ph -> P = ( Poly1 ` ( S |`s B ) ) )
17 16 fveq2d 
 |-  ( ph -> ( algSc ` P ) = ( algSc ` ( Poly1 ` ( S |`s B ) ) ) )
18 8 17 eqtrid 
 |-  ( ph -> C = ( algSc ` ( Poly1 ` ( S |`s B ) ) ) )
19 18 fveq1d 
 |-  ( ph -> ( C ` X ) = ( ( algSc ` ( Poly1 ` ( S |`s B ) ) ) ` X ) )
20 19 fveq2d 
 |-  ( ph -> ( ( S evalSub1 B ) ` ( C ` X ) ) = ( ( S evalSub1 B ) ` ( ( algSc ` ( Poly1 ` ( S |`s B ) ) ) ` X ) ) )
21 eqid 
 |-  ( S evalSub1 B ) = ( S evalSub1 B )
22 eqid 
 |-  ( Poly1 ` ( S |`s B ) ) = ( Poly1 ` ( S |`s B ) )
23 eqid 
 |-  ( S |`s B ) = ( S |`s B )
24 eqid 
 |-  ( algSc ` ( Poly1 ` ( S |`s B ) ) ) = ( algSc ` ( Poly1 ` ( S |`s B ) ) )
25 crngring 
 |-  ( S e. CRing -> S e. Ring )
26 6 subrgid 
 |-  ( S e. Ring -> B e. ( SubRing ` S ) )
27 9 25 26 3syl 
 |-  ( ph -> B e. ( SubRing ` S ) )
28 6 subrgss 
 |-  ( R e. ( SubRing ` S ) -> R C_ B )
29 10 28 syl 
 |-  ( ph -> R C_ B )
30 29 11 sseldd 
 |-  ( ph -> X e. B )
31 21 22 23 6 24 9 27 30 evls1sca 
 |-  ( ph -> ( ( S evalSub1 B ) ` ( ( algSc ` ( Poly1 ` ( S |`s B ) ) ) ` X ) ) = ( B X. { X } ) )
32 20 31 eqtrd 
 |-  ( ph -> ( ( S evalSub1 B ) ` ( C ` X ) ) = ( B X. { X } ) )
33 2 6 evl1fval1 
 |-  O = ( S evalSub1 B )
34 33 a1i 
 |-  ( ph -> O = ( S evalSub1 B ) )
35 34 fveq1d 
 |-  ( ph -> ( O ` ( C ` X ) ) = ( ( S evalSub1 B ) ` ( C ` X ) ) )
36 1 3 4 6 7 9 10 11 evls1sca 
 |-  ( ph -> ( Q ` ( A ` X ) ) = ( B X. { X } ) )
37 32 35 36 3eqtr4rd 
 |-  ( ph -> ( Q ` ( A ` X ) ) = ( O ` ( C ` X ) ) )