fcores

Description: Every composite function ( G o. F ) can be written as composition of restrictions of the composed functions (to their minimum domains). (Contributed by GL and AV, 17-Sep-2024)

	Ref	Expression
Hypotheses	fcores.f	$⊢ φ \to F : A ⟶ B$
	fcores.e	$⊢ E = ran F \cap C$
	fcores.p	$⊢ P = F^{-1} [C]$
	fcores.x	$⊢ X = {F ↾}_{P}$
	fcores.g	$⊢ φ \to G : C ⟶ D$
	fcores.y	$⊢ Y = {G ↾}_{E}$
Assertion	fcores	$⊢ φ \to G \circ F = Y \circ X$

Proof

Step	Hyp	Ref	Expression
1		fcores.f	$⊢ φ \to F : A ⟶ B$
2		fcores.e	$⊢ E = ran F \cap C$
3		fcores.p	$⊢ P = F^{-1} [C]$
4		fcores.x	$⊢ X = {F ↾}_{P}$
5		fcores.g	$⊢ φ \to G : C ⟶ D$
6		fcores.y	$⊢ Y = {G ↾}_{E}$
7	1	ffund	$⊢ φ \to Fun F$
8		fcof	$⊢ (G : C ⟶ D \land Fun F) \to (G \circ F) : F^{-1} [C] ⟶ D$
9	5 7 8	syl2anc	$⊢ φ \to (G \circ F) : F^{-1} [C] ⟶ D$
10	9	ffnd	$⊢ φ \to (G \circ F) Fn F^{-1} [C]$
11	3	fneq2i	$⊢ (G \circ F) Fn P \leftrightarrow (G \circ F) Fn F^{-1} [C]$
12	10 11	sylibr	$⊢ φ \to (G \circ F) Fn P$
13	1 2 3 4 5 6	fcoreslem4	$⊢ φ \to (Y \circ X) Fn P$
14	4	fveq1i	$⊢ X (x) = ({F ↾}_{P}) (x)$
15		simpr	$⊢ (φ \land x \in P) \to x \in P$
16	15	fvresd	$⊢ (φ \land x \in P) \to ({F ↾}_{P}) (x) = F (x)$
17	14 16	eqtrid	$⊢ (φ \land x \in P) \to X (x) = F (x)$
18	17	fveq2d	$⊢ (φ \land x \in P) \to Y (X (x)) = Y (F (x))$
19	6	fveq1i	$⊢ Y (F (x)) = ({G ↾}_{E}) (F (x))$
20		cnvimass	$⊢ F^{-1} [C] \subseteq dom F$
21	3 20	eqsstri	$⊢ P \subseteq dom F$
22	21	sseli	$⊢ x \in P \to x \in dom F$
23		fvelrn	$⊢ (Fun F \land x \in dom F) \to F (x) \in ran F$
24	7 22 23	syl2an	$⊢ (φ \land x \in P) \to F (x) \in ran F$
25	3	eleq2i	$⊢ x \in P \leftrightarrow x \in F^{-1} [C]$
26	25	biimpi	$⊢ x \in P \to x \in F^{-1} [C]$
27		fvimacnvi	$⊢ (Fun F \land x \in F^{-1} [C]) \to F (x) \in C$
28	7 26 27	syl2an	$⊢ (φ \land x \in P) \to F (x) \in C$
29	24 28	elind	$⊢ (φ \land x \in P) \to F (x) \in (ran F \cap C)$
30	29 2	eleqtrrdi	$⊢ (φ \land x \in P) \to F (x) \in E$
31	30	fvresd	$⊢ (φ \land x \in P) \to ({G ↾}_{E}) (F (x)) = G (F (x))$
32	19 31	eqtrid	$⊢ (φ \land x \in P) \to Y (F (x)) = G (F (x))$
33	18 32	eqtrd	$⊢ (φ \land x \in P) \to Y (X (x)) = G (F (x))$
34	1 2 3 4	fcoreslem3	$⊢ φ \to X : P \underset{onto}{⟶} E$
35		fof	$⊢ X : P \underset{onto}{⟶} E \to X : P ⟶ E$
36	34 35	syl	$⊢ φ \to X : P ⟶ E$
37	36	adantr	$⊢ (φ \land x \in P) \to X : P ⟶ E$
38	37 15	fvco3d	$⊢ (φ \land x \in P) \to (Y \circ X) (x) = Y (X (x))$
39	1	adantr	$⊢ (φ \land x \in P) \to F : A ⟶ B$
40	21	a1i	$⊢ φ \to P \subseteq dom F$
41	40	sselda	$⊢ (φ \land x \in P) \to x \in dom F$
42	1	fdmd	$⊢ φ \to dom F = A$
43	42	eqcomd	$⊢ φ \to A = dom F$
44	43	eleq2d	$⊢ φ \to (x \in A \leftrightarrow x \in dom F)$
45	44	adantr	$⊢ (φ \land x \in P) \to (x \in A \leftrightarrow x \in dom F)$
46	41 45	mpbird	$⊢ (φ \land x \in P) \to x \in A$
47	39 46	fvco3d	$⊢ (φ \land x \in P) \to (G \circ F) (x) = G (F (x))$
48	33 38 47	3eqtr4rd	$⊢ (φ \land x \in P) \to (G \circ F) (x) = (Y \circ X) (x)$
49	12 13 48	eqfnfvd	$⊢ φ \to G \circ F = Y \circ X$

Metamath Proof Explorer

Theorem fcores

Proof