Metamath Proof Explorer

Theorem endmndlem

Description: A diagonal hom-set in a category equipped with the restriction of the composition has a structure of monoid. See also df-mndtc for converting a monoid to a category. Lemma for bj-endmnd . (Contributed by Zhi Wang, 25-Sep-2024)

Ref Expression
Hypotheses endmndlem.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
endmndlem.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
endmndlem.o ⊢ · = ( comp ‘ 𝐶 )
endmndlem.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
endmndlem.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
endmndlem.m ⊢ ( 𝜑 → ( 𝑋 𝐻 𝑋 ) = ( Base ‘ 𝑀 ) )
endmndlem.p ⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) = ( +g ‘ 𝑀 ) )
Assertion endmndlem ( 𝜑 → 𝑀 ∈ Mnd )

Proof

Step Hyp Ref Expression
1 endmndlem.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 endmndlem.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
3 endmndlem.o ⊢ · = ( comp ‘ 𝐶 )
4 endmndlem.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
5 endmndlem.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 endmndlem.m ⊢ ( 𝜑 → ( 𝑋 𝐻 𝑋 ) = ( Base ‘ 𝑀 ) )
7 endmndlem.p ⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) = ( +g ‘ 𝑀 ) )
8 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ) → 𝐶 ∈ Cat )
9 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ) → 𝑋 ∈ 𝐵 )
10 simp3 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ) → 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) )
11 simp2 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ) → 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) )
12 1 2 3 8 9 9 9 10 11 catcocl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ) → ( 𝑓 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) ∈ ( 𝑋 𝐻 𝑋 ) )
13 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∧ 𝑘 ∈ ( 𝑋 𝐻 𝑋 ) ) ) → 𝐶 ∈ Cat )
14 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∧ 𝑘 ∈ ( 𝑋 𝐻 𝑋 ) ) ) → 𝑋 ∈ 𝐵 )
15 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∧ 𝑘 ∈ ( 𝑋 𝐻 𝑋 ) ) ) → 𝑘 ∈ ( 𝑋 𝐻 𝑋 ) )
16 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∧ 𝑘 ∈ ( 𝑋 𝐻 𝑋 ) ) ) → 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) )
17 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∧ 𝑘 ∈ ( 𝑋 𝐻 𝑋 ) ) ) → 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) )
18 1 2 3 13 14 14 14 15 16 14 17 catass ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∧ 𝑘 ∈ ( 𝑋 𝐻 𝑋 ) ) ) → ( ( 𝑓 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑘 ) = ( 𝑓 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑘 ) ) )
19 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
20 1 2 19 4 5 catidcl ⊢ ( 𝜑 → ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ∈ ( 𝑋 𝐻 𝑋 ) )
21 4 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ) → 𝐶 ∈ Cat )
22 5 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ) → 𝑋 ∈ 𝐵 )
23 simpr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ) → 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) )
24 1 2 19 21 22 3 22 23 catlid ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ) → ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = 𝑓 )
25 1 2 19 21 22 3 22 23 catrid ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ) → ( 𝑓 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) = 𝑓 )
26 6 7 12 18 20 24 25 ismndd ⊢ ( 𝜑 → 𝑀 ∈ Mnd )