MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rcaninv Structured version   Visualization version   GIF version

Theorem rcaninv 17747
Description: Right cancellation of an inverse of an isomorphism. (Contributed by AV, 5-Apr-2020.)
Hypotheses
Ref Expression
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
Ref Expression
rcaninv (πœ‘ β†’ ((𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅) β†’ 𝐺 = 𝐻))

Proof of Theorem rcaninv
StepHypRef Expression
1 rcaninv.b . . . . . 6 𝐡 = (Baseβ€˜πΆ)
2 eqid 2726 . . . . . 6 (Hom β€˜πΆ) = (Hom β€˜πΆ)
3 eqid 2726 . . . . . 6 (compβ€˜πΆ) = (compβ€˜πΆ)
4 rcaninv.c . . . . . 6 (πœ‘ β†’ 𝐢 ∈ Cat)
5 rcaninv.y . . . . . 6 (πœ‘ β†’ π‘Œ ∈ 𝐡)
6 rcaninv.x . . . . . 6 (πœ‘ β†’ 𝑋 ∈ 𝐡)
7 eqid 2726 . . . . . . . 8 (Isoβ€˜πΆ) = (Isoβ€˜πΆ)
81, 2, 7, 4, 5, 6isohom 17729 . . . . . . 7 (πœ‘ β†’ (π‘Œ(Isoβ€˜πΆ)𝑋) βŠ† (π‘Œ(Hom β€˜πΆ)𝑋))
9 rcaninv.f . . . . . . 7 (πœ‘ β†’ 𝐹 ∈ (π‘Œ(Isoβ€˜πΆ)𝑋))
108, 9sseldd 3978 . . . . . 6 (πœ‘ β†’ 𝐹 ∈ (π‘Œ(Hom β€˜πΆ)𝑋))
111, 2, 7, 4, 6, 5isohom 17729 . . . . . . 7 (πœ‘ β†’ (𝑋(Isoβ€˜πΆ)π‘Œ) βŠ† (𝑋(Hom β€˜πΆ)π‘Œ))
12 rcaninv.n . . . . . . . . 9 𝑁 = (Invβ€˜πΆ)
131, 12, 4, 5, 6, 7invf 17721 . . . . . . . 8 (πœ‘ β†’ (π‘Œπ‘π‘‹):(π‘Œ(Isoβ€˜πΆ)𝑋)⟢(𝑋(Isoβ€˜πΆ)π‘Œ))
1413, 9ffvelcdmd 7080 . . . . . . 7 (πœ‘ β†’ ((π‘Œπ‘π‘‹)β€˜πΉ) ∈ (𝑋(Isoβ€˜πΆ)π‘Œ))
1511, 14sseldd 3978 . . . . . 6 (πœ‘ β†’ ((π‘Œπ‘π‘‹)β€˜πΉ) ∈ (𝑋(Hom β€˜πΆ)π‘Œ))
16 rcaninv.z . . . . . 6 (πœ‘ β†’ 𝑍 ∈ 𝐡)
17 rcaninv.g . . . . . 6 (πœ‘ β†’ 𝐺 ∈ (π‘Œ(Hom β€˜πΆ)𝑍))
181, 2, 3, 4, 5, 6, 5, 10, 15, 16, 17catass 17636 . . . . 5 (πœ‘ β†’ ((𝐺(βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍)((π‘Œπ‘π‘‹)β€˜πΉ))(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)𝑍)𝐹) = (𝐺(βŸ¨π‘Œ, π‘ŒβŸ©(compβ€˜πΆ)𝑍)(((π‘Œπ‘π‘‹)β€˜πΉ)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)𝐹)))
19 eqid 2726 . . . . . . . 8 (Idβ€˜πΆ) = (Idβ€˜πΆ)
20 eqid 2726 . . . . . . . 8 (βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ) = (βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)
211, 7, 12, 4, 5, 6, 9, 19, 20invcoisoid 17745 . . . . . . 7 (πœ‘ β†’ (((π‘Œπ‘π‘‹)β€˜πΉ)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)𝐹) = ((Idβ€˜πΆ)β€˜π‘Œ))
2221eqcomd 2732 . . . . . 6 (πœ‘ β†’ ((Idβ€˜πΆ)β€˜π‘Œ) = (((π‘Œπ‘π‘‹)β€˜πΉ)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)𝐹))
2322oveq2d 7420 . . . . 5 (πœ‘ β†’ (𝐺(βŸ¨π‘Œ, π‘ŒβŸ©(compβ€˜πΆ)𝑍)((Idβ€˜πΆ)β€˜π‘Œ)) = (𝐺(βŸ¨π‘Œ, π‘ŒβŸ©(compβ€˜πΆ)𝑍)(((π‘Œπ‘π‘‹)β€˜πΉ)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)𝐹)))
241, 2, 19, 4, 5, 3, 16, 17catrid 17634 . . . . 5 (πœ‘ β†’ (𝐺(βŸ¨π‘Œ, π‘ŒβŸ©(compβ€˜πΆ)𝑍)((Idβ€˜πΆ)β€˜π‘Œ)) = 𝐺)
2518, 23, 243eqtr2rd 2773 . . . 4 (πœ‘ β†’ 𝐺 = ((𝐺(βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍)((π‘Œπ‘π‘‹)β€˜πΉ))(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)𝑍)𝐹))
2625adantr 480 . . 3 ((πœ‘ ∧ (𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅)) β†’ 𝐺 = ((𝐺(βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍)((π‘Œπ‘π‘‹)β€˜πΉ))(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)𝑍)𝐹))
27 rcaninv.o . . . . . . . . 9 ⚬ = (βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍)
2827eqcomi 2735 . . . . . . . 8 (βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍) = ⚬
2928a1i 11 . . . . . . 7 (πœ‘ β†’ (βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍) = ⚬ )
30 eqidd 2727 . . . . . . 7 (πœ‘ β†’ 𝐺 = 𝐺)
31 rcaninv.1 . . . . . . . . 9 𝑅 = ((π‘Œπ‘π‘‹)β€˜πΉ)
3231eqcomi 2735 . . . . . . . 8 ((π‘Œπ‘π‘‹)β€˜πΉ) = 𝑅
3332a1i 11 . . . . . . 7 (πœ‘ β†’ ((π‘Œπ‘π‘‹)β€˜πΉ) = 𝑅)
3429, 30, 33oveq123d 7425 . . . . . 6 (πœ‘ β†’ (𝐺(βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍)((π‘Œπ‘π‘‹)β€˜πΉ)) = (𝐺 ⚬ 𝑅))
3534adantr 480 . . . . 5 ((πœ‘ ∧ (𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅)) β†’ (𝐺(βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍)((π‘Œπ‘π‘‹)β€˜πΉ)) = (𝐺 ⚬ 𝑅))
36 simpr 484 . . . . 5 ((πœ‘ ∧ (𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅)) β†’ (𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅))
3735, 36eqtrd 2766 . . . 4 ((πœ‘ ∧ (𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅)) β†’ (𝐺(βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍)((π‘Œπ‘π‘‹)β€˜πΉ)) = (𝐻 ⚬ 𝑅))
3837oveq1d 7419 . . 3 ((πœ‘ ∧ (𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅)) β†’ ((𝐺(βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍)((π‘Œπ‘π‘‹)β€˜πΉ))(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)𝑍)𝐹) = ((𝐻 ⚬ 𝑅)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)𝑍)𝐹))
3927oveqi 7417 . . . . . . 7 (𝐻 ⚬ 𝑅) = (𝐻(βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍)𝑅)
4039oveq1i 7414 . . . . . 6 ((𝐻 ⚬ 𝑅)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)𝑍)𝐹) = ((𝐻(βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍)𝑅)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)𝑍)𝐹)
4140a1i 11 . . . . 5 (πœ‘ β†’ ((𝐻 ⚬ 𝑅)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)𝑍)𝐹) = ((𝐻(βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍)𝑅)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)𝑍)𝐹))
4231, 15eqeltrid 2831 . . . . . . 7 (πœ‘ β†’ 𝑅 ∈ (𝑋(Hom β€˜πΆ)π‘Œ))
43 rcaninv.h . . . . . . 7 (πœ‘ β†’ 𝐻 ∈ (π‘Œ(Hom β€˜πΆ)𝑍))
441, 2, 3, 4, 5, 6, 5, 10, 42, 16, 43catass 17636 . . . . . 6 (πœ‘ β†’ ((𝐻(βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍)𝑅)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)𝑍)𝐹) = (𝐻(βŸ¨π‘Œ, π‘ŒβŸ©(compβ€˜πΆ)𝑍)(𝑅(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)𝐹)))
4531oveq1i 7414 . . . . . . . 8 (𝑅(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)𝐹) = (((π‘Œπ‘π‘‹)β€˜πΉ)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)𝐹)
4645oveq2i 7415 . . . . . . 7 (𝐻(βŸ¨π‘Œ, π‘ŒβŸ©(compβ€˜πΆ)𝑍)(𝑅(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)𝐹)) = (𝐻(βŸ¨π‘Œ, π‘ŒβŸ©(compβ€˜πΆ)𝑍)(((π‘Œπ‘π‘‹)β€˜πΉ)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)𝐹))
4746a1i 11 . . . . . 6 (πœ‘ β†’ (𝐻(βŸ¨π‘Œ, π‘ŒβŸ©(compβ€˜πΆ)𝑍)(𝑅(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)𝐹)) = (𝐻(βŸ¨π‘Œ, π‘ŒβŸ©(compβ€˜πΆ)𝑍)(((π‘Œπ‘π‘‹)β€˜πΉ)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)𝐹)))
4821oveq2d 7420 . . . . . 6 (πœ‘ β†’ (𝐻(βŸ¨π‘Œ, π‘ŒβŸ©(compβ€˜πΆ)𝑍)(((π‘Œπ‘π‘‹)β€˜πΉ)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)𝐹)) = (𝐻(βŸ¨π‘Œ, π‘ŒβŸ©(compβ€˜πΆ)𝑍)((Idβ€˜πΆ)β€˜π‘Œ)))
4944, 47, 483eqtrd 2770 . . . . 5 (πœ‘ β†’ ((𝐻(βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍)𝑅)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)𝑍)𝐹) = (𝐻(βŸ¨π‘Œ, π‘ŒβŸ©(compβ€˜πΆ)𝑍)((Idβ€˜πΆ)β€˜π‘Œ)))
501, 2, 19, 4, 5, 3, 16, 43catrid 17634 . . . . 5 (πœ‘ β†’ (𝐻(βŸ¨π‘Œ, π‘ŒβŸ©(compβ€˜πΆ)𝑍)((Idβ€˜πΆ)β€˜π‘Œ)) = 𝐻)
5141, 49, 503eqtrd 2770 . . . 4 (πœ‘ β†’ ((𝐻 ⚬ 𝑅)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)𝑍)𝐹) = 𝐻)
5251adantr 480 . . 3 ((πœ‘ ∧ (𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅)) β†’ ((𝐻 ⚬ 𝑅)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)𝑍)𝐹) = 𝐻)
5326, 38, 523eqtrd 2770 . 2 ((πœ‘ ∧ (𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅)) β†’ 𝐺 = 𝐻)
5453ex 412 1 (πœ‘ β†’ ((𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅) β†’ 𝐺 = 𝐻))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 395   = wceq 1533   ∈ wcel 2098  βŸ¨cop 4629  β€˜cfv 6536  (class class class)co 7404  Basecbs 17150  Hom chom 17214  compcco 17215  Catccat 17614  Idccid 17615  Invcinv 17698  Isociso 17699
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-iota 6488  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-1st 7971  df-2nd 7972  df-cat 17618  df-cid 17619  df-sect 17700  df-inv 17701  df-iso 17702
This theorem is referenced by:  initoeu2lem0  17972
  Copyright terms: Public domain W3C validator