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 = 1 st V × V -1 F 1 st V × V 2 nd V × V -1 G 2 nd V × V
fsplitfpar.s S = 1 st I -1 A
Assertion fsplitfpar F Fn A G Fn A H S = x A F x G x

Proof

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