Theorem rcaninv

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

	Ref	Expression
Hypotheses	rcaninv.b	$$⊢B={\mathrm{Base}}_C$$
	rcaninv.n	$$⊢N=\mathrm{Inv}\left(C\right)$$
	rcaninv.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	rcaninv.x	$$⊢\phi \to X\in B$$
	rcaninv.y	$$⊢\phi \to Y\in B$$
	rcaninv.z	$$⊢\phi \to Z\in B$$
	rcaninv.f	$$⊢\phi \to F\in \left(Y\mathrm{Iso}\left(C\right)X\right)$$
	rcaninv.g	$$⊢\phi \to G\in \left(Y\mathrm{Hom}\left(C\right)Z\right)$$
	rcaninv.h	$$⊢\phi \to H\in \left(Y\mathrm{Hom}\left(C\right)Z\right)$$
	rcaninv.1	$$⊢R=\left(YNX\right)\left(F\right)$$
	rcaninv.o	No typesetting found for |- .o. = ( <. X , Y >. ( comp ` C ) Z ) with typecode |-
Assertion	rcaninv	Could not format assertion : No typesetting found for |- ( ph -> ( ( G .o. R ) = ( H .o. R ) -> G = H ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		rcaninv.b	$$⊢B={\mathrm{Base}}_C$$
2		rcaninv.n	$$⊢N=\mathrm{Inv}\left(C\right)$$
3		rcaninv.c	$$⊢\phi \to C\in \mathrm{Cat}$$
4		rcaninv.x	$$⊢\phi \to X\in B$$
5		rcaninv.y	$$⊢\phi \to Y\in B$$
6		rcaninv.z	$$⊢\phi \to Z\in B$$
7		rcaninv.f	$$⊢\phi \to F\in \left(Y\mathrm{Iso}\left(C\right)X\right)$$
8		rcaninv.g	$$⊢\phi \to G\in \left(Y\mathrm{Hom}\left(C\right)Z\right)$$
9		rcaninv.h	$$⊢\phi \to H\in \left(Y\mathrm{Hom}\left(C\right)Z\right)$$
10		rcaninv.1	$$⊢R=\left(YNX\right)\left(F\right)$$
11		rcaninv.o	Could not format .o. = ( <. X , Y >. ( comp ` C ) Z ) : No typesetting found for |- .o. = ( <. X , Y >. ( comp ` C ) Z ) with typecode |-
12		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
13		eqid	$$⊢\mathrm{comp}\left(C\right)=\mathrm{comp}\left(C\right)$$
14		eqid	$$⊢\mathrm{Iso}\left(C\right)=\mathrm{Iso}\left(C\right)$$
15	1 12 14 3 5 4	isohom	$$⊢\phi \to Y\mathrm{Iso}\left(C\right)X\subseteq Y\mathrm{Hom}\left(C\right)X$$
16	15 7	sseldd	$$⊢\phi \to F\in \left(Y\mathrm{Hom}\left(C\right)X\right)$$
17	1 12 14 3 4 5	isohom	$$⊢\phi \to X\mathrm{Iso}\left(C\right)Y\subseteq X\mathrm{Hom}\left(C\right)Y$$
18	1 2 3 5 4 14	invf	$$⊢\phi \to \left(YNX\right):Y\mathrm{Iso}\left(C\right)X⟶X\mathrm{Iso}\left(C\right)Y$$
19	18 7	ffvelrnd	$$⊢\phi \to \left(YNX\right)\left(F\right)\in \left(X\mathrm{Iso}\left(C\right)Y\right)$$
20	17 19	sseldd	$$⊢\phi \to \left(YNX\right)\left(F\right)\in \left(X\mathrm{Hom}\left(C\right)Y\right)$$
21	1 12 13 3 5 4 5 16 20 6 8	catass	$$⊢\phi \to \left(G\left(⟨X,Y⟩\mathrm{comp}\left(C\right)Z\right)\left(YNX\right)\left(F\right)\right)\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Z\right)F=G\left(⟨Y,Y⟩\mathrm{comp}\left(C\right)Z\right)\left(\left(YNX\right)\left(F\right)\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Y\right)F\right)$$
22		eqid	$$⊢\mathrm{Id}\left(C\right)=\mathrm{Id}\left(C\right)$$
23		eqid	$$⊢⟨Y,X⟩\mathrm{comp}\left(C\right)Y=⟨Y,X⟩\mathrm{comp}\left(C\right)Y$$
24	1 14 2 3 5 4 7 22 23	invcoisoid	$$⊢\phi \to \left(YNX\right)\left(F\right)\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Y\right)F=\mathrm{Id}\left(C\right)\left(Y\right)$$
25	24	eqcomd	$$⊢\phi \to \mathrm{Id}\left(C\right)\left(Y\right)=\left(YNX\right)\left(F\right)\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Y\right)F$$
26	25	oveq2d	$$⊢\phi \to G\left(⟨Y,Y⟩\mathrm{comp}\left(C\right)Z\right)\mathrm{Id}\left(C\right)\left(Y\right)=G\left(⟨Y,Y⟩\mathrm{comp}\left(C\right)Z\right)\left(\left(YNX\right)\left(F\right)\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Y\right)F\right)$$
27	1 12 22 3 5 13 6 8	catrid	$$⊢\phi \to G\left(⟨Y,Y⟩\mathrm{comp}\left(C\right)Z\right)\mathrm{Id}\left(C\right)\left(Y\right)=G$$
28	21 26 27	3eqtr2rd	$$⊢\phi \to G=\left(G\left(⟨X,Y⟩\mathrm{comp}\left(C\right)Z\right)\left(YNX\right)\left(F\right)\right)\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Z\right)F$$
29	28	adantr	Could not format ( ( ph /\ ( G .o. R ) = ( H .o. R ) ) -> G = ( ( G ( <. X , Y >. ( comp ` C ) Z ) ( ( Y N X ) ` F ) ) ( <. Y , X >. ( comp ` C ) Z ) F ) ) : No typesetting found for |- ( ( ph /\ ( G .o. R ) = ( H .o. R ) ) -> G = ( ( G ( <. X , Y >. ( comp ` C ) Z ) ( ( Y N X ) ` F ) ) ( <. Y , X >. ( comp ` C ) Z ) F ) ) with typecode |-
30	11	eqcomi	Could not format ( <. X , Y >. ( comp ` C ) Z ) = .o. : No typesetting found for |- ( <. X , Y >. ( comp ` C ) Z ) = .o. with typecode |-
31	30	a1i	Could not format ( ph -> ( <. X , Y >. ( comp ` C ) Z ) = .o. ) : No typesetting found for |- ( ph -> ( <. X , Y >. ( comp ` C ) Z ) = .o. ) with typecode |-
32		eqidd	$$⊢\phi \to G=G$$
33	10	eqcomi	$$⊢\left(YNX\right)\left(F\right)=R$$
34	33	a1i	$$⊢\phi \to \left(YNX\right)\left(F\right)=R$$
35	31 32 34	oveq123d	Could not format ( ph -> ( G ( <. X , Y >. ( comp ` C ) Z ) ( ( Y N X ) ` F ) ) = ( G .o. R ) ) : No typesetting found for |- ( ph -> ( G ( <. X , Y >. ( comp ` C ) Z ) ( ( Y N X ) ` F ) ) = ( G .o. R ) ) with typecode |-
36	35	adantr	Could not format ( ( ph /\ ( G .o. R ) = ( H .o. R ) ) -> ( G ( <. X , Y >. ( comp ` C ) Z ) ( ( Y N X ) ` F ) ) = ( G .o. R ) ) : No typesetting found for |- ( ( ph /\ ( G .o. R ) = ( H .o. R ) ) -> ( G ( <. X , Y >. ( comp ` C ) Z ) ( ( Y N X ) ` F ) ) = ( G .o. R ) ) with typecode |-
37		simpr	Could not format ( ( ph /\ ( G .o. R ) = ( H .o. R ) ) -> ( G .o. R ) = ( H .o. R ) ) : No typesetting found for |- ( ( ph /\ ( G .o. R ) = ( H .o. R ) ) -> ( G .o. R ) = ( H .o. R ) ) with typecode |-
38	36 37	eqtrd	Could not format ( ( ph /\ ( G .o. R ) = ( H .o. R ) ) -> ( G ( <. X , Y >. ( comp ` C ) Z ) ( ( Y N X ) ` F ) ) = ( H .o. R ) ) : No typesetting found for |- ( ( ph /\ ( G .o. R ) = ( H .o. R ) ) -> ( G ( <. X , Y >. ( comp ` C ) Z ) ( ( Y N X ) ` F ) ) = ( H .o. R ) ) with typecode |-
39	38	oveq1d	Could not format ( ( ph /\ ( G .o. R ) = ( H .o. R ) ) -> ( ( G ( <. X , Y >. ( comp ` C ) Z ) ( ( Y N X ) ` F ) ) ( <. Y , X >. ( comp ` C ) Z ) F ) = ( ( H .o. R ) ( <. Y , X >. ( comp ` C ) Z ) F ) ) : No typesetting found for |- ( ( ph /\ ( G .o. R ) = ( H .o. R ) ) -> ( ( G ( <. X , Y >. ( comp ` C ) Z ) ( ( Y N X ) ` F ) ) ( <. Y , X >. ( comp ` C ) Z ) F ) = ( ( H .o. R ) ( <. Y , X >. ( comp ` C ) Z ) F ) ) with typecode |-
40	11	oveqi	Could not format ( H .o. R ) = ( H ( <. X , Y >. ( comp ` C ) Z ) R ) : No typesetting found for |- ( H .o. R ) = ( H ( <. X , Y >. ( comp ` C ) Z ) R ) with typecode |-
41	40	oveq1i	Could not format ( ( H .o. R ) ( <. Y , X >. ( comp ` C ) Z ) F ) = ( ( H ( <. X , Y >. ( comp ` C ) Z ) R ) ( <. Y , X >. ( comp ` C ) Z ) F ) : No typesetting found for |- ( ( H .o. R ) ( <. Y , X >. ( comp ` C ) Z ) F ) = ( ( H ( <. X , Y >. ( comp ` C ) Z ) R ) ( <. Y , X >. ( comp ` C ) Z ) F ) with typecode |-
42	41	a1i	Could not format ( ph -> ( ( H .o. R ) ( <. Y , X >. ( comp ` C ) Z ) F ) = ( ( H ( <. X , Y >. ( comp ` C ) Z ) R ) ( <. Y , X >. ( comp ` C ) Z ) F ) ) : No typesetting found for |- ( ph -> ( ( H .o. R ) ( <. Y , X >. ( comp ` C ) Z ) F ) = ( ( H ( <. X , Y >. ( comp ` C ) Z ) R ) ( <. Y , X >. ( comp ` C ) Z ) F ) ) with typecode |-
43	10 20	eqeltrid	$$⊢\phi \to R\in \left(X\mathrm{Hom}\left(C\right)Y\right)$$
44	1 12 13 3 5 4 5 16 43 6 9	catass	$$⊢\phi \to \left(H\left(⟨X,Y⟩\mathrm{comp}\left(C\right)Z\right)R\right)\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Z\right)F=H\left(⟨Y,Y⟩\mathrm{comp}\left(C\right)Z\right)\left(R\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Y\right)F\right)$$
45	10	oveq1i	$$⊢R\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Y\right)F=\left(YNX\right)\left(F\right)\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Y\right)F$$
46	45	oveq2i	$$⊢H\left(⟨Y,Y⟩\mathrm{comp}\left(C\right)Z\right)\left(R\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Y\right)F\right)=H\left(⟨Y,Y⟩\mathrm{comp}\left(C\right)Z\right)\left(\left(YNX\right)\left(F\right)\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Y\right)F\right)$$
47	46	a1i	$$⊢\phi \to H\left(⟨Y,Y⟩\mathrm{comp}\left(C\right)Z\right)\left(R\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Y\right)F\right)=H\left(⟨Y,Y⟩\mathrm{comp}\left(C\right)Z\right)\left(\left(YNX\right)\left(F\right)\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Y\right)F\right)$$
48	24	oveq2d	$$⊢\phi \to H\left(⟨Y,Y⟩\mathrm{comp}\left(C\right)Z\right)\left(\left(YNX\right)\left(F\right)\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Y\right)F\right)=H\left(⟨Y,Y⟩\mathrm{comp}\left(C\right)Z\right)\mathrm{Id}\left(C\right)\left(Y\right)$$
49	44 47 48	3eqtrd	$$⊢\phi \to \left(H\left(⟨X,Y⟩\mathrm{comp}\left(C\right)Z\right)R\right)\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Z\right)F=H\left(⟨Y,Y⟩\mathrm{comp}\left(C\right)Z\right)\mathrm{Id}\left(C\right)\left(Y\right)$$
50	1 12 22 3 5 13 6 9	catrid	$$⊢\phi \to H\left(⟨Y,Y⟩\mathrm{comp}\left(C\right)Z\right)\mathrm{Id}\left(C\right)\left(Y\right)=H$$
51	42 49 50	3eqtrd	Could not format ( ph -> ( ( H .o. R ) ( <. Y , X >. ( comp ` C ) Z ) F ) = H ) : No typesetting found for |- ( ph -> ( ( H .o. R ) ( <. Y , X >. ( comp ` C ) Z ) F ) = H ) with typecode |-
52	51	adantr	Could not format ( ( ph /\ ( G .o. R ) = ( H .o. R ) ) -> ( ( H .o. R ) ( <. Y , X >. ( comp ` C ) Z ) F ) = H ) : No typesetting found for |- ( ( ph /\ ( G .o. R ) = ( H .o. R ) ) -> ( ( H .o. R ) ( <. Y , X >. ( comp ` C ) Z ) F ) = H ) with typecode |-
53	29 39 52	3eqtrd	Could not format ( ( ph /\ ( G .o. R ) = ( H .o. R ) ) -> G = H ) : No typesetting found for |- ( ( ph /\ ( G .o. R ) = ( H .o. R ) ) -> G = H ) with typecode |-
54	53	ex	Could not format ( ph -> ( ( G .o. R ) = ( H .o. R ) -> G = H ) ) : No typesetting found for |- ( ph -> ( ( G .o. R ) = ( H .o. R ) -> G = H ) ) with typecode |-