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 ⊢ ( 𝜑 → ( ( 𝐺 ⚬ 𝑅 ) = ( 𝐻 ⚬ 𝑅 ) → 𝐺 = 𝐻 ) )