Metamath Proof Explorer


Theorem rcaninv

Description: Right cancellation of an inverse of an isomorphism. (Contributed by AV, 5-Apr-2020)

Ref Expression
Hypotheses rcaninv.b 𝐵 = ( Base ‘ 𝐶 )
rcaninv.n 𝑁 = ( Inv ‘ 𝐶 )
rcaninv.c ( 𝜑𝐶 ∈ Cat )
rcaninv.x ( 𝜑𝑋𝐵 )
rcaninv.y ( 𝜑𝑌𝐵 )
rcaninv.z ( 𝜑𝑍𝐵 )
rcaninv.f ( 𝜑𝐹 ∈ ( 𝑌 ( Iso ‘ 𝐶 ) 𝑋 ) )
rcaninv.g ( 𝜑𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑍 ) )
rcaninv.h ( 𝜑𝐻 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑍 ) )
rcaninv.1 𝑅 = ( ( 𝑌 𝑁 𝑋 ) ‘ 𝐹 )
rcaninv.o = ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 )
Assertion rcaninv ( 𝜑 → ( ( 𝐺 𝑅 ) = ( 𝐻 𝑅 ) → 𝐺 = 𝐻 ) )

Proof

Step Hyp Ref Expression
1 rcaninv.b 𝐵 = ( Base ‘ 𝐶 )
2 rcaninv.n 𝑁 = ( Inv ‘ 𝐶 )
3 rcaninv.c ( 𝜑𝐶 ∈ Cat )
4 rcaninv.x ( 𝜑𝑋𝐵 )
5 rcaninv.y ( 𝜑𝑌𝐵 )
6 rcaninv.z ( 𝜑𝑍𝐵 )
7 rcaninv.f ( 𝜑𝐹 ∈ ( 𝑌 ( Iso ‘ 𝐶 ) 𝑋 ) )
8 rcaninv.g ( 𝜑𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑍 ) )
9 rcaninv.h ( 𝜑𝐻 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑍 ) )
10 rcaninv.1 𝑅 = ( ( 𝑌 𝑁 𝑋 ) ‘ 𝐹 )
11 rcaninv.o = ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 )
12 eqid ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
13 eqid ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
14 eqid ( Iso ‘ 𝐶 ) = ( Iso ‘ 𝐶 )
15 1 12 14 3 5 4 isohom ( 𝜑 → ( 𝑌 ( Iso ‘ 𝐶 ) 𝑋 ) ⊆ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) )
16 15 7 sseldd ( 𝜑𝐹 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) )
17 1 12 14 3 4 5 isohom ( 𝜑 → ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ⊆ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
18 1 2 3 5 4 14 invf ( 𝜑 → ( 𝑌 𝑁 𝑋 ) : ( 𝑌 ( Iso ‘ 𝐶 ) 𝑋 ) ⟶ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) )
19 18 7 ffvelrnd ( 𝜑 → ( ( 𝑌 𝑁 𝑋 ) ‘ 𝐹 ) ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) )
20 17 19 sseldd ( 𝜑 → ( ( 𝑌 𝑁 𝑋 ) ‘ 𝐹 ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
21 1 12 13 3 5 4 5 16 20 6 8 catass ( 𝜑 → ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) ( ( 𝑌 𝑁 𝑋 ) ‘ 𝐹 ) ) ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝐹 ) = ( 𝐺 ( ⟨ 𝑌 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) ( ( ( 𝑌 𝑁 𝑋 ) ‘ 𝐹 ) ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐹 ) ) )
22 eqid ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
23 eqid ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) = ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 )
24 1 14 2 3 5 4 7 22 23 invcoisoid ( 𝜑 → ( ( ( 𝑌 𝑁 𝑋 ) ‘ 𝐹 ) ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) )
25 24 eqcomd ( 𝜑 → ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) = ( ( ( 𝑌 𝑁 𝑋 ) ‘ 𝐹 ) ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐹 ) )
26 25 oveq2d ( 𝜑 → ( 𝐺 ( ⟨ 𝑌 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) = ( 𝐺 ( ⟨ 𝑌 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) ( ( ( 𝑌 𝑁 𝑋 ) ‘ 𝐹 ) ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐹 ) ) )
27 1 12 22 3 5 13 6 8 catrid ( 𝜑 → ( 𝐺 ( ⟨ 𝑌 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) = 𝐺 )
28 21 26 27 3eqtr2rd ( 𝜑𝐺 = ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) ( ( 𝑌 𝑁 𝑋 ) ‘ 𝐹 ) ) ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝐹 ) )
29 28 adantr ( ( 𝜑 ∧ ( 𝐺 𝑅 ) = ( 𝐻 𝑅 ) ) → 𝐺 = ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) ( ( 𝑌 𝑁 𝑋 ) ‘ 𝐹 ) ) ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝐹 ) )
30 11 eqcomi ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) =
31 30 a1i ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) = )
32 eqidd ( 𝜑𝐺 = 𝐺 )
33 10 eqcomi ( ( 𝑌 𝑁 𝑋 ) ‘ 𝐹 ) = 𝑅
34 33 a1i ( 𝜑 → ( ( 𝑌 𝑁 𝑋 ) ‘ 𝐹 ) = 𝑅 )
35 31 32 34 oveq123d ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) ( ( 𝑌 𝑁 𝑋 ) ‘ 𝐹 ) ) = ( 𝐺 𝑅 ) )
36 35 adantr ( ( 𝜑 ∧ ( 𝐺 𝑅 ) = ( 𝐻 𝑅 ) ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) ( ( 𝑌 𝑁 𝑋 ) ‘ 𝐹 ) ) = ( 𝐺 𝑅 ) )
37 simpr ( ( 𝜑 ∧ ( 𝐺 𝑅 ) = ( 𝐻 𝑅 ) ) → ( 𝐺 𝑅 ) = ( 𝐻 𝑅 ) )
38 36 37 eqtrd ( ( 𝜑 ∧ ( 𝐺 𝑅 ) = ( 𝐻 𝑅 ) ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) ( ( 𝑌 𝑁 𝑋 ) ‘ 𝐹 ) ) = ( 𝐻 𝑅 ) )
39 38 oveq1d ( ( 𝜑 ∧ ( 𝐺 𝑅 ) = ( 𝐻 𝑅 ) ) → ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) ( ( 𝑌 𝑁 𝑋 ) ‘ 𝐹 ) ) ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝐹 ) = ( ( 𝐻 𝑅 ) ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝐹 ) )
40 11 oveqi ( 𝐻 𝑅 ) = ( 𝐻 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝑅 )
41 40 oveq1i ( ( 𝐻 𝑅 ) ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝐹 ) = ( ( 𝐻 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝑅 ) ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝐹 )
42 41 a1i ( 𝜑 → ( ( 𝐻 𝑅 ) ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝐹 ) = ( ( 𝐻 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝑅 ) ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝐹 ) )
43 10 20 eqeltrid ( 𝜑𝑅 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
44 1 12 13 3 5 4 5 16 43 6 9 catass ( 𝜑 → ( ( 𝐻 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝑅 ) ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝐹 ) = ( 𝐻 ( ⟨ 𝑌 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) ( 𝑅 ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐹 ) ) )
45 10 oveq1i ( 𝑅 ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐹 ) = ( ( ( 𝑌 𝑁 𝑋 ) ‘ 𝐹 ) ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐹 )
46 45 oveq2i ( 𝐻 ( ⟨ 𝑌 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) ( 𝑅 ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐹 ) ) = ( 𝐻 ( ⟨ 𝑌 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) ( ( ( 𝑌 𝑁 𝑋 ) ‘ 𝐹 ) ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐹 ) )
47 46 a1i ( 𝜑 → ( 𝐻 ( ⟨ 𝑌 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) ( 𝑅 ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐹 ) ) = ( 𝐻 ( ⟨ 𝑌 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) ( ( ( 𝑌 𝑁 𝑋 ) ‘ 𝐹 ) ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐹 ) ) )
48 24 oveq2d ( 𝜑 → ( 𝐻 ( ⟨ 𝑌 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) ( ( ( 𝑌 𝑁 𝑋 ) ‘ 𝐹 ) ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐹 ) ) = ( 𝐻 ( ⟨ 𝑌 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) )
49 44 47 48 3eqtrd ( 𝜑 → ( ( 𝐻 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝑅 ) ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝐹 ) = ( 𝐻 ( ⟨ 𝑌 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) )
50 1 12 22 3 5 13 6 9 catrid ( 𝜑 → ( 𝐻 ( ⟨ 𝑌 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) = 𝐻 )
51 42 49 50 3eqtrd ( 𝜑 → ( ( 𝐻 𝑅 ) ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝐹 ) = 𝐻 )
52 51 adantr ( ( 𝜑 ∧ ( 𝐺 𝑅 ) = ( 𝐻 𝑅 ) ) → ( ( 𝐻 𝑅 ) ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝐹 ) = 𝐻 )
53 29 39 52 3eqtrd ( ( 𝜑 ∧ ( 𝐺 𝑅 ) = ( 𝐻 𝑅 ) ) → 𝐺 = 𝐻 )
54 53 ex ( 𝜑 → ( ( 𝐺 𝑅 ) = ( 𝐻 𝑅 ) → 𝐺 = 𝐻 ) )