| Step | Hyp | Ref
| Expression |
| 1 | | zrtermoringc.c |
. . . . . . . . . 10
⊢ 𝐶 = (RingCat‘𝑈) |
| 2 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘𝐶) =
(Base‘𝐶) |
| 3 | | zrtermoringc.u |
. . . . . . . . . 10
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
| 4 | 1, 2, 3 | ringcbas 20650 |
. . . . . . . . 9
⊢ (𝜑 → (Base‘𝐶) = (𝑈 ∩ Ring)) |
| 5 | 4 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝜑 → (𝑟 ∈ (Base‘𝐶) ↔ 𝑟 ∈ (𝑈 ∩ Ring))) |
| 6 | | elin 3967 |
. . . . . . . . 9
⊢ (𝑟 ∈ (𝑈 ∩ Ring) ↔ (𝑟 ∈ 𝑈 ∧ 𝑟 ∈ Ring)) |
| 7 | 6 | simprbi 496 |
. . . . . . . 8
⊢ (𝑟 ∈ (𝑈 ∩ Ring) → 𝑟 ∈ Ring) |
| 8 | 5, 7 | biimtrdi 253 |
. . . . . . 7
⊢ (𝜑 → (𝑟 ∈ (Base‘𝐶) → 𝑟 ∈ Ring)) |
| 9 | 8 | imp 406 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → 𝑟 ∈ Ring) |
| 10 | | zrtermoringc.z |
. . . . . . 7
⊢ (𝜑 → 𝑍 ∈ (Ring ∖
NzRing)) |
| 11 | 10 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → 𝑍 ∈ (Ring ∖
NzRing)) |
| 12 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘𝑟) =
(Base‘𝑟) |
| 13 | | eqid 2737 |
. . . . . . 7
⊢
(0g‘𝑍) = (0g‘𝑍) |
| 14 | | eqid 2737 |
. . . . . . 7
⊢ (𝑥 ∈ (Base‘𝑟) ↦
(0g‘𝑍)) =
(𝑥 ∈ (Base‘𝑟) ↦
(0g‘𝑍)) |
| 15 | 12, 13, 14 | c0rhm 20534 |
. . . . . 6
⊢ ((𝑟 ∈ Ring ∧ 𝑍 ∈ (Ring ∖ NzRing))
→ (𝑥 ∈
(Base‘𝑟) ↦
(0g‘𝑍))
∈ (𝑟 RingHom 𝑍)) |
| 16 | 9, 11, 15 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)) ∈ (𝑟 RingHom 𝑍)) |
| 17 | | simpr 484 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)) ∈ (𝑟 RingHom 𝑍)) → (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)) ∈ (𝑟 RingHom 𝑍)) |
| 18 | 3 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → 𝑈 ∈ 𝑉) |
| 19 | | eqid 2737 |
. . . . . . . . . 10
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
| 20 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → 𝑟 ∈ (Base‘𝐶)) |
| 21 | | zrtermoringc.e |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑍 ∈ 𝑈) |
| 22 | 10 | eldifad 3963 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑍 ∈ Ring) |
| 23 | 21, 22 | elind 4200 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑍 ∈ (𝑈 ∩ Ring)) |
| 24 | 23, 4 | eleqtrrd 2844 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑍 ∈ (Base‘𝐶)) |
| 25 | 24 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → 𝑍 ∈ (Base‘𝐶)) |
| 26 | 1, 2, 18, 19, 20, 25 | ringchom 20652 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → (𝑟(Hom ‘𝐶)𝑍) = (𝑟 RingHom 𝑍)) |
| 27 | 26 | eqcomd 2743 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → (𝑟 RingHom 𝑍) = (𝑟(Hom ‘𝐶)𝑍)) |
| 28 | 27 | eleq2d 2827 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → ((𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)) ∈ (𝑟 RingHom 𝑍) ↔ (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)) ∈ (𝑟(Hom ‘𝐶)𝑍))) |
| 29 | 28 | biimpa 476 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)) ∈ (𝑟 RingHom 𝑍)) → (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)) ∈ (𝑟(Hom ‘𝐶)𝑍)) |
| 30 | 26 | eleq2d 2827 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → (ℎ ∈ (𝑟(Hom ‘𝐶)𝑍) ↔ ℎ ∈ (𝑟 RingHom 𝑍))) |
| 31 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘𝑍) =
(Base‘𝑍) |
| 32 | 12, 31 | rhmf 20485 |
. . . . . . . . . 10
⊢ (ℎ ∈ (𝑟 RingHom 𝑍) → ℎ:(Base‘𝑟)⟶(Base‘𝑍)) |
| 33 | 30, 32 | biimtrdi 253 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → (ℎ ∈ (𝑟(Hom ‘𝐶)𝑍) → ℎ:(Base‘𝑟)⟶(Base‘𝑍))) |
| 34 | 33 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)) ∈ (𝑟 RingHom 𝑍)) → (ℎ ∈ (𝑟(Hom ‘𝐶)𝑍) → ℎ:(Base‘𝑟)⟶(Base‘𝑍))) |
| 35 | | ffn 6736 |
. . . . . . . . . . 11
⊢ (ℎ:(Base‘𝑟)⟶(Base‘𝑍) → ℎ Fn (Base‘𝑟)) |
| 36 | 35 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)) ∈ (𝑟 RingHom 𝑍)) ∧ ℎ:(Base‘𝑟)⟶(Base‘𝑍)) → ℎ Fn (Base‘𝑟)) |
| 37 | | fvex 6919 |
. . . . . . . . . . . 12
⊢
(0g‘𝑍) ∈ V |
| 38 | 37, 14 | fnmpti 6711 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (Base‘𝑟) ↦
(0g‘𝑍)) Fn
(Base‘𝑟) |
| 39 | 38 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)) ∈ (𝑟 RingHom 𝑍)) ∧ ℎ:(Base‘𝑟)⟶(Base‘𝑍)) → (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)) Fn (Base‘𝑟)) |
| 40 | 31, 13 | 0ringbas 20528 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑍 ∈ (Ring ∖ NzRing)
→ (Base‘𝑍) =
{(0g‘𝑍)}) |
| 41 | 10, 40 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (Base‘𝑍) = {(0g‘𝑍)}) |
| 42 | 41 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → (Base‘𝑍) = {(0g‘𝑍)}) |
| 43 | 42 | feq3d 6723 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → (ℎ:(Base‘𝑟)⟶(Base‘𝑍) ↔ ℎ:(Base‘𝑟)⟶{(0g‘𝑍)})) |
| 44 | | fvconst 7184 |
. . . . . . . . . . . . . . 15
⊢ ((ℎ:(Base‘𝑟)⟶{(0g‘𝑍)} ∧ 𝑎 ∈ (Base‘𝑟)) → (ℎ‘𝑎) = (0g‘𝑍)) |
| 45 | 44 | ex 412 |
. . . . . . . . . . . . . 14
⊢ (ℎ:(Base‘𝑟)⟶{(0g‘𝑍)} → (𝑎 ∈ (Base‘𝑟) → (ℎ‘𝑎) = (0g‘𝑍))) |
| 46 | 43, 45 | biimtrdi 253 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → (ℎ:(Base‘𝑟)⟶(Base‘𝑍) → (𝑎 ∈ (Base‘𝑟) → (ℎ‘𝑎) = (0g‘𝑍)))) |
| 47 | 46 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)) ∈ (𝑟 RingHom 𝑍)) → (ℎ:(Base‘𝑟)⟶(Base‘𝑍) → (𝑎 ∈ (Base‘𝑟) → (ℎ‘𝑎) = (0g‘𝑍)))) |
| 48 | 47 | imp31 417 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)) ∈ (𝑟 RingHom 𝑍)) ∧ ℎ:(Base‘𝑟)⟶(Base‘𝑍)) ∧ 𝑎 ∈ (Base‘𝑟)) → (ℎ‘𝑎) = (0g‘𝑍)) |
| 49 | | eqidd 2738 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ (Base‘𝑟) → (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)) = (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍))) |
| 50 | | eqidd 2738 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ (Base‘𝑟) ∧ 𝑥 = 𝑎) → (0g‘𝑍) = (0g‘𝑍)) |
| 51 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ (Base‘𝑟) → 𝑎 ∈ (Base‘𝑟)) |
| 52 | 37 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ (Base‘𝑟) →
(0g‘𝑍)
∈ V) |
| 53 | 49, 50, 51, 52 | fvmptd 7023 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (Base‘𝑟) → ((𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍))‘𝑎) = (0g‘𝑍)) |
| 54 | 53 | adantl 481 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)) ∈ (𝑟 RingHom 𝑍)) ∧ ℎ:(Base‘𝑟)⟶(Base‘𝑍)) ∧ 𝑎 ∈ (Base‘𝑟)) → ((𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍))‘𝑎) = (0g‘𝑍)) |
| 55 | 48, 54 | eqtr4d 2780 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)) ∈ (𝑟 RingHom 𝑍)) ∧ ℎ:(Base‘𝑟)⟶(Base‘𝑍)) ∧ 𝑎 ∈ (Base‘𝑟)) → (ℎ‘𝑎) = ((𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍))‘𝑎)) |
| 56 | 36, 39, 55 | eqfnfvd 7054 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)) ∈ (𝑟 RingHom 𝑍)) ∧ ℎ:(Base‘𝑟)⟶(Base‘𝑍)) → ℎ = (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍))) |
| 57 | 56 | ex 412 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)) ∈ (𝑟 RingHom 𝑍)) → (ℎ:(Base‘𝑟)⟶(Base‘𝑍) → ℎ = (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)))) |
| 58 | 34, 57 | syld 47 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)) ∈ (𝑟 RingHom 𝑍)) → (ℎ ∈ (𝑟(Hom ‘𝐶)𝑍) → ℎ = (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)))) |
| 59 | 58 | alrimiv 1927 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)) ∈ (𝑟 RingHom 𝑍)) → ∀ℎ(ℎ ∈ (𝑟(Hom ‘𝐶)𝑍) → ℎ = (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)))) |
| 60 | 17, 29, 59 | 3jca 1129 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)) ∈ (𝑟 RingHom 𝑍)) → ((𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)) ∈ (𝑟 RingHom 𝑍) ∧ (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)) ∈ (𝑟(Hom ‘𝐶)𝑍) ∧ ∀ℎ(ℎ ∈ (𝑟(Hom ‘𝐶)𝑍) → ℎ = (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍))))) |
| 61 | 16, 60 | mpdan 687 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → ((𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)) ∈ (𝑟 RingHom 𝑍) ∧ (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)) ∈ (𝑟(Hom ‘𝐶)𝑍) ∧ ∀ℎ(ℎ ∈ (𝑟(Hom ‘𝐶)𝑍) → ℎ = (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍))))) |
| 62 | | eleq1 2829 |
. . . . 5
⊢ (ℎ = (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)) → (ℎ ∈ (𝑟(Hom ‘𝐶)𝑍) ↔ (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)) ∈ (𝑟(Hom ‘𝐶)𝑍))) |
| 63 | 62 | eqeu 3712 |
. . . 4
⊢ (((𝑥 ∈ (Base‘𝑟) ↦
(0g‘𝑍))
∈ (𝑟 RingHom 𝑍) ∧ (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)) ∈ (𝑟(Hom ‘𝐶)𝑍) ∧ ∀ℎ(ℎ ∈ (𝑟(Hom ‘𝐶)𝑍) → ℎ = (𝑥 ∈ (Base‘𝑟) ↦ (0g‘𝑍)))) → ∃!ℎ ℎ ∈ (𝑟(Hom ‘𝐶)𝑍)) |
| 64 | 61, 63 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → ∃!ℎ ℎ ∈ (𝑟(Hom ‘𝐶)𝑍)) |
| 65 | 64 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑟 ∈ (Base‘𝐶)∃!ℎ ℎ ∈ (𝑟(Hom ‘𝐶)𝑍)) |
| 66 | 1 | ringccat 20663 |
. . . 4
⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat) |
| 67 | 3, 66 | syl 17 |
. . 3
⊢ (𝜑 → 𝐶 ∈ Cat) |
| 68 | 2, 19, 67, 24 | istermo 18042 |
. 2
⊢ (𝜑 → (𝑍 ∈ (TermO‘𝐶) ↔ ∀𝑟 ∈ (Base‘𝐶)∃!ℎ ℎ ∈ (𝑟(Hom ‘𝐶)𝑍))) |
| 69 | 65, 68 | mpbird 257 |
1
⊢ (𝜑 → 𝑍 ∈ (TermO‘𝐶)) |