Proof of Theorem invco
Step | Hyp | Ref
| Expression |
1 | | invfval.b |
. . 3
⊢ 𝐵 = (Base‘𝐶) |
2 | | invco.o |
. . 3
⊢ · =
(comp‘𝐶) |
3 | | eqid 2738 |
. . 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 17133 |
. . . . . . 7
⊢ (𝜑 → (𝑋𝐼𝑌) = dom (𝑋𝑁𝑌)) |
12 | 8, 11 | eleqtrd 2835 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ dom (𝑋𝑁𝑌)) |
13 | 1, 9, 4, 5, 6 | invfun 17132 |
. . . . . . 7
⊢ (𝜑 → Fun (𝑋𝑁𝑌)) |
14 | | funfvbrb 6822 |
. . . . . . 7
⊢ (Fun
(𝑋𝑁𝑌) → (𝐹 ∈ dom (𝑋𝑁𝑌) ↔ 𝐹(𝑋𝑁𝑌)((𝑋𝑁𝑌)‘𝐹))) |
15 | 13, 14 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐹 ∈ dom (𝑋𝑁𝑌) ↔ 𝐹(𝑋𝑁𝑌)((𝑋𝑁𝑌)‘𝐹))) |
16 | 12, 15 | mpbid 235 |
. . . . 5
⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)((𝑋𝑁𝑌)‘𝐹)) |
17 | 1, 9, 4, 5, 6, 3 | isinv 17128 |
. . . . 5
⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)((𝑋𝑁𝑌)‘𝐹) ↔ (𝐹(𝑋(Sect‘𝐶)𝑌)((𝑋𝑁𝑌)‘𝐹) ∧ ((𝑋𝑁𝑌)‘𝐹)(𝑌(Sect‘𝐶)𝑋)𝐹))) |
18 | 16, 17 | mpbid 235 |
. . . 4
⊢ (𝜑 → (𝐹(𝑋(Sect‘𝐶)𝑌)((𝑋𝑁𝑌)‘𝐹) ∧ ((𝑋𝑁𝑌)‘𝐹)(𝑌(Sect‘𝐶)𝑋)𝐹)) |
19 | 18 | simpld 498 |
. . 3
⊢ (𝜑 → 𝐹(𝑋(Sect‘𝐶)𝑌)((𝑋𝑁𝑌)‘𝐹)) |
20 | | invco.f |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ (𝑌𝐼𝑍)) |
21 | 1, 9, 4, 6, 7, 10 | isoval 17133 |
. . . . . . 7
⊢ (𝜑 → (𝑌𝐼𝑍) = dom (𝑌𝑁𝑍)) |
22 | 20, 21 | eleqtrd 2835 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ dom (𝑌𝑁𝑍)) |
23 | 1, 9, 4, 6, 7 | invfun 17132 |
. . . . . . 7
⊢ (𝜑 → Fun (𝑌𝑁𝑍)) |
24 | | funfvbrb 6822 |
. . . . . . 7
⊢ (Fun
(𝑌𝑁𝑍) → (𝐺 ∈ dom (𝑌𝑁𝑍) ↔ 𝐺(𝑌𝑁𝑍)((𝑌𝑁𝑍)‘𝐺))) |
25 | 23, 24 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐺 ∈ dom (𝑌𝑁𝑍) ↔ 𝐺(𝑌𝑁𝑍)((𝑌𝑁𝑍)‘𝐺))) |
26 | 22, 25 | mpbid 235 |
. . . . 5
⊢ (𝜑 → 𝐺(𝑌𝑁𝑍)((𝑌𝑁𝑍)‘𝐺)) |
27 | 1, 9, 4, 6, 7, 3 | isinv 17128 |
. . . . 5
⊢ (𝜑 → (𝐺(𝑌𝑁𝑍)((𝑌𝑁𝑍)‘𝐺) ↔ (𝐺(𝑌(Sect‘𝐶)𝑍)((𝑌𝑁𝑍)‘𝐺) ∧ ((𝑌𝑁𝑍)‘𝐺)(𝑍(Sect‘𝐶)𝑌)𝐺))) |
28 | 26, 27 | mpbid 235 |
. . . 4
⊢ (𝜑 → (𝐺(𝑌(Sect‘𝐶)𝑍)((𝑌𝑁𝑍)‘𝐺) ∧ ((𝑌𝑁𝑍)‘𝐺)(𝑍(Sect‘𝐶)𝑌)𝐺)) |
29 | 28 | simpld 498 |
. . 3
⊢ (𝜑 → 𝐺(𝑌(Sect‘𝐶)𝑍)((𝑌𝑁𝑍)‘𝐺)) |
30 | 1, 2, 3, 4, 5, 6, 7, 19, 29 | sectco 17124 |
. 2
⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹)(𝑋(Sect‘𝐶)𝑍)(((𝑋𝑁𝑌)‘𝐹)(〈𝑍, 𝑌〉 · 𝑋)((𝑌𝑁𝑍)‘𝐺))) |
31 | 28 | simprd 499 |
. . 3
⊢ (𝜑 → ((𝑌𝑁𝑍)‘𝐺)(𝑍(Sect‘𝐶)𝑌)𝐺) |
32 | 18 | simprd 499 |
. . 3
⊢ (𝜑 → ((𝑋𝑁𝑌)‘𝐹)(𝑌(Sect‘𝐶)𝑋)𝐹) |
33 | 1, 2, 3, 4, 7, 6, 5, 31, 32 | sectco 17124 |
. 2
⊢ (𝜑 → (((𝑋𝑁𝑌)‘𝐹)(〈𝑍, 𝑌〉 · 𝑋)((𝑌𝑁𝑍)‘𝐺))(𝑍(Sect‘𝐶)𝑋)(𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹)) |
34 | 1, 9, 4, 5, 7, 3 | isinv 17128 |
. 2
⊢ (𝜑 → ((𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹)(𝑋𝑁𝑍)(((𝑋𝑁𝑌)‘𝐹)(〈𝑍, 𝑌〉 · 𝑋)((𝑌𝑁𝑍)‘𝐺)) ↔ ((𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹)(𝑋(Sect‘𝐶)𝑍)(((𝑋𝑁𝑌)‘𝐹)(〈𝑍, 𝑌〉 · 𝑋)((𝑌𝑁𝑍)‘𝐺)) ∧ (((𝑋𝑁𝑌)‘𝐹)(〈𝑍, 𝑌〉 · 𝑋)((𝑌𝑁𝑍)‘𝐺))(𝑍(Sect‘𝐶)𝑋)(𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹)))) |
35 | 30, 33, 34 | mpbir2and 713 |
1
⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹)(𝑋𝑁𝑍)(((𝑋𝑁𝑌)‘𝐹)(〈𝑍, 𝑌〉 · 𝑋)((𝑌𝑁𝑍)‘𝐺))) |