Metamath Proof Explorer


Theorem fsplitfpar

Description: Merge two functions with a common argument in parallel. Combination of fsplit and fpar . (Contributed by AV, 3-Jan-2024)

Ref Expression
Hypotheses fsplitfpar.h
|- H = ( ( `' ( 1st |` ( _V X. _V ) ) o. ( F o. ( 1st |` ( _V X. _V ) ) ) ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. ( G o. ( 2nd |` ( _V X. _V ) ) ) ) )
fsplitfpar.s
|- S = ( `' ( 1st |` _I ) |` A )
Assertion fsplitfpar
|- ( ( F Fn A /\ G Fn A ) -> ( H o. S ) = ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. ) )

Proof

Step Hyp Ref Expression
1 fsplitfpar.h
 |-  H = ( ( `' ( 1st |` ( _V X. _V ) ) o. ( F o. ( 1st |` ( _V X. _V ) ) ) ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. ( G o. ( 2nd |` ( _V X. _V ) ) ) ) )
2 fsplitfpar.s
 |-  S = ( `' ( 1st |` _I ) |` A )
3 fsplit
 |-  `' ( 1st |` _I ) = ( x e. _V |-> <. x , x >. )
4 3 reseq1i
 |-  ( `' ( 1st |` _I ) |` A ) = ( ( x e. _V |-> <. x , x >. ) |` A )
5 2 4 eqtri
 |-  S = ( ( x e. _V |-> <. x , x >. ) |` A )
6 5 fveq1i
 |-  ( S ` a ) = ( ( ( x e. _V |-> <. x , x >. ) |` A ) ` a )
7 6 a1i
 |-  ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( S ` a ) = ( ( ( x e. _V |-> <. x , x >. ) |` A ) ` a ) )
8 fvres
 |-  ( a e. A -> ( ( ( x e. _V |-> <. x , x >. ) |` A ) ` a ) = ( ( x e. _V |-> <. x , x >. ) ` a ) )
9 eqidd
 |-  ( a e. A -> ( x e. _V |-> <. x , x >. ) = ( x e. _V |-> <. x , x >. ) )
10 id
 |-  ( x = a -> x = a )
11 10 10 opeq12d
 |-  ( x = a -> <. x , x >. = <. a , a >. )
12 11 adantl
 |-  ( ( a e. A /\ x = a ) -> <. x , x >. = <. a , a >. )
13 elex
 |-  ( a e. A -> a e. _V )
14 opex
 |-  <. a , a >. e. _V
15 14 a1i
 |-  ( a e. A -> <. a , a >. e. _V )
16 9 12 13 15 fvmptd
 |-  ( a e. A -> ( ( x e. _V |-> <. x , x >. ) ` a ) = <. a , a >. )
17 8 16 eqtrd
 |-  ( a e. A -> ( ( ( x e. _V |-> <. x , x >. ) |` A ) ` a ) = <. a , a >. )
18 17 adantl
 |-  ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( ( ( x e. _V |-> <. x , x >. ) |` A ) ` a ) = <. a , a >. )
19 7 18 eqtrd
 |-  ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( S ` a ) = <. a , a >. )
20 19 fveq2d
 |-  ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( H ` ( S ` a ) ) = ( H ` <. a , a >. ) )
21 df-ov
 |-  ( a H a ) = ( H ` <. a , a >. )
22 1 fpar
 |-  ( ( F Fn A /\ G Fn A ) -> H = ( x e. A , y e. A |-> <. ( F ` x ) , ( G ` y ) >. ) )
23 22 adantr
 |-  ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> H = ( x e. A , y e. A |-> <. ( F ` x ) , ( G ` y ) >. ) )
24 fveq2
 |-  ( x = a -> ( F ` x ) = ( F ` a ) )
25 24 adantr
 |-  ( ( x = a /\ y = a ) -> ( F ` x ) = ( F ` a ) )
26 fveq2
 |-  ( y = a -> ( G ` y ) = ( G ` a ) )
27 26 adantl
 |-  ( ( x = a /\ y = a ) -> ( G ` y ) = ( G ` a ) )
28 25 27 opeq12d
 |-  ( ( x = a /\ y = a ) -> <. ( F ` x ) , ( G ` y ) >. = <. ( F ` a ) , ( G ` a ) >. )
29 28 adantl
 |-  ( ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) /\ ( x = a /\ y = a ) ) -> <. ( F ` x ) , ( G ` y ) >. = <. ( F ` a ) , ( G ` a ) >. )
30 simpr
 |-  ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> a e. A )
31 opex
 |-  <. ( F ` a ) , ( G ` a ) >. e. _V
32 31 a1i
 |-  ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> <. ( F ` a ) , ( G ` a ) >. e. _V )
33 23 29 30 30 32 ovmpod
 |-  ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( a H a ) = <. ( F ` a ) , ( G ` a ) >. )
34 21 33 eqtr3id
 |-  ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( H ` <. a , a >. ) = <. ( F ` a ) , ( G ` a ) >. )
35 20 34 eqtrd
 |-  ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( H ` ( S ` a ) ) = <. ( F ` a ) , ( G ` a ) >. )
36 eqid
 |-  ( a e. _V |-> <. a , a >. ) = ( a e. _V |-> <. a , a >. )
37 36 fnmpt
 |-  ( A. a e. _V <. a , a >. e. _V -> ( a e. _V |-> <. a , a >. ) Fn _V )
38 14 a1i
 |-  ( a e. _V -> <. a , a >. e. _V )
39 37 38 mprg
 |-  ( a e. _V |-> <. a , a >. ) Fn _V
40 ssv
 |-  A C_ _V
41 fnssres
 |-  ( ( ( a e. _V |-> <. a , a >. ) Fn _V /\ A C_ _V ) -> ( ( a e. _V |-> <. a , a >. ) |` A ) Fn A )
42 39 40 41 mp2an
 |-  ( ( a e. _V |-> <. a , a >. ) |` A ) Fn A
43 fsplit
 |-  `' ( 1st |` _I ) = ( a e. _V |-> <. a , a >. )
44 43 reseq1i
 |-  ( `' ( 1st |` _I ) |` A ) = ( ( a e. _V |-> <. a , a >. ) |` A )
45 2 44 eqtri
 |-  S = ( ( a e. _V |-> <. a , a >. ) |` A )
46 45 fneq1i
 |-  ( S Fn A <-> ( ( a e. _V |-> <. a , a >. ) |` A ) Fn A )
47 42 46 mpbir
 |-  S Fn A
48 47 a1i
 |-  ( ( F Fn A /\ G Fn A ) -> S Fn A )
49 fvco2
 |-  ( ( S Fn A /\ a e. A ) -> ( ( H o. S ) ` a ) = ( H ` ( S ` a ) ) )
50 48 49 sylan
 |-  ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( ( H o. S ) ` a ) = ( H ` ( S ` a ) ) )
51 fveq2
 |-  ( x = a -> ( G ` x ) = ( G ` a ) )
52 24 51 opeq12d
 |-  ( x = a -> <. ( F ` x ) , ( G ` x ) >. = <. ( F ` a ) , ( G ` a ) >. )
53 eqid
 |-  ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. ) = ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. )
54 52 53 31 fvmpt
 |-  ( a e. A -> ( ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. ) ` a ) = <. ( F ` a ) , ( G ` a ) >. )
55 54 adantl
 |-  ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. ) ` a ) = <. ( F ` a ) , ( G ` a ) >. )
56 35 50 55 3eqtr4d
 |-  ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( ( H o. S ) ` a ) = ( ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. ) ` a ) )
57 56 ralrimiva
 |-  ( ( F Fn A /\ G Fn A ) -> A. a e. A ( ( H o. S ) ` a ) = ( ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. ) ` a ) )
58 opex
 |-  <. ( F ` x ) , ( G ` y ) >. e. _V
59 58 a1i
 |-  ( ( ( F Fn A /\ G Fn A ) /\ ( x e. A /\ y e. A ) ) -> <. ( F ` x ) , ( G ` y ) >. e. _V )
60 59 ralrimivva
 |-  ( ( F Fn A /\ G Fn A ) -> A. x e. A A. y e. A <. ( F ` x ) , ( G ` y ) >. e. _V )
61 eqid
 |-  ( x e. A , y e. A |-> <. ( F ` x ) , ( G ` y ) >. ) = ( x e. A , y e. A |-> <. ( F ` x ) , ( G ` y ) >. )
62 61 fnmpo
 |-  ( A. x e. A A. y e. A <. ( F ` x ) , ( G ` y ) >. e. _V -> ( x e. A , y e. A |-> <. ( F ` x ) , ( G ` y ) >. ) Fn ( A X. A ) )
63 60 62 syl
 |-  ( ( F Fn A /\ G Fn A ) -> ( x e. A , y e. A |-> <. ( F ` x ) , ( G ` y ) >. ) Fn ( A X. A ) )
64 22 fneq1d
 |-  ( ( F Fn A /\ G Fn A ) -> ( H Fn ( A X. A ) <-> ( x e. A , y e. A |-> <. ( F ` x ) , ( G ` y ) >. ) Fn ( A X. A ) ) )
65 63 64 mpbird
 |-  ( ( F Fn A /\ G Fn A ) -> H Fn ( A X. A ) )
66 14 a1i
 |-  ( ( ( F Fn A /\ G Fn A ) /\ a e. _V ) -> <. a , a >. e. _V )
67 66 ralrimiva
 |-  ( ( F Fn A /\ G Fn A ) -> A. a e. _V <. a , a >. e. _V )
68 67 37 syl
 |-  ( ( F Fn A /\ G Fn A ) -> ( a e. _V |-> <. a , a >. ) Fn _V )
69 68 40 41 sylancl
 |-  ( ( F Fn A /\ G Fn A ) -> ( ( a e. _V |-> <. a , a >. ) |` A ) Fn A )
70 69 46 sylibr
 |-  ( ( F Fn A /\ G Fn A ) -> S Fn A )
71 45 rneqi
 |-  ran S = ran ( ( a e. _V |-> <. a , a >. ) |` A )
72 mptima
 |-  ( ( a e. _V |-> <. a , a >. ) " A ) = ran ( a e. ( _V i^i A ) |-> <. a , a >. )
73 df-ima
 |-  ( ( a e. _V |-> <. a , a >. ) " A ) = ran ( ( a e. _V |-> <. a , a >. ) |` A )
74 eqid
 |-  ( a e. ( _V i^i A ) |-> <. a , a >. ) = ( a e. ( _V i^i A ) |-> <. a , a >. )
75 74 rnmpt
 |-  ran ( a e. ( _V i^i A ) |-> <. a , a >. ) = { p | E. a e. ( _V i^i A ) p = <. a , a >. }
76 72 73 75 3eqtr3i
 |-  ran ( ( a e. _V |-> <. a , a >. ) |` A ) = { p | E. a e. ( _V i^i A ) p = <. a , a >. }
77 71 76 eqtri
 |-  ran S = { p | E. a e. ( _V i^i A ) p = <. a , a >. }
78 elinel2
 |-  ( a e. ( _V i^i A ) -> a e. A )
79 simpl
 |-  ( ( a e. A /\ p = <. a , a >. ) -> a e. A )
80 79 79 opelxpd
 |-  ( ( a e. A /\ p = <. a , a >. ) -> <. a , a >. e. ( A X. A ) )
81 eleq1
 |-  ( p = <. a , a >. -> ( p e. ( A X. A ) <-> <. a , a >. e. ( A X. A ) ) )
82 81 adantl
 |-  ( ( a e. A /\ p = <. a , a >. ) -> ( p e. ( A X. A ) <-> <. a , a >. e. ( A X. A ) ) )
83 80 82 mpbird
 |-  ( ( a e. A /\ p = <. a , a >. ) -> p e. ( A X. A ) )
84 83 ex
 |-  ( a e. A -> ( p = <. a , a >. -> p e. ( A X. A ) ) )
85 78 84 syl
 |-  ( a e. ( _V i^i A ) -> ( p = <. a , a >. -> p e. ( A X. A ) ) )
86 85 rexlimiv
 |-  ( E. a e. ( _V i^i A ) p = <. a , a >. -> p e. ( A X. A ) )
87 86 abssi
 |-  { p | E. a e. ( _V i^i A ) p = <. a , a >. } C_ ( A X. A )
88 87 a1i
 |-  ( ( F Fn A /\ G Fn A ) -> { p | E. a e. ( _V i^i A ) p = <. a , a >. } C_ ( A X. A ) )
89 77 88 eqsstrid
 |-  ( ( F Fn A /\ G Fn A ) -> ran S C_ ( A X. A ) )
90 fnco
 |-  ( ( H Fn ( A X. A ) /\ S Fn A /\ ran S C_ ( A X. A ) ) -> ( H o. S ) Fn A )
91 65 70 89 90 syl3anc
 |-  ( ( F Fn A /\ G Fn A ) -> ( H o. S ) Fn A )
92 opex
 |-  <. ( F ` x ) , ( G ` x ) >. e. _V
93 92 a1i
 |-  ( ( ( F Fn A /\ G Fn A ) /\ x e. A ) -> <. ( F ` x ) , ( G ` x ) >. e. _V )
94 93 ralrimiva
 |-  ( ( F Fn A /\ G Fn A ) -> A. x e. A <. ( F ` x ) , ( G ` x ) >. e. _V )
95 53 fnmpt
 |-  ( A. x e. A <. ( F ` x ) , ( G ` x ) >. e. _V -> ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. ) Fn A )
96 94 95 syl
 |-  ( ( F Fn A /\ G Fn A ) -> ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. ) Fn A )
97 eqfnfv
 |-  ( ( ( H o. S ) Fn A /\ ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. ) Fn A ) -> ( ( H o. S ) = ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. ) <-> A. a e. A ( ( H o. S ) ` a ) = ( ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. ) ` a ) ) )
98 91 96 97 syl2anc
 |-  ( ( F Fn A /\ G Fn A ) -> ( ( H o. S ) = ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. ) <-> A. a e. A ( ( H o. S ) ` a ) = ( ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. ) ` a ) ) )
99 57 98 mpbird
 |-  ( ( F Fn A /\ G Fn A ) -> ( H o. S ) = ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. ) )