rcaninv

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

	Ref	Expression
Hypotheses	rcaninv.b	$⊢ B = {Base}_{C}$
	rcaninv.n	$⊢ N = Inv (C)$
	rcaninv.c	$⊢ φ \to C \in Cat$
	rcaninv.x	$⊢ φ \to X \in B$
	rcaninv.y	$⊢ φ \to Y \in B$
	rcaninv.z	$⊢ φ \to Z \in B$
	rcaninv.f	$⊢ φ \to F \in (Y Iso (C) X)$
	rcaninv.g	$⊢ φ \to G \in (Y Hom (C) Z)$
	rcaninv.h	$⊢ φ \to H \in (Y Hom (C) Z)$
	rcaninv.1	$⊢ R = (Y N X) (F)$
	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 = {Base}_{C}$
2		rcaninv.n	$⊢ N = Inv (C)$
3		rcaninv.c	$⊢ φ \to C \in Cat$
4		rcaninv.x	$⊢ φ \to X \in B$
5		rcaninv.y	$⊢ φ \to Y \in B$
6		rcaninv.z	$⊢ φ \to Z \in B$
7		rcaninv.f	$⊢ φ \to F \in (Y Iso (C) X)$
8		rcaninv.g	$⊢ φ \to G \in (Y Hom (C) Z)$
9		rcaninv.h	$⊢ φ \to H \in (Y Hom (C) Z)$
10		rcaninv.1	$⊢ R = (Y N X) (F)$
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	$⊢ Hom (C) = Hom (C)$
13		eqid	$⊢ comp (C) = comp (C)$
14		eqid	$⊢ Iso (C) = Iso (C)$
15	1 12 14 3 5 4	isohom	$⊢ φ \to Y Iso (C) X \subseteq Y Hom (C) X$
16	15 7	sseldd	$⊢ φ \to F \in (Y Hom (C) X)$
17	1 12 14 3 4 5	isohom	$⊢ φ \to X Iso (C) Y \subseteq X Hom (C) Y$
18	1 2 3 5 4 14	invf	$⊢ φ \to (Y N X) : Y Iso (C) X ⟶ X Iso (C) Y$
19	18 7	ffvelcdmd	$⊢ φ \to (Y N X) (F) \in (X Iso (C) Y)$
20	17 19	sseldd	$⊢ φ \to (Y N X) (F) \in (X Hom (C) Y)$
21	1 12 13 3 5 4 5 16 20 6 8	catass	$⊢ φ \to (G (⟨X, Y⟩ comp (C) Z) (Y N X) (F)) (⟨Y, X⟩ comp (C) Z) F = G (⟨Y, Y⟩ comp (C) Z) ((Y N X) (F) (⟨Y, X⟩ comp (C) Y) F)$
22		eqid	$⊢ Id (C) = Id (C)$
23		eqid	$⊢ ⟨Y, X⟩ comp (C) Y = ⟨Y, X⟩ comp (C) Y$
24	1 14 2 3 5 4 7 22 23	invcoisoid	$⊢ φ \to (Y N X) (F) (⟨Y, X⟩ comp (C) Y) F = Id (C) (Y)$
25	24	eqcomd	$⊢ φ \to Id (C) (Y) = (Y N X) (F) (⟨Y, X⟩ comp (C) Y) F$
26	25	oveq2d	$⊢ φ \to G (⟨Y, Y⟩ comp (C) Z) Id (C) (Y) = G (⟨Y, Y⟩ comp (C) Z) ((Y N X) (F) (⟨Y, X⟩ comp (C) Y) F)$
27	1 12 22 3 5 13 6 8	catrid	$⊢ φ \to G (⟨Y, Y⟩ comp (C) Z) Id (C) (Y) = G$
28	21 26 27	3eqtr2rd	$⊢ φ \to G = (G (⟨X, Y⟩ comp (C) Z) (Y N X) (F)) (⟨Y, X⟩ comp (C) Z) 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	$⊢ φ \to G = G$
33	10	eqcomi	$⊢ (Y N X) (F) = R$
34	33	a1i	$⊢ φ \to (Y N X) (F) = 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	$⊢ φ \to R \in (X Hom (C) Y)$
44	1 12 13 3 5 4 5 16 43 6 9	catass	$⊢ φ \to (H (⟨X, Y⟩ comp (C) Z) R) (⟨Y, X⟩ comp (C) Z) F = H (⟨Y, Y⟩ comp (C) Z) (R (⟨Y, X⟩ comp (C) Y) F)$
45	10	oveq1i	$⊢ R (⟨Y, X⟩ comp (C) Y) F = (Y N X) (F) (⟨Y, X⟩ comp (C) Y) F$
46	45	oveq2i	$⊢ H (⟨Y, Y⟩ comp (C) Z) (R (⟨Y, X⟩ comp (C) Y) F) = H (⟨Y, Y⟩ comp (C) Z) ((Y N X) (F) (⟨Y, X⟩ comp (C) Y) F)$
47	46	a1i	$⊢ φ \to H (⟨Y, Y⟩ comp (C) Z) (R (⟨Y, X⟩ comp (C) Y) F) = H (⟨Y, Y⟩ comp (C) Z) ((Y N X) (F) (⟨Y, X⟩ comp (C) Y) F)$
48	24	oveq2d	$⊢ φ \to H (⟨Y, Y⟩ comp (C) Z) ((Y N X) (F) (⟨Y, X⟩ comp (C) Y) F) = H (⟨Y, Y⟩ comp (C) Z) Id (C) (Y)$
49	44 47 48	3eqtrd	$⊢ φ \to (H (⟨X, Y⟩ comp (C) Z) R) (⟨Y, X⟩ comp (C) Z) F = H (⟨Y, Y⟩ comp (C) Z) Id (C) (Y)$
50	1 12 22 3 5 13 6 9	catrid	$⊢ φ \to H (⟨Y, Y⟩ comp (C) Z) Id (C) (Y) = 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 \|-

Metamath Proof Explorer

Theorem rcaninv

Proof