# 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}=\left({\left({{1}^{st}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ \left({F}\circ \left({{1}^{st}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)\right)\right)\cap \left({\left({{2}^{nd}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ \left({G}\circ \left({{2}^{nd}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)\right)\right)$
fsplitfpar.s ${⊢}{S}={{\left({{1}^{st}↾}_{\mathrm{I}}\right)}^{-1}↾}_{{A}}$
Assertion fsplitfpar ${⊢}\left({F}Fn{A}\wedge {G}Fn{A}\right)\to {H}\circ {S}=\left({x}\in {A}⟼⟨{F}\left({x}\right),{G}\left({x}\right)⟩\right)$

### Proof

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