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=1stV×V-1F1stV×V2ndV×V-1G2ndV×V
fsplitfpar.s S=1stI-1A
Assertion fsplitfpar FFnAGFnAHS=xAFxGx

Proof

Step Hyp Ref Expression
1 fsplitfpar.h H=1stV×V-1F1stV×V2ndV×V-1G2ndV×V
2 fsplitfpar.s S=1stI-1A
3 fsplit 1stI-1=xVxx
4 3 reseq1i 1stI-1A=xVxxA
5 2 4 eqtri S=xVxxA
6 5 fveq1i Sa=xVxxAa
7 6 a1i FFnAGFnAaASa=xVxxAa
8 fvres aAxVxxAa=xVxxa
9 eqidd aAxVxx=xVxx
10 id x=ax=a
11 10 10 opeq12d x=axx=aa
12 11 adantl aAx=axx=aa
13 elex aAaV
14 opex aaV
15 14 a1i aAaaV
16 9 12 13 15 fvmptd aAxVxxa=aa
17 8 16 eqtrd aAxVxxAa=aa
18 17 adantl FFnAGFnAaAxVxxAa=aa
19 7 18 eqtrd FFnAGFnAaASa=aa
20 19 fveq2d FFnAGFnAaAHSa=Haa
21 df-ov aHa=Haa
22 1 fpar FFnAGFnAH=xA,yAFxGy
23 22 adantr FFnAGFnAaAH=xA,yAFxGy
24 fveq2 x=aFx=Fa
25 24 adantr x=ay=aFx=Fa
26 fveq2 y=aGy=Ga
27 26 adantl x=ay=aGy=Ga
28 25 27 opeq12d x=ay=aFxGy=FaGa
29 28 adantl FFnAGFnAaAx=ay=aFxGy=FaGa
30 simpr FFnAGFnAaAaA
31 opex FaGaV
32 31 a1i FFnAGFnAaAFaGaV
33 23 29 30 30 32 ovmpod FFnAGFnAaAaHa=FaGa
34 21 33 eqtr3id FFnAGFnAaAHaa=FaGa
35 20 34 eqtrd FFnAGFnAaAHSa=FaGa
36 eqid aVaa=aVaa
37 36 fnmpt aVaaVaVaaFnV
38 14 a1i aVaaV
39 37 38 mprg aVaaFnV
40 ssv AV
41 fnssres aVaaFnVAVaVaaAFnA
42 39 40 41 mp2an aVaaAFnA
43 fsplit 1stI-1=aVaa
44 43 reseq1i 1stI-1A=aVaaA
45 2 44 eqtri S=aVaaA
46 45 fneq1i SFnAaVaaAFnA
47 42 46 mpbir SFnA
48 47 a1i FFnAGFnASFnA
49 fvco2 SFnAaAHSa=HSa
50 48 49 sylan FFnAGFnAaAHSa=HSa
51 fveq2 x=aGx=Ga
52 24 51 opeq12d x=aFxGx=FaGa
53 eqid xAFxGx=xAFxGx
54 52 53 31 fvmpt aAxAFxGxa=FaGa
55 54 adantl FFnAGFnAaAxAFxGxa=FaGa
56 35 50 55 3eqtr4d FFnAGFnAaAHSa=xAFxGxa
57 56 ralrimiva FFnAGFnAaAHSa=xAFxGxa
58 opex FxGyV
59 58 a1i FFnAGFnAxAyAFxGyV
60 59 ralrimivva FFnAGFnAxAyAFxGyV
61 eqid xA,yAFxGy=xA,yAFxGy
62 61 fnmpo xAyAFxGyVxA,yAFxGyFnA×A
63 60 62 syl FFnAGFnAxA,yAFxGyFnA×A
64 22 fneq1d FFnAGFnAHFnA×AxA,yAFxGyFnA×A
65 63 64 mpbird FFnAGFnAHFnA×A
66 14 a1i FFnAGFnAaVaaV
67 66 ralrimiva FFnAGFnAaVaaV
68 67 37 syl FFnAGFnAaVaaFnV
69 68 40 41 sylancl FFnAGFnAaVaaAFnA
70 69 46 sylibr FFnAGFnASFnA
71 45 rneqi ranS=ranaVaaA
72 mptima aVaaA=ranaVAaa
73 df-ima aVaaA=ranaVaaA
74 eqid aVAaa=aVAaa
75 74 rnmpt ranaVAaa=p|aVAp=aa
76 72 73 75 3eqtr3i ranaVaaA=p|aVAp=aa
77 71 76 eqtri ranS=p|aVAp=aa
78 elinel2 aVAaA
79 simpl aAp=aaaA
80 79 79 opelxpd aAp=aaaaA×A
81 eleq1 p=aapA×AaaA×A
82 81 adantl aAp=aapA×AaaA×A
83 80 82 mpbird aAp=aapA×A
84 83 ex aAp=aapA×A
85 78 84 syl aVAp=aapA×A
86 85 rexlimiv aVAp=aapA×A
87 86 abssi p|aVAp=aaA×A
88 87 a1i FFnAGFnAp|aVAp=aaA×A
89 77 88 eqsstrid FFnAGFnAranSA×A
90 fnco HFnA×ASFnAranSA×AHSFnA
91 65 70 89 90 syl3anc FFnAGFnAHSFnA
92 opex FxGxV
93 92 a1i FFnAGFnAxAFxGxV
94 93 ralrimiva FFnAGFnAxAFxGxV
95 53 fnmpt xAFxGxVxAFxGxFnA
96 94 95 syl FFnAGFnAxAFxGxFnA
97 eqfnfv HSFnAxAFxGxFnAHS=xAFxGxaAHSa=xAFxGxa
98 91 96 97 syl2anc FFnAGFnAHS=xAFxGxaAHSa=xAFxGxa
99 57 98 mpbird FFnAGFnAHS=xAFxGx