ofval

Description: Evaluate a function operation at a point. (Contributed by Mario Carneiro, 20-Jul-2014)

	Ref	Expression
Hypotheses	offval.1	\|- ( ph -> F Fn A )
	offval.2	\|- ( ph -> G Fn B )
	offval.3	\|- ( ph -> A e. V )
	offval.4	\|- ( ph -> B e. W )
	offval.5	\|- ( A i^i B ) = S
	ofval.6	\|- ( ( ph /\ X e. A ) -> ( F ` X ) = C )
	ofval.7	\|- ( ( ph /\ X e. B ) -> ( G ` X ) = D )
Assertion	ofval	\|- ( ( ph /\ X e. S ) -> ( ( F oF R G ) ` X ) = ( C R D ) )

Proof

Step	Hyp	Ref	Expression
1		offval.1	\|- ( ph -> F Fn A )
2		offval.2	\|- ( ph -> G Fn B )
3		offval.3	\|- ( ph -> A e. V )
4		offval.4	\|- ( ph -> B e. W )
5		offval.5	\|- ( A i^i B ) = S
6		ofval.6	\|- ( ( ph /\ X e. A ) -> ( F ` X ) = C )
7		ofval.7	\|- ( ( ph /\ X e. B ) -> ( G ` X ) = D )
8		eqidd	\|- ( ( ph /\ x e. A ) -> ( F ` x ) = ( F ` x ) )
9		eqidd	\|- ( ( ph /\ x e. B ) -> ( G ` x ) = ( G ` x ) )
10	1 2 3 4 5 8 9	offval	\|- ( ph -> ( F oF R G ) = ( x e. S \|-> ( ( F ` x ) R ( G ` x ) ) ) )
11	10	fveq1d	\|- ( ph -> ( ( F oF R G ) ` X ) = ( ( x e. S \|-> ( ( F ` x ) R ( G ` x ) ) ) ` X ) )
12	11	adantr	\|- ( ( ph /\ X e. S ) -> ( ( F oF R G ) ` X ) = ( ( x e. S \|-> ( ( F ` x ) R ( G ` x ) ) ) ` X ) )
13		fveq2	\|- ( x = X -> ( F ` x ) = ( F ` X ) )
14		fveq2	\|- ( x = X -> ( G ` x ) = ( G ` X ) )
15	13 14	oveq12d	\|- ( x = X -> ( ( F ` x ) R ( G ` x ) ) = ( ( F ` X ) R ( G ` X ) ) )
16		eqid	\|- ( x e. S \|-> ( ( F ` x ) R ( G ` x ) ) ) = ( x e. S \|-> ( ( F ` x ) R ( G ` x ) ) )
17		ovex	\|- ( ( F ` X ) R ( G ` X ) ) e. _V
18	15 16 17	fvmpt	\|- ( X e. S -> ( ( x e. S \|-> ( ( F ` x ) R ( G ` x ) ) ) ` X ) = ( ( F ` X ) R ( G ` X ) ) )
19	18	adantl	\|- ( ( ph /\ X e. S ) -> ( ( x e. S \|-> ( ( F ` x ) R ( G ` x ) ) ) ` X ) = ( ( F ` X ) R ( G ` X ) ) )
20		inss1	\|- ( A i^i B ) C_ A
21	5 20	eqsstrri	\|- S C_ A
22	21	sseli	\|- ( X e. S -> X e. A )
23	22 6	sylan2	\|- ( ( ph /\ X e. S ) -> ( F ` X ) = C )
24		inss2	\|- ( A i^i B ) C_ B
25	5 24	eqsstrri	\|- S C_ B
26	25	sseli	\|- ( X e. S -> X e. B )
27	26 7	sylan2	\|- ( ( ph /\ X e. S ) -> ( G ` X ) = D )
28	23 27	oveq12d	\|- ( ( ph /\ X e. S ) -> ( ( F ` X ) R ( G ` X ) ) = ( C R D ) )
29	12 19 28	3eqtrd	\|- ( ( ph /\ X e. S ) -> ( ( F oF R G ) ` X ) = ( C R D ) )

Metamath Proof Explorer

Theorem ofval

Proof