Theorem 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	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	fcores.e	⊢ 𝐸 = ( ran 𝐹 ∩ 𝐶 )
	fcores.p	⊢ 𝑃 = ( ◡ 𝐹 “ 𝐶 )
	fcores.x	⊢ 𝑋 = ( 𝐹 ↾ 𝑃 )
	fcores.g	⊢ ( 𝜑 → 𝐺 : 𝐶 ⟶ 𝐷 )
	fcores.y	⊢ 𝑌 = ( 𝐺 ↾ 𝐸 )
Assertion	fcores	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑌 ∘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		fcores.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		fcores.e	⊢ 𝐸 = ( ran 𝐹 ∩ 𝐶 )
3		fcores.p	⊢ 𝑃 = ( ◡ 𝐹 “ 𝐶 )
4		fcores.x	⊢ 𝑋 = ( 𝐹 ↾ 𝑃 )
5		fcores.g	⊢ ( 𝜑 → 𝐺 : 𝐶 ⟶ 𝐷 )
6		fcores.y	⊢ 𝑌 = ( 𝐺 ↾ 𝐸 )
7	1	ffund	⊢ ( 𝜑 → Fun 𝐹 )
8		fcof	⊢ ( ( 𝐺 : 𝐶 ⟶ 𝐷 ∧ Fun 𝐹 ) → ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐶 ) ⟶ 𝐷 )
9	5 7 8	syl2anc	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐶 ) ⟶ 𝐷 )
10	9	ffnd	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) Fn ( ◡ 𝐹 “ 𝐶 ) )
11	3	fneq2i	⊢ ( ( 𝐺 ∘ 𝐹 ) Fn 𝑃 ↔ ( 𝐺 ∘ 𝐹 ) Fn ( ◡ 𝐹 “ 𝐶 ) )
12	10 11	sylibr	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) Fn 𝑃 )
13	1 2 3 4 5 6	fcoreslem4	⊢ ( 𝜑 → ( 𝑌 ∘ 𝑋 ) Fn 𝑃 )
14	4	fveq1i	⊢ ( 𝑋 ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝑃 ) ‘ 𝑥 )
15		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → 𝑥 ∈ 𝑃 )
16	15	fvresd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → ( ( 𝐹 ↾ 𝑃 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
17	14 16	syl5eq	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → ( 𝑋 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
18	17	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → ( 𝑌 ‘ ( 𝑋 ‘ 𝑥 ) ) = ( 𝑌 ‘ ( 𝐹 ‘ 𝑥 ) ) )
19	6	fveq1i	⊢ ( 𝑌 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐺 ↾ 𝐸 ) ‘ ( 𝐹 ‘ 𝑥 ) )
20		cnvimass	⊢ ( ◡ 𝐹 “ 𝐶 ) ⊆ dom 𝐹
21	3 20	eqsstri	⊢ 𝑃 ⊆ dom 𝐹
22	21	sseli	⊢ ( 𝑥 ∈ 𝑃 → 𝑥 ∈ dom 𝐹 )
23		fvelrn	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 )
24	7 22 23	syl2an	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 )
25	3	eleq2i	⊢ ( 𝑥 ∈ 𝑃 ↔ 𝑥 ∈ ( ◡ 𝐹 “ 𝐶 ) )
26	25	biimpi	⊢ ( 𝑥 ∈ 𝑃 → 𝑥 ∈ ( ◡ 𝐹 “ 𝐶 ) )
27		fvimacnvi	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ ( ◡ 𝐹 “ 𝐶 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 )
28	7 26 27	syl2an	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 )
29	24 28	elind	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ran 𝐹 ∩ 𝐶 ) )
30	29 2	eleqtrrdi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐸 )
31	30	fvresd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → ( ( 𝐺 ↾ 𝐸 ) ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) )
32	19 31	syl5eq	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → ( 𝑌 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) )
33	18 32	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → ( 𝑌 ‘ ( 𝑋 ‘ 𝑥 ) ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) )
34	1 2 3 4	fcoreslem3	⊢ ( 𝜑 → 𝑋 : 𝑃 –onto→ 𝐸 )
35		fof	⊢ ( 𝑋 : 𝑃 –onto→ 𝐸 → 𝑋 : 𝑃 ⟶ 𝐸 )
36	34 35	syl	⊢ ( 𝜑 → 𝑋 : 𝑃 ⟶ 𝐸 )
37	36	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → 𝑋 : 𝑃 ⟶ 𝐸 )
38	37 15	fvco3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → ( ( 𝑌 ∘ 𝑋 ) ‘ 𝑥 ) = ( 𝑌 ‘ ( 𝑋 ‘ 𝑥 ) ) )
39	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
40	21	a1i	⊢ ( 𝜑 → 𝑃 ⊆ dom 𝐹 )
41	40	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → 𝑥 ∈ dom 𝐹 )
42	1	fdmd	⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
43	42	eqcomd	⊢ ( 𝜑 → 𝐴 = dom 𝐹 )
44	43	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ dom 𝐹 ) )
45	44	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ dom 𝐹 ) )
46	41 45	mpbird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → 𝑥 ∈ 𝐴 )
47	39 46	fvco3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) )
48	33 38 47	3eqtr4rd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) = ( ( 𝑌 ∘ 𝑋 ) ‘ 𝑥 ) )
49	12 13 48	eqfnfvd	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑌 ∘ 𝑋 ) )