Step | Hyp | Ref
| Expression |
1 | | srhmsubcALTV.c |
. . . 4
⊢ 𝐶 = (𝑈 ∩ 𝑆) |
2 | | eleq1w 2820 |
. . . . . . 7
⊢ (𝑟 = 𝑥 → (𝑟 ∈ Ring ↔ 𝑥 ∈ Ring)) |
3 | | srhmsubcALTV.s |
. . . . . . 7
⊢
∀𝑟 ∈
𝑆 𝑟 ∈ Ring |
4 | 2, 3 | vtoclri 3501 |
. . . . . 6
⊢ (𝑥 ∈ 𝑆 → 𝑥 ∈ Ring) |
5 | 4 | ssriv 3905 |
. . . . 5
⊢ 𝑆 ⊆ Ring |
6 | | sslin 4149 |
. . . . 5
⊢ (𝑆 ⊆ Ring → (𝑈 ∩ 𝑆) ⊆ (𝑈 ∩ Ring)) |
7 | 5, 6 | mp1i 13 |
. . . 4
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∩ 𝑆) ⊆ (𝑈 ∩ Ring)) |
8 | 1, 7 | eqsstrid 3949 |
. . 3
⊢ (𝑈 ∈ 𝑉 → 𝐶 ⊆ (𝑈 ∩ Ring)) |
9 | | ssid 3923 |
. . . . . 6
⊢ (𝑥 RingHom 𝑦) ⊆ (𝑥 RingHom 𝑦) |
10 | | eqid 2737 |
. . . . . . 7
⊢
(RingCatALTV‘𝑈) = (RingCatALTV‘𝑈) |
11 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘(RingCatALTV‘𝑈)) = (Base‘(RingCatALTV‘𝑈)) |
12 | | simpl 486 |
. . . . . . 7
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑈 ∈ 𝑉) |
13 | | eqid 2737 |
. . . . . . 7
⊢ (Hom
‘(RingCatALTV‘𝑈)) = (Hom ‘(RingCatALTV‘𝑈)) |
14 | 3, 1 | srhmsubcALTVlem1 45323 |
. . . . . . . 8
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ (Base‘(RingCatALTV‘𝑈))) |
15 | 14 | adantrr 717 |
. . . . . . 7
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑥 ∈ (Base‘(RingCatALTV‘𝑈))) |
16 | 3, 1 | srhmsubcALTVlem1 45323 |
. . . . . . . 8
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ (Base‘(RingCatALTV‘𝑈))) |
17 | 16 | adantrl 716 |
. . . . . . 7
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑦 ∈ (Base‘(RingCatALTV‘𝑈))) |
18 | 10, 11, 12, 13, 15, 17 | ringchomALTV 45279 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(Hom ‘(RingCatALTV‘𝑈))𝑦) = (𝑥 RingHom 𝑦)) |
19 | 9, 18 | sseqtrrid 3954 |
. . . . 5
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 RingHom 𝑦) ⊆ (𝑥(Hom ‘(RingCatALTV‘𝑈))𝑦)) |
20 | | srhmsubcALTV.j |
. . . . . . 7
⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠)) |
21 | 20 | a1i 11 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))) |
22 | | oveq12 7222 |
. . . . . . 7
⊢ ((𝑟 = 𝑥 ∧ 𝑠 = 𝑦) → (𝑟 RingHom 𝑠) = (𝑥 RingHom 𝑦)) |
23 | 22 | adantl 485 |
. . . . . 6
⊢ (((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) ∧ (𝑟 = 𝑥 ∧ 𝑠 = 𝑦)) → (𝑟 RingHom 𝑠) = (𝑥 RingHom 𝑦)) |
24 | | simprl 771 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑥 ∈ 𝐶) |
25 | | simprr 773 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑦 ∈ 𝐶) |
26 | | ovexd 7248 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 RingHom 𝑦) ∈ V) |
27 | 21, 23, 24, 25, 26 | ovmpod 7361 |
. . . . 5
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥𝐽𝑦) = (𝑥 RingHom 𝑦)) |
28 | | eqid 2737 |
. . . . . 6
⊢
(Homf ‘(RingCatALTV‘𝑈)) = (Homf
‘(RingCatALTV‘𝑈)) |
29 | 28, 11, 13, 15, 17 | homfval 17195 |
. . . . 5
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(Homf
‘(RingCatALTV‘𝑈))𝑦) = (𝑥(Hom ‘(RingCatALTV‘𝑈))𝑦)) |
30 | 19, 27, 29 | 3sstr4d 3948 |
. . . 4
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥𝐽𝑦) ⊆ (𝑥(Homf
‘(RingCatALTV‘𝑈))𝑦)) |
31 | 30 | ralrimivva 3112 |
. . 3
⊢ (𝑈 ∈ 𝑉 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝐽𝑦) ⊆ (𝑥(Homf
‘(RingCatALTV‘𝑈))𝑦)) |
32 | | ovex 7246 |
. . . . . 6
⊢ (𝑟 RingHom 𝑠) ∈ V |
33 | 20, 32 | fnmpoi 7840 |
. . . . 5
⊢ 𝐽 Fn (𝐶 × 𝐶) |
34 | 33 | a1i 11 |
. . . 4
⊢ (𝑈 ∈ 𝑉 → 𝐽 Fn (𝐶 × 𝐶)) |
35 | 28, 11 | homffn 17196 |
. . . . 5
⊢
(Homf ‘(RingCatALTV‘𝑈)) Fn ((Base‘(RingCatALTV‘𝑈)) ×
(Base‘(RingCatALTV‘𝑈))) |
36 | | id 22 |
. . . . . . . . 9
⊢ (𝑈 ∈ 𝑉 → 𝑈 ∈ 𝑉) |
37 | 10, 11, 36 | ringcbasALTV 45277 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝑉 → (Base‘(RingCatALTV‘𝑈)) = (𝑈 ∩ Ring)) |
38 | 37 | eqcomd 2743 |
. . . . . . 7
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∩ Ring) =
(Base‘(RingCatALTV‘𝑈))) |
39 | 38 | sqxpeqd 5583 |
. . . . . 6
⊢ (𝑈 ∈ 𝑉 → ((𝑈 ∩ Ring) × (𝑈 ∩ Ring)) =
((Base‘(RingCatALTV‘𝑈)) ×
(Base‘(RingCatALTV‘𝑈)))) |
40 | 39 | fneq2d 6473 |
. . . . 5
⊢ (𝑈 ∈ 𝑉 → ((Homf
‘(RingCatALTV‘𝑈)) Fn ((𝑈 ∩ Ring) × (𝑈 ∩ Ring)) ↔ (Homf
‘(RingCatALTV‘𝑈)) Fn ((Base‘(RingCatALTV‘𝑈)) ×
(Base‘(RingCatALTV‘𝑈))))) |
41 | 35, 40 | mpbiri 261 |
. . . 4
⊢ (𝑈 ∈ 𝑉 → (Homf
‘(RingCatALTV‘𝑈)) Fn ((𝑈 ∩ Ring) × (𝑈 ∩ Ring))) |
42 | | inex1g 5212 |
. . . 4
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∩ Ring) ∈ V) |
43 | 34, 41, 42 | isssc 17325 |
. . 3
⊢ (𝑈 ∈ 𝑉 → (𝐽 ⊆cat
(Homf ‘(RingCatALTV‘𝑈)) ↔ (𝐶 ⊆ (𝑈 ∩ Ring) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝐽𝑦) ⊆ (𝑥(Homf
‘(RingCatALTV‘𝑈))𝑦)))) |
44 | 8, 31, 43 | mpbir2and 713 |
. 2
⊢ (𝑈 ∈ 𝑉 → 𝐽 ⊆cat
(Homf ‘(RingCatALTV‘𝑈))) |
45 | 1 | elin2 4111 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐶 ↔ (𝑥 ∈ 𝑈 ∧ 𝑥 ∈ 𝑆)) |
46 | 4 | adantl 485 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑈 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ Ring) |
47 | 45, 46 | sylbi 220 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ Ring) |
48 | 47 | adantl 485 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ Ring) |
49 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘𝑥) =
(Base‘𝑥) |
50 | 49 | idrhm 19751 |
. . . . . 6
⊢ (𝑥 ∈ Ring → ( I ↾
(Base‘𝑥)) ∈
(𝑥 RingHom 𝑥)) |
51 | 48, 50 | syl 17 |
. . . . 5
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → ( I ↾ (Base‘𝑥)) ∈ (𝑥 RingHom 𝑥)) |
52 | | eqid 2737 |
. . . . . 6
⊢
(Id‘(RingCatALTV‘𝑈)) = (Id‘(RingCatALTV‘𝑈)) |
53 | | simpl 486 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → 𝑈 ∈ 𝑉) |
54 | 10, 11, 52, 53, 14, 49 | ringcidALTV 45285 |
. . . . 5
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → ((Id‘(RingCatALTV‘𝑈))‘𝑥) = ( I ↾ (Base‘𝑥))) |
55 | 20 | a1i 11 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))) |
56 | | oveq12 7222 |
. . . . . . 7
⊢ ((𝑟 = 𝑥 ∧ 𝑠 = 𝑥) → (𝑟 RingHom 𝑠) = (𝑥 RingHom 𝑥)) |
57 | 56 | adantl 485 |
. . . . . 6
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑟 = 𝑥 ∧ 𝑠 = 𝑥)) → (𝑟 RingHom 𝑠) = (𝑥 RingHom 𝑥)) |
58 | | simpr 488 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ 𝐶) |
59 | | ovexd 7248 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → (𝑥 RingHom 𝑥) ∈ V) |
60 | 55, 57, 58, 58, 59 | ovmpod 7361 |
. . . . 5
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → (𝑥𝐽𝑥) = (𝑥 RingHom 𝑥)) |
61 | 51, 54, 60 | 3eltr4d 2853 |
. . . 4
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → ((Id‘(RingCatALTV‘𝑈))‘𝑥) ∈ (𝑥𝐽𝑥)) |
62 | | eqid 2737 |
. . . . . . . . 9
⊢
(comp‘(RingCatALTV‘𝑈)) = (comp‘(RingCatALTV‘𝑈)) |
63 | 10 | ringccatALTV 45284 |
. . . . . . . . . 10
⊢ (𝑈 ∈ 𝑉 → (RingCatALTV‘𝑈) ∈ Cat) |
64 | 63 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → (RingCatALTV‘𝑈) ∈ Cat) |
65 | 14 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝑥 ∈ (Base‘(RingCatALTV‘𝑈))) |
66 | 65 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → 𝑥 ∈ (Base‘(RingCatALTV‘𝑈))) |
67 | 16 | ad2ant2r 747 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝑦 ∈ (Base‘(RingCatALTV‘𝑈))) |
68 | 67 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → 𝑦 ∈ (Base‘(RingCatALTV‘𝑈))) |
69 | 3, 1 | srhmsubcALTVlem1 45323 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑧 ∈ 𝐶) → 𝑧 ∈ (Base‘(RingCatALTV‘𝑈))) |
70 | 69 | ad2ant2rl 749 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝑧 ∈ (Base‘(RingCatALTV‘𝑈))) |
71 | 70 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → 𝑧 ∈ (Base‘(RingCatALTV‘𝑈))) |
72 | 53 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝑈 ∈ 𝑉) |
73 | | simpl 486 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶) → 𝑦 ∈ 𝐶) |
74 | 58, 73 | anim12i 616 |
. . . . . . . . . . . . . . 15
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) |
75 | 72, 74 | jca 515 |
. . . . . . . . . . . . . 14
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶))) |
76 | 3, 1, 20 | srhmsubcALTVlem2 45324 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥𝐽𝑦) = (𝑥(Hom ‘(RingCatALTV‘𝑈))𝑦)) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑥𝐽𝑦) = (𝑥(Hom ‘(RingCatALTV‘𝑈))𝑦)) |
78 | 77 | eleq2d 2823 |
. . . . . . . . . . . 12
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑓 ∈ (𝑥𝐽𝑦) ↔ 𝑓 ∈ (𝑥(Hom ‘(RingCatALTV‘𝑈))𝑦))) |
79 | 78 | biimpcd 252 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ (𝑥𝐽𝑦) → (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝑓 ∈ (𝑥(Hom ‘(RingCatALTV‘𝑈))𝑦))) |
80 | 79 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)) → (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝑓 ∈ (𝑥(Hom ‘(RingCatALTV‘𝑈))𝑦))) |
81 | 80 | impcom 411 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → 𝑓 ∈ (𝑥(Hom ‘(RingCatALTV‘𝑈))𝑦)) |
82 | 3, 1, 20 | srhmsubcALTVlem2 45324 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑦𝐽𝑧) = (𝑦(Hom ‘(RingCatALTV‘𝑈))𝑧)) |
83 | 82 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑦𝐽𝑧) = (𝑦(Hom ‘(RingCatALTV‘𝑈))𝑧)) |
84 | 83 | eleq2d 2823 |
. . . . . . . . . . . 12
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑔 ∈ (𝑦𝐽𝑧) ↔ 𝑔 ∈ (𝑦(Hom ‘(RingCatALTV‘𝑈))𝑧))) |
85 | 84 | biimpd 232 |
. . . . . . . . . . 11
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑔 ∈ (𝑦𝐽𝑧) → 𝑔 ∈ (𝑦(Hom ‘(RingCatALTV‘𝑈))𝑧))) |
86 | 85 | adantld 494 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → ((𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)) → 𝑔 ∈ (𝑦(Hom ‘(RingCatALTV‘𝑈))𝑧))) |
87 | 86 | imp 410 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → 𝑔 ∈ (𝑦(Hom ‘(RingCatALTV‘𝑈))𝑧)) |
88 | 11, 13, 62, 64, 66, 68, 71, 81, 87 | catcocl 17188 |
. . . . . . . 8
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘(RingCatALTV‘𝑈))𝑧)𝑓) ∈ (𝑥(Hom ‘(RingCatALTV‘𝑈))𝑧)) |
89 | 10, 11, 72, 13, 65, 70 | ringchomALTV 45279 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑥(Hom ‘(RingCatALTV‘𝑈))𝑧) = (𝑥 RingHom 𝑧)) |
90 | 89 | eqcomd 2743 |
. . . . . . . . 9
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑥 RingHom 𝑧) = (𝑥(Hom ‘(RingCatALTV‘𝑈))𝑧)) |
91 | 90 | adantr 484 |
. . . . . . . 8
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → (𝑥 RingHom 𝑧) = (𝑥(Hom ‘(RingCatALTV‘𝑈))𝑧)) |
92 | 88, 91 | eleqtrrd 2841 |
. . . . . . 7
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘(RingCatALTV‘𝑈))𝑧)𝑓) ∈ (𝑥 RingHom 𝑧)) |
93 | 20 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))) |
94 | | oveq12 7222 |
. . . . . . . . . 10
⊢ ((𝑟 = 𝑥 ∧ 𝑠 = 𝑧) → (𝑟 RingHom 𝑠) = (𝑥 RingHom 𝑧)) |
95 | 94 | adantl 485 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑟 = 𝑥 ∧ 𝑠 = 𝑧)) → (𝑟 RingHom 𝑠) = (𝑥 RingHom 𝑧)) |
96 | 58 | adantr 484 |
. . . . . . . . 9
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝑥 ∈ 𝐶) |
97 | | simprr 773 |
. . . . . . . . 9
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝑧 ∈ 𝐶) |
98 | | ovexd 7248 |
. . . . . . . . 9
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑥 RingHom 𝑧) ∈ V) |
99 | 93, 95, 96, 97, 98 | ovmpod 7361 |
. . . . . . . 8
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑥𝐽𝑧) = (𝑥 RingHom 𝑧)) |
100 | 99 | adantr 484 |
. . . . . . 7
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → (𝑥𝐽𝑧) = (𝑥 RingHom 𝑧)) |
101 | 92, 100 | eleqtrrd 2841 |
. . . . . 6
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘(RingCatALTV‘𝑈))𝑧)𝑓) ∈ (𝑥𝐽𝑧)) |
102 | 101 | ralrimivva 3112 |
. . . . 5
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘(RingCatALTV‘𝑈))𝑧)𝑓) ∈ (𝑥𝐽𝑧)) |
103 | 102 | ralrimivva 3112 |
. . . 4
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → ∀𝑦 ∈ 𝐶 ∀𝑧 ∈ 𝐶 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘(RingCatALTV‘𝑈))𝑧)𝑓) ∈ (𝑥𝐽𝑧)) |
104 | 61, 103 | jca 515 |
. . 3
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) →
(((Id‘(RingCatALTV‘𝑈))‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦 ∈ 𝐶 ∀𝑧 ∈ 𝐶 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘(RingCatALTV‘𝑈))𝑧)𝑓) ∈ (𝑥𝐽𝑧))) |
105 | 104 | ralrimiva 3105 |
. 2
⊢ (𝑈 ∈ 𝑉 → ∀𝑥 ∈ 𝐶 (((Id‘(RingCatALTV‘𝑈))‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦 ∈ 𝐶 ∀𝑧 ∈ 𝐶 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘(RingCatALTV‘𝑈))𝑧)𝑓) ∈ (𝑥𝐽𝑧))) |
106 | 28, 52, 62, 63, 34 | issubc2 17342 |
. 2
⊢ (𝑈 ∈ 𝑉 → (𝐽 ∈
(Subcat‘(RingCatALTV‘𝑈)) ↔ (𝐽 ⊆cat
(Homf ‘(RingCatALTV‘𝑈)) ∧ ∀𝑥 ∈ 𝐶 (((Id‘(RingCatALTV‘𝑈))‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦 ∈ 𝐶 ∀𝑧 ∈ 𝐶 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘(RingCatALTV‘𝑈))𝑧)𝑓) ∈ (𝑥𝐽𝑧))))) |
107 | 44, 105, 106 | mpbir2and 713 |
1
⊢ (𝑈 ∈ 𝑉 → 𝐽 ∈
(Subcat‘(RingCatALTV‘𝑈))) |