Theorem ofcfval

Description: Value of an operation applied to a function and a constant. (Contributed by Thierry Arnoux, 30-Jan-2017)

	Ref	Expression
Hypotheses	ofcfval.1	|- ( ph -> F Fn A )
	ofcfval.2	|- ( ph -> A e. V )
	ofcfval.3	|- ( ph -> C e. W )
	ofcfval.6	|- ( ( ph /\ x e. A ) -> ( F ` x ) = B )
Assertion	ofcfval	|- ( ph -> ( F oFC R C ) = ( x e. A |-> ( B R C ) ) )

Proof

Step	Hyp	Ref	Expression
1		ofcfval.1	|- ( ph -> F Fn A )
2		ofcfval.2	|- ( ph -> A e. V )
3		ofcfval.3	|- ( ph -> C e. W )
4		ofcfval.6	|- ( ( ph /\ x e. A ) -> ( F ` x ) = B )
5		df-ofc	|- oFC R = ( f e. _V , c e. _V |-> ( x e. dom f |-> ( ( f ` x ) R c ) ) )
6	5	a1i	|- ( ph -> oFC R = ( f e. _V , c e. _V |-> ( x e. dom f |-> ( ( f ` x ) R c ) ) ) )
7		simprl	|- ( ( ph /\ ( f = F /\ c = C ) ) -> f = F )
8	7	dmeqd	|- ( ( ph /\ ( f = F /\ c = C ) ) -> dom f = dom F )
9	7	fveq1d	|- ( ( ph /\ ( f = F /\ c = C ) ) -> ( f ` x ) = ( F ` x ) )
10		simprr	|- ( ( ph /\ ( f = F /\ c = C ) ) -> c = C )
11	9 10	oveq12d	|- ( ( ph /\ ( f = F /\ c = C ) ) -> ( ( f ` x ) R c ) = ( ( F ` x ) R C ) )
12	8 11	mpteq12dv	|- ( ( ph /\ ( f = F /\ c = C ) ) -> ( x e. dom f |-> ( ( f ` x ) R c ) ) = ( x e. dom F |-> ( ( F ` x ) R C ) ) )
13		fnex	|- ( ( F Fn A /\ A e. V ) -> F e. _V )
14	1 2 13	syl2anc	|- ( ph -> F e. _V )
15	3	elexd	|- ( ph -> C e. _V )
16	1	fndmd	|- ( ph -> dom F = A )
17	16 2	eqeltrd	|- ( ph -> dom F e. V )
18	17	mptexd	|- ( ph -> ( x e. dom F |-> ( ( F ` x ) R C ) ) e. _V )
19	6 12 14 15 18	ovmpod	|- ( ph -> ( F oFC R C ) = ( x e. dom F |-> ( ( F ` x ) R C ) ) )
20	16	eleq2d	|- ( ph -> ( x e. dom F <-> x e. A ) )
21	20	pm5.32i	|- ( ( ph /\ x e. dom F ) <-> ( ph /\ x e. A ) )
22	21 4	sylbi	|- ( ( ph /\ x e. dom F ) -> ( F ` x ) = B )
23	22	oveq1d	|- ( ( ph /\ x e. dom F ) -> ( ( F ` x ) R C ) = ( B R C ) )
24	16 23	mpteq12dva	|- ( ph -> ( x e. dom F |-> ( ( F ` x ) R C ) ) = ( x e. A |-> ( B R C ) ) )
25	19 24	eqtrd	|- ( ph -> ( F oFC R C ) = ( x e. A |-> ( B R C ) ) )