| Step | Hyp | Ref
| Expression |
| 1 | | ax-1 6 |
. 2
⊢
((ZeroO‘𝐶) =
∅ → (𝜑 →
(ZeroO‘𝐶) =
∅)) |
| 2 | | neq0 4352 |
. . 3
⊢ (¬
(ZeroO‘𝐶) = ∅
↔ ∃ℎ ℎ ∈ (ZeroO‘𝐶)) |
| 3 | | nzerooringczr.u |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
| 4 | | nzerooringczr.c |
. . . . . . . . 9
⊢ 𝐶 = (RingCat‘𝑈) |
| 5 | 4 | ringccat 20663 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat) |
| 6 | 3, 5 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ Cat) |
| 7 | | iszeroi 18054 |
. . . . . . 7
⊢ ((𝐶 ∈ Cat ∧ ℎ ∈ (ZeroO‘𝐶)) → (ℎ ∈ (Base‘𝐶) ∧ (ℎ ∈ (InitO‘𝐶) ∧ ℎ ∈ (TermO‘𝐶)))) |
| 8 | 6, 7 | sylan 580 |
. . . . . 6
⊢ ((𝜑 ∧ ℎ ∈ (ZeroO‘𝐶)) → (ℎ ∈ (Base‘𝐶) ∧ (ℎ ∈ (InitO‘𝐶) ∧ ℎ ∈ (TermO‘𝐶)))) |
| 9 | | nzerooringczr.z |
. . . . . . . . 9
⊢ (𝜑 → 𝑍 ∈ (Ring ∖
NzRing)) |
| 10 | | nzerooringczr.e |
. . . . . . . . 9
⊢ (𝜑 → 𝑍 ∈ 𝑈) |
| 11 | 3, 4, 9, 10 | zrtermoringc 20675 |
. . . . . . . 8
⊢ (𝜑 → 𝑍 ∈ (TermO‘𝐶)) |
| 12 | | nzerooringczr.i |
. . . . . . . . . 10
⊢ (𝜑 → ℤring
∈ 𝑈) |
| 13 | 3, 12, 4 | irinitoringc 21490 |
. . . . . . . . 9
⊢ (𝜑 → ℤring
∈ (InitO‘𝐶)) |
| 14 | 6 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ ℎ ∈ (InitO‘𝐶)) ∧ ℤring ∈
(InitO‘𝐶)) →
𝐶 ∈
Cat) |
| 15 | | simplr 769 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ ℎ ∈ (InitO‘𝐶)) ∧ ℤring ∈
(InitO‘𝐶)) →
ℎ ∈ (InitO‘𝐶)) |
| 16 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ ℎ ∈ (InitO‘𝐶)) ∧ ℤring ∈
(InitO‘𝐶)) →
ℤring ∈ (InitO‘𝐶)) |
| 17 | 14, 15, 16 | initoeu1w 18057 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ ℎ ∈ (InitO‘𝐶)) ∧ ℤring ∈
(InitO‘𝐶)) →
ℎ(
≃𝑐 ‘𝐶)ℤring) |
| 18 | 6 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ℎ ∈ (TermO‘𝐶)) ∧ 𝑍 ∈ (TermO‘𝐶)) → 𝐶 ∈ Cat) |
| 19 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ℎ ∈ (TermO‘𝐶)) ∧ 𝑍 ∈ (TermO‘𝐶)) → 𝑍 ∈ (TermO‘𝐶)) |
| 20 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ℎ ∈ (TermO‘𝐶)) ∧ 𝑍 ∈ (TermO‘𝐶)) → ℎ ∈ (TermO‘𝐶)) |
| 21 | 18, 19, 20 | termoeu1w 18064 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ ℎ ∈ (TermO‘𝐶)) ∧ 𝑍 ∈ (TermO‘𝐶)) → 𝑍( ≃𝑐 ‘𝐶)ℎ) |
| 22 | | cictr 17849 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐶 ∈ Cat ∧ 𝑍( ≃𝑐
‘𝐶)ℎ ∧ ℎ( ≃𝑐 ‘𝐶)ℤring) →
𝑍(
≃𝑐 ‘𝐶)ℤring) |
| 23 | 6, 22 | syl3an1 1164 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑍( ≃𝑐 ‘𝐶)ℎ ∧ ℎ( ≃𝑐 ‘𝐶)ℤring) →
𝑍(
≃𝑐 ‘𝐶)ℤring) |
| 24 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(Iso‘𝐶) =
(Iso‘𝐶) |
| 25 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(Base‘𝐶) =
(Base‘𝐶) |
| 26 | 9 | eldifad 3963 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → 𝑍 ∈ Ring) |
| 27 | 10, 26 | elind 4200 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝑍 ∈ (𝑈 ∩ Ring)) |
| 28 | 4, 25, 3 | ringcbas 20650 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → (Base‘𝐶) = (𝑈 ∩ Ring)) |
| 29 | 27, 28 | eleqtrrd 2844 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝑍 ∈ (Base‘𝐶)) |
| 30 | | zringring 21460 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
ℤring ∈ Ring |
| 31 | 30 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → ℤring
∈ Ring) |
| 32 | 12, 31 | elind 4200 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → ℤring
∈ (𝑈 ∩
Ring)) |
| 33 | 32, 28 | eleqtrrd 2844 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → ℤring
∈ (Base‘𝐶)) |
| 34 | 24, 25, 6, 29, 33 | cic 17843 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝑍( ≃𝑐 ‘𝐶)ℤring ↔
∃𝑓 𝑓 ∈ (𝑍(Iso‘𝐶)ℤring))) |
| 35 | | n0 4353 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑍(Iso‘𝐶)ℤring) ≠ ∅ ↔
∃𝑓 𝑓 ∈ (𝑍(Iso‘𝐶)ℤring)) |
| 36 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
| 37 | 25, 36, 24, 6, 29, 33 | isohom 17820 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → (𝑍(Iso‘𝐶)ℤring) ⊆ (𝑍(Hom ‘𝐶)ℤring)) |
| 38 | | ssn0 4404 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑍(Iso‘𝐶)ℤring) ⊆ (𝑍(Hom ‘𝐶)ℤring) ∧ (𝑍(Iso‘𝐶)ℤring) ≠ ∅)
→ (𝑍(Hom ‘𝐶)ℤring) ≠
∅) |
| 39 | 4, 25, 3, 36, 29, 33 | ringchom 20652 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → (𝑍(Hom ‘𝐶)ℤring) = (𝑍 RingHom
ℤring)) |
| 40 | 39 | neeq1d 3000 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → ((𝑍(Hom ‘𝐶)ℤring) ≠ ∅ ↔
(𝑍 RingHom
ℤring) ≠ ∅)) |
| 41 | | zringnzr 21471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
ℤring ∈ NzRing |
| 42 | | nrhmzr 20537 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑍 ∈ (Ring ∖ NzRing)
∧ ℤring ∈ NzRing) → (𝑍 RingHom ℤring) =
∅) |
| 43 | 9, 41, 42 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → (𝑍 RingHom ℤring) =
∅) |
| 44 | | eqneqall 2951 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑍 RingHom ℤring)
= ∅ → ((𝑍
RingHom ℤring) ≠ ∅ → (ZeroO‘𝐶) = ∅)) |
| 45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → ((𝑍 RingHom ℤring) ≠
∅ → (ZeroO‘𝐶) = ∅)) |
| 46 | 40, 45 | sylbid 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → ((𝑍(Hom ‘𝐶)ℤring) ≠ ∅ →
(ZeroO‘𝐶) =
∅)) |
| 47 | 38, 46 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑍(Iso‘𝐶)ℤring) ⊆ (𝑍(Hom ‘𝐶)ℤring) ∧ (𝑍(Iso‘𝐶)ℤring) ≠ ∅)
→ (𝜑 →
(ZeroO‘𝐶) =
∅)) |
| 48 | 47 | expcom 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑍(Iso‘𝐶)ℤring) ≠ ∅ →
((𝑍(Iso‘𝐶)ℤring) ⊆
(𝑍(Hom ‘𝐶)ℤring) →
(𝜑 → (ZeroO‘𝐶) = ∅))) |
| 49 | 48 | com13 88 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → ((𝑍(Iso‘𝐶)ℤring) ⊆ (𝑍(Hom ‘𝐶)ℤring) → ((𝑍(Iso‘𝐶)ℤring) ≠ ∅ →
(ZeroO‘𝐶) =
∅))) |
| 50 | 37, 49 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → ((𝑍(Iso‘𝐶)ℤring) ≠ ∅ →
(ZeroO‘𝐶) =
∅)) |
| 51 | 35, 50 | biimtrrid 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (∃𝑓 𝑓 ∈ (𝑍(Iso‘𝐶)ℤring) →
(ZeroO‘𝐶) =
∅)) |
| 52 | 34, 51 | sylbid 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝑍( ≃𝑐 ‘𝐶)ℤring →
(ZeroO‘𝐶) =
∅)) |
| 53 | 52 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑍( ≃𝑐 ‘𝐶)ℎ ∧ ℎ( ≃𝑐 ‘𝐶)ℤring) →
(𝑍(
≃𝑐 ‘𝐶)ℤring →
(ZeroO‘𝐶) =
∅)) |
| 54 | 23, 53 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑍( ≃𝑐 ‘𝐶)ℎ ∧ ℎ( ≃𝑐 ‘𝐶)ℤring) →
(ZeroO‘𝐶) =
∅) |
| 55 | 54 | 3exp 1120 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑍( ≃𝑐 ‘𝐶)ℎ → (ℎ( ≃𝑐 ‘𝐶)ℤring →
(ZeroO‘𝐶) =
∅))) |
| 56 | 55 | a1dd 50 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑍( ≃𝑐 ‘𝐶)ℎ → (ℎ ∈ (Base‘𝐶) → (ℎ( ≃𝑐 ‘𝐶)ℤring →
(ZeroO‘𝐶) =
∅)))) |
| 57 | 56 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ ℎ ∈ (TermO‘𝐶)) ∧ 𝑍 ∈ (TermO‘𝐶)) → (𝑍( ≃𝑐 ‘𝐶)ℎ → (ℎ ∈ (Base‘𝐶) → (ℎ( ≃𝑐 ‘𝐶)ℤring →
(ZeroO‘𝐶) =
∅)))) |
| 58 | 21, 57 | mpd 15 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ℎ ∈ (TermO‘𝐶)) ∧ 𝑍 ∈ (TermO‘𝐶)) → (ℎ ∈ (Base‘𝐶) → (ℎ( ≃𝑐 ‘𝐶)ℤring →
(ZeroO‘𝐶) =
∅))) |
| 59 | 58 | exp31 419 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (ℎ ∈ (TermO‘𝐶) → (𝑍 ∈ (TermO‘𝐶) → (ℎ ∈ (Base‘𝐶) → (ℎ( ≃𝑐 ‘𝐶)ℤring →
(ZeroO‘𝐶) =
∅))))) |
| 60 | 59 | com34 91 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (ℎ ∈ (TermO‘𝐶) → (ℎ ∈ (Base‘𝐶) → (𝑍 ∈ (TermO‘𝐶) → (ℎ( ≃𝑐 ‘𝐶)ℤring →
(ZeroO‘𝐶) =
∅))))) |
| 61 | 60 | com25 99 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (ℎ( ≃𝑐 ‘𝐶)ℤring →
(ℎ ∈ (Base‘𝐶) → (𝑍 ∈ (TermO‘𝐶) → (ℎ ∈ (TermO‘𝐶) → (ZeroO‘𝐶) = ∅))))) |
| 62 | 61 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ ℎ ∈ (InitO‘𝐶)) ∧ ℤring ∈
(InitO‘𝐶)) →
(ℎ(
≃𝑐 ‘𝐶)ℤring → (ℎ ∈ (Base‘𝐶) → (𝑍 ∈ (TermO‘𝐶) → (ℎ ∈ (TermO‘𝐶) → (ZeroO‘𝐶) = ∅))))) |
| 63 | 17, 62 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ℎ ∈ (InitO‘𝐶)) ∧ ℤring ∈
(InitO‘𝐶)) →
(ℎ ∈ (Base‘𝐶) → (𝑍 ∈ (TermO‘𝐶) → (ℎ ∈ (TermO‘𝐶) → (ZeroO‘𝐶) = ∅)))) |
| 64 | 63 | ex 412 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ℎ ∈ (InitO‘𝐶)) → (ℤring ∈
(InitO‘𝐶) →
(ℎ ∈ (Base‘𝐶) → (𝑍 ∈ (TermO‘𝐶) → (ℎ ∈ (TermO‘𝐶) → (ZeroO‘𝐶) = ∅))))) |
| 65 | 64 | com25 99 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ℎ ∈ (InitO‘𝐶)) → (ℎ ∈ (TermO‘𝐶) → (ℎ ∈ (Base‘𝐶) → (𝑍 ∈ (TermO‘𝐶) → (ℤring ∈
(InitO‘𝐶) →
(ZeroO‘𝐶) =
∅))))) |
| 66 | 65 | expimpd 453 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((ℎ ∈ (InitO‘𝐶) ∧ ℎ ∈ (TermO‘𝐶)) → (ℎ ∈ (Base‘𝐶) → (𝑍 ∈ (TermO‘𝐶) → (ℤring ∈
(InitO‘𝐶) →
(ZeroO‘𝐶) =
∅))))) |
| 67 | 66 | com23 86 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℎ ∈ (Base‘𝐶) → ((ℎ ∈ (InitO‘𝐶) ∧ ℎ ∈ (TermO‘𝐶)) → (𝑍 ∈ (TermO‘𝐶) → (ℤring ∈
(InitO‘𝐶) →
(ZeroO‘𝐶) =
∅))))) |
| 68 | 67 | impd 410 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℎ ∈ (Base‘𝐶) ∧ (ℎ ∈ (InitO‘𝐶) ∧ ℎ ∈ (TermO‘𝐶))) → (𝑍 ∈ (TermO‘𝐶) → (ℤring ∈
(InitO‘𝐶) →
(ZeroO‘𝐶) =
∅)))) |
| 69 | 68 | com24 95 |
. . . . . . . . 9
⊢ (𝜑 → (ℤring
∈ (InitO‘𝐶)
→ (𝑍 ∈
(TermO‘𝐶) →
((ℎ ∈ (Base‘𝐶) ∧ (ℎ ∈ (InitO‘𝐶) ∧ ℎ ∈ (TermO‘𝐶))) → (ZeroO‘𝐶) = ∅)))) |
| 70 | 13, 69 | mpd 15 |
. . . . . . . 8
⊢ (𝜑 → (𝑍 ∈ (TermO‘𝐶) → ((ℎ ∈ (Base‘𝐶) ∧ (ℎ ∈ (InitO‘𝐶) ∧ ℎ ∈ (TermO‘𝐶))) → (ZeroO‘𝐶) = ∅))) |
| 71 | 11, 70 | mpd 15 |
. . . . . . 7
⊢ (𝜑 → ((ℎ ∈ (Base‘𝐶) ∧ (ℎ ∈ (InitO‘𝐶) ∧ ℎ ∈ (TermO‘𝐶))) → (ZeroO‘𝐶) = ∅)) |
| 72 | 71 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ℎ ∈ (ZeroO‘𝐶)) → ((ℎ ∈ (Base‘𝐶) ∧ (ℎ ∈ (InitO‘𝐶) ∧ ℎ ∈ (TermO‘𝐶))) → (ZeroO‘𝐶) = ∅)) |
| 73 | 8, 72 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ ℎ ∈ (ZeroO‘𝐶)) → (ZeroO‘𝐶) = ∅) |
| 74 | 73 | expcom 413 |
. . . 4
⊢ (ℎ ∈ (ZeroO‘𝐶) → (𝜑 → (ZeroO‘𝐶) = ∅)) |
| 75 | 74 | exlimiv 1930 |
. . 3
⊢
(∃ℎ ℎ ∈ (ZeroO‘𝐶) → (𝜑 → (ZeroO‘𝐶) = ∅)) |
| 76 | 2, 75 | sylbi 217 |
. 2
⊢ (¬
(ZeroO‘𝐶) = ∅
→ (𝜑 →
(ZeroO‘𝐶) =
∅)) |
| 77 | 1, 76 | pm2.61i 182 |
1
⊢ (𝜑 → (ZeroO‘𝐶) = ∅) |