Metamath Proof Explorer

Theorem ofsubid

Description: Function analogue of subid . (Contributed by Steve Rodriguez, 5-Nov-2015)

Ref Expression
Assertion ofsubid 
|- ( ( A e. V /\ F : A --> CC ) -> ( F oF - F ) = ( A X. { 0 } ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. V /\ F : A --> CC ) -> A e. V )
2 ffn 
 |-  ( F : A --> CC -> F Fn A )
3 2 adantl 
 |-  ( ( A e. V /\ F : A --> CC ) -> F Fn A )
4 c0ex 
 |-  0 e. _V
5 4 fconst 
 |-  ( A X. { 0 } ) : A --> { 0 }
6 ffn 
 |-  ( ( A X. { 0 } ) : A --> { 0 } -> ( A X. { 0 } ) Fn A )
7 5 6 mp1i 
 |-  ( ( A e. V /\ F : A --> CC ) -> ( A X. { 0 } ) Fn A )
8 eqidd 
 |-  ( ( ( A e. V /\ F : A --> CC ) /\ x e. A ) -> ( F ` x ) = ( F ` x ) )
9 ffvelrn 
 |-  ( ( F : A --> CC /\ x e. A ) -> ( F ` x ) e. CC )
10 9 subidd 
 |-  ( ( F : A --> CC /\ x e. A ) -> ( ( F ` x ) - ( F ` x ) ) = 0 )
11 10 adantll 
 |-  ( ( ( A e. V /\ F : A --> CC ) /\ x e. A ) -> ( ( F ` x ) - ( F ` x ) ) = 0 )
12 4 fvconst2 
 |-  ( x e. A -> ( ( A X. { 0 } ) ` x ) = 0 )
13 12 adantl 
 |-  ( ( ( A e. V /\ F : A --> CC ) /\ x e. A ) -> ( ( A X. { 0 } ) ` x ) = 0 )
14 11 13 eqtr4d 
 |-  ( ( ( A e. V /\ F : A --> CC ) /\ x e. A ) -> ( ( F ` x ) - ( F ` x ) ) = ( ( A X. { 0 } ) ` x ) )
15 1 3 3 7 8 8 14 offveq 
 |-  ( ( A e. V /\ F : A --> CC ) -> ( F oF - F ) = ( A X. { 0 } ) )