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	biimpi	$⊢ \underset{˙}{+} Fn C \to \underset{˙}{+} : C ⟶ ran \underset{˙}{+}$
8	7	adantr	$⊢ (\underset{˙}{+} Fn C \land ran F \times ran G \subseteq C) \to \underset{˙}{+} : C ⟶ ran \underset{˙}{+}$
9	8	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{˙}{+}$
10		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$
11		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$
12		fnfvelrn	$⊢ (F Fn A \land a \in A) \to F (a) \in ran F$
13	11 12	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$
14		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$
15		fnfvelrn	$⊢ (G Fn A \land a \in A) \to G (a) \in ran G$
16	14 15	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$
17	13 16	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)$
18	10 17	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$
19	9 18	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)⟩))$
20		df-ov	$⊢ F (a) \underset{˙}{+} G (a) = \underset{˙}{+} (⟨F (a), G (a)⟩)$
21	20	eqcomi	$⊢ \underset{˙}{+} (⟨F (a), G (a)⟩) = F (a) \underset{˙}{+} G (a)$
22	21	mpteq2i	$⊢ (a \in A ⟼ \underset{˙}{+} (⟨F (a), G (a)⟩)) = (a \in A ⟼ F (a) \underset{˙}{+} G (a))$
23	19 22	syl6eq	$⊢ ((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))$
24		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))$
25		fndm	$⊢ F Fn A \to dom F = A$
26		fndm	$⊢ G Fn A \to dom G = A$
27	25 26	ineqan12d	$⊢ (F Fn A \land G Fn A) \to dom F \cap dom G = A \cap A$
28		inidm	$⊢ A \cap A = A$
29	27 28	syl6eq	$⊢ (F Fn A \land G Fn A) \to dom F \cap dom G = A$
30	29	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))$
31	24 30	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))$
32	31	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$
33	32	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$
34	5 23 33	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