| Step | Hyp | Ref
| Expression |
| 1 | | zrinitorngc.c |
. . . . . . . . . 10
⊢ 𝐶 = (RngCat‘𝑈) |
| 2 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘𝐶) =
(Base‘𝐶) |
| 3 | | zrinitorngc.u |
. . . . . . . . . 10
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
| 4 | 1, 2, 3 | rngcbas 20621 |
. . . . . . . . 9
⊢ (𝜑 → (Base‘𝐶) = (𝑈 ∩ Rng)) |
| 5 | 4 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝜑 → (𝑟 ∈ (Base‘𝐶) ↔ 𝑟 ∈ (𝑈 ∩ Rng))) |
| 6 | | elin 3967 |
. . . . . . . . 9
⊢ (𝑟 ∈ (𝑈 ∩ Rng) ↔ (𝑟 ∈ 𝑈 ∧ 𝑟 ∈ Rng)) |
| 7 | 6 | simprbi 496 |
. . . . . . . 8
⊢ (𝑟 ∈ (𝑈 ∩ Rng) → 𝑟 ∈ Rng) |
| 8 | 5, 7 | biimtrdi 253 |
. . . . . . 7
⊢ (𝜑 → (𝑟 ∈ (Base‘𝐶) → 𝑟 ∈ Rng)) |
| 9 | 8 | imp 406 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → 𝑟 ∈ Rng) |
| 10 | | zrinitorngc.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 | zrrnghm 20536 |
. . . . . 6
⊢ ((𝑟 ∈ Rng ∧ 𝑍 ∈ (Ring ∖ NzRing))
→ (𝑥 ∈
(Base‘𝑍) ↦
(0g‘𝑟))
∈ (𝑍 RngHom 𝑟)) |
| 16 | 9, 11, 15 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍 RngHom 𝑟)) |
| 17 | | simpr 484 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍 RngHom 𝑟)) → (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍 RngHom 𝑟)) |
| 18 | 3 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → 𝑈 ∈ 𝑉) |
| 19 | | eqid 2737 |
. . . . . . . . . 10
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
| 20 | | zrinitorngc.e |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑍 ∈ 𝑈) |
| 21 | | eldifi 4131 |
. . . . . . . . . . . . . 14
⊢ (𝑍 ∈ (Ring ∖ NzRing)
→ 𝑍 ∈
Ring) |
| 22 | | ringrng 20282 |
. . . . . . . . . . . . . 14
⊢ (𝑍 ∈ Ring → 𝑍 ∈ Rng) |
| 23 | 10, 21, 22 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑍 ∈ Rng) |
| 24 | 20, 23 | elind 4200 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑍 ∈ (𝑈 ∩ Rng)) |
| 25 | 24, 4 | eleqtrrd 2844 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑍 ∈ (Base‘𝐶)) |
| 26 | 25 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → 𝑍 ∈ (Base‘𝐶)) |
| 27 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → 𝑟 ∈ (Base‘𝐶)) |
| 28 | 1, 2, 18, 19, 26, 27 | rngchom 20623 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → (𝑍(Hom ‘𝐶)𝑟) = (𝑍 RngHom 𝑟)) |
| 29 | 28 | eqcomd 2743 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → (𝑍 RngHom 𝑟) = (𝑍(Hom ‘𝐶)𝑟)) |
| 30 | 29 | eleq2d 2827 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → ((𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍 RngHom 𝑟) ↔ (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍(Hom ‘𝐶)𝑟))) |
| 31 | 30 | biimpa 476 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍 RngHom 𝑟)) → (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍(Hom ‘𝐶)𝑟)) |
| 32 | 28 | eleq2d 2827 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → (ℎ ∈ (𝑍(Hom ‘𝐶)𝑟) ↔ ℎ ∈ (𝑍 RngHom 𝑟))) |
| 33 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑟) =
(Base‘𝑟) |
| 34 | 12, 33 | rnghmf 20448 |
. . . . . . . . . . . 12
⊢ (ℎ ∈ (𝑍 RngHom 𝑟) → ℎ:(Base‘𝑍)⟶(Base‘𝑟)) |
| 35 | 32, 34 | biimtrdi 253 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → (ℎ ∈ (𝑍(Hom ‘𝐶)𝑟) → ℎ:(Base‘𝑍)⟶(Base‘𝑟))) |
| 36 | 35 | imp 406 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) → ℎ:(Base‘𝑍)⟶(Base‘𝑟)) |
| 37 | | ffn 6736 |
. . . . . . . . . . . 12
⊢ (ℎ:(Base‘𝑍)⟶(Base‘𝑟) → ℎ Fn (Base‘𝑍)) |
| 38 | 37 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) ∧ ℎ:(Base‘𝑍)⟶(Base‘𝑟)) → ℎ Fn (Base‘𝑍)) |
| 39 | | fvex 6919 |
. . . . . . . . . . . . 13
⊢
(0g‘𝑟) ∈ V |
| 40 | 39, 14 | fnmpti 6711 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (Base‘𝑍) ↦
(0g‘𝑟)) Fn
(Base‘𝑍) |
| 41 | 40 | a1i 11 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) ∧ ℎ:(Base‘𝑍)⟶(Base‘𝑟)) → (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) Fn (Base‘𝑍)) |
| 42 | 32 | biimpa 476 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) → ℎ ∈ (𝑍 RngHom 𝑟)) |
| 43 | | rnghmghm 20447 |
. . . . . . . . . . . . . 14
⊢ (ℎ ∈ (𝑍 RngHom 𝑟) → ℎ ∈ (𝑍 GrpHom 𝑟)) |
| 44 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(0g‘𝑍) = (0g‘𝑍) |
| 45 | 44, 13 | ghmid 19240 |
. . . . . . . . . . . . . 14
⊢ (ℎ ∈ (𝑍 GrpHom 𝑟) → (ℎ‘(0g‘𝑍)) = (0g‘𝑟)) |
| 46 | 42, 43, 45 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) → (ℎ‘(0g‘𝑍)) = (0g‘𝑟)) |
| 47 | 46 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) ∧ ℎ:(Base‘𝑍)⟶(Base‘𝑟)) ∧ 𝑎 ∈ (Base‘𝑍)) → (ℎ‘(0g‘𝑍)) = (0g‘𝑟)) |
| 48 | 12, 44 | 0ringbas 20528 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑍 ∈ (Ring ∖ NzRing)
→ (Base‘𝑍) =
{(0g‘𝑍)}) |
| 49 | 10, 48 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (Base‘𝑍) = {(0g‘𝑍)}) |
| 50 | 49 | eleq2d 2827 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑎 ∈ (Base‘𝑍) ↔ 𝑎 ∈ {(0g‘𝑍)})) |
| 51 | | elsni 4643 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈
{(0g‘𝑍)}
→ 𝑎 =
(0g‘𝑍)) |
| 52 | 51 | fveq2d 6910 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈
{(0g‘𝑍)}
→ (ℎ‘𝑎) = (ℎ‘(0g‘𝑍))) |
| 53 | 50, 52 | biimtrdi 253 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑎 ∈ (Base‘𝑍) → (ℎ‘𝑎) = (ℎ‘(0g‘𝑍)))) |
| 54 | 53 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → (𝑎 ∈ (Base‘𝑍) → (ℎ‘𝑎) = (ℎ‘(0g‘𝑍)))) |
| 55 | 54 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) ∧ ℎ:(Base‘𝑍)⟶(Base‘𝑟)) → (𝑎 ∈ (Base‘𝑍) → (ℎ‘𝑎) = (ℎ‘(0g‘𝑍)))) |
| 56 | 55 | imp 406 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) ∧ ℎ:(Base‘𝑍)⟶(Base‘𝑟)) ∧ 𝑎 ∈ (Base‘𝑍)) → (ℎ‘𝑎) = (ℎ‘(0g‘𝑍))) |
| 57 | | eqidd 2738 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ (Base‘𝑍) → (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) = (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟))) |
| 58 | | eqidd 2738 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ (Base‘𝑍) ∧ 𝑥 = 𝑎) → (0g‘𝑟) = (0g‘𝑟)) |
| 59 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ (Base‘𝑍) → 𝑎 ∈ (Base‘𝑍)) |
| 60 | 39 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ (Base‘𝑍) →
(0g‘𝑟)
∈ V) |
| 61 | 57, 58, 59, 60 | fvmptd 7023 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ (Base‘𝑍) → ((𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟))‘𝑎) = (0g‘𝑟)) |
| 62 | 61 | adantl 481 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) ∧ ℎ:(Base‘𝑍)⟶(Base‘𝑟)) ∧ 𝑎 ∈ (Base‘𝑍)) → ((𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟))‘𝑎) = (0g‘𝑟)) |
| 63 | 47, 56, 62 | 3eqtr4d 2787 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) ∧ ℎ:(Base‘𝑍)⟶(Base‘𝑟)) ∧ 𝑎 ∈ (Base‘𝑍)) → (ℎ‘𝑎) = ((𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟))‘𝑎)) |
| 64 | 38, 41, 63 | eqfnfvd 7054 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) ∧ ℎ:(Base‘𝑍)⟶(Base‘𝑟)) → ℎ = (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟))) |
| 65 | 36, 64 | mpdan 687 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) → ℎ = (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟))) |
| 66 | 65 | ex 412 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → (ℎ ∈ (𝑍(Hom ‘𝐶)𝑟) → ℎ = (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)))) |
| 67 | 66 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍 RngHom 𝑟)) → (ℎ ∈ (𝑍(Hom ‘𝐶)𝑟) → ℎ = (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)))) |
| 68 | 67 | alrimiv 1927 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍 RngHom 𝑟)) → ∀ℎ(ℎ ∈ (𝑍(Hom ‘𝐶)𝑟) → ℎ = (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)))) |
| 69 | 17, 31, 68 | 3jca 1129 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍 RngHom 𝑟)) → ((𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍 RngHom 𝑟) ∧ (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍(Hom ‘𝐶)𝑟) ∧ ∀ℎ(ℎ ∈ (𝑍(Hom ‘𝐶)𝑟) → ℎ = (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟))))) |
| 70 | 16, 69 | mpdan 687 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → ((𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍 RngHom 𝑟) ∧ (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍(Hom ‘𝐶)𝑟) ∧ ∀ℎ(ℎ ∈ (𝑍(Hom ‘𝐶)𝑟) → ℎ = (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟))))) |
| 71 | | eleq1 2829 |
. . . . 5
⊢ (ℎ = (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) → (ℎ ∈ (𝑍(Hom ‘𝐶)𝑟) ↔ (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍(Hom ‘𝐶)𝑟))) |
| 72 | 71 | eqeu 3712 |
. . . 4
⊢ (((𝑥 ∈ (Base‘𝑍) ↦
(0g‘𝑟))
∈ (𝑍 RngHom 𝑟) ∧ (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍(Hom ‘𝐶)𝑟) ∧ ∀ℎ(ℎ ∈ (𝑍(Hom ‘𝐶)𝑟) → ℎ = (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)))) → ∃!ℎ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) |
| 73 | 70, 72 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → ∃!ℎ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) |
| 74 | 73 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑟 ∈ (Base‘𝐶)∃!ℎ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) |
| 75 | 1 | rngccat 20634 |
. . . 4
⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat) |
| 76 | 3, 75 | syl 17 |
. . 3
⊢ (𝜑 → 𝐶 ∈ Cat) |
| 77 | 2, 19, 76, 25 | isinito 18041 |
. 2
⊢ (𝜑 → (𝑍 ∈ (InitO‘𝐶) ↔ ∀𝑟 ∈ (Base‘𝐶)∃!ℎ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟))) |
| 78 | 74, 77 | mpbird 257 |
1
⊢ (𝜑 → 𝑍 ∈ (InitO‘𝐶)) |