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