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