Metamath Proof Explorer

Theorem staffval

Description: The functionalization of the involution component of a structure. (Contributed by Mario Carneiro, 6-Oct-2015)

Ref Expression
Hypotheses staffval.b 
|- B = ( Base ` R )
staffval.i 
|- .* = ( *r ` R )
staffval.f 
|- .xb = ( *rf ` R )
Assertion staffval 
|- .xb = ( x e. B |-> ( .* ` x ) )

Proof

Step Hyp Ref Expression
1 staffval.b 
 |-  B = ( Base ` R )
2 staffval.i 
 |-  .* = ( *r ` R )
3 staffval.f 
 |-  .xb = ( *rf ` R )
4 fveq2 
 |-  ( f = R -> ( Base ` f ) = ( Base ` R ) )
5 4 1 eqtr4di 
 |-  ( f = R -> ( Base ` f ) = B )
6 fveq2 
 |-  ( f = R -> ( *r ` f ) = ( *r ` R ) )
7 6 2 eqtr4di 
 |-  ( f = R -> ( *r ` f ) = .* )
8 7 fveq1d 
 |-  ( f = R -> ( ( *r ` f ) ` x ) = ( .* ` x ) )
9 5 8 mpteq12dv 
 |-  ( f = R -> ( x e. ( Base ` f ) |-> ( ( *r ` f ) ` x ) ) = ( x e. B |-> ( .* ` x ) ) )
10 df-staf 
 |-  *rf = ( f e. _V |-> ( x e. ( Base ` f ) |-> ( ( *r ` f ) ` x ) ) )
11 eqid 
 |-  ( x e. B |-> ( .* ` x ) ) = ( x e. B |-> ( .* ` x ) )
12 fvrn0 
 |-  ( .* ` x ) e. ( ran .* u. { (/) } )
13 12 a1i 
 |-  ( x e. B -> ( .* ` x ) e. ( ran .* u. { (/) } ) )
14 11 13 fmpti 
 |-  ( x e. B |-> ( .* ` x ) ) : B --> ( ran .* u. { (/) } )
15 1 fvexi 
 |-  B e. _V
16 2 fvexi 
 |-  .* e. _V
17 16 rnex 
 |-  ran .* e. _V
18 p0ex 
 |-  { (/) } e. _V
19 17 18 unex 
 |-  ( ran .* u. { (/) } ) e. _V
20 fex2 
 |-  ( ( ( x e. B |-> ( .* ` x ) ) : B --> ( ran .* u. { (/) } ) /\ B e. _V /\ ( ran .* u. { (/) } ) e. _V ) -> ( x e. B |-> ( .* ` x ) ) e. _V )
21 14 15 19 20 mp3an 
 |-  ( x e. B |-> ( .* ` x ) ) e. _V
22 9 10 21 fvmpt 
 |-  ( R e. _V -> ( *rf ` R ) = ( x e. B |-> ( .* ` x ) ) )
23 fvprc 
 |-  ( -. R e. _V -> ( *rf ` R ) = (/) )
24 mpt0 
 |-  ( x e. (/) |-> ( .* ` x ) ) = (/)
25 23 24 eqtr4di 
 |-  ( -. R e. _V -> ( *rf ` R ) = ( x e. (/) |-> ( .* ` x ) ) )
26 fvprc 
 |-  ( -. R e. _V -> ( Base ` R ) = (/) )
27 1 26 syl5eq 
 |-  ( -. R e. _V -> B = (/) )
28 27 mpteq1d 
 |-  ( -. R e. _V -> ( x e. B |-> ( .* ` x ) ) = ( x e. (/) |-> ( .* ` x ) ) )
29 25 28 eqtr4d 
 |-  ( -. R e. _V -> ( *rf ` R ) = ( x e. B |-> ( .* ` x ) ) )
30 22 29 pm2.61i 
 |-  ( *rf ` R ) = ( x e. B |-> ( .* ` x ) )
31 3 30 eqtri 
 |-  .xb = ( x e. B |-> ( .* ` x ) )