Metamath Proof Explorer

Theorem evl1fval

Description: Value of the simple/same ring evaluation map. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses evl1fval.o 
|- O = ( eval1 ` R )
evl1fval.q 
|- Q = ( 1o eval R )
evl1fval.b 
|- B = ( Base ` R )
Assertion evl1fval 
|- O = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. Q )

Proof

Step Hyp Ref Expression
1 evl1fval.o 
 |-  O = ( eval1 ` R )
2 evl1fval.q 
 |-  Q = ( 1o eval R )
3 evl1fval.b 
 |-  B = ( Base ` R )
4 fvexd 
 |-  ( r = R -> ( Base ` r ) e. _V )
5 id 
 |-  ( b = ( Base ` r ) -> b = ( Base ` r ) )
6 fveq2 
 |-  ( r = R -> ( Base ` r ) = ( Base ` R ) )
7 6 3 eqtr4di 
 |-  ( r = R -> ( Base ` r ) = B )
8 5 7 sylan9eqr 
 |-  ( ( r = R /\ b = ( Base ` r ) ) -> b = B )
9 8 oveq1d 
 |-  ( ( r = R /\ b = ( Base ` r ) ) -> ( b ^m 1o ) = ( B ^m 1o ) )
10 8 9 oveq12d 
 |-  ( ( r = R /\ b = ( Base ` r ) ) -> ( b ^m ( b ^m 1o ) ) = ( B ^m ( B ^m 1o ) ) )
11 8 mpteq1d 
 |-  ( ( r = R /\ b = ( Base ` r ) ) -> ( y e. b |-> ( 1o X. { y } ) ) = ( y e. B |-> ( 1o X. { y } ) ) )
12 11 coeq2d 
 |-  ( ( r = R /\ b = ( Base ` r ) ) -> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) = ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) )
13 10 12 mpteq12dv 
 |-  ( ( r = R /\ b = ( Base ` r ) ) -> ( 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 } ) ) ) ) )
14 simpl 
 |-  ( ( r = R /\ b = ( Base ` r ) ) -> r = R )
15 14 oveq2d 
 |-  ( ( r = R /\ b = ( Base ` r ) ) -> ( 1o eval r ) = ( 1o eval R ) )
16 15 2 eqtr4di 
 |-  ( ( r = R /\ b = ( Base ` r ) ) -> ( 1o eval r ) = Q )
17 13 16 coeq12d 
 |-  ( ( r = R /\ b = ( Base ` r ) ) -> ( ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) ) o. ( 1o eval r ) ) = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. Q ) )
18 4 17 csbied 
 |-  ( r = R -> [_ ( Base ` r ) / b ]_ ( ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) ) o. ( 1o eval r ) ) = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. Q ) )
19 df-evl1 
 |-  eval1 = ( r e. _V |-> [_ ( Base ` r ) / b ]_ ( ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) ) o. ( 1o eval r ) ) )
20 ovex 
 |-  ( B ^m ( B ^m 1o ) ) e. _V
21 20 mptex 
 |-  ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) e. _V
22 2 ovexi 
 |-  Q e. _V
23 21 22 coex 
 |-  ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. Q ) e. _V
24 18 19 23 fvmpt 
 |-  ( R e. _V -> ( eval1 ` R ) = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. Q ) )
25 1 24 syl5eq 
 |-  ( R e. _V -> O = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. Q ) )
26 fvprc 
 |-  ( -. R e. _V -> ( eval1 ` R ) = (/) )
27 1 26 syl5eq 
 |-  ( -. R e. _V -> O = (/) )
28 co02 
 |-  ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. (/) ) = (/)
29 27 28 eqtr4di 
 |-  ( -. R e. _V -> O = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. (/) ) )
30 df-evl 
 |-  eval = ( i e. _V , r e. _V |-> ( ( i evalSub r ) ` ( Base ` r ) ) )
31 30 reldmmpo 
 |-  Rel dom eval
32 31 ovprc2 
 |-  ( -. R e. _V -> ( 1o eval R ) = (/) )
33 2 32 syl5eq 
 |-  ( -. R e. _V -> Q = (/) )
34 33 coeq2d 
 |-  ( -. R e. _V -> ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. Q ) = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. (/) ) )
35 29 34 eqtr4d 
 |-  ( -. R e. _V -> O = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. Q ) )
36 25 35 pm2.61i 
 |-  O = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. Q )