This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝜑 ∧ 𝑍 ∈ 𝑃 ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑍 ) = ( 𝑌 ‘ ( 𝑋 ‘ 𝑍 ) ) )