offsplitfpar

Description: Express the function operation map oF by the functions defined in fsplit and fpar . (Contributed by AV, 4-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	offsplitfpar	$⊢ ((F Fn A \land G Fn A) \land (F \in V \land G \in W) \land (\underset{˙}{+} Fn C \land ran F \times ran G \subseteq C)) \to \underset{˙}{+} \circ (H \circ S) = F {\underset{˙}{+}}_{f} G$

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	1 2	fsplitfpar	$⊢ (F Fn A \land G Fn A) \to H \circ S = (a \in A ⟼ ⟨F (a), G (a)⟩)$
4	3	coeq2d	$⊢ (F Fn A \land G Fn A) \to \underset{˙}{+} \circ (H \circ S) = \underset{˙}{+} \circ (a \in A ⟼ ⟨F (a), G (a)⟩)$
5	4	3ad2ant1	$⊢ ((F Fn A \land G Fn A) \land (F \in V \land G \in W) \land (\underset{˙}{+} Fn C \land ran F \times ran G \subseteq C)) \to \underset{˙}{+} \circ (H \circ S) = \underset{˙}{+} \circ (a \in A ⟼ ⟨F (a), G (a)⟩)$
6		dffn3	$⊢ \underset{˙}{+} Fn C \leftrightarrow \underset{˙}{+} : C ⟶ ran \underset{˙}{+}$
7	6	birani	$⊢ (\underset{˙}{+} Fn C \land ran F \times ran G \subseteq C) \to \underset{˙}{+} : C ⟶ ran \underset{˙}{+}$
8	7	3ad2ant3	$⊢ ((F Fn A \land G Fn A) \land (F \in V \land G \in W) \land (\underset{˙}{+} Fn C \land ran F \times ran G \subseteq C)) \to \underset{˙}{+} : C ⟶ ran \underset{˙}{+}$
9		simpl3r	$⊢ (((F Fn A \land G Fn A) \land (F \in V \land G \in W) \land (\underset{˙}{+} Fn C \land ran F \times ran G \subseteq C)) \land a \in A) \to ran F \times ran G \subseteq C$
10		simp1l	$⊢ ((F Fn A \land G Fn A) \land (F \in V \land G \in W) \land (\underset{˙}{+} Fn C \land ran F \times ran G \subseteq C)) \to F Fn A$
11		fnfvelrn	$⊢ (F Fn A \land a \in A) \to F (a) \in ran F$
12	10 11	sylan	$⊢ (((F Fn A \land G Fn A) \land (F \in V \land G \in W) \land (\underset{˙}{+} Fn C \land ran F \times ran G \subseteq C)) \land a \in A) \to F (a) \in ran F$
13		simp1r	$⊢ ((F Fn A \land G Fn A) \land (F \in V \land G \in W) \land (\underset{˙}{+} Fn C \land ran F \times ran G \subseteq C)) \to G Fn A$
14		fnfvelrn	$⊢ (G Fn A \land a \in A) \to G (a) \in ran G$
15	13 14	sylan	$⊢ (((F Fn A \land G Fn A) \land (F \in V \land G \in W) \land (\underset{˙}{+} Fn C \land ran F \times ran G \subseteq C)) \land a \in A) \to G (a) \in ran G$
16	12 15	opelxpd	$⊢ (((F Fn A \land G Fn A) \land (F \in V \land G \in W) \land (\underset{˙}{+} Fn C \land ran F \times ran G \subseteq C)) \land a \in A) \to ⟨F (a), G (a)⟩ \in (ran F \times ran G)$
17	9 16	sseldd	$⊢ (((F Fn A \land G Fn A) \land (F \in V \land G \in W) \land (\underset{˙}{+} Fn C \land ran F \times ran G \subseteq C)) \land a \in A) \to ⟨F (a), G (a)⟩ \in C$
18	8 17	cofmpt	$⊢ ((F Fn A \land G Fn A) \land (F \in V \land G \in W) \land (\underset{˙}{+} Fn C \land ran F \times ran G \subseteq C)) \to \underset{˙}{+} \circ (a \in A ⟼ ⟨F (a), G (a)⟩) = (a \in A ⟼ \underset{˙}{+} (⟨F (a), G (a)⟩))$
19		df-ov	$⊢ F (a) \underset{˙}{+} G (a) = \underset{˙}{+} (⟨F (a), G (a)⟩)$
20	19	eqcomi	$⊢ \underset{˙}{+} (⟨F (a), G (a)⟩) = F (a) \underset{˙}{+} G (a)$
21	20	mpteq2i	$⊢ (a \in A ⟼ \underset{˙}{+} (⟨F (a), G (a)⟩)) = (a \in A ⟼ F (a) \underset{˙}{+} G (a))$
22	18 21	eqtrdi	$⊢ ((F Fn A \land G Fn A) \land (F \in V \land G \in W) \land (\underset{˙}{+} Fn C \land ran F \times ran G \subseteq C)) \to \underset{˙}{+} \circ (a \in A ⟼ ⟨F (a), G (a)⟩) = (a \in A ⟼ F (a) \underset{˙}{+} G (a))$
23		offval3	$⊢ (F \in V \land G \in W) \to F {\underset{˙}{+}}_{f} G = (a \in (dom F \cap dom G) ⟼ F (a) \underset{˙}{+} G (a))$
24		fndm	$⊢ F Fn A \to dom F = A$
25		fndm	$⊢ G Fn A \to dom G = A$
26	24 25	ineqan12d	$⊢ (F Fn A \land G Fn A) \to dom F \cap dom G = A \cap A$
27		inidm	$⊢ A \cap A = A$
28	26 27	eqtrdi	$⊢ (F Fn A \land G Fn A) \to dom F \cap dom G = A$
29	28	mpteq1d	$⊢ (F Fn A \land G Fn A) \to (a \in (dom F \cap dom G) ⟼ F (a) \underset{˙}{+} G (a)) = (a \in A ⟼ F (a) \underset{˙}{+} G (a))$
30	23 29	sylan9eqr	$⊢ ((F Fn A \land G Fn A) \land (F \in V \land G \in W)) \to F {\underset{˙}{+}}_{f} G = (a \in A ⟼ F (a) \underset{˙}{+} G (a))$
31	30	eqcomd	$⊢ ((F Fn A \land G Fn A) \land (F \in V \land G \in W)) \to (a \in A ⟼ F (a) \underset{˙}{+} G (a)) = F {\underset{˙}{+}}_{f} G$
32	31	3adant3	$⊢ ((F Fn A \land G Fn A) \land (F \in V \land G \in W) \land (\underset{˙}{+} Fn C \land ran F \times ran G \subseteq C)) \to (a \in A ⟼ F (a) \underset{˙}{+} G (a)) = F {\underset{˙}{+}}_{f} G$
33	5 22 32	3eqtrd	$⊢ ((F Fn A \land G Fn A) \land (F \in V \land G \in W) \land (\underset{˙}{+} Fn C \land ran F \times ran G \subseteq C)) \to \underset{˙}{+} \circ (H \circ S) = F {\underset{˙}{+}}_{f} G$

Metamath Proof Explorer

Theorem offsplitfpar

Proof