Metamath Proof Explorer


Theorem offvalfv

Description: The function operation expressed as a mapping with function values. (Contributed by AV, 6-Apr-2019)

Ref Expression
Hypotheses offvalfv.a
|- ( ph -> A e. V )
offvalfv.f
|- ( ph -> F Fn A )
offvalfv.g
|- ( ph -> G Fn A )
Assertion offvalfv
|- ( ph -> ( F oF R G ) = ( x e. A |-> ( ( F ` x ) R ( G ` x ) ) ) )

Proof

Step Hyp Ref Expression
1 offvalfv.a
 |-  ( ph -> A e. V )
2 offvalfv.f
 |-  ( ph -> F Fn A )
3 offvalfv.g
 |-  ( ph -> G Fn A )
4 fnfvelrn
 |-  ( ( F Fn A /\ x e. A ) -> ( F ` x ) e. ran F )
5 2 4 sylan
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) e. ran F )
6 fnfvelrn
 |-  ( ( G Fn A /\ x e. A ) -> ( G ` x ) e. ran G )
7 3 6 sylan
 |-  ( ( ph /\ x e. A ) -> ( G ` x ) e. ran G )
8 dffn5
 |-  ( F Fn A <-> F = ( x e. A |-> ( F ` x ) ) )
9 2 8 sylib
 |-  ( ph -> F = ( x e. A |-> ( F ` x ) ) )
10 dffn5
 |-  ( G Fn A <-> G = ( x e. A |-> ( G ` x ) ) )
11 3 10 sylib
 |-  ( ph -> G = ( x e. A |-> ( G ` x ) ) )
12 1 5 7 9 11 offval2
 |-  ( ph -> ( F oF R G ) = ( x e. A |-> ( ( F ` x ) R ( G ` x ) ) ) )