Proof of Theorem monsect
| Step | Hyp | Ref
| Expression |
| 1 | | monsect.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐺(𝑌𝑆𝑋)𝐹) |
| 2 | | sectmon.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐶) |
| 3 | | eqid 2737 |
. . . . . . . . 9
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
| 4 | | eqid 2737 |
. . . . . . . . 9
⊢
(comp‘𝐶) =
(comp‘𝐶) |
| 5 | | eqid 2737 |
. . . . . . . . 9
⊢
(Id‘𝐶) =
(Id‘𝐶) |
| 6 | | sectmon.s |
. . . . . . . . 9
⊢ 𝑆 = (Sect‘𝐶) |
| 7 | | sectmon.c |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ Cat) |
| 8 | | sectmon.y |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
| 9 | | sectmon.x |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 10 | 2, 3, 4, 5, 6, 7, 8, 9 | issect 17797 |
. . . . . . . 8
⊢ (𝜑 → (𝐺(𝑌𝑆𝑋)𝐹 ↔ (𝐺 ∈ (𝑌(Hom ‘𝐶)𝑋) ∧ 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ (𝐹(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝐺) = ((Id‘𝐶)‘𝑌)))) |
| 11 | 1, 10 | mpbid 232 |
. . . . . . 7
⊢ (𝜑 → (𝐺 ∈ (𝑌(Hom ‘𝐶)𝑋) ∧ 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ (𝐹(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝐺) = ((Id‘𝐶)‘𝑌))) |
| 12 | 11 | simp3d 1145 |
. . . . . 6
⊢ (𝜑 → (𝐹(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝐺) = ((Id‘𝐶)‘𝑌)) |
| 13 | 12 | oveq1d 7446 |
. . . . 5
⊢ (𝜑 → ((𝐹(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝐺)(〈𝑋, 𝑌〉(comp‘𝐶)𝑌)𝐹) = (((Id‘𝐶)‘𝑌)(〈𝑋, 𝑌〉(comp‘𝐶)𝑌)𝐹)) |
| 14 | 11 | simp2d 1144 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌)) |
| 15 | 11 | simp1d 1143 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ (𝑌(Hom ‘𝐶)𝑋)) |
| 16 | 2, 3, 4, 7, 9, 8, 9, 14, 15, 8, 14 | catass 17729 |
. . . . 5
⊢ (𝜑 → ((𝐹(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)𝐺)(〈𝑋, 𝑌〉(comp‘𝐶)𝑌)𝐹) = (𝐹(〈𝑋, 𝑋〉(comp‘𝐶)𝑌)(𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹))) |
| 17 | 2, 3, 5, 7, 9, 4, 8, 14 | catlid 17726 |
. . . . . 6
⊢ (𝜑 → (((Id‘𝐶)‘𝑌)(〈𝑋, 𝑌〉(comp‘𝐶)𝑌)𝐹) = 𝐹) |
| 18 | 2, 3, 5, 7, 9, 4, 8, 14 | catrid 17727 |
. . . . . 6
⊢ (𝜑 → (𝐹(〈𝑋, 𝑋〉(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)) = 𝐹) |
| 19 | 17, 18 | eqtr4d 2780 |
. . . . 5
⊢ (𝜑 → (((Id‘𝐶)‘𝑌)(〈𝑋, 𝑌〉(comp‘𝐶)𝑌)𝐹) = (𝐹(〈𝑋, 𝑋〉(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋))) |
| 20 | 13, 16, 19 | 3eqtr3d 2785 |
. . . 4
⊢ (𝜑 → (𝐹(〈𝑋, 𝑋〉(comp‘𝐶)𝑌)(𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹)) = (𝐹(〈𝑋, 𝑋〉(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋))) |
| 21 | | sectmon.m |
. . . . 5
⊢ 𝑀 = (Mono‘𝐶) |
| 22 | | monsect.1 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝑋𝑀𝑌)) |
| 23 | 2, 3, 4, 7, 9, 8, 9, 14, 15 | catcocl 17728 |
. . . . 5
⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) ∈ (𝑋(Hom ‘𝐶)𝑋)) |
| 24 | 2, 3, 5, 7, 9 | catidcl 17725 |
. . . . 5
⊢ (𝜑 → ((Id‘𝐶)‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋)) |
| 25 | 2, 3, 4, 21, 7, 9,
8, 9, 22, 23, 24 | moni 17780 |
. . . 4
⊢ (𝜑 → ((𝐹(〈𝑋, 𝑋〉(comp‘𝐶)𝑌)(𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹)) = (𝐹(〈𝑋, 𝑋〉(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)) ↔ (𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋))) |
| 26 | 20, 25 | mpbid 232 |
. . 3
⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋)) |
| 27 | 2, 3, 4, 5, 6, 7, 9, 8, 14, 15 | issect2 17798 |
. . 3
⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ (𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋))) |
| 28 | 26, 27 | mpbird 257 |
. 2
⊢ (𝜑 → 𝐹(𝑋𝑆𝑌)𝐺) |
| 29 | | monsect.n |
. . 3
⊢ 𝑁 = (Inv‘𝐶) |
| 30 | 2, 29, 7, 9, 8, 6 | isinv 17804 |
. 2
⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹(𝑋𝑆𝑌)𝐺 ∧ 𝐺(𝑌𝑆𝑋)𝐹))) |
| 31 | 28, 1, 30 | mpbir2and 713 |
1
⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)𝐺) |