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 ) >. ) )