Metamath Proof Explorer

Theorem evls1fval

Description: Value of the univariate polynomial evaluation map function. (Contributed by AV, 7-Sep-2019)

Ref Expression
Hypotheses evls1fval.q 
|- Q = ( S evalSub1 R )
evls1fval.e 
|- E = ( 1o evalSub S )
evls1fval.b 
|- B = ( Base ` S )
Assertion evls1fval 
|- ( ( S e. V /\ R e. ~P B ) -> Q = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( E ` R ) ) )

Proof

Step Hyp Ref Expression
1 evls1fval.q 
 |-  Q = ( S evalSub1 R )
2 evls1fval.e 
 |-  E = ( 1o evalSub S )
3 evls1fval.b 
 |-  B = ( Base ` S )
4 elex 
 |-  ( S e. V -> S e. _V )
5 4 adantr 
 |-  ( ( S e. V /\ R e. ~P B ) -> S e. _V )
6 simpr 
 |-  ( ( S e. V /\ R e. ~P B ) -> R e. ~P B )
7 ovex 
 |-  ( B ^m ( B ^m 1o ) ) e. _V
8 7 mptex 
 |-  ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) e. _V
9 fvex 
 |-  ( E ` R ) e. _V
10 8 9 coex 
 |-  ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( E ` R ) ) e. _V
11 10 a1i 
 |-  ( ( S e. V /\ R e. ~P B ) -> ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( E ` R ) ) e. _V )
12 fveq2 
 |-  ( s = S -> ( Base ` s ) = ( Base ` S ) )
13 12 adantr 
 |-  ( ( s = S /\ r = R ) -> ( Base ` s ) = ( Base ` S ) )
14 13 3 eqtr4di 
 |-  ( ( s = S /\ r = R ) -> ( Base ` s ) = B )
15 14 csbeq1d 
 |-  ( ( s = S /\ r = R ) -> [_ ( Base ` s ) / b ]_ ( ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub s ) ` r ) ) = [_ B / b ]_ ( ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub s ) ` r ) ) )
16 3 fvexi 
 |-  B e. _V
17 16 a1i 
 |-  ( ( s = S /\ r = R ) -> B e. _V )
18 id 
 |-  ( b = B -> b = B )
19 oveq1 
 |-  ( b = B -> ( b ^m 1o ) = ( B ^m 1o ) )
20 18 19 oveq12d 
 |-  ( b = B -> ( b ^m ( b ^m 1o ) ) = ( B ^m ( B ^m 1o ) ) )
21 mpteq1 
 |-  ( b = B -> ( y e. b |-> ( 1o X. { y } ) ) = ( y e. B |-> ( 1o X. { y } ) ) )
22 21 coeq2d 
 |-  ( b = B -> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) = ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) )
23 20 22 mpteq12dv 
 |-  ( b = B -> ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) ) = ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) )
24 23 coeq1d 
 |-  ( b = B -> ( ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub s ) ` r ) ) = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub s ) ` r ) ) )
25 24 adantl 
 |-  ( ( ( s = S /\ r = R ) /\ b = B ) -> ( ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub s ) ` r ) ) = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub s ) ` r ) ) )
26 17 25 csbied 
 |-  ( ( s = S /\ r = R ) -> [_ B / b ]_ ( ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub s ) ` r ) ) = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub s ) ` r ) ) )
27 oveq2 
 |-  ( s = S -> ( 1o evalSub s ) = ( 1o evalSub S ) )
28 27 2 eqtr4di 
 |-  ( s = S -> ( 1o evalSub s ) = E )
29 28 adantr 
 |-  ( ( s = S /\ r = R ) -> ( 1o evalSub s ) = E )
30 simpr 
 |-  ( ( s = S /\ r = R ) -> r = R )
31 29 30 fveq12d 
 |-  ( ( s = S /\ r = R ) -> ( ( 1o evalSub s ) ` r ) = ( E ` R ) )
32 31 coeq2d 
 |-  ( ( s = S /\ r = R ) -> ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub s ) ` r ) ) = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( E ` R ) ) )
33 15 26 32 3eqtrd 
 |-  ( ( s = S /\ r = R ) -> [_ ( Base ` s ) / b ]_ ( ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub s ) ` r ) ) = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( E ` R ) ) )
34 12 3 eqtr4di 
 |-  ( s = S -> ( Base ` s ) = B )
35 34 pweqd 
 |-  ( s = S -> ~P ( Base ` s ) = ~P B )
36 df-evls1 
 |-  evalSub1 = ( s e. _V , r e. ~P ( Base ` s ) |-> [_ ( Base ` s ) / b ]_ ( ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub s ) ` r ) ) )
37 33 35 36 ovmpox 
 |-  ( ( S e. _V /\ R e. ~P B /\ ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( E ` R ) ) e. _V ) -> ( S evalSub1 R ) = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( E ` R ) ) )
38 5 6 11 37 syl3anc 
 |-  ( ( S e. V /\ R e. ~P B ) -> ( S evalSub1 R ) = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( E ` R ) ) )
39 1 38 syl5eq 
 |-  ( ( S e. V /\ R e. ~P B ) -> Q = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( E ` R ) ) )