Metamath Proof Explorer

Theorem chrval

Description: Definition substitution of the ring characteristic. (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypotheses chrval.o 
|- O = ( od ` R )
chrval.u 
|- .1. = ( 1r ` R )
chrval.c 
|- C = ( chr ` R )
Assertion chrval 
|- ( O ` .1. ) = C

Proof

Step Hyp Ref Expression
1 chrval.o 
 |-  O = ( od ` R )
2 chrval.u 
 |-  .1. = ( 1r ` R )
3 chrval.c 
 |-  C = ( chr ` R )
4 fveq2 
 |-  ( r = R -> ( od ` r ) = ( od ` R ) )
5 4 1 eqtr4di 
 |-  ( r = R -> ( od ` r ) = O )
6 fveq2 
 |-  ( r = R -> ( 1r ` r ) = ( 1r ` R ) )
7 6 2 eqtr4di 
 |-  ( r = R -> ( 1r ` r ) = .1. )
8 5 7 fveq12d 
 |-  ( r = R -> ( ( od ` r ) ` ( 1r ` r ) ) = ( O ` .1. ) )
9 df-chr 
 |-  chr = ( r e. _V |-> ( ( od ` r ) ` ( 1r ` r ) ) )
10 fvex 
 |-  ( O ` .1. ) e. _V
11 8 9 10 fvmpt 
 |-  ( R e. _V -> ( chr ` R ) = ( O ` .1. ) )
12 fvprc 
 |-  ( -. R e. _V -> ( chr ` R ) = (/) )
13 fvprc 
 |-  ( -. R e. _V -> ( od ` R ) = (/) )
14 1 13 syl5eq 
 |-  ( -. R e. _V -> O = (/) )
15 14 fveq1d 
 |-  ( -. R e. _V -> ( O ` .1. ) = ( (/) ` .1. ) )
16 0fv 
 |-  ( (/) ` .1. ) = (/)
17 15 16 eqtrdi 
 |-  ( -. R e. _V -> ( O ` .1. ) = (/) )
18 12 17 eqtr4d 
 |-  ( -. R e. _V -> ( chr ` R ) = ( O ` .1. ) )
19 11 18 pm2.61i 
 |-  ( chr ` R ) = ( O ` .1. )
20 3 19 eqtr2i 
 |-  ( O ` .1. ) = C