Theorem ofresid

Description: Applying an operation restricted to the range of the functions does not change the function operation. (Contributed by Thierry Arnoux, 14-Feb-2018)

	Ref	Expression
Hypotheses	ofresid.1	|- ( ph -> F : A --> B )
	ofresid.2	|- ( ph -> G : A --> B )
	ofresid.3	|- ( ph -> A e. V )
Assertion	ofresid	|- ( ph -> ( F oF R G ) = ( F oF ( R |` ( B X. B ) ) G ) )

Proof

Step	Hyp	Ref	Expression
1		ofresid.1	|- ( ph -> F : A --> B )
2		ofresid.2	|- ( ph -> G : A --> B )
3		ofresid.3	|- ( ph -> A e. V )
4	1	ffvelcdmda	|- ( ( ph /\ x e. A ) -> ( F ` x ) e. B )
5	2	ffvelcdmda	|- ( ( ph /\ x e. A ) -> ( G ` x ) e. B )
6	4 5	opelxpd	|- ( ( ph /\ x e. A ) -> <. ( F ` x ) , ( G ` x ) >. e. ( B X. B ) )
7	6	fvresd	|- ( ( ph /\ x e. A ) -> ( ( R |` ( B X. B ) ) ` <. ( F ` x ) , ( G ` x ) >. ) = ( R ` <. ( F ` x ) , ( G ` x ) >. ) )
8	7	eqcomd	|- ( ( ph /\ x e. A ) -> ( R ` <. ( F ` x ) , ( G ` x ) >. ) = ( ( R |` ( B X. B ) ) ` <. ( F ` x ) , ( G ` x ) >. ) )
9		df-ov	|- ( ( F ` x ) R ( G ` x ) ) = ( R ` <. ( F ` x ) , ( G ` x ) >. )
10		df-ov	|- ( ( F ` x ) ( R |` ( B X. B ) ) ( G ` x ) ) = ( ( R |` ( B X. B ) ) ` <. ( F ` x ) , ( G ` x ) >. )
11	8 9 10	3eqtr4g	|- ( ( ph /\ x e. A ) -> ( ( F ` x ) R ( G ` x ) ) = ( ( F ` x ) ( R |` ( B X. B ) ) ( G ` x ) ) )
12	11	mpteq2dva	|- ( ph -> ( x e. A |-> ( ( F ` x ) R ( G ` x ) ) ) = ( x e. A |-> ( ( F ` x ) ( R |` ( B X. B ) ) ( G ` x ) ) ) )
13	1	ffnd	|- ( ph -> F Fn A )
14	2	ffnd	|- ( ph -> G Fn A )
15		inidm	|- ( A i^i A ) = A
16		eqidd	|- ( ( ph /\ x e. A ) -> ( F ` x ) = ( F ` x ) )
17		eqidd	|- ( ( ph /\ x e. A ) -> ( G ` x ) = ( G ` x ) )
18	13 14 3 3 15 16 17	offval	|- ( ph -> ( F oF R G ) = ( x e. A |-> ( ( F ` x ) R ( G ` x ) ) ) )
19	13 14 3 3 15 16 17	offval	|- ( ph -> ( F oF ( R |` ( B X. B ) ) G ) = ( x e. A |-> ( ( F ` x ) ( R |` ( B X. B ) ) ( G ` x ) ) ) )
20	12 18 19	3eqtr4d	|- ( ph -> ( F oF R G ) = ( F oF ( R |` ( B X. B ) ) G ) )