Proof of Theorem sectco
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sectco.b | . . . 4
⊢ 𝐵 = (Base‘𝐶) | 
| 2 |  | eqid 2737 | . . . 4
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) | 
| 3 |  | sectco.o | . . . 4
⊢  · =
(comp‘𝐶) | 
| 4 |  | sectco.c | . . . 4
⊢ (𝜑 → 𝐶 ∈ Cat) | 
| 5 |  | sectco.x | . . . 4
⊢ (𝜑 → 𝑋 ∈ 𝐵) | 
| 6 |  | sectco.z | . . . 4
⊢ (𝜑 → 𝑍 ∈ 𝐵) | 
| 7 |  | sectco.y | . . . 4
⊢ (𝜑 → 𝑌 ∈ 𝐵) | 
| 8 |  | sectco.1 | . . . . . . 7
⊢ (𝜑 → 𝐹(𝑋𝑆𝑌)𝐺) | 
| 9 |  | eqid 2737 | . . . . . . . 8
⊢
(Id‘𝐶) =
(Id‘𝐶) | 
| 10 |  | sectco.s | . . . . . . . 8
⊢ 𝑆 = (Sect‘𝐶) | 
| 11 | 1, 2, 3, 9, 10, 4,
5, 7 | issect 17797 | . . . . . . 7
⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐺 ∈ (𝑌(Hom ‘𝐶)𝑋) ∧ (𝐺(〈𝑋, 𝑌〉 · 𝑋)𝐹) = ((Id‘𝐶)‘𝑋)))) | 
| 12 | 8, 11 | mpbid 232 | . . . . . 6
⊢ (𝜑 → (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐺 ∈ (𝑌(Hom ‘𝐶)𝑋) ∧ (𝐺(〈𝑋, 𝑌〉 · 𝑋)𝐹) = ((Id‘𝐶)‘𝑋))) | 
| 13 | 12 | simp1d 1143 | . . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌)) | 
| 14 |  | sectco.2 | . . . . . . 7
⊢ (𝜑 → 𝐻(𝑌𝑆𝑍)𝐾) | 
| 15 | 1, 2, 3, 9, 10, 4,
7, 6 | issect 17797 | . . . . . . 7
⊢ (𝜑 → (𝐻(𝑌𝑆𝑍)𝐾 ↔ (𝐻 ∈ (𝑌(Hom ‘𝐶)𝑍) ∧ 𝐾 ∈ (𝑍(Hom ‘𝐶)𝑌) ∧ (𝐾(〈𝑌, 𝑍〉 · 𝑌)𝐻) = ((Id‘𝐶)‘𝑌)))) | 
| 16 | 14, 15 | mpbid 232 | . . . . . 6
⊢ (𝜑 → (𝐻 ∈ (𝑌(Hom ‘𝐶)𝑍) ∧ 𝐾 ∈ (𝑍(Hom ‘𝐶)𝑌) ∧ (𝐾(〈𝑌, 𝑍〉 · 𝑌)𝐻) = ((Id‘𝐶)‘𝑌))) | 
| 17 | 16 | simp1d 1143 | . . . . 5
⊢ (𝜑 → 𝐻 ∈ (𝑌(Hom ‘𝐶)𝑍)) | 
| 18 | 1, 2, 3, 4, 5, 7, 6, 13, 17 | catcocl 17728 | . . . 4
⊢ (𝜑 → (𝐻(〈𝑋, 𝑌〉 · 𝑍)𝐹) ∈ (𝑋(Hom ‘𝐶)𝑍)) | 
| 19 | 16 | simp2d 1144 | . . . 4
⊢ (𝜑 → 𝐾 ∈ (𝑍(Hom ‘𝐶)𝑌)) | 
| 20 | 12 | simp2d 1144 | . . . 4
⊢ (𝜑 → 𝐺 ∈ (𝑌(Hom ‘𝐶)𝑋)) | 
| 21 | 1, 2, 3, 4, 5, 6, 7, 18, 19, 5, 20 | catass 17729 | . . 3
⊢ (𝜑 → ((𝐺(〈𝑍, 𝑌〉 · 𝑋)𝐾)(〈𝑋, 𝑍〉 · 𝑋)(𝐻(〈𝑋, 𝑌〉 · 𝑍)𝐹)) = (𝐺(〈𝑋, 𝑌〉 · 𝑋)(𝐾(〈𝑋, 𝑍〉 · 𝑌)(𝐻(〈𝑋, 𝑌〉 · 𝑍)𝐹)))) | 
| 22 | 16 | simp3d 1145 | . . . . . 6
⊢ (𝜑 → (𝐾(〈𝑌, 𝑍〉 · 𝑌)𝐻) = ((Id‘𝐶)‘𝑌)) | 
| 23 | 22 | oveq1d 7446 | . . . . 5
⊢ (𝜑 → ((𝐾(〈𝑌, 𝑍〉 · 𝑌)𝐻)(〈𝑋, 𝑌〉 · 𝑌)𝐹) = (((Id‘𝐶)‘𝑌)(〈𝑋, 𝑌〉 · 𝑌)𝐹)) | 
| 24 | 1, 2, 3, 4, 5, 7, 6, 13, 17, 7, 19 | catass 17729 | . . . . 5
⊢ (𝜑 → ((𝐾(〈𝑌, 𝑍〉 · 𝑌)𝐻)(〈𝑋, 𝑌〉 · 𝑌)𝐹) = (𝐾(〈𝑋, 𝑍〉 · 𝑌)(𝐻(〈𝑋, 𝑌〉 · 𝑍)𝐹))) | 
| 25 | 1, 2, 9, 4, 5, 3, 7, 13 | catlid 17726 | . . . . 5
⊢ (𝜑 → (((Id‘𝐶)‘𝑌)(〈𝑋, 𝑌〉 · 𝑌)𝐹) = 𝐹) | 
| 26 | 23, 24, 25 | 3eqtr3d 2785 | . . . 4
⊢ (𝜑 → (𝐾(〈𝑋, 𝑍〉 · 𝑌)(𝐻(〈𝑋, 𝑌〉 · 𝑍)𝐹)) = 𝐹) | 
| 27 | 26 | oveq2d 7447 | . . 3
⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑋)(𝐾(〈𝑋, 𝑍〉 · 𝑌)(𝐻(〈𝑋, 𝑌〉 · 𝑍)𝐹))) = (𝐺(〈𝑋, 𝑌〉 · 𝑋)𝐹)) | 
| 28 | 12 | simp3d 1145 | . . 3
⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑋)𝐹) = ((Id‘𝐶)‘𝑋)) | 
| 29 | 21, 27, 28 | 3eqtrd 2781 | . 2
⊢ (𝜑 → ((𝐺(〈𝑍, 𝑌〉 · 𝑋)𝐾)(〈𝑋, 𝑍〉 · 𝑋)(𝐻(〈𝑋, 𝑌〉 · 𝑍)𝐹)) = ((Id‘𝐶)‘𝑋)) | 
| 30 | 1, 2, 3, 4, 6, 7, 5, 19, 20 | catcocl 17728 | . . 3
⊢ (𝜑 → (𝐺(〈𝑍, 𝑌〉 · 𝑋)𝐾) ∈ (𝑍(Hom ‘𝐶)𝑋)) | 
| 31 | 1, 2, 3, 9, 10, 4,
5, 6, 18, 30 | issect2 17798 | . 2
⊢ (𝜑 → ((𝐻(〈𝑋, 𝑌〉 · 𝑍)𝐹)(𝑋𝑆𝑍)(𝐺(〈𝑍, 𝑌〉 · 𝑋)𝐾) ↔ ((𝐺(〈𝑍, 𝑌〉 · 𝑋)𝐾)(〈𝑋, 𝑍〉 · 𝑋)(𝐻(〈𝑋, 𝑌〉 · 𝑍)𝐹)) = ((Id‘𝐶)‘𝑋))) | 
| 32 | 29, 31 | mpbird 257 | 1
⊢ (𝜑 → (𝐻(〈𝑋, 𝑌〉 · 𝑍)𝐹)(𝑋𝑆𝑍)(𝐺(〈𝑍, 𝑌〉 · 𝑋)𝐾)) |