Proof of Theorem invco
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | invfval.b | . . 3
⊢ 𝐵 = (Base‘𝐶) | 
| 2 |  | invco.o | . . 3
⊢  · =
(comp‘𝐶) | 
| 3 |  | eqid 2736 | . . 3
⊢
(Sect‘𝐶) =
(Sect‘𝐶) | 
| 4 |  | invfval.c | . . 3
⊢ (𝜑 → 𝐶 ∈ Cat) | 
| 5 |  | invfval.x | . . 3
⊢ (𝜑 → 𝑋 ∈ 𝐵) | 
| 6 |  | invfval.y | . . 3
⊢ (𝜑 → 𝑌 ∈ 𝐵) | 
| 7 |  | invco.z | . . 3
⊢ (𝜑 → 𝑍 ∈ 𝐵) | 
| 8 |  | invinv.f | . . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) | 
| 9 |  | invfval.n | . . . . . . . 8
⊢ 𝑁 = (Inv‘𝐶) | 
| 10 |  | isoval.n | . . . . . . . 8
⊢ 𝐼 = (Iso‘𝐶) | 
| 11 | 1, 9, 4, 5, 6, 10 | isoval 17810 | . . . . . . 7
⊢ (𝜑 → (𝑋𝐼𝑌) = dom (𝑋𝑁𝑌)) | 
| 12 | 8, 11 | eleqtrd 2842 | . . . . . 6
⊢ (𝜑 → 𝐹 ∈ dom (𝑋𝑁𝑌)) | 
| 13 | 1, 9, 4, 5, 6 | invfun 17809 | . . . . . . 7
⊢ (𝜑 → Fun (𝑋𝑁𝑌)) | 
| 14 |  | funfvbrb 7070 | . . . . . . 7
⊢ (Fun
(𝑋𝑁𝑌) → (𝐹 ∈ dom (𝑋𝑁𝑌) ↔ 𝐹(𝑋𝑁𝑌)((𝑋𝑁𝑌)‘𝐹))) | 
| 15 | 13, 14 | syl 17 | . . . . . 6
⊢ (𝜑 → (𝐹 ∈ dom (𝑋𝑁𝑌) ↔ 𝐹(𝑋𝑁𝑌)((𝑋𝑁𝑌)‘𝐹))) | 
| 16 | 12, 15 | mpbid 232 | . . . . 5
⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)((𝑋𝑁𝑌)‘𝐹)) | 
| 17 | 1, 9, 4, 5, 6, 3 | isinv 17805 | . . . . 5
⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)((𝑋𝑁𝑌)‘𝐹) ↔ (𝐹(𝑋(Sect‘𝐶)𝑌)((𝑋𝑁𝑌)‘𝐹) ∧ ((𝑋𝑁𝑌)‘𝐹)(𝑌(Sect‘𝐶)𝑋)𝐹))) | 
| 18 | 16, 17 | mpbid 232 | . . . 4
⊢ (𝜑 → (𝐹(𝑋(Sect‘𝐶)𝑌)((𝑋𝑁𝑌)‘𝐹) ∧ ((𝑋𝑁𝑌)‘𝐹)(𝑌(Sect‘𝐶)𝑋)𝐹)) | 
| 19 | 18 | simpld 494 | . . 3
⊢ (𝜑 → 𝐹(𝑋(Sect‘𝐶)𝑌)((𝑋𝑁𝑌)‘𝐹)) | 
| 20 |  | invco.f | . . . . . . 7
⊢ (𝜑 → 𝐺 ∈ (𝑌𝐼𝑍)) | 
| 21 | 1, 9, 4, 6, 7, 10 | isoval 17810 | . . . . . . 7
⊢ (𝜑 → (𝑌𝐼𝑍) = dom (𝑌𝑁𝑍)) | 
| 22 | 20, 21 | eleqtrd 2842 | . . . . . 6
⊢ (𝜑 → 𝐺 ∈ dom (𝑌𝑁𝑍)) | 
| 23 | 1, 9, 4, 6, 7 | invfun 17809 | . . . . . . 7
⊢ (𝜑 → Fun (𝑌𝑁𝑍)) | 
| 24 |  | funfvbrb 7070 | . . . . . . 7
⊢ (Fun
(𝑌𝑁𝑍) → (𝐺 ∈ dom (𝑌𝑁𝑍) ↔ 𝐺(𝑌𝑁𝑍)((𝑌𝑁𝑍)‘𝐺))) | 
| 25 | 23, 24 | syl 17 | . . . . . 6
⊢ (𝜑 → (𝐺 ∈ dom (𝑌𝑁𝑍) ↔ 𝐺(𝑌𝑁𝑍)((𝑌𝑁𝑍)‘𝐺))) | 
| 26 | 22, 25 | mpbid 232 | . . . . 5
⊢ (𝜑 → 𝐺(𝑌𝑁𝑍)((𝑌𝑁𝑍)‘𝐺)) | 
| 27 | 1, 9, 4, 6, 7, 3 | isinv 17805 | . . . . 5
⊢ (𝜑 → (𝐺(𝑌𝑁𝑍)((𝑌𝑁𝑍)‘𝐺) ↔ (𝐺(𝑌(Sect‘𝐶)𝑍)((𝑌𝑁𝑍)‘𝐺) ∧ ((𝑌𝑁𝑍)‘𝐺)(𝑍(Sect‘𝐶)𝑌)𝐺))) | 
| 28 | 26, 27 | mpbid 232 | . . . 4
⊢ (𝜑 → (𝐺(𝑌(Sect‘𝐶)𝑍)((𝑌𝑁𝑍)‘𝐺) ∧ ((𝑌𝑁𝑍)‘𝐺)(𝑍(Sect‘𝐶)𝑌)𝐺)) | 
| 29 | 28 | simpld 494 | . . 3
⊢ (𝜑 → 𝐺(𝑌(Sect‘𝐶)𝑍)((𝑌𝑁𝑍)‘𝐺)) | 
| 30 | 1, 2, 3, 4, 5, 6, 7, 19, 29 | sectco 17801 | . 2
⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹)(𝑋(Sect‘𝐶)𝑍)(((𝑋𝑁𝑌)‘𝐹)(〈𝑍, 𝑌〉 · 𝑋)((𝑌𝑁𝑍)‘𝐺))) | 
| 31 | 28 | simprd 495 | . . 3
⊢ (𝜑 → ((𝑌𝑁𝑍)‘𝐺)(𝑍(Sect‘𝐶)𝑌)𝐺) | 
| 32 | 18 | simprd 495 | . . 3
⊢ (𝜑 → ((𝑋𝑁𝑌)‘𝐹)(𝑌(Sect‘𝐶)𝑋)𝐹) | 
| 33 | 1, 2, 3, 4, 7, 6, 5, 31, 32 | sectco 17801 | . 2
⊢ (𝜑 → (((𝑋𝑁𝑌)‘𝐹)(〈𝑍, 𝑌〉 · 𝑋)((𝑌𝑁𝑍)‘𝐺))(𝑍(Sect‘𝐶)𝑋)(𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹)) | 
| 34 | 1, 9, 4, 5, 7, 3 | isinv 17805 | . 2
⊢ (𝜑 → ((𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹)(𝑋𝑁𝑍)(((𝑋𝑁𝑌)‘𝐹)(〈𝑍, 𝑌〉 · 𝑋)((𝑌𝑁𝑍)‘𝐺)) ↔ ((𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹)(𝑋(Sect‘𝐶)𝑍)(((𝑋𝑁𝑌)‘𝐹)(〈𝑍, 𝑌〉 · 𝑋)((𝑌𝑁𝑍)‘𝐺)) ∧ (((𝑋𝑁𝑌)‘𝐹)(〈𝑍, 𝑌〉 · 𝑋)((𝑌𝑁𝑍)‘𝐺))(𝑍(Sect‘𝐶)𝑋)(𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹)))) | 
| 35 | 30, 33, 34 | mpbir2and 713 | 1
⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹)(𝑋𝑁𝑍)(((𝑋𝑁𝑌)‘𝐹)(〈𝑍, 𝑌〉 · 𝑋)((𝑌𝑁𝑍)‘𝐺))) |