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

Metamath Proof Explorer

Theorem comfeqval

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

Ref Expression
Hypotheses comfeqval.b ⊢ B = Base C
comfeqval.h ⊢ H = Hom ⁡ C
comfeqval.1 ⊢ · ˙ = comp ⁡ C
comfeqval.2 ⊢ ∙ ˙ = comp ⁡ D
comfeqval.3 ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
comfeqval.4 ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ D
comfeqval.x ⊢ φ → X ∈ B
comfeqval.y ⊢ φ → Y ∈ B
comfeqval.z ⊢ φ → Z ∈ B
comfeqval.f ⊢ φ → F ∈ X H Y
comfeqval.g ⊢ φ → G ∈ Y H Z
Assertion comfeqval ⊢ φ → G X Y · ˙ Z F = G X Y ∙ ˙ Z F

Proof

Step Hyp Ref Expression
1 comfeqval.b ⊢ B = Base C
2 comfeqval.h ⊢ H = Hom ⁡ C
3 comfeqval.1 ⊢ · ˙ = comp ⁡ C
4 comfeqval.2 ⊢ ∙ ˙ = comp ⁡ D
5 comfeqval.3 ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
6 comfeqval.4 ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ D
7 comfeqval.x ⊢ φ → X ∈ B
8 comfeqval.y ⊢ φ → Y ∈ B
9 comfeqval.z ⊢ φ → Z ∈ B
10 comfeqval.f ⊢ φ → F ∈ X H Y
11 comfeqval.g ⊢ φ → G ∈ Y H Z
12 6 oveqd ⊢ φ → X Y comp 𝑓 ⁡ C Z = X Y comp 𝑓 ⁡ D Z
13 12 oveqd ⊢ φ → G X Y comp 𝑓 ⁡ C Z F = G X Y comp 𝑓 ⁡ D Z F
14 eqid ⊢ comp 𝑓 ⁡ C = comp 𝑓 ⁡ C
15 14 1 2 3 7 8 9 10 11 comfval ⊢ φ → G X Y comp 𝑓 ⁡ C Z F = G X Y · ˙ Z F
16 eqid ⊢ comp 𝑓 ⁡ D = comp 𝑓 ⁡ D
17 eqid ⊢ Base D = Base D
18 eqid ⊢ Hom ⁡ D = Hom ⁡ D
19 5 homfeqbas ⊢ φ → Base C = Base D
20 1 19 eqtrid ⊢ φ → B = Base D
21 7 20 eleqtrd ⊢ φ → X ∈ Base D
22 8 20 eleqtrd ⊢ φ → Y ∈ Base D
23 9 20 eleqtrd ⊢ φ → Z ∈ Base D
24 1 2 18 5 7 8 homfeqval ⊢ φ → X H Y = X Hom ⁡ D Y
25 10 24 eleqtrd ⊢ φ → F ∈ X Hom ⁡ D Y
26 1 2 18 5 8 9 homfeqval ⊢ φ → Y H Z = Y Hom ⁡ D Z
27 11 26 eleqtrd ⊢ φ → G ∈ Y Hom ⁡ D Z
28 16 17 18 4 21 22 23 25 27 comfval ⊢ φ → G X Y comp 𝑓 ⁡ D Z F = G X Y ∙ ˙ Z F
29 13 15 28 3eqtr3d ⊢ φ → G X Y · ˙ Z F = G X Y ∙ ˙ Z F