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

Theorem rcaninv 17784
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 2728 . . . . . 6 (Hom β€˜πΆ) = (Hom β€˜πΆ)
3 eqid 2728 . . . . . 6 (compβ€˜πΆ) = (compβ€˜πΆ)
4 rcaninv.c . . . . . 6 (πœ‘ β†’ 𝐢 ∈ Cat)
5 rcaninv.y . . . . . 6 (πœ‘ β†’ π‘Œ ∈ 𝐡)
6 rcaninv.x . . . . . 6 (πœ‘ β†’ 𝑋 ∈ 𝐡)
7 eqid 2728 . . . . . . . 8 (Isoβ€˜πΆ) = (Isoβ€˜πΆ)
81, 2, 7, 4, 5, 6isohom 17766 . . . . . . 7 (πœ‘ β†’ (π‘Œ(Isoβ€˜πΆ)𝑋) βŠ† (π‘Œ(Hom β€˜πΆ)𝑋))
9 rcaninv.f . . . . . . 7 (πœ‘ β†’ 𝐹 ∈ (π‘Œ(Isoβ€˜πΆ)𝑋))
108, 9sseldd 3983 . . . . . 6 (πœ‘ β†’ 𝐹 ∈ (π‘Œ(Hom β€˜πΆ)𝑋))
111, 2, 7, 4, 6, 5isohom 17766 . . . . . . 7 (πœ‘ β†’ (𝑋(Isoβ€˜πΆ)π‘Œ) βŠ† (𝑋(Hom β€˜πΆ)π‘Œ))
12 rcaninv.n . . . . . . . . 9 𝑁 = (Invβ€˜πΆ)
131, 12, 4, 5, 6, 7invf 17758 . . . . . . . 8 (πœ‘ β†’ (π‘Œπ‘π‘‹):(π‘Œ(Isoβ€˜πΆ)𝑋)⟢(𝑋(Isoβ€˜πΆ)π‘Œ))
1413, 9ffvelcdmd 7100 . . . . . . 7 (πœ‘ β†’ ((π‘Œπ‘π‘‹)β€˜πΉ) ∈ (𝑋(Isoβ€˜πΆ)π‘Œ))
1511, 14sseldd 3983 . . . . . 6 (πœ‘ β†’ ((π‘Œπ‘π‘‹)β€˜πΉ) ∈ (𝑋(Hom β€˜πΆ)π‘Œ))
16 rcaninv.z . . . . . 6 (πœ‘ β†’ 𝑍 ∈ 𝐡)
17 rcaninv.g . . . . . 6 (πœ‘ β†’ 𝐺 ∈ (π‘Œ(Hom β€˜πΆ)𝑍))
181, 2, 3, 4, 5, 6, 5, 10, 15, 16, 17catass 17673 . . . . 5 (πœ‘ β†’ ((𝐺(βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍)((π‘Œπ‘π‘‹)β€˜πΉ))(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)𝑍)𝐹) = (𝐺(βŸ¨π‘Œ, π‘ŒβŸ©(compβ€˜πΆ)𝑍)(((π‘Œπ‘π‘‹)β€˜πΉ)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)𝐹)))
19 eqid 2728 . . . . . . . 8 (Idβ€˜πΆ) = (Idβ€˜πΆ)
20 eqid 2728 . . . . . . . 8 (βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ) = (βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)
211, 7, 12, 4, 5, 6, 9, 19, 20invcoisoid 17782 . . . . . . 7 (πœ‘ β†’ (((π‘Œπ‘π‘‹)β€˜πΉ)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)𝐹) = ((Idβ€˜πΆ)β€˜π‘Œ))
2221eqcomd 2734 . . . . . 6 (πœ‘ β†’ ((Idβ€˜πΆ)β€˜π‘Œ) = (((π‘Œπ‘π‘‹)β€˜πΉ)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)𝐹))
2322oveq2d 7442 . . . . 5 (πœ‘ β†’ (𝐺(βŸ¨π‘Œ, π‘ŒβŸ©(compβ€˜πΆ)𝑍)((Idβ€˜πΆ)β€˜π‘Œ)) = (𝐺(βŸ¨π‘Œ, π‘ŒβŸ©(compβ€˜πΆ)𝑍)(((π‘Œπ‘π‘‹)β€˜πΉ)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)𝐹)))
241, 2, 19, 4, 5, 3, 16, 17catrid 17671 . . . . 5 (πœ‘ β†’ (𝐺(βŸ¨π‘Œ, π‘ŒβŸ©(compβ€˜πΆ)𝑍)((Idβ€˜πΆ)β€˜π‘Œ)) = 𝐺)
2518, 23, 243eqtr2rd 2775 . . . 4 (πœ‘ β†’ 𝐺 = ((𝐺(βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍)((π‘Œπ‘π‘‹)β€˜πΉ))(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)𝑍)𝐹))
2625adantr 479 . . 3 ((πœ‘ ∧ (𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅)) β†’ 𝐺 = ((𝐺(βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍)((π‘Œπ‘π‘‹)β€˜πΉ))(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)𝑍)𝐹))
27 rcaninv.o . . . . . . . . 9 ⚬ = (βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍)
2827eqcomi 2737 . . . . . . . 8 (βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍) = ⚬
2928a1i 11 . . . . . . 7 (πœ‘ β†’ (βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍) = ⚬ )
30 eqidd 2729 . . . . . . 7 (πœ‘ β†’ 𝐺 = 𝐺)
31 rcaninv.1 . . . . . . . . 9 𝑅 = ((π‘Œπ‘π‘‹)β€˜πΉ)
3231eqcomi 2737 . . . . . . . 8 ((π‘Œπ‘π‘‹)β€˜πΉ) = 𝑅
3332a1i 11 . . . . . . 7 (πœ‘ β†’ ((π‘Œπ‘π‘‹)β€˜πΉ) = 𝑅)
3429, 30, 33oveq123d 7447 . . . . . 6 (πœ‘ β†’ (𝐺(βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍)((π‘Œπ‘π‘‹)β€˜πΉ)) = (𝐺 ⚬ 𝑅))
3534adantr 479 . . . . 5 ((πœ‘ ∧ (𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅)) β†’ (𝐺(βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍)((π‘Œπ‘π‘‹)β€˜πΉ)) = (𝐺 ⚬ 𝑅))
36 simpr 483 . . . . 5 ((πœ‘ ∧ (𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅)) β†’ (𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅))
3735, 36eqtrd 2768 . . . 4 ((πœ‘ ∧ (𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅)) β†’ (𝐺(βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍)((π‘Œπ‘π‘‹)β€˜πΉ)) = (𝐻 ⚬ 𝑅))
3837oveq1d 7441 . . 3 ((πœ‘ ∧ (𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅)) β†’ ((𝐺(βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍)((π‘Œπ‘π‘‹)β€˜πΉ))(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)𝑍)𝐹) = ((𝐻 ⚬ 𝑅)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)𝑍)𝐹))
3927oveqi 7439 . . . . . . 7 (𝐻 ⚬ 𝑅) = (𝐻(βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍)𝑅)
4039oveq1i 7436 . . . . . 6 ((𝐻 ⚬ 𝑅)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)𝑍)𝐹) = ((𝐻(βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍)𝑅)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)𝑍)𝐹)
4140a1i 11 . . . . 5 (πœ‘ β†’ ((𝐻 ⚬ 𝑅)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)𝑍)𝐹) = ((𝐻(βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍)𝑅)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)𝑍)𝐹))
4231, 15eqeltrid 2833 . . . . . . 7 (πœ‘ β†’ 𝑅 ∈ (𝑋(Hom β€˜πΆ)π‘Œ))
43 rcaninv.h . . . . . . 7 (πœ‘ β†’ 𝐻 ∈ (π‘Œ(Hom β€˜πΆ)𝑍))
441, 2, 3, 4, 5, 6, 5, 10, 42, 16, 43catass 17673 . . . . . 6 (πœ‘ β†’ ((𝐻(βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍)𝑅)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)𝑍)𝐹) = (𝐻(βŸ¨π‘Œ, π‘ŒβŸ©(compβ€˜πΆ)𝑍)(𝑅(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)𝐹)))
4531oveq1i 7436 . . . . . . . 8 (𝑅(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)𝐹) = (((π‘Œπ‘π‘‹)β€˜πΉ)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)𝐹)
4645oveq2i 7437 . . . . . . 7 (𝐻(βŸ¨π‘Œ, π‘ŒβŸ©(compβ€˜πΆ)𝑍)(𝑅(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)𝐹)) = (𝐻(βŸ¨π‘Œ, π‘ŒβŸ©(compβ€˜πΆ)𝑍)(((π‘Œπ‘π‘‹)β€˜πΉ)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)𝐹))
4746a1i 11 . . . . . 6 (πœ‘ β†’ (𝐻(βŸ¨π‘Œ, π‘ŒβŸ©(compβ€˜πΆ)𝑍)(𝑅(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)𝐹)) = (𝐻(βŸ¨π‘Œ, π‘ŒβŸ©(compβ€˜πΆ)𝑍)(((π‘Œπ‘π‘‹)β€˜πΉ)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)𝐹)))
4821oveq2d 7442 . . . . . 6 (πœ‘ β†’ (𝐻(βŸ¨π‘Œ, π‘ŒβŸ©(compβ€˜πΆ)𝑍)(((π‘Œπ‘π‘‹)β€˜πΉ)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)𝐹)) = (𝐻(βŸ¨π‘Œ, π‘ŒβŸ©(compβ€˜πΆ)𝑍)((Idβ€˜πΆ)β€˜π‘Œ)))
4944, 47, 483eqtrd 2772 . . . . 5 (πœ‘ β†’ ((𝐻(βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑍)𝑅)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)𝑍)𝐹) = (𝐻(βŸ¨π‘Œ, π‘ŒβŸ©(compβ€˜πΆ)𝑍)((Idβ€˜πΆ)β€˜π‘Œ)))
501, 2, 19, 4, 5, 3, 16, 43catrid 17671 . . . . 5 (πœ‘ β†’ (𝐻(βŸ¨π‘Œ, π‘ŒβŸ©(compβ€˜πΆ)𝑍)((Idβ€˜πΆ)β€˜π‘Œ)) = 𝐻)
5141, 49, 503eqtrd 2772 . . . 4 (πœ‘ β†’ ((𝐻 ⚬ 𝑅)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)𝑍)𝐹) = 𝐻)
5251adantr 479 . . 3 ((πœ‘ ∧ (𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅)) β†’ ((𝐻 ⚬ 𝑅)(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)𝑍)𝐹) = 𝐻)
5326, 38, 523eqtrd 2772 . 2 ((πœ‘ ∧ (𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅)) β†’ 𝐺 = 𝐻)
5453ex 411 1 (πœ‘ β†’ ((𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅) β†’ 𝐺 = 𝐻))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 394   = wceq 1533   ∈ wcel 2098  βŸ¨cop 4638  β€˜cfv 6553  (class class class)co 7426  Basecbs 17187  Hom chom 17251  compcco 17252  Catccat 17651  Idccid 17652  Invcinv 17735  Isociso 17736
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 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-1st 7999  df-2nd 8000  df-cat 17655  df-cid 17656  df-sect 17737  df-inv 17738  df-iso 17739
This theorem is referenced by:  initoeu2lem0  18009
  Copyright terms: Public domain W3C validator