Step | Hyp | Ref
| Expression |
1 | | zrinitorngc.c |
. . . . . . . . . 10
⊢ 𝐶 = (RngCat‘𝑈) |
2 | | eqid 2740 |
. . . . . . . . . 10
⊢
(Base‘𝐶) =
(Base‘𝐶) |
3 | | zrinitorngc.u |
. . . . . . . . . 10
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
4 | 1, 2, 3 | rngcbas 45492 |
. . . . . . . . 9
⊢ (𝜑 → (Base‘𝐶) = (𝑈 ∩ Rng)) |
5 | 4 | eleq2d 2826 |
. . . . . . . 8
⊢ (𝜑 → (𝑟 ∈ (Base‘𝐶) ↔ 𝑟 ∈ (𝑈 ∩ Rng))) |
6 | | elin 3908 |
. . . . . . . . 9
⊢ (𝑟 ∈ (𝑈 ∩ Rng) ↔ (𝑟 ∈ 𝑈 ∧ 𝑟 ∈ Rng)) |
7 | 6 | simprbi 497 |
. . . . . . . 8
⊢ (𝑟 ∈ (𝑈 ∩ Rng) → 𝑟 ∈ Rng) |
8 | 5, 7 | syl6bi 252 |
. . . . . . 7
⊢ (𝜑 → (𝑟 ∈ (Base‘𝐶) → 𝑟 ∈ Rng)) |
9 | 8 | imp 407 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → 𝑟 ∈ Rng) |
10 | | zrinitorngc.z |
. . . . . . 7
⊢ (𝜑 → 𝑍 ∈ (Ring ∖
NzRing)) |
11 | 10 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → 𝑍 ∈ (Ring ∖
NzRing)) |
12 | | eqid 2740 |
. . . . . . 7
⊢
(Base‘𝑍) =
(Base‘𝑍) |
13 | | eqid 2740 |
. . . . . . 7
⊢
(0g‘𝑟) = (0g‘𝑟) |
14 | | eqid 2740 |
. . . . . . 7
⊢ (𝑥 ∈ (Base‘𝑍) ↦
(0g‘𝑟)) =
(𝑥 ∈ (Base‘𝑍) ↦
(0g‘𝑟)) |
15 | 12, 13, 14 | zrrnghm 45444 |
. . . . . 6
⊢ ((𝑟 ∈ Rng ∧ 𝑍 ∈ (Ring ∖ NzRing))
→ (𝑥 ∈
(Base‘𝑍) ↦
(0g‘𝑟))
∈ (𝑍 RngHomo 𝑟)) |
16 | 9, 11, 15 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍 RngHomo 𝑟)) |
17 | | simpr 485 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍 RngHomo 𝑟)) → (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍 RngHomo 𝑟)) |
18 | 3 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → 𝑈 ∈ 𝑉) |
19 | | eqid 2740 |
. . . . . . . . . 10
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
20 | | zrinitorngc.e |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑍 ∈ 𝑈) |
21 | | eldifi 4066 |
. . . . . . . . . . . . . 14
⊢ (𝑍 ∈ (Ring ∖ NzRing)
→ 𝑍 ∈
Ring) |
22 | | ringrng 45406 |
. . . . . . . . . . . . . 14
⊢ (𝑍 ∈ Ring → 𝑍 ∈ Rng) |
23 | 10, 21, 22 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑍 ∈ Rng) |
24 | 20, 23 | elind 4133 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑍 ∈ (𝑈 ∩ Rng)) |
25 | 24, 4 | eleqtrrd 2844 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑍 ∈ (Base‘𝐶)) |
26 | 25 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → 𝑍 ∈ (Base‘𝐶)) |
27 | | simpr 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → 𝑟 ∈ (Base‘𝐶)) |
28 | 1, 2, 18, 19, 26, 27 | rngchom 45494 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → (𝑍(Hom ‘𝐶)𝑟) = (𝑍 RngHomo 𝑟)) |
29 | 28 | eqcomd 2746 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → (𝑍 RngHomo 𝑟) = (𝑍(Hom ‘𝐶)𝑟)) |
30 | 29 | eleq2d 2826 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → ((𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍 RngHomo 𝑟) ↔ (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍(Hom ‘𝐶)𝑟))) |
31 | 30 | biimpa 477 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍 RngHomo 𝑟)) → (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍(Hom ‘𝐶)𝑟)) |
32 | 28 | eleq2d 2826 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → (ℎ ∈ (𝑍(Hom ‘𝐶)𝑟) ↔ ℎ ∈ (𝑍 RngHomo 𝑟))) |
33 | | eqid 2740 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑟) =
(Base‘𝑟) |
34 | 12, 33 | rnghmf 45426 |
. . . . . . . . . . . 12
⊢ (ℎ ∈ (𝑍 RngHomo 𝑟) → ℎ:(Base‘𝑍)⟶(Base‘𝑟)) |
35 | 32, 34 | syl6bi 252 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → (ℎ ∈ (𝑍(Hom ‘𝐶)𝑟) → ℎ:(Base‘𝑍)⟶(Base‘𝑟))) |
36 | 35 | imp 407 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) → ℎ:(Base‘𝑍)⟶(Base‘𝑟)) |
37 | | ffn 6598 |
. . . . . . . . . . . 12
⊢ (ℎ:(Base‘𝑍)⟶(Base‘𝑟) → ℎ Fn (Base‘𝑍)) |
38 | 37 | adantl 482 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) ∧ ℎ:(Base‘𝑍)⟶(Base‘𝑟)) → ℎ Fn (Base‘𝑍)) |
39 | | fvex 6784 |
. . . . . . . . . . . . 13
⊢
(0g‘𝑟) ∈ V |
40 | 39, 14 | fnmpti 6574 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (Base‘𝑍) ↦
(0g‘𝑟)) Fn
(Base‘𝑍) |
41 | 40 | a1i 11 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) ∧ ℎ:(Base‘𝑍)⟶(Base‘𝑟)) → (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) Fn (Base‘𝑍)) |
42 | 32 | biimpa 477 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) → ℎ ∈ (𝑍 RngHomo 𝑟)) |
43 | | rnghmghm 45425 |
. . . . . . . . . . . . . 14
⊢ (ℎ ∈ (𝑍 RngHomo 𝑟) → ℎ ∈ (𝑍 GrpHom 𝑟)) |
44 | | eqid 2740 |
. . . . . . . . . . . . . . 15
⊢
(0g‘𝑍) = (0g‘𝑍) |
45 | 44, 13 | ghmid 18838 |
. . . . . . . . . . . . . 14
⊢ (ℎ ∈ (𝑍 GrpHom 𝑟) → (ℎ‘(0g‘𝑍)) = (0g‘𝑟)) |
46 | 42, 43, 45 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) → (ℎ‘(0g‘𝑍)) = (0g‘𝑟)) |
47 | 46 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) ∧ ℎ:(Base‘𝑍)⟶(Base‘𝑟)) ∧ 𝑎 ∈ (Base‘𝑍)) → (ℎ‘(0g‘𝑍)) = (0g‘𝑟)) |
48 | 12, 44 | 0ringbas 45398 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑍 ∈ (Ring ∖ NzRing)
→ (Base‘𝑍) =
{(0g‘𝑍)}) |
49 | 10, 48 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (Base‘𝑍) = {(0g‘𝑍)}) |
50 | 49 | eleq2d 2826 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑎 ∈ (Base‘𝑍) ↔ 𝑎 ∈ {(0g‘𝑍)})) |
51 | | elsni 4584 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈
{(0g‘𝑍)}
→ 𝑎 =
(0g‘𝑍)) |
52 | 51 | fveq2d 6775 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈
{(0g‘𝑍)}
→ (ℎ‘𝑎) = (ℎ‘(0g‘𝑍))) |
53 | 50, 52 | syl6bi 252 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑎 ∈ (Base‘𝑍) → (ℎ‘𝑎) = (ℎ‘(0g‘𝑍)))) |
54 | 53 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → (𝑎 ∈ (Base‘𝑍) → (ℎ‘𝑎) = (ℎ‘(0g‘𝑍)))) |
55 | 54 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) ∧ ℎ:(Base‘𝑍)⟶(Base‘𝑟)) → (𝑎 ∈ (Base‘𝑍) → (ℎ‘𝑎) = (ℎ‘(0g‘𝑍)))) |
56 | 55 | imp 407 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) ∧ ℎ:(Base‘𝑍)⟶(Base‘𝑟)) ∧ 𝑎 ∈ (Base‘𝑍)) → (ℎ‘𝑎) = (ℎ‘(0g‘𝑍))) |
57 | | eqidd 2741 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ (Base‘𝑍) → (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) = (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟))) |
58 | | eqidd 2741 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ (Base‘𝑍) ∧ 𝑥 = 𝑎) → (0g‘𝑟) = (0g‘𝑟)) |
59 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ (Base‘𝑍) → 𝑎 ∈ (Base‘𝑍)) |
60 | 39 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ (Base‘𝑍) →
(0g‘𝑟)
∈ V) |
61 | 57, 58, 59, 60 | fvmptd 6879 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ (Base‘𝑍) → ((𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟))‘𝑎) = (0g‘𝑟)) |
62 | 61 | adantl 482 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) ∧ ℎ:(Base‘𝑍)⟶(Base‘𝑟)) ∧ 𝑎 ∈ (Base‘𝑍)) → ((𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟))‘𝑎) = (0g‘𝑟)) |
63 | 47, 56, 62 | 3eqtr4d 2790 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) ∧ ℎ:(Base‘𝑍)⟶(Base‘𝑟)) ∧ 𝑎 ∈ (Base‘𝑍)) → (ℎ‘𝑎) = ((𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟))‘𝑎)) |
64 | 38, 41, 63 | eqfnfvd 6909 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) ∧ ℎ:(Base‘𝑍)⟶(Base‘𝑟)) → ℎ = (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟))) |
65 | 36, 64 | mpdan 684 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) → ℎ = (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟))) |
66 | 65 | ex 413 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → (ℎ ∈ (𝑍(Hom ‘𝐶)𝑟) → ℎ = (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)))) |
67 | 66 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍 RngHomo 𝑟)) → (ℎ ∈ (𝑍(Hom ‘𝐶)𝑟) → ℎ = (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)))) |
68 | 67 | alrimiv 1934 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍 RngHomo 𝑟)) → ∀ℎ(ℎ ∈ (𝑍(Hom ‘𝐶)𝑟) → ℎ = (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)))) |
69 | 17, 31, 68 | 3jca 1127 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) ∧ (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍 RngHomo 𝑟)) → ((𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍 RngHomo 𝑟) ∧ (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍(Hom ‘𝐶)𝑟) ∧ ∀ℎ(ℎ ∈ (𝑍(Hom ‘𝐶)𝑟) → ℎ = (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟))))) |
70 | 16, 69 | mpdan 684 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → ((𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍 RngHomo 𝑟) ∧ (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍(Hom ‘𝐶)𝑟) ∧ ∀ℎ(ℎ ∈ (𝑍(Hom ‘𝐶)𝑟) → ℎ = (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟))))) |
71 | | eleq1 2828 |
. . . . 5
⊢ (ℎ = (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) → (ℎ ∈ (𝑍(Hom ‘𝐶)𝑟) ↔ (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍(Hom ‘𝐶)𝑟))) |
72 | 71 | eqeu 3645 |
. . . 4
⊢ (((𝑥 ∈ (Base‘𝑍) ↦
(0g‘𝑟))
∈ (𝑍 RngHomo 𝑟) ∧ (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)) ∈ (𝑍(Hom ‘𝐶)𝑟) ∧ ∀ℎ(ℎ ∈ (𝑍(Hom ‘𝐶)𝑟) → ℎ = (𝑥 ∈ (Base‘𝑍) ↦ (0g‘𝑟)))) → ∃!ℎ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) |
73 | 70, 72 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → ∃!ℎ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) |
74 | 73 | ralrimiva 3110 |
. 2
⊢ (𝜑 → ∀𝑟 ∈ (Base‘𝐶)∃!ℎ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟)) |
75 | 1 | rngccat 45505 |
. . . 4
⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat) |
76 | 3, 75 | syl 17 |
. . 3
⊢ (𝜑 → 𝐶 ∈ Cat) |
77 | 2, 19, 76, 25 | isinito 17709 |
. 2
⊢ (𝜑 → (𝑍 ∈ (InitO‘𝐶) ↔ ∀𝑟 ∈ (Base‘𝐶)∃!ℎ ℎ ∈ (𝑍(Hom ‘𝐶)𝑟))) |
78 | 74, 77 | mpbird 256 |
1
⊢ (𝜑 → 𝑍 ∈ (InitO‘𝐶)) |