Step | Hyp | Ref
| Expression |
1 | | srhmsubcALTV.c |
. . . 4
⊢ 𝐶 = (𝑈 ∩ 𝑆) |
2 | | eleq1 2676 |
. . . . . . 7
⊢ (𝑟 = 𝑥 → (𝑟 ∈ Ring ↔ 𝑥 ∈ Ring)) |
3 | | srhmsubcALTV.s |
. . . . . . 7
⊢
∀𝑟 ∈
𝑆 𝑟 ∈ Ring |
4 | 2, 3 | vtoclri 3256 |
. . . . . 6
⊢ (𝑥 ∈ 𝑆 → 𝑥 ∈ Ring) |
5 | 4 | ssriv 3572 |
. . . . 5
⊢ 𝑆 ⊆ Ring |
6 | | sslin 3801 |
. . . . 5
⊢ (𝑆 ⊆ Ring → (𝑈 ∩ 𝑆) ⊆ (𝑈 ∩ Ring)) |
7 | 5, 6 | mp1i 13 |
. . . 4
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∩ 𝑆) ⊆ (𝑈 ∩ Ring)) |
8 | 1, 7 | syl5eqss 3612 |
. . 3
⊢ (𝑈 ∈ 𝑉 → 𝐶 ⊆ (𝑈 ∩ Ring)) |
9 | | ssid 3587 |
. . . . . 6
⊢ (𝑥 RingHom 𝑦) ⊆ (𝑥 RingHom 𝑦) |
10 | | eqid 2610 |
. . . . . . 7
⊢
(RingCatALTV‘𝑈) = (RingCatALTV‘𝑈) |
11 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘(RingCatALTV‘𝑈)) = (Base‘(RingCatALTV‘𝑈)) |
12 | | simpl 472 |
. . . . . . 7
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑈 ∈ 𝑉) |
13 | | eqid 2610 |
. . . . . . 7
⊢ (Hom
‘(RingCatALTV‘𝑈)) = (Hom ‘(RingCatALTV‘𝑈)) |
14 | 3, 1 | srhmsubcALTVlem2 41885 |
. . . . . . . 8
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ (Base‘(RingCatALTV‘𝑈))) |
15 | 14 | adantrr 749 |
. . . . . . 7
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑥 ∈ (Base‘(RingCatALTV‘𝑈))) |
16 | 3, 1 | srhmsubcALTVlem2 41885 |
. . . . . . . 8
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ (Base‘(RingCatALTV‘𝑈))) |
17 | 16 | adantrl 748 |
. . . . . . 7
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑦 ∈ (Base‘(RingCatALTV‘𝑈))) |
18 | 10, 11, 12, 13, 15, 17 | ringchomALTV 41840 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(Hom ‘(RingCatALTV‘𝑈))𝑦) = (𝑥 RingHom 𝑦)) |
19 | 9, 18 | syl5sseqr 3617 |
. . . . 5
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 RingHom 𝑦) ⊆ (𝑥(Hom ‘(RingCatALTV‘𝑈))𝑦)) |
20 | | srhmsubcALTV.j |
. . . . . . 7
⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠)) |
21 | 20 | a1i 11 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))) |
22 | | oveq12 6558 |
. . . . . . 7
⊢ ((𝑟 = 𝑥 ∧ 𝑠 = 𝑦) → (𝑟 RingHom 𝑠) = (𝑥 RingHom 𝑦)) |
23 | 22 | adantl 481 |
. . . . . 6
⊢ (((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) ∧ (𝑟 = 𝑥 ∧ 𝑠 = 𝑦)) → (𝑟 RingHom 𝑠) = (𝑥 RingHom 𝑦)) |
24 | | simprl 790 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑥 ∈ 𝐶) |
25 | | simprr 792 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑦 ∈ 𝐶) |
26 | | ovex 6577 |
. . . . . . 7
⊢ (𝑥 RingHom 𝑦) ∈ V |
27 | 26 | a1i 11 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 RingHom 𝑦) ∈ V) |
28 | 21, 23, 24, 25, 27 | ovmpt2d 6686 |
. . . . 5
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥𝐽𝑦) = (𝑥 RingHom 𝑦)) |
29 | | eqid 2610 |
. . . . . 6
⊢
(Homf ‘(RingCatALTV‘𝑈)) = (Homf
‘(RingCatALTV‘𝑈)) |
30 | 29, 11, 13, 15, 17 | homfval 16175 |
. . . . 5
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(Homf
‘(RingCatALTV‘𝑈))𝑦) = (𝑥(Hom ‘(RingCatALTV‘𝑈))𝑦)) |
31 | 19, 28, 30 | 3sstr4d 3611 |
. . . 4
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥𝐽𝑦) ⊆ (𝑥(Homf
‘(RingCatALTV‘𝑈))𝑦)) |
32 | 31 | ralrimivva 2954 |
. . 3
⊢ (𝑈 ∈ 𝑉 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝐽𝑦) ⊆ (𝑥(Homf
‘(RingCatALTV‘𝑈))𝑦)) |
33 | | ovex 6577 |
. . . . . 6
⊢ (𝑟 RingHom 𝑠) ∈ V |
34 | 20, 33 | fnmpt2i 7128 |
. . . . 5
⊢ 𝐽 Fn (𝐶 × 𝐶) |
35 | 34 | a1i 11 |
. . . 4
⊢ (𝑈 ∈ 𝑉 → 𝐽 Fn (𝐶 × 𝐶)) |
36 | 29, 11 | homffn 16176 |
. . . . 5
⊢
(Homf ‘(RingCatALTV‘𝑈)) Fn ((Base‘(RingCatALTV‘𝑈)) ×
(Base‘(RingCatALTV‘𝑈))) |
37 | | id 22 |
. . . . . . . . 9
⊢ (𝑈 ∈ 𝑉 → 𝑈 ∈ 𝑉) |
38 | 10, 11, 37 | ringcbasALTV 41838 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝑉 → (Base‘(RingCatALTV‘𝑈)) = (𝑈 ∩ Ring)) |
39 | 38 | eqcomd 2616 |
. . . . . . 7
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∩ Ring) =
(Base‘(RingCatALTV‘𝑈))) |
40 | 39 | sqxpeqd 5065 |
. . . . . 6
⊢ (𝑈 ∈ 𝑉 → ((𝑈 ∩ Ring) × (𝑈 ∩ Ring)) =
((Base‘(RingCatALTV‘𝑈)) ×
(Base‘(RingCatALTV‘𝑈)))) |
41 | 40 | fneq2d 5896 |
. . . . 5
⊢ (𝑈 ∈ 𝑉 → ((Homf
‘(RingCatALTV‘𝑈)) Fn ((𝑈 ∩ Ring) × (𝑈 ∩ Ring)) ↔ (Homf
‘(RingCatALTV‘𝑈)) Fn ((Base‘(RingCatALTV‘𝑈)) ×
(Base‘(RingCatALTV‘𝑈))))) |
42 | 36, 41 | mpbiri 247 |
. . . 4
⊢ (𝑈 ∈ 𝑉 → (Homf
‘(RingCatALTV‘𝑈)) Fn ((𝑈 ∩ Ring) × (𝑈 ∩ Ring))) |
43 | | inex1g 4729 |
. . . 4
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∩ Ring) ∈ V) |
44 | 35, 42, 43 | isssc 16303 |
. . 3
⊢ (𝑈 ∈ 𝑉 → (𝐽 ⊆cat
(Homf ‘(RingCatALTV‘𝑈)) ↔ (𝐶 ⊆ (𝑈 ∩ Ring) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝐽𝑦) ⊆ (𝑥(Homf
‘(RingCatALTV‘𝑈))𝑦)))) |
45 | 8, 32, 44 | mpbir2and 959 |
. 2
⊢ (𝑈 ∈ 𝑉 → 𝐽 ⊆cat
(Homf ‘(RingCatALTV‘𝑈))) |
46 | 1 | elin2 3763 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐶 ↔ (𝑥 ∈ 𝑈 ∧ 𝑥 ∈ 𝑆)) |
47 | 4 | adantl 481 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑈 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ Ring) |
48 | 46, 47 | sylbi 206 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ Ring) |
49 | 48 | adantl 481 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ Ring) |
50 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘𝑥) =
(Base‘𝑥) |
51 | 50 | idrhm 18554 |
. . . . . 6
⊢ (𝑥 ∈ Ring → ( I ↾
(Base‘𝑥)) ∈
(𝑥 RingHom 𝑥)) |
52 | 49, 51 | syl 17 |
. . . . 5
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → ( I ↾ (Base‘𝑥)) ∈ (𝑥 RingHom 𝑥)) |
53 | | eqid 2610 |
. . . . . 6
⊢
(Id‘(RingCatALTV‘𝑈)) = (Id‘(RingCatALTV‘𝑈)) |
54 | | simpl 472 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → 𝑈 ∈ 𝑉) |
55 | 10, 11, 53, 54, 14, 50 | ringcidALTV 41846 |
. . . . 5
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → ((Id‘(RingCatALTV‘𝑈))‘𝑥) = ( I ↾ (Base‘𝑥))) |
56 | 20 | a1i 11 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))) |
57 | | oveq12 6558 |
. . . . . . 7
⊢ ((𝑟 = 𝑥 ∧ 𝑠 = 𝑥) → (𝑟 RingHom 𝑠) = (𝑥 RingHom 𝑥)) |
58 | 57 | adantl 481 |
. . . . . 6
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑟 = 𝑥 ∧ 𝑠 = 𝑥)) → (𝑟 RingHom 𝑠) = (𝑥 RingHom 𝑥)) |
59 | | simpr 476 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ 𝐶) |
60 | | ovex 6577 |
. . . . . . 7
⊢ (𝑥 RingHom 𝑥) ∈ V |
61 | 60 | a1i 11 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → (𝑥 RingHom 𝑥) ∈ V) |
62 | 56, 58, 59, 59, 61 | ovmpt2d 6686 |
. . . . 5
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → (𝑥𝐽𝑥) = (𝑥 RingHom 𝑥)) |
63 | 52, 55, 62 | 3eltr4d 2703 |
. . . 4
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → ((Id‘(RingCatALTV‘𝑈))‘𝑥) ∈ (𝑥𝐽𝑥)) |
64 | | eqid 2610 |
. . . . . . . . 9
⊢
(comp‘(RingCatALTV‘𝑈)) = (comp‘(RingCatALTV‘𝑈)) |
65 | 10 | ringccatALTV 41845 |
. . . . . . . . . 10
⊢ (𝑈 ∈ 𝑉 → (RingCatALTV‘𝑈) ∈ Cat) |
66 | 65 | ad3antrrr 762 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → (RingCatALTV‘𝑈) ∈ Cat) |
67 | 14 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝑥 ∈ (Base‘(RingCatALTV‘𝑈))) |
68 | 67 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → 𝑥 ∈ (Base‘(RingCatALTV‘𝑈))) |
69 | 16 | ad2ant2r 779 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝑦 ∈ (Base‘(RingCatALTV‘𝑈))) |
70 | 69 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → 𝑦 ∈ (Base‘(RingCatALTV‘𝑈))) |
71 | 3, 1 | srhmsubcALTVlem2 41885 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑧 ∈ 𝐶) → 𝑧 ∈ (Base‘(RingCatALTV‘𝑈))) |
72 | 71 | ad2ant2rl 781 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝑧 ∈ (Base‘(RingCatALTV‘𝑈))) |
73 | 72 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → 𝑧 ∈ (Base‘(RingCatALTV‘𝑈))) |
74 | 54 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝑈 ∈ 𝑉) |
75 | | simpl 472 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶) → 𝑦 ∈ 𝐶) |
76 | 59, 75 | anim12i 588 |
. . . . . . . . . . . . . . 15
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) |
77 | 74, 76 | jca 553 |
. . . . . . . . . . . . . 14
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶))) |
78 | 3, 1, 20 | srhmsubcALTVlem3 41886 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥𝐽𝑦) = (𝑥(Hom ‘(RingCatALTV‘𝑈))𝑦)) |
79 | 77, 78 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑥𝐽𝑦) = (𝑥(Hom ‘(RingCatALTV‘𝑈))𝑦)) |
80 | 79 | eleq2d 2673 |
. . . . . . . . . . . 12
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑓 ∈ (𝑥𝐽𝑦) ↔ 𝑓 ∈ (𝑥(Hom ‘(RingCatALTV‘𝑈))𝑦))) |
81 | 80 | biimpcd 238 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ (𝑥𝐽𝑦) → (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝑓 ∈ (𝑥(Hom ‘(RingCatALTV‘𝑈))𝑦))) |
82 | 81 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)) → (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝑓 ∈ (𝑥(Hom ‘(RingCatALTV‘𝑈))𝑦))) |
83 | 82 | impcom 445 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → 𝑓 ∈ (𝑥(Hom ‘(RingCatALTV‘𝑈))𝑦)) |
84 | 3, 1, 20 | srhmsubcALTVlem3 41886 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑦𝐽𝑧) = (𝑦(Hom ‘(RingCatALTV‘𝑈))𝑧)) |
85 | 84 | adantlr 747 |
. . . . . . . . . . . . 13
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑦𝐽𝑧) = (𝑦(Hom ‘(RingCatALTV‘𝑈))𝑧)) |
86 | 85 | eleq2d 2673 |
. . . . . . . . . . . 12
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑔 ∈ (𝑦𝐽𝑧) ↔ 𝑔 ∈ (𝑦(Hom ‘(RingCatALTV‘𝑈))𝑧))) |
87 | 86 | biimpd 218 |
. . . . . . . . . . 11
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑔 ∈ (𝑦𝐽𝑧) → 𝑔 ∈ (𝑦(Hom ‘(RingCatALTV‘𝑈))𝑧))) |
88 | 87 | adantld 482 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → ((𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)) → 𝑔 ∈ (𝑦(Hom ‘(RingCatALTV‘𝑈))𝑧))) |
89 | 88 | imp 444 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → 𝑔 ∈ (𝑦(Hom ‘(RingCatALTV‘𝑈))𝑧)) |
90 | 11, 13, 64, 66, 68, 70, 73, 83, 89 | catcocl 16169 |
. . . . . . . 8
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘(RingCatALTV‘𝑈))𝑧)𝑓) ∈ (𝑥(Hom ‘(RingCatALTV‘𝑈))𝑧)) |
91 | 10, 11, 74, 13, 67, 72 | ringchomALTV 41840 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑥(Hom ‘(RingCatALTV‘𝑈))𝑧) = (𝑥 RingHom 𝑧)) |
92 | 91 | eqcomd 2616 |
. . . . . . . . 9
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑥 RingHom 𝑧) = (𝑥(Hom ‘(RingCatALTV‘𝑈))𝑧)) |
93 | 92 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → (𝑥 RingHom 𝑧) = (𝑥(Hom ‘(RingCatALTV‘𝑈))𝑧)) |
94 | 90, 93 | eleqtrrd 2691 |
. . . . . . 7
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘(RingCatALTV‘𝑈))𝑧)𝑓) ∈ (𝑥 RingHom 𝑧)) |
95 | 20 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))) |
96 | | oveq12 6558 |
. . . . . . . . . 10
⊢ ((𝑟 = 𝑥 ∧ 𝑠 = 𝑧) → (𝑟 RingHom 𝑠) = (𝑥 RingHom 𝑧)) |
97 | 96 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑟 = 𝑥 ∧ 𝑠 = 𝑧)) → (𝑟 RingHom 𝑠) = (𝑥 RingHom 𝑧)) |
98 | 59 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝑥 ∈ 𝐶) |
99 | | simprr 792 |
. . . . . . . . 9
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝑧 ∈ 𝐶) |
100 | | ovex 6577 |
. . . . . . . . . 10
⊢ (𝑥 RingHom 𝑧) ∈ V |
101 | 100 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑥 RingHom 𝑧) ∈ V) |
102 | 95, 97, 98, 99, 101 | ovmpt2d 6686 |
. . . . . . . 8
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑥𝐽𝑧) = (𝑥 RingHom 𝑧)) |
103 | 102 | adantr 480 |
. . . . . . 7
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → (𝑥𝐽𝑧) = (𝑥 RingHom 𝑧)) |
104 | 94, 103 | eleqtrrd 2691 |
. . . . . 6
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘(RingCatALTV‘𝑈))𝑧)𝑓) ∈ (𝑥𝐽𝑧)) |
105 | 104 | ralrimivva 2954 |
. . . . 5
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘(RingCatALTV‘𝑈))𝑧)𝑓) ∈ (𝑥𝐽𝑧)) |
106 | 105 | ralrimivva 2954 |
. . . 4
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → ∀𝑦 ∈ 𝐶 ∀𝑧 ∈ 𝐶 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘(RingCatALTV‘𝑈))𝑧)𝑓) ∈ (𝑥𝐽𝑧)) |
107 | 63, 106 | jca 553 |
. . 3
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) →
(((Id‘(RingCatALTV‘𝑈))‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦 ∈ 𝐶 ∀𝑧 ∈ 𝐶 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘(RingCatALTV‘𝑈))𝑧)𝑓) ∈ (𝑥𝐽𝑧))) |
108 | 107 | ralrimiva 2949 |
. 2
⊢ (𝑈 ∈ 𝑉 → ∀𝑥 ∈ 𝐶 (((Id‘(RingCatALTV‘𝑈))‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦 ∈ 𝐶 ∀𝑧 ∈ 𝐶 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘(RingCatALTV‘𝑈))𝑧)𝑓) ∈ (𝑥𝐽𝑧))) |
109 | 29, 53, 64, 65, 35 | issubc2 16319 |
. 2
⊢ (𝑈 ∈ 𝑉 → (𝐽 ∈
(Subcat‘(RingCatALTV‘𝑈)) ↔ (𝐽 ⊆cat
(Homf ‘(RingCatALTV‘𝑈)) ∧ ∀𝑥 ∈ 𝐶 (((Id‘(RingCatALTV‘𝑈))‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦 ∈ 𝐶 ∀𝑧 ∈ 𝐶 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘(RingCatALTV‘𝑈))𝑧)𝑓) ∈ (𝑥𝐽𝑧))))) |
110 | 45, 108, 109 | mpbir2and 959 |
1
⊢ (𝑈 ∈ 𝑉 → 𝐽 ∈
(Subcat‘(RingCatALTV‘𝑈))) |