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

Metamath Proof Explorer

Theorem ofresid

Proof