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 ) ) )