This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ofval

Description: Evaluate a function operation at a point. (Contributed by Mario Carneiro, 20-Jul-2014)

Ref Expression
Hypotheses offval.1 
|- ( ph -> F Fn A )
offval.2 
|- ( ph -> G Fn B )
offval.3 
|- ( ph -> A e. V )
offval.4 
|- ( ph -> B e. W )
offval.5 
|- ( A i^i B ) = S
ofval.6 
|- ( ( ph /\ X e. A ) -> ( F ` X ) = C )
ofval.7 
|- ( ( ph /\ X e. B ) -> ( G ` X ) = D )
Assertion ofval 
|- ( ( ph /\ X e. S ) -> ( ( F oF R G ) ` X ) = ( C R D ) )

Proof

Step Hyp Ref Expression
1 offval.1 
 |-  ( ph -> F Fn A )
2 offval.2 
 |-  ( ph -> G Fn B )
3 offval.3 
 |-  ( ph -> A e. V )
4 offval.4 
 |-  ( ph -> B e. W )
5 offval.5 
 |-  ( A i^i B ) = S
6 ofval.6 
 |-  ( ( ph /\ X e. A ) -> ( F ` X ) = C )
7 ofval.7 
 |-  ( ( ph /\ X e. B ) -> ( G ` X ) = D )
8 eqidd 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) = ( F ` x ) )
9 eqidd 
 |-  ( ( ph /\ x e. B ) -> ( G ` x ) = ( G ` x ) )
10 1 2 3 4 5 8 9 offval 
 |-  ( ph -> ( F oF R G ) = ( x e. S |-> ( ( F ` x ) R ( G ` x ) ) ) )
11 10 fveq1d 
 |-  ( ph -> ( ( F oF R G ) ` X ) = ( ( x e. S |-> ( ( F ` x ) R ( G ` x ) ) ) ` X ) )
12 11 adantr 
 |-  ( ( ph /\ X e. S ) -> ( ( F oF R G ) ` X ) = ( ( x e. S |-> ( ( F ` x ) R ( G ` x ) ) ) ` X ) )
13 fveq2 
 |-  ( x = X -> ( F ` x ) = ( F ` X ) )
14 fveq2 
 |-  ( x = X -> ( G ` x ) = ( G ` X ) )
15 13 14 oveq12d 
 |-  ( x = X -> ( ( F ` x ) R ( G ` x ) ) = ( ( F ` X ) R ( G ` X ) ) )
16 eqid 
 |-  ( x e. S |-> ( ( F ` x ) R ( G ` x ) ) ) = ( x e. S |-> ( ( F ` x ) R ( G ` x ) ) )
17 ovex 
 |-  ( ( F ` X ) R ( G ` X ) ) e. _V
18 15 16 17 fvmpt 
 |-  ( X e. S -> ( ( x e. S |-> ( ( F ` x ) R ( G ` x ) ) ) ` X ) = ( ( F ` X ) R ( G ` X ) ) )
19 18 adantl 
 |-  ( ( ph /\ X e. S ) -> ( ( x e. S |-> ( ( F ` x ) R ( G ` x ) ) ) ` X ) = ( ( F ` X ) R ( G ` X ) ) )
20 inss1 
 |-  ( A i^i B ) C_ A
21 5 20 eqsstrri 
 |-  S C_ A
22 21 sseli 
 |-  ( X e. S -> X e. A )
23 22 6 sylan2 
 |-  ( ( ph /\ X e. S ) -> ( F ` X ) = C )
24 inss2 
 |-  ( A i^i B ) C_ B
25 5 24 eqsstrri 
 |-  S C_ B
26 25 sseli 
 |-  ( X e. S -> X e. B )
27 26 7 sylan2 
 |-  ( ( ph /\ X e. S ) -> ( G ` X ) = D )
28 23 27 oveq12d 
 |-  ( ( ph /\ X e. S ) -> ( ( F ` X ) R ( G ` X ) ) = ( C R D ) )
29 12 19 28 3eqtrd 
 |-  ( ( ph /\ X e. S ) -> ( ( F oF R G ) ` X ) = ( C R D ) )