Metamath Proof Explorer

Theorem offval

Description: Value of an operation applied to two functions. (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
offval.6 
|- ( ( ph /\ x e. A ) -> ( F ` x ) = C )
offval.7 
|- ( ( ph /\ x e. B ) -> ( G ` x ) = D )
Assertion offval 
|- ( ph -> ( F oF R G ) = ( x e. S |-> ( 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 offval.6 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) = C )
7 offval.7 
 |-  ( ( ph /\ x e. B ) -> ( G ` x ) = D )
8 fnex 
 |-  ( ( F Fn A /\ A e. V ) -> F e. _V )
9 1 3 8 syl2anc 
 |-  ( ph -> F e. _V )
10 fnex 
 |-  ( ( G Fn B /\ B e. W ) -> G e. _V )
11 2 4 10 syl2anc 
 |-  ( ph -> G e. _V )
12 1 fndmd 
 |-  ( ph -> dom F = A )
13 2 fndmd 
 |-  ( ph -> dom G = B )
14 12 13 ineq12d 
 |-  ( ph -> ( dom F i^i dom G ) = ( A i^i B ) )
15 14 5 eqtrdi 
 |-  ( ph -> ( dom F i^i dom G ) = S )
16 15 mpteq1d 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) = ( x e. S |-> ( ( F ` x ) R ( G ` x ) ) ) )
17 inex1g 
 |-  ( A e. V -> ( A i^i B ) e. _V )
18 5 17 eqeltrrid 
 |-  ( A e. V -> S e. _V )
19 mptexg 
 |-  ( S e. _V -> ( x e. S |-> ( ( F ` x ) R ( G ` x ) ) ) e. _V )
20 3 18 19 3syl 
 |-  ( ph -> ( x e. S |-> ( ( F ` x ) R ( G ` x ) ) ) e. _V )
21 16 20 eqeltrd 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) e. _V )
22 dmeq 
 |-  ( f = F -> dom f = dom F )
23 dmeq 
 |-  ( g = G -> dom g = dom G )
24 22 23 ineqan12d 
 |-  ( ( f = F /\ g = G ) -> ( dom f i^i dom g ) = ( dom F i^i dom G ) )
25 fveq1 
 |-  ( f = F -> ( f ` x ) = ( F ` x ) )
26 fveq1 
 |-  ( g = G -> ( g ` x ) = ( G ` x ) )
27 25 26 oveqan12d 
 |-  ( ( f = F /\ g = G ) -> ( ( f ` x ) R ( g ` x ) ) = ( ( F ` x ) R ( G ` x ) ) )
28 24 27 mpteq12dv 
 |-  ( ( f = F /\ g = G ) -> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) = ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) )
29 df-of 
 |-  oF R = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) )
30 28 29 ovmpoga 
 |-  ( ( F e. _V /\ G e. _V /\ ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) e. _V ) -> ( F oF R G ) = ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) )
31 9 11 21 30 syl3anc 
 |-  ( ph -> ( F oF R G ) = ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) )
32 5 eleq2i 
 |-  ( x e. ( A i^i B ) <-> x e. S )
33 elin 
 |-  ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
34 32 33 bitr3i 
 |-  ( x e. S <-> ( x e. A /\ x e. B ) )
35 6 adantrr 
 |-  ( ( ph /\ ( x e. A /\ x e. B ) ) -> ( F ` x ) = C )
36 7 adantrl 
 |-  ( ( ph /\ ( x e. A /\ x e. B ) ) -> ( G ` x ) = D )
37 35 36 oveq12d 
 |-  ( ( ph /\ ( x e. A /\ x e. B ) ) -> ( ( F ` x ) R ( G ` x ) ) = ( C R D ) )
38 34 37 sylan2b 
 |-  ( ( ph /\ x e. S ) -> ( ( F ` x ) R ( G ` x ) ) = ( C R D ) )
39 38 mpteq2dva 
 |-  ( ph -> ( x e. S |-> ( ( F ` x ) R ( G ` x ) ) ) = ( x e. S |-> ( C R D ) ) )
40 31 16 39 3eqtrd 
 |-  ( ph -> ( F oF R G ) = ( x e. S |-> ( C R D ) ) )