Metamath Proof Explorer


Theorem arwrid

Description: Right identity of a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses arwlid.h 𝐻 = ( Homa𝐶 )
arwlid.o · = ( compa𝐶 )
arwlid.a 1 = ( Ida𝐶 )
arwlid.f ( 𝜑𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
Assertion arwrid ( 𝜑 → ( 𝐹 · ( 1𝑋 ) ) = 𝐹 )

Proof

Step Hyp Ref Expression
1 arwlid.h 𝐻 = ( Homa𝐶 )
2 arwlid.o · = ( compa𝐶 )
3 arwlid.a 1 = ( Ida𝐶 )
4 arwlid.f ( 𝜑𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
5 eqid ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
6 1 homarcl ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → 𝐶 ∈ Cat )
7 4 6 syl ( 𝜑𝐶 ∈ Cat )
8 eqid ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
9 1 5 homarcl2 ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) )
10 4 9 syl ( 𝜑 → ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) )
11 10 simpld ( 𝜑𝑋 ∈ ( Base ‘ 𝐶 ) )
12 3 5 7 8 11 ida2 ( 𝜑 → ( 2nd ‘ ( 1𝑋 ) ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) )
13 12 oveq2d ( 𝜑 → ( ( 2nd𝐹 ) ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( 2nd ‘ ( 1𝑋 ) ) ) = ( ( 2nd𝐹 ) ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) )
14 eqid ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
15 eqid ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
16 10 simprd ( 𝜑𝑌 ∈ ( Base ‘ 𝐶 ) )
17 1 14 homahom ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ( 2nd𝐹 ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
18 4 17 syl ( 𝜑 → ( 2nd𝐹 ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
19 5 14 8 7 11 15 16 18 catrid ( 𝜑 → ( ( 2nd𝐹 ) ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) = ( 2nd𝐹 ) )
20 13 19 eqtrd ( 𝜑 → ( ( 2nd𝐹 ) ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( 2nd ‘ ( 1𝑋 ) ) ) = ( 2nd𝐹 ) )
21 20 oteq3d ( 𝜑 → ⟨ 𝑋 , 𝑌 , ( ( 2nd𝐹 ) ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( 2nd ‘ ( 1𝑋 ) ) ) ⟩ = ⟨ 𝑋 , 𝑌 , ( 2nd𝐹 ) ⟩ )
22 3 5 7 11 1 idahom ( 𝜑 → ( 1𝑋 ) ∈ ( 𝑋 𝐻 𝑋 ) )
23 2 1 22 4 15 coaval ( 𝜑 → ( 𝐹 · ( 1𝑋 ) ) = ⟨ 𝑋 , 𝑌 , ( ( 2nd𝐹 ) ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( 2nd ‘ ( 1𝑋 ) ) ) ⟩ )
24 1 homadmcd ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → 𝐹 = ⟨ 𝑋 , 𝑌 , ( 2nd𝐹 ) ⟩ )
25 4 24 syl ( 𝜑𝐹 = ⟨ 𝑋 , 𝑌 , ( 2nd𝐹 ) ⟩ )
26 21 23 25 3eqtr4d ( 𝜑 → ( 𝐹 · ( 1𝑋 ) ) = 𝐹 )