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

Proof

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

Metamath Proof Explorer

Theorem fsplitfpar

Proof