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

Metamath Proof Explorer

Theorem bj-endcomp

Description: Composition law of the monoid of endomorphisms on an object of a category. (Contributed by BJ, 5-Apr-2024) (Proof modification is discouraged.)

Ref Expression
Hypotheses bj-endval.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
bj-endval.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
Assertion bj-endcomp ( 𝜑 → ( +g ‘ ( ( End ‘ 𝐶 ) ‘ 𝑋 ) ) = ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) )

Proof

Step Hyp Ref Expression
1 bj-endval.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
2 bj-endval.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
3 plusgid ⊢ +g = Slot ( +g ‘ ndx )
4 fvexd ⊢ ( 𝜑 → ( ( End ‘ 𝐶 ) ‘ 𝑋 ) ∈ V )
5 3 4 strfvnd ⊢ ( 𝜑 → ( +g ‘ ( ( End ‘ 𝐶 ) ‘ 𝑋 ) ) = ( ( ( End ‘ 𝐶 ) ‘ 𝑋 ) ‘ ( +g ‘ ndx ) ) )
6 1 2 bj-endval ⊢ ( 𝜑 → ( ( End ‘ 𝐶 ) ‘ 𝑋 ) = { ⟨ ( Base ‘ ndx ) , ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ⟩ } )
7 6 fveq1d ⊢ ( 𝜑 → ( ( ( End ‘ 𝐶 ) ‘ 𝑋 ) ‘ ( +g ‘ ndx ) ) = ( { ⟨ ( Base ‘ ndx ) , ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ⟩ } ‘ ( +g ‘ ndx ) ) )
8 basendxnplusgndx ⊢ ( Base ‘ ndx ) ≠ ( +g ‘ ndx )
9 fvex ⊢ ( +g ‘ ndx ) ∈ V
10 ovex ⊢ ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ∈ V
11 9 10 fvpr2 ⊢ ( ( Base ‘ ndx ) ≠ ( +g ‘ ndx ) → ( { ⟨ ( Base ‘ ndx ) , ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ⟩ } ‘ ( +g ‘ ndx ) ) = ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) )
12 8 11 mp1i ⊢ ( 𝜑 → ( { ⟨ ( Base ‘ ndx ) , ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ⟩ } ‘ ( +g ‘ ndx ) ) = ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) )
13 5 7 12 3eqtrd ⊢ ( 𝜑 → ( +g ‘ ( ( End ‘ 𝐶 ) ‘ 𝑋 ) ) = ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) )