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

Theorem invcoisoid 17302
Description: The inverse of an isomorphism composed with the isomorphism is the identity. (Contributed by AV, 5-Apr-2020.)
Hypotheses
Ref Expression
invisoinv.b 𝐵 = (Base‘𝐶)
invisoinv.i 𝐼 = (Iso‘𝐶)
invisoinv.n 𝑁 = (Inv‘𝐶)
invisoinv.c (𝜑𝐶 ∈ Cat)
invisoinv.x (𝜑𝑋𝐵)
invisoinv.y (𝜑𝑌𝐵)
invisoinv.f (𝜑𝐹 ∈ (𝑋𝐼𝑌))
invcoisoid.1 1 = (Id‘𝐶)
invcoisoid.o = (⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)
Assertion
Ref Expression
invcoisoid (𝜑 → (((𝑋𝑁𝑌)‘𝐹) 𝐹) = ( 1𝑋))

Proof of Theorem invcoisoid
StepHypRef Expression
1 invisoinv.b . . . 4 𝐵 = (Base‘𝐶)
2 invisoinv.i . . . 4 𝐼 = (Iso‘𝐶)
3 invisoinv.n . . . 4 𝑁 = (Inv‘𝐶)
4 invisoinv.c . . . 4 (𝜑𝐶 ∈ Cat)
5 invisoinv.x . . . 4 (𝜑𝑋𝐵)
6 invisoinv.y . . . 4 (𝜑𝑌𝐵)
7 invisoinv.f . . . 4 (𝜑𝐹 ∈ (𝑋𝐼𝑌))
81, 2, 3, 4, 5, 6, 7invisoinvr 17301 . . 3 (𝜑𝐹(𝑋𝑁𝑌)((𝑋𝑁𝑌)‘𝐹))
9 eqid 2737 . . . . 5 (Sect‘𝐶) = (Sect‘𝐶)
101, 3, 4, 5, 6, 9isinv 17270 . . . 4 (𝜑 → (𝐹(𝑋𝑁𝑌)((𝑋𝑁𝑌)‘𝐹) ↔ (𝐹(𝑋(Sect‘𝐶)𝑌)((𝑋𝑁𝑌)‘𝐹) ∧ ((𝑋𝑁𝑌)‘𝐹)(𝑌(Sect‘𝐶)𝑋)𝐹)))
11 simpl 486 . . . 4 ((𝐹(𝑋(Sect‘𝐶)𝑌)((𝑋𝑁𝑌)‘𝐹) ∧ ((𝑋𝑁𝑌)‘𝐹)(𝑌(Sect‘𝐶)𝑋)𝐹) → 𝐹(𝑋(Sect‘𝐶)𝑌)((𝑋𝑁𝑌)‘𝐹))
1210, 11syl6bi 256 . . 3 (𝜑 → (𝐹(𝑋𝑁𝑌)((𝑋𝑁𝑌)‘𝐹) → 𝐹(𝑋(Sect‘𝐶)𝑌)((𝑋𝑁𝑌)‘𝐹)))
138, 12mpd 15 . 2 (𝜑𝐹(𝑋(Sect‘𝐶)𝑌)((𝑋𝑁𝑌)‘𝐹))
14 eqid 2737 . . . 4 (Hom ‘𝐶) = (Hom ‘𝐶)
15 eqid 2737 . . . 4 (comp‘𝐶) = (comp‘𝐶)
16 invcoisoid.1 . . . 4 1 = (Id‘𝐶)
171, 14, 2, 4, 5, 6isohom 17286 . . . . 5 (𝜑 → (𝑋𝐼𝑌) ⊆ (𝑋(Hom ‘𝐶)𝑌))
1817, 7sseldd 3907 . . . 4 (𝜑𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌))
191, 14, 2, 4, 6, 5isohom 17286 . . . . 5 (𝜑 → (𝑌𝐼𝑋) ⊆ (𝑌(Hom ‘𝐶)𝑋))
201, 3, 4, 5, 6, 2invf 17278 . . . . . 6 (𝜑 → (𝑋𝑁𝑌):(𝑋𝐼𝑌)⟶(𝑌𝐼𝑋))
2120, 7ffvelrnd 6910 . . . . 5 (𝜑 → ((𝑋𝑁𝑌)‘𝐹) ∈ (𝑌𝐼𝑋))
2219, 21sseldd 3907 . . . 4 (𝜑 → ((𝑋𝑁𝑌)‘𝐹) ∈ (𝑌(Hom ‘𝐶)𝑋))
231, 14, 15, 16, 9, 4, 5, 6, 18, 22issect2 17264 . . 3 (𝜑 → (𝐹(𝑋(Sect‘𝐶)𝑌)((𝑋𝑁𝑌)‘𝐹) ↔ (((𝑋𝑁𝑌)‘𝐹)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝐹) = ( 1𝑋)))
24 invcoisoid.o . . . . . . 7 = (⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)
2524a1i 11 . . . . . 6 (𝜑 = (⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋))
2625eqcomd 2743 . . . . 5 (𝜑 → (⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋) = )
2726oveqd 7235 . . . 4 (𝜑 → (((𝑋𝑁𝑌)‘𝐹)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝐹) = (((𝑋𝑁𝑌)‘𝐹) 𝐹))
2827eqeq1d 2739 . . 3 (𝜑 → ((((𝑋𝑁𝑌)‘𝐹)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝐹) = ( 1𝑋) ↔ (((𝑋𝑁𝑌)‘𝐹) 𝐹) = ( 1𝑋)))
2923, 28bitrd 282 . 2 (𝜑 → (𝐹(𝑋(Sect‘𝐶)𝑌)((𝑋𝑁𝑌)‘𝐹) ↔ (((𝑋𝑁𝑌)‘𝐹) 𝐹) = ( 1𝑋)))
3013, 29mpbid 235 1 (𝜑 → (((𝑋𝑁𝑌)‘𝐹) 𝐹) = ( 1𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1543  wcel 2110  cop 4552   class class class wbr 5058  cfv 6385  (class class class)co 7218  Basecbs 16765  Hom chom 16818  compcco 16819  Catccat 17172  Idccid 17173  Sectcsect 17254  Invcinv 17255  Isociso 17256
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5184  ax-sep 5197  ax-nul 5204  ax-pow 5263  ax-pr 5327  ax-un 7528
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3415  df-sbc 3700  df-csb 3817  df-dif 3874  df-un 3876  df-in 3878  df-ss 3888  df-nul 4243  df-if 4445  df-pw 4520  df-sn 4547  df-pr 4549  df-op 4553  df-uni 4825  df-iun 4911  df-br 5059  df-opab 5121  df-mpt 5141  df-id 5460  df-xp 5562  df-rel 5563  df-cnv 5564  df-co 5565  df-dm 5566  df-rn 5567  df-res 5568  df-ima 5569  df-iota 6343  df-fun 6387  df-fn 6388  df-f 6389  df-f1 6390  df-fo 6391  df-f1o 6392  df-fv 6393  df-riota 7175  df-ov 7221  df-oprab 7222  df-mpo 7223  df-1st 7766  df-2nd 7767  df-cat 17176  df-cid 17177  df-sect 17257  df-inv 17258  df-iso 17259
This theorem is referenced by:  rcaninv  17304
  Copyright terms: Public domain W3C validator