Proof of Theorem rngcsect
Step | Hyp | Ref
| Expression |
1 | | rngcsect.b |
. . 3
⊢ 𝐵 = (Base‘𝐶) |
2 | | eqid 2738 |
. . 3
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
3 | | eqid 2738 |
. . 3
⊢
(comp‘𝐶) =
(comp‘𝐶) |
4 | | eqid 2738 |
. . 3
⊢
(Id‘𝐶) =
(Id‘𝐶) |
5 | | rngcsect.n |
. . 3
⊢ 𝑆 = (Sect‘𝐶) |
6 | | rngcsect.u |
. . . 4
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
7 | | rngcsect.c |
. . . . 5
⊢ 𝐶 = (RngCat‘𝑈) |
8 | 7 | rngccat 45536 |
. . . 4
⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat) |
9 | 6, 8 | syl 17 |
. . 3
⊢ (𝜑 → 𝐶 ∈ Cat) |
10 | | rngcsect.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
11 | | rngcsect.y |
. . 3
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
12 | 1, 2, 3, 4, 5, 9, 10, 11 | issect 17465 |
. 2
⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐺 ∈ (𝑌(Hom ‘𝐶)𝑋) ∧ (𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋)))) |
13 | 7, 1, 6, 2, 10, 11 | rngchom 45525 |
. . . . . . 7
⊢ (𝜑 → (𝑋(Hom ‘𝐶)𝑌) = (𝑋 RngHomo 𝑌)) |
14 | 13 | eleq2d 2824 |
. . . . . 6
⊢ (𝜑 → (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ↔ 𝐹 ∈ (𝑋 RngHomo 𝑌))) |
15 | 7, 1, 6, 2, 11, 10 | rngchom 45525 |
. . . . . . 7
⊢ (𝜑 → (𝑌(Hom ‘𝐶)𝑋) = (𝑌 RngHomo 𝑋)) |
16 | 15 | eleq2d 2824 |
. . . . . 6
⊢ (𝜑 → (𝐺 ∈ (𝑌(Hom ‘𝐶)𝑋) ↔ 𝐺 ∈ (𝑌 RngHomo 𝑋))) |
17 | 14, 16 | anbi12d 631 |
. . . . 5
⊢ (𝜑 → ((𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐺 ∈ (𝑌(Hom ‘𝐶)𝑋)) ↔ (𝐹 ∈ (𝑋 RngHomo 𝑌) ∧ 𝐺 ∈ (𝑌 RngHomo 𝑋)))) |
18 | 17 | anbi1d 630 |
. . . 4
⊢ (𝜑 → (((𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐺 ∈ (𝑌(Hom ‘𝐶)𝑋)) ∧ (𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋)) ↔ ((𝐹 ∈ (𝑋 RngHomo 𝑌) ∧ 𝐺 ∈ (𝑌 RngHomo 𝑋)) ∧ (𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋)))) |
19 | 6 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RngHomo 𝑌) ∧ 𝐺 ∈ (𝑌 RngHomo 𝑋))) → 𝑈 ∈ 𝑉) |
20 | 10 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RngHomo 𝑌) ∧ 𝐺 ∈ (𝑌 RngHomo 𝑋))) → 𝑋 ∈ 𝐵) |
21 | 7, 1, 6 | rngcbas 45523 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 = (𝑈 ∩ Rng)) |
22 | 21 | eleq2d 2824 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 ∈ 𝐵 ↔ 𝑋 ∈ (𝑈 ∩ Rng))) |
23 | | inss1 4162 |
. . . . . . . . . . . 12
⊢ (𝑈 ∩ Rng) ⊆ 𝑈 |
24 | 23 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑈 ∩ Rng) ⊆ 𝑈) |
25 | 24 | sseld 3920 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 ∈ (𝑈 ∩ Rng) → 𝑋 ∈ 𝑈)) |
26 | 22, 25 | sylbid 239 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 ∈ 𝐵 → 𝑋 ∈ 𝑈)) |
27 | 26 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RngHomo 𝑌) ∧ 𝐺 ∈ (𝑌 RngHomo 𝑋))) → (𝑋 ∈ 𝐵 → 𝑋 ∈ 𝑈)) |
28 | 20, 27 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RngHomo 𝑌) ∧ 𝐺 ∈ (𝑌 RngHomo 𝑋))) → 𝑋 ∈ 𝑈) |
29 | 11 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RngHomo 𝑌) ∧ 𝐺 ∈ (𝑌 RngHomo 𝑋))) → 𝑌 ∈ 𝐵) |
30 | 21 | eleq2d 2824 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑌 ∈ 𝐵 ↔ 𝑌 ∈ (𝑈 ∩ Rng))) |
31 | 24 | sseld 3920 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑌 ∈ (𝑈 ∩ Rng) → 𝑌 ∈ 𝑈)) |
32 | 30, 31 | sylbid 239 |
. . . . . . . . 9
⊢ (𝜑 → (𝑌 ∈ 𝐵 → 𝑌 ∈ 𝑈)) |
33 | 32 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RngHomo 𝑌) ∧ 𝐺 ∈ (𝑌 RngHomo 𝑋))) → (𝑌 ∈ 𝐵 → 𝑌 ∈ 𝑈)) |
34 | 29, 33 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RngHomo 𝑌) ∧ 𝐺 ∈ (𝑌 RngHomo 𝑋))) → 𝑌 ∈ 𝑈) |
35 | | eqid 2738 |
. . . . . . . . . 10
⊢
(Base‘𝑋) =
(Base‘𝑋) |
36 | | eqid 2738 |
. . . . . . . . . 10
⊢
(Base‘𝑌) =
(Base‘𝑌) |
37 | 35, 36 | rnghmf 45457 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑋 RngHomo 𝑌) → 𝐹:(Base‘𝑋)⟶(Base‘𝑌)) |
38 | 37 | adantr 481 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑋 RngHomo 𝑌) ∧ 𝐺 ∈ (𝑌 RngHomo 𝑋)) → 𝐹:(Base‘𝑋)⟶(Base‘𝑌)) |
39 | 38 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RngHomo 𝑌) ∧ 𝐺 ∈ (𝑌 RngHomo 𝑋))) → 𝐹:(Base‘𝑋)⟶(Base‘𝑌)) |
40 | 36, 35 | rnghmf 45457 |
. . . . . . . . 9
⊢ (𝐺 ∈ (𝑌 RngHomo 𝑋) → 𝐺:(Base‘𝑌)⟶(Base‘𝑋)) |
41 | 40 | adantl 482 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑋 RngHomo 𝑌) ∧ 𝐺 ∈ (𝑌 RngHomo 𝑋)) → 𝐺:(Base‘𝑌)⟶(Base‘𝑋)) |
42 | 41 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RngHomo 𝑌) ∧ 𝐺 ∈ (𝑌 RngHomo 𝑋))) → 𝐺:(Base‘𝑌)⟶(Base‘𝑋)) |
43 | 7, 19, 3, 28, 34, 28, 39, 42 | rngcco 45529 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RngHomo 𝑌) ∧ 𝐺 ∈ (𝑌 RngHomo 𝑋))) → (𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = (𝐺 ∘ 𝐹)) |
44 | | rngcsect.e |
. . . . . . . 8
⊢ 𝐸 = (Base‘𝑋) |
45 | 7, 1, 4, 6, 10, 44 | rngcid 45537 |
. . . . . . 7
⊢ (𝜑 → ((Id‘𝐶)‘𝑋) = ( I ↾ 𝐸)) |
46 | 45 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RngHomo 𝑌) ∧ 𝐺 ∈ (𝑌 RngHomo 𝑋))) → ((Id‘𝐶)‘𝑋) = ( I ↾ 𝐸)) |
47 | 43, 46 | eqeq12d 2754 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RngHomo 𝑌) ∧ 𝐺 ∈ (𝑌 RngHomo 𝑋))) → ((𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋) ↔ (𝐺 ∘ 𝐹) = ( I ↾ 𝐸))) |
48 | 47 | pm5.32da 579 |
. . . 4
⊢ (𝜑 → (((𝐹 ∈ (𝑋 RngHomo 𝑌) ∧ 𝐺 ∈ (𝑌 RngHomo 𝑋)) ∧ (𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋)) ↔ ((𝐹 ∈ (𝑋 RngHomo 𝑌) ∧ 𝐺 ∈ (𝑌 RngHomo 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐸)))) |
49 | 18, 48 | bitrd 278 |
. . 3
⊢ (𝜑 → (((𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐺 ∈ (𝑌(Hom ‘𝐶)𝑋)) ∧ (𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋)) ↔ ((𝐹 ∈ (𝑋 RngHomo 𝑌) ∧ 𝐺 ∈ (𝑌 RngHomo 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐸)))) |
50 | | df-3an 1088 |
. . 3
⊢ ((𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐺 ∈ (𝑌(Hom ‘𝐶)𝑋) ∧ (𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋)) ↔ ((𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐺 ∈ (𝑌(Hom ‘𝐶)𝑋)) ∧ (𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋))) |
51 | | df-3an 1088 |
. . 3
⊢ ((𝐹 ∈ (𝑋 RngHomo 𝑌) ∧ 𝐺 ∈ (𝑌 RngHomo 𝑋) ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐸)) ↔ ((𝐹 ∈ (𝑋 RngHomo 𝑌) ∧ 𝐺 ∈ (𝑌 RngHomo 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐸))) |
52 | 49, 50, 51 | 3bitr4g 314 |
. 2
⊢ (𝜑 → ((𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐺 ∈ (𝑌(Hom ‘𝐶)𝑋) ∧ (𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋)) ↔ (𝐹 ∈ (𝑋 RngHomo 𝑌) ∧ 𝐺 ∈ (𝑌 RngHomo 𝑋) ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐸)))) |
53 | 12, 52 | bitrd 278 |
1
⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ (𝐹 ∈ (𝑋 RngHomo 𝑌) ∧ 𝐺 ∈ (𝑌 RngHomo 𝑋) ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐸)))) |