Metamath Proof Explorer

Theorem ofnegsub

Description: Function analogue of negsub . (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Assertion ofnegsub 
|- ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> ( F oF + ( ( A X. { -u 1 } ) oF x. G ) ) = ( F oF - G ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> A e. V )
2 simp2 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> F : A --> CC )
3 2 ffnd 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> F Fn A )
4 ax-1cn 
 |-  1 e. CC
5 4 negcli 
 |-  -u 1 e. CC
6 fnconstg 
 |-  ( -u 1 e. CC -> ( A X. { -u 1 } ) Fn A )
7 5 6 mp1i 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> ( A X. { -u 1 } ) Fn A )
8 simp3 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> G : A --> CC )
9 8 ffnd 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> G Fn A )
10 inidm 
 |-  ( A i^i A ) = A
11 7 9 1 1 10 offn 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> ( ( A X. { -u 1 } ) oF x. G ) Fn A )
12 3 9 1 1 10 offn 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> ( F oF - G ) Fn A )
13 eqidd 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) /\ x e. A ) -> ( F ` x ) = ( F ` x ) )
14 5 a1i 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> -u 1 e. CC )
15 eqidd 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) /\ x e. A ) -> ( G ` x ) = ( G ` x ) )
16 1 14 9 15 ofc1 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) /\ x e. A ) -> ( ( ( A X. { -u 1 } ) oF x. G ) ` x ) = ( -u 1 x. ( G ` x ) ) )
17 8 ffvelrnda 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) /\ x e. A ) -> ( G ` x ) e. CC )
18 17 mulm1d 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) /\ x e. A ) -> ( -u 1 x. ( G ` x ) ) = -u ( G ` x ) )
19 16 18 eqtrd 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) /\ x e. A ) -> ( ( ( A X. { -u 1 } ) oF x. G ) ` x ) = -u ( G ` x ) )
20 2 ffvelrnda 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) /\ x e. A ) -> ( F ` x ) e. CC )
21 20 17 negsubd 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) /\ x e. A ) -> ( ( F ` x ) + -u ( G ` x ) ) = ( ( F ` x ) - ( G ` x ) ) )
22 3 9 1 1 10 13 15 ofval 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) /\ x e. A ) -> ( ( F oF - G ) ` x ) = ( ( F ` x ) - ( G ` x ) ) )
23 21 22 eqtr4d 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) /\ x e. A ) -> ( ( F ` x ) + -u ( G ` x ) ) = ( ( F oF - G ) ` x ) )
24 1 3 11 12 13 19 23 offveq 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> ( F oF + ( ( A X. { -u 1 } ) oF x. G ) ) = ( F oF - G ) )