Metamath Proof Explorer


Theorem fvmpopr2d

Description: Value of an operation given by maps-to notation. (Contributed by Rohan Ridenour, 14-May-2024)

Ref Expression
Hypotheses fvmpopr2d.1
|- ( ph -> F = ( a e. A , b e. B |-> C ) )
fvmpopr2d.2
|- ( ph -> P = <. a , b >. )
fvmpopr2d.3
|- ( ( ph /\ a e. A /\ b e. B ) -> C e. V )
Assertion fvmpopr2d
|- ( ( ph /\ a e. A /\ b e. B ) -> ( F ` P ) = C )

Proof

Step Hyp Ref Expression
1 fvmpopr2d.1
 |-  ( ph -> F = ( a e. A , b e. B |-> C ) )
2 fvmpopr2d.2
 |-  ( ph -> P = <. a , b >. )
3 fvmpopr2d.3
 |-  ( ( ph /\ a e. A /\ b e. B ) -> C e. V )
4 df-ov
 |-  ( a ( a e. A , b e. B |-> C ) b ) = ( ( a e. A , b e. B |-> C ) ` <. a , b >. )
5 1 3ad2ant1
 |-  ( ( ph /\ a e. A /\ b e. B ) -> F = ( a e. A , b e. B |-> C ) )
6 2 3ad2ant1
 |-  ( ( ph /\ a e. A /\ b e. B ) -> P = <. a , b >. )
7 5 6 fveq12d
 |-  ( ( ph /\ a e. A /\ b e. B ) -> ( F ` P ) = ( ( a e. A , b e. B |-> C ) ` <. a , b >. ) )
8 4 7 eqtr4id
 |-  ( ( ph /\ a e. A /\ b e. B ) -> ( a ( a e. A , b e. B |-> C ) b ) = ( F ` P ) )
9 nfcv
 |-  F/_ c C
10 nfcv
 |-  F/_ d C
11 nfcv
 |-  F/_ a d
12 nfcsb1v
 |-  F/_ a [_ c / a ]_ C
13 11 12 nfcsbw
 |-  F/_ a [_ d / b ]_ [_ c / a ]_ C
14 nfcsb1v
 |-  F/_ b [_ d / b ]_ [_ c / a ]_ C
15 csbeq1a
 |-  ( a = c -> C = [_ c / a ]_ C )
16 csbeq1a
 |-  ( b = d -> [_ c / a ]_ C = [_ d / b ]_ [_ c / a ]_ C )
17 15 16 sylan9eq
 |-  ( ( a = c /\ b = d ) -> C = [_ d / b ]_ [_ c / a ]_ C )
18 9 10 13 14 17 cbvmpo
 |-  ( a e. A , b e. B |-> C ) = ( c e. A , d e. B |-> [_ d / b ]_ [_ c / a ]_ C )
19 18 oveqi
 |-  ( a ( a e. A , b e. B |-> C ) b ) = ( a ( c e. A , d e. B |-> [_ d / b ]_ [_ c / a ]_ C ) b )
20 eqidd
 |-  ( ( ph /\ a e. A /\ b e. B ) -> ( c e. A , d e. B |-> [_ d / b ]_ [_ c / a ]_ C ) = ( c e. A , d e. B |-> [_ d / b ]_ [_ c / a ]_ C ) )
21 equcom
 |-  ( a = c <-> c = a )
22 equcom
 |-  ( b = d <-> d = b )
23 21 22 anbi12i
 |-  ( ( a = c /\ b = d ) <-> ( c = a /\ d = b ) )
24 23 17 sylbir
 |-  ( ( c = a /\ d = b ) -> C = [_ d / b ]_ [_ c / a ]_ C )
25 24 eqcomd
 |-  ( ( c = a /\ d = b ) -> [_ d / b ]_ [_ c / a ]_ C = C )
26 25 adantl
 |-  ( ( ( ph /\ a e. A /\ b e. B ) /\ ( c = a /\ d = b ) ) -> [_ d / b ]_ [_ c / a ]_ C = C )
27 simp2
 |-  ( ( ph /\ a e. A /\ b e. B ) -> a e. A )
28 simp3
 |-  ( ( ph /\ a e. A /\ b e. B ) -> b e. B )
29 20 26 27 28 3 ovmpod
 |-  ( ( ph /\ a e. A /\ b e. B ) -> ( a ( c e. A , d e. B |-> [_ d / b ]_ [_ c / a ]_ C ) b ) = C )
30 19 29 eqtrid
 |-  ( ( ph /\ a e. A /\ b e. B ) -> ( a ( a e. A , b e. B |-> C ) b ) = C )
31 8 30 eqtr3d
 |-  ( ( ph /\ a e. A /\ b e. B ) -> ( F ` P ) = C )