Metamath Proof Explorer

Theorem comfeqval

Description: Equality of two compositions. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses comfeqval.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
comfeqval.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
comfeqval.1 ⊢ · = ( comp ‘ 𝐶 )
comfeqval.2 ⊢ ∙ = ( comp ‘ 𝐷 )
comfeqval.3 ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
comfeqval.4 ⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
comfeqval.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
comfeqval.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
comfeqval.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
comfeqval.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
comfeqval.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) )
Assertion comfeqval ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ∙ 𝑍 ) 𝐹 ) )

Proof

Step Hyp Ref Expression
1 comfeqval.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 comfeqval.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
3 comfeqval.1 ⊢ · = ( comp ‘ 𝐶 )
4 comfeqval.2 ⊢ ∙ = ( comp ‘ 𝐷 )
5 comfeqval.3 ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
6 comfeqval.4 ⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
7 comfeqval.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8 comfeqval.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9 comfeqval.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
10 comfeqval.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
11 comfeqval.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) )
12 6 oveqd ⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ( compf ‘ 𝐶 ) 𝑍 ) = ( ⟨ 𝑋 , 𝑌 ⟩ ( compf ‘ 𝐷 ) 𝑍 ) )
13 12 oveqd ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( compf ‘ 𝐶 ) 𝑍 ) 𝐹 ) = ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( compf ‘ 𝐷 ) 𝑍 ) 𝐹 ) )
14 eqid ⊢ ( compf ‘ 𝐶 ) = ( compf ‘ 𝐶 )
15 14 1 2 3 7 8 9 10 11 comfval ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( compf ‘ 𝐶 ) 𝑍 ) 𝐹 ) = ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) )
16 eqid ⊢ ( compf ‘ 𝐷 ) = ( compf ‘ 𝐷 )
17 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
18 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
19 5 homfeqbas ⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) )
20 1 19 syl5eq ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐷 ) )
21 7 20 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐷 ) )
22 8 20 eleqtrd ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐷 ) )
23 9 20 eleqtrd ⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ 𝐷 ) )
24 1 2 18 5 7 8 homfeqval ⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( 𝑋 ( Hom ‘ 𝐷 ) 𝑌 ) )
25 10 24 eleqtrd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐷 ) 𝑌 ) )
26 1 2 18 5 8 9 homfeqval ⊢ ( 𝜑 → ( 𝑌 𝐻 𝑍 ) = ( 𝑌 ( Hom ‘ 𝐷 ) 𝑍 ) )
27 11 26 eleqtrd ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐷 ) 𝑍 ) )
28 16 17 18 4 21 22 23 25 27 comfval ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( compf ‘ 𝐷 ) 𝑍 ) 𝐹 ) = ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ∙ 𝑍 ) 𝐹 ) )
29 13 15 28 3eqtr3d ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ∙ 𝑍 ) 𝐹 ) )