Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > invcoisoid | Structured version Visualization version GIF version |
Description: The inverse of an isomorphism composed with the isomorphism is the identity. (Contributed by AV, 5-Apr-2020.) |
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‘𝐶)𝑋) |
Ref | Expression |
---|---|
invcoisoid | ⊢ (𝜑 → (((𝑋𝑁𝑌)‘𝐹) ⚬ 𝐹) = ( 1 ‘𝑋)) |
Step | Hyp | Ref | 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 ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) | |
8 | 1, 2, 3, 4, 5, 6, 7 | invisoinvr 17301 | . . 3 ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)((𝑋𝑁𝑌)‘𝐹)) |
9 | eqid 2737 | . . . . 5 ⊢ (Sect‘𝐶) = (Sect‘𝐶) | |
10 | 1, 3, 4, 5, 6, 9 | isinv 17270 | . . . 4 ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)((𝑋𝑁𝑌)‘𝐹) ↔ (𝐹(𝑋(Sect‘𝐶)𝑌)((𝑋𝑁𝑌)‘𝐹) ∧ ((𝑋𝑁𝑌)‘𝐹)(𝑌(Sect‘𝐶)𝑋)𝐹))) |
11 | simpl 486 | . . . 4 ⊢ ((𝐹(𝑋(Sect‘𝐶)𝑌)((𝑋𝑁𝑌)‘𝐹) ∧ ((𝑋𝑁𝑌)‘𝐹)(𝑌(Sect‘𝐶)𝑋)𝐹) → 𝐹(𝑋(Sect‘𝐶)𝑌)((𝑋𝑁𝑌)‘𝐹)) | |
12 | 10, 11 | syl6bi 256 | . . 3 ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)((𝑋𝑁𝑌)‘𝐹) → 𝐹(𝑋(Sect‘𝐶)𝑌)((𝑋𝑁𝑌)‘𝐹))) |
13 | 8, 12 | mpd 15 | . 2 ⊢ (𝜑 → 𝐹(𝑋(Sect‘𝐶)𝑌)((𝑋𝑁𝑌)‘𝐹)) |
14 | eqid 2737 | . . . 4 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶) | |
15 | eqid 2737 | . . . 4 ⊢ (comp‘𝐶) = (comp‘𝐶) | |
16 | invcoisoid.1 | . . . 4 ⊢ 1 = (Id‘𝐶) | |
17 | 1, 14, 2, 4, 5, 6 | isohom 17286 | . . . . 5 ⊢ (𝜑 → (𝑋𝐼𝑌) ⊆ (𝑋(Hom ‘𝐶)𝑌)) |
18 | 17, 7 | sseldd 3907 | . . . 4 ⊢ (𝜑 → 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌)) |
19 | 1, 14, 2, 4, 6, 5 | isohom 17286 | . . . . 5 ⊢ (𝜑 → (𝑌𝐼𝑋) ⊆ (𝑌(Hom ‘𝐶)𝑋)) |
20 | 1, 3, 4, 5, 6, 2 | invf 17278 | . . . . . 6 ⊢ (𝜑 → (𝑋𝑁𝑌):(𝑋𝐼𝑌)⟶(𝑌𝐼𝑋)) |
21 | 20, 7 | ffvelrnd 6910 | . . . . 5 ⊢ (𝜑 → ((𝑋𝑁𝑌)‘𝐹) ∈ (𝑌𝐼𝑋)) |
22 | 19, 21 | sseldd 3907 | . . . 4 ⊢ (𝜑 → ((𝑋𝑁𝑌)‘𝐹) ∈ (𝑌(Hom ‘𝐶)𝑋)) |
23 | 1, 14, 15, 16, 9, 4, 5, 6, 18, 22 | issect2 17264 | . . 3 ⊢ (𝜑 → (𝐹(𝑋(Sect‘𝐶)𝑌)((𝑋𝑁𝑌)‘𝐹) ↔ (((𝑋𝑁𝑌)‘𝐹)(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ( 1 ‘𝑋))) |
24 | invcoisoid.o | . . . . . . 7 ⊢ ⚬ = (〈𝑋, 𝑌〉(comp‘𝐶)𝑋) | |
25 | 24 | a1i 11 | . . . . . 6 ⊢ (𝜑 → ⚬ = (〈𝑋, 𝑌〉(comp‘𝐶)𝑋)) |
26 | 25 | eqcomd 2743 | . . . . 5 ⊢ (𝜑 → (〈𝑋, 𝑌〉(comp‘𝐶)𝑋) = ⚬ ) |
27 | 26 | oveqd 7235 | . . . 4 ⊢ (𝜑 → (((𝑋𝑁𝑌)‘𝐹)(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = (((𝑋𝑁𝑌)‘𝐹) ⚬ 𝐹)) |
28 | 27 | eqeq1d 2739 | . . 3 ⊢ (𝜑 → ((((𝑋𝑁𝑌)‘𝐹)(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ( 1 ‘𝑋) ↔ (((𝑋𝑁𝑌)‘𝐹) ⚬ 𝐹) = ( 1 ‘𝑋))) |
29 | 23, 28 | bitrd 282 | . 2 ⊢ (𝜑 → (𝐹(𝑋(Sect‘𝐶)𝑌)((𝑋𝑁𝑌)‘𝐹) ↔ (((𝑋𝑁𝑌)‘𝐹) ⚬ 𝐹) = ( 1 ‘𝑋))) |
30 | 13, 29 | mpbid 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 |