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 ) ) )