Theorem fcoresf1lem

Description: Lemma for fcoresf1 . (Contributed by AV, 18-Sep-2024)

	Ref	Expression
Hypotheses	fcores.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	fcores.e	⊢ 𝐸 = ( ran 𝐹 ∩ 𝐶 )
	fcores.p	⊢ 𝑃 = ( ◡ 𝐹 “ 𝐶 )
	fcores.x	⊢ 𝑋 = ( 𝐹 ↾ 𝑃 )
	fcores.g	⊢ ( 𝜑 → 𝐺 : 𝐶 ⟶ 𝐷 )
	fcores.y	⊢ 𝑌 = ( 𝐺 ↾ 𝐸 )
Assertion	fcoresf1lem	⊢ ( ( 𝜑 ∧ 𝑍 ∈ 𝑃 ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑍 ) = ( 𝑌 ‘ ( 𝑋 ‘ 𝑍 ) ) )

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 2 3 4 5 6	fcores	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑌 ∘ 𝑋 ) )
8	7	fveq1d	⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑍 ) = ( ( 𝑌 ∘ 𝑋 ) ‘ 𝑍 ) )
9	8	adantr	⊢ ( ( 𝜑 ∧ 𝑍 ∈ 𝑃 ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑍 ) = ( ( 𝑌 ∘ 𝑋 ) ‘ 𝑍 ) )
10	1 2 3 4	fcoreslem3	⊢ ( 𝜑 → 𝑋 : 𝑃 –onto→ 𝐸 )
11		fof	⊢ ( 𝑋 : 𝑃 –onto→ 𝐸 → 𝑋 : 𝑃 ⟶ 𝐸 )
12	10 11	syl	⊢ ( 𝜑 → 𝑋 : 𝑃 ⟶ 𝐸 )
13	12	adantr	⊢ ( ( 𝜑 ∧ 𝑍 ∈ 𝑃 ) → 𝑋 : 𝑃 ⟶ 𝐸 )
14		simpr	⊢ ( ( 𝜑 ∧ 𝑍 ∈ 𝑃 ) → 𝑍 ∈ 𝑃 )
15	13 14	fvco3d	⊢ ( ( 𝜑 ∧ 𝑍 ∈ 𝑃 ) → ( ( 𝑌 ∘ 𝑋 ) ‘ 𝑍 ) = ( 𝑌 ‘ ( 𝑋 ‘ 𝑍 ) ) )
16	9 15	eqtrd	⊢ ( ( 𝜑 ∧ 𝑍 ∈ 𝑃 ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑍 ) = ( 𝑌 ‘ ( 𝑋 ‘ 𝑍 ) ) )