Proof of Theorem ringcsect
Step | Hyp | Ref
| Expression |
1 | | ringcsect.b |
. . 3
⊢ 𝐵 = (Base‘𝐶) |
2 | | eqid 2739 |
. . 3
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
3 | | eqid 2739 |
. . 3
⊢
(comp‘𝐶) =
(comp‘𝐶) |
4 | | eqid 2739 |
. . 3
⊢
(Id‘𝐶) =
(Id‘𝐶) |
5 | | ringcsect.n |
. . 3
⊢ 𝑆 = (Sect‘𝐶) |
6 | | ringcsect.u |
. . . 4
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
7 | | ringcsect.c |
. . . . 5
⊢ 𝐶 = (RingCat‘𝑈) |
8 | 7 | ringccat 45534 |
. . . 4
⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat) |
9 | 6, 8 | syl 17 |
. . 3
⊢ (𝜑 → 𝐶 ∈ Cat) |
10 | | ringcsect.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
11 | | ringcsect.y |
. . 3
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
12 | 1, 2, 3, 4, 5, 9, 10, 11 | issect 17446 |
. 2
⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐺 ∈ (𝑌(Hom ‘𝐶)𝑋) ∧ (𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋)))) |
13 | 7, 1, 6, 2, 10, 11 | ringchom 45523 |
. . . . . . 7
⊢ (𝜑 → (𝑋(Hom ‘𝐶)𝑌) = (𝑋 RingHom 𝑌)) |
14 | 13 | eleq2d 2825 |
. . . . . 6
⊢ (𝜑 → (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ↔ 𝐹 ∈ (𝑋 RingHom 𝑌))) |
15 | 7, 1, 6, 2, 11, 10 | ringchom 45523 |
. . . . . . 7
⊢ (𝜑 → (𝑌(Hom ‘𝐶)𝑋) = (𝑌 RingHom 𝑋)) |
16 | 15 | eleq2d 2825 |
. . . . . 6
⊢ (𝜑 → (𝐺 ∈ (𝑌(Hom ‘𝐶)𝑋) ↔ 𝐺 ∈ (𝑌 RingHom 𝑋))) |
17 | 14, 16 | anbi12d 630 |
. . . . 5
⊢ (𝜑 → ((𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐺 ∈ (𝑌(Hom ‘𝐶)𝑋)) ↔ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)))) |
18 | 17 | anbi1d 629 |
. . . 4
⊢ (𝜑 → (((𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐺 ∈ (𝑌(Hom ‘𝐶)𝑋)) ∧ (𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋)) ↔ ((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋)))) |
19 | 6 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))) → 𝑈 ∈ 𝑉) |
20 | 10 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))) → 𝑋 ∈ 𝐵) |
21 | 7, 1, 6 | ringcbas 45521 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 = (𝑈 ∩ Ring)) |
22 | 21 | eleq2d 2825 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 ∈ 𝐵 ↔ 𝑋 ∈ (𝑈 ∩ Ring))) |
23 | | inss1 4167 |
. . . . . . . . . . . 12
⊢ (𝑈 ∩ Ring) ⊆ 𝑈 |
24 | 23 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑈 ∩ Ring) ⊆ 𝑈) |
25 | 24 | sseld 3924 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 ∈ (𝑈 ∩ Ring) → 𝑋 ∈ 𝑈)) |
26 | 22, 25 | sylbid 239 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 ∈ 𝐵 → 𝑋 ∈ 𝑈)) |
27 | 26 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))) → (𝑋 ∈ 𝐵 → 𝑋 ∈ 𝑈)) |
28 | 20, 27 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))) → 𝑋 ∈ 𝑈) |
29 | 11 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))) → 𝑌 ∈ 𝐵) |
30 | 21 | eleq2d 2825 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑌 ∈ 𝐵 ↔ 𝑌 ∈ (𝑈 ∩ Ring))) |
31 | 24 | sseld 3924 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑌 ∈ (𝑈 ∩ Ring) → 𝑌 ∈ 𝑈)) |
32 | 30, 31 | sylbid 239 |
. . . . . . . . 9
⊢ (𝜑 → (𝑌 ∈ 𝐵 → 𝑌 ∈ 𝑈)) |
33 | 32 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))) → (𝑌 ∈ 𝐵 → 𝑌 ∈ 𝑈)) |
34 | 29, 33 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))) → 𝑌 ∈ 𝑈) |
35 | | eqid 2739 |
. . . . . . . . . 10
⊢
(Base‘𝑋) =
(Base‘𝑋) |
36 | | eqid 2739 |
. . . . . . . . . 10
⊢
(Base‘𝑌) =
(Base‘𝑌) |
37 | 35, 36 | rhmf 19951 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑋 RingHom 𝑌) → 𝐹:(Base‘𝑋)⟶(Base‘𝑌)) |
38 | 37 | adantr 480 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) → 𝐹:(Base‘𝑋)⟶(Base‘𝑌)) |
39 | 38 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))) → 𝐹:(Base‘𝑋)⟶(Base‘𝑌)) |
40 | 36, 35 | rhmf 19951 |
. . . . . . . . 9
⊢ (𝐺 ∈ (𝑌 RingHom 𝑋) → 𝐺:(Base‘𝑌)⟶(Base‘𝑋)) |
41 | 40 | adantl 481 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) → 𝐺:(Base‘𝑌)⟶(Base‘𝑋)) |
42 | 41 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))) → 𝐺:(Base‘𝑌)⟶(Base‘𝑋)) |
43 | 7, 19, 3, 28, 34, 28, 39, 42 | ringcco 45527 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))) → (𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = (𝐺 ∘ 𝐹)) |
44 | | ringcsect.e |
. . . . . . . 8
⊢ 𝐸 = (Base‘𝑋) |
45 | 7, 1, 4, 6, 10, 44 | ringcid 45535 |
. . . . . . 7
⊢ (𝜑 → ((Id‘𝐶)‘𝑋) = ( I ↾ 𝐸)) |
46 | 45 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))) → ((Id‘𝐶)‘𝑋) = ( I ↾ 𝐸)) |
47 | 43, 46 | eqeq12d 2755 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))) → ((𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋) ↔ (𝐺 ∘ 𝐹) = ( I ↾ 𝐸))) |
48 | 47 | pm5.32da 578 |
. . . 4
⊢ (𝜑 → (((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋)) ↔ ((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐸)))) |
49 | 18, 48 | bitrd 278 |
. . 3
⊢ (𝜑 → (((𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐺 ∈ (𝑌(Hom ‘𝐶)𝑋)) ∧ (𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋)) ↔ ((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐸)))) |
50 | | df-3an 1087 |
. . 3
⊢ ((𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐺 ∈ (𝑌(Hom ‘𝐶)𝑋) ∧ (𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋)) ↔ ((𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐺 ∈ (𝑌(Hom ‘𝐶)𝑋)) ∧ (𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋))) |
51 | | df-3an 1087 |
. . 3
⊢ ((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋) ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐸)) ↔ ((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐸))) |
52 | 49, 50, 51 | 3bitr4g 313 |
. 2
⊢ (𝜑 → ((𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐺 ∈ (𝑌(Hom ‘𝐶)𝑋) ∧ (𝐺(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋)) ↔ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋) ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐸)))) |
53 | 12, 52 | bitrd 278 |
1
⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋) ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐸)))) |