Metamath Proof Explorer

Theorem ofmpteq

Description: Value of a pointwise operation on two functions defined using maps-to notation. (Contributed by Stefan O'Rear, 5-Oct-2014)

Ref Expression
Assertion ofmpteq 
|- ( ( A e. V /\ ( x e. A |-> B ) Fn A /\ ( x e. A |-> C ) Fn A ) -> ( ( x e. A |-> B ) oF R ( x e. A |-> C ) ) = ( x e. A |-> ( B R C ) ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. V /\ ( x e. A |-> B ) Fn A /\ ( x e. A |-> C ) Fn A ) -> A e. V )
2 simpr 
 |-  ( ( ( A e. V /\ ( x e. A |-> B ) Fn A /\ ( x e. A |-> C ) Fn A ) /\ a e. A ) -> a e. A )
3 simpl2 
 |-  ( ( ( A e. V /\ ( x e. A |-> B ) Fn A /\ ( x e. A |-> C ) Fn A ) /\ a e. A ) -> ( x e. A |-> B ) Fn A )
4 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
5 4 mptfng 
 |-  ( A. x e. A B e. _V <-> ( x e. A |-> B ) Fn A )
6 3 5 sylibr 
 |-  ( ( ( A e. V /\ ( x e. A |-> B ) Fn A /\ ( x e. A |-> C ) Fn A ) /\ a e. A ) -> A. x e. A B e. _V )
7 nfcsb1v 
 |-  F/_ x [_ a / x ]_ B
8 7 nfel1 
 |-  F/ x [_ a / x ]_ B e. _V
9 csbeq1a 
 |-  ( x = a -> B = [_ a / x ]_ B )
10 9 eleq1d 
 |-  ( x = a -> ( B e. _V <-> [_ a / x ]_ B e. _V ) )
11 8 10 rspc 
 |-  ( a e. A -> ( A. x e. A B e. _V -> [_ a / x ]_ B e. _V ) )
12 2 6 11 sylc 
 |-  ( ( ( A e. V /\ ( x e. A |-> B ) Fn A /\ ( x e. A |-> C ) Fn A ) /\ a e. A ) -> [_ a / x ]_ B e. _V )
13 simpl3 
 |-  ( ( ( A e. V /\ ( x e. A |-> B ) Fn A /\ ( x e. A |-> C ) Fn A ) /\ a e. A ) -> ( x e. A |-> C ) Fn A )
14 eqid 
 |-  ( x e. A |-> C ) = ( x e. A |-> C )
15 14 mptfng 
 |-  ( A. x e. A C e. _V <-> ( x e. A |-> C ) Fn A )
16 13 15 sylibr 
 |-  ( ( ( A e. V /\ ( x e. A |-> B ) Fn A /\ ( x e. A |-> C ) Fn A ) /\ a e. A ) -> A. x e. A C e. _V )
17 nfcsb1v 
 |-  F/_ x [_ a / x ]_ C
18 17 nfel1 
 |-  F/ x [_ a / x ]_ C e. _V
19 csbeq1a 
 |-  ( x = a -> C = [_ a / x ]_ C )
20 19 eleq1d 
 |-  ( x = a -> ( C e. _V <-> [_ a / x ]_ C e. _V ) )
21 18 20 rspc 
 |-  ( a e. A -> ( A. x e. A C e. _V -> [_ a / x ]_ C e. _V ) )
22 2 16 21 sylc 
 |-  ( ( ( A e. V /\ ( x e. A |-> B ) Fn A /\ ( x e. A |-> C ) Fn A ) /\ a e. A ) -> [_ a / x ]_ C e. _V )
23 nfcv 
 |-  F/_ a B
24 23 7 9 cbvmpt 
 |-  ( x e. A |-> B ) = ( a e. A |-> [_ a / x ]_ B )
25 24 a1i 
 |-  ( ( A e. V /\ ( x e. A |-> B ) Fn A /\ ( x e. A |-> C ) Fn A ) -> ( x e. A |-> B ) = ( a e. A |-> [_ a / x ]_ B ) )
26 nfcv 
 |-  F/_ a C
27 26 17 19 cbvmpt 
 |-  ( x e. A |-> C ) = ( a e. A |-> [_ a / x ]_ C )
28 27 a1i 
 |-  ( ( A e. V /\ ( x e. A |-> B ) Fn A /\ ( x e. A |-> C ) Fn A ) -> ( x e. A |-> C ) = ( a e. A |-> [_ a / x ]_ C ) )
29 1 12 22 25 28 offval2 
 |-  ( ( A e. V /\ ( x e. A |-> B ) Fn A /\ ( x e. A |-> C ) Fn A ) -> ( ( x e. A |-> B ) oF R ( x e. A |-> C ) ) = ( a e. A |-> ( [_ a / x ]_ B R [_ a / x ]_ C ) ) )
30 nfcv 
 |-  F/_ a ( B R C )
31 nfcv 
 |-  F/_ x R
32 7 31 17 nfov 
 |-  F/_ x ( [_ a / x ]_ B R [_ a / x ]_ C )
33 9 19 oveq12d 
 |-  ( x = a -> ( B R C ) = ( [_ a / x ]_ B R [_ a / x ]_ C ) )
34 30 32 33 cbvmpt 
 |-  ( x e. A |-> ( B R C ) ) = ( a e. A |-> ( [_ a / x ]_ B R [_ a / x ]_ C ) )
35 29 34 eqtr4di 
 |-  ( ( A e. V /\ ( x e. A |-> B ) Fn A /\ ( x e. A |-> C ) Fn A ) -> ( ( x e. A |-> B ) oF R ( x e. A |-> C ) ) = ( x e. A |-> ( B R C ) ) )