Theorem ofres

Description: Restrict the operands of a function operation to the same domain as that of the operation itself. (Contributed by Mario Carneiro, 15-Sep-2014)

	Ref	Expression
Hypotheses	ofres.1	|- ( ph -> F Fn A )
	ofres.2	|- ( ph -> G Fn B )
	ofres.3	|- ( ph -> A e. V )
	ofres.4	|- ( ph -> B e. W )
	ofres.5	|- ( A i^i B ) = C
Assertion	ofres	|- ( ph -> ( F oF R G ) = ( ( F |` C ) oF R ( G |` C ) ) )

Proof

Step	Hyp	Ref	Expression
1		ofres.1	|- ( ph -> F Fn A )
2		ofres.2	|- ( ph -> G Fn B )
3		ofres.3	|- ( ph -> A e. V )
4		ofres.4	|- ( ph -> B e. W )
5		ofres.5	|- ( A i^i B ) = C
6		eqidd	|- ( ( ph /\ x e. A ) -> ( F ` x ) = ( F ` x ) )
7		eqidd	|- ( ( ph /\ x e. B ) -> ( G ` x ) = ( G ` x ) )
8	1 2 3 4 5 6 7	offval	|- ( ph -> ( F oF R G ) = ( x e. C |-> ( ( F ` x ) R ( G ` x ) ) ) )
9		inss1	|- ( A i^i B ) C_ A
10	5 9	eqsstrri	|- C C_ A
11		fnssres	|- ( ( F Fn A /\ C C_ A ) -> ( F |` C ) Fn C )
12	1 10 11	sylancl	|- ( ph -> ( F |` C ) Fn C )
13		inss2	|- ( A i^i B ) C_ B
14	5 13	eqsstrri	|- C C_ B
15		fnssres	|- ( ( G Fn B /\ C C_ B ) -> ( G |` C ) Fn C )
16	2 14 15	sylancl	|- ( ph -> ( G |` C ) Fn C )
17		ssexg	|- ( ( C C_ A /\ A e. V ) -> C e. _V )
18	10 3 17	sylancr	|- ( ph -> C e. _V )
19		inidm	|- ( C i^i C ) = C
20		fvres	|- ( x e. C -> ( ( F |` C ) ` x ) = ( F ` x ) )
21	20	adantl	|- ( ( ph /\ x e. C ) -> ( ( F |` C ) ` x ) = ( F ` x ) )
22		fvres	|- ( x e. C -> ( ( G |` C ) ` x ) = ( G ` x ) )
23	22	adantl	|- ( ( ph /\ x e. C ) -> ( ( G |` C ) ` x ) = ( G ` x ) )
24	12 16 18 18 19 21 23	offval	|- ( ph -> ( ( F |` C ) oF R ( G |` C ) ) = ( x e. C |-> ( ( F ` x ) R ( G ` x ) ) ) )
25	8 24	eqtr4d	|- ( ph -> ( F oF R G ) = ( ( F |` C ) oF R ( G |` C ) ) )