| Step | Hyp | Ref
| Expression |
| 1 | | ringcvalALTV.c |
. 2
⊢ 𝐶 = (RingCatALTV‘𝑈) |
| 2 | | df-ringcALTV 48204 |
. . . 4
⊢
RingCatALTV = (𝑢
∈ V ↦ ⦋(𝑢 ∩ Ring) / 𝑏⦌{〈(Base‘ndx), 𝑏〉, 〈(Hom ‘ndx),
(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 RingHom 𝑦))〉, 〈(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) RingHom 𝑧), 𝑓 ∈ ((1st ‘𝑣) RingHom (2nd
‘𝑣)) ↦ (𝑔 ∘ 𝑓)))〉}) |
| 3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → RingCatALTV = (𝑢 ∈ V ↦
⦋(𝑢 ∩
Ring) / 𝑏⦌{〈(Base‘ndx), 𝑏〉, 〈(Hom ‘ndx),
(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 RingHom 𝑦))〉, 〈(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) RingHom 𝑧), 𝑓 ∈ ((1st ‘𝑣) RingHom (2nd
‘𝑣)) ↦ (𝑔 ∘ 𝑓)))〉})) |
| 4 | | vex 3484 |
. . . . . 6
⊢ 𝑢 ∈ V |
| 5 | 4 | inex1 5317 |
. . . . 5
⊢ (𝑢 ∩ Ring) ∈
V |
| 6 | 5 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → (𝑢 ∩ Ring) ∈ V) |
| 7 | | ineq1 4213 |
. . . . . 6
⊢ (𝑢 = 𝑈 → (𝑢 ∩ Ring) = (𝑈 ∩ Ring)) |
| 8 | 7 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → (𝑢 ∩ Ring) = (𝑈 ∩ Ring)) |
| 9 | | ringcvalALTV.b |
. . . . . 6
⊢ (𝜑 → 𝐵 = (𝑈 ∩ Ring)) |
| 10 | 9 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → 𝐵 = (𝑈 ∩ Ring)) |
| 11 | 8, 10 | eqtr4d 2780 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → (𝑢 ∩ Ring) = 𝐵) |
| 12 | | simpr 484 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵) |
| 13 | 12 | opeq2d 4880 |
. . . . 5
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → 〈(Base‘ndx), 𝑏〉 = 〈(Base‘ndx),
𝐵〉) |
| 14 | | eqidd 2738 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑥 RingHom 𝑦) = (𝑥 RingHom 𝑦)) |
| 15 | 12, 12, 14 | mpoeq123dv 7508 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 RingHom 𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 RingHom 𝑦))) |
| 16 | | ringcvalALTV.h |
. . . . . . . 8
⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 RingHom 𝑦))) |
| 17 | 16 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 RingHom 𝑦))) |
| 18 | 15, 17 | eqtr4d 2780 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 RingHom 𝑦)) = 𝐻) |
| 19 | 18 | opeq2d 4880 |
. . . . 5
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → 〈(Hom ‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 RingHom 𝑦))〉 = 〈(Hom ‘ndx), 𝐻〉) |
| 20 | 12 | sqxpeqd 5717 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑏 × 𝑏) = (𝐵 × 𝐵)) |
| 21 | | eqidd 2738 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑔 ∈ ((2nd ‘𝑣) RingHom 𝑧), 𝑓 ∈ ((1st ‘𝑣) RingHom (2nd
‘𝑣)) ↦ (𝑔 ∘ 𝑓)) = (𝑔 ∈ ((2nd ‘𝑣) RingHom 𝑧), 𝑓 ∈ ((1st ‘𝑣) RingHom (2nd
‘𝑣)) ↦ (𝑔 ∘ 𝑓))) |
| 22 | 20, 12, 21 | mpoeq123dv 7508 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) RingHom 𝑧), 𝑓 ∈ ((1st ‘𝑣) RingHom (2nd
‘𝑣)) ↦ (𝑔 ∘ 𝑓))) = (𝑣 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑣) RingHom 𝑧), 𝑓 ∈ ((1st ‘𝑣) RingHom (2nd
‘𝑣)) ↦ (𝑔 ∘ 𝑓)))) |
| 23 | | ringcvalALTV.o |
. . . . . . . 8
⊢ (𝜑 → · = (𝑣 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑣) RingHom 𝑧), 𝑓 ∈ ((1st ‘𝑣) RingHom (2nd
‘𝑣)) ↦ (𝑔 ∘ 𝑓)))) |
| 24 | 23 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → · = (𝑣 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑣) RingHom 𝑧), 𝑓 ∈ ((1st ‘𝑣) RingHom (2nd
‘𝑣)) ↦ (𝑔 ∘ 𝑓)))) |
| 25 | 22, 24 | eqtr4d 2780 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) RingHom 𝑧), 𝑓 ∈ ((1st ‘𝑣) RingHom (2nd
‘𝑣)) ↦ (𝑔 ∘ 𝑓))) = · ) |
| 26 | 25 | opeq2d 4880 |
. . . . 5
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → 〈(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) RingHom 𝑧), 𝑓 ∈ ((1st ‘𝑣) RingHom (2nd
‘𝑣)) ↦ (𝑔 ∘ 𝑓)))〉 = 〈(comp‘ndx), ·
〉) |
| 27 | 13, 19, 26 | tpeq123d 4748 |
. . . 4
⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → {〈(Base‘ndx), 𝑏〉, 〈(Hom ‘ndx),
(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 RingHom 𝑦))〉, 〈(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) RingHom 𝑧), 𝑓 ∈ ((1st ‘𝑣) RingHom (2nd
‘𝑣)) ↦ (𝑔 ∘ 𝑓)))〉} = {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx),
𝐻〉,
〈(comp‘ndx), ·
〉}) |
| 28 | 6, 11, 27 | csbied2 3936 |
. . 3
⊢ ((𝜑 ∧ 𝑢 = 𝑈) → ⦋(𝑢 ∩ Ring) / 𝑏⦌{〈(Base‘ndx), 𝑏〉, 〈(Hom ‘ndx),
(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 RingHom 𝑦))〉, 〈(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) RingHom 𝑧), 𝑓 ∈ ((1st ‘𝑣) RingHom (2nd
‘𝑣)) ↦ (𝑔 ∘ 𝑓)))〉} = {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx),
𝐻〉,
〈(comp‘ndx), ·
〉}) |
| 29 | | ringcvalALTV.u |
. . . 4
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
| 30 | | elex 3501 |
. . . 4
⊢ (𝑈 ∈ 𝑉 → 𝑈 ∈ V) |
| 31 | 29, 30 | syl 17 |
. . 3
⊢ (𝜑 → 𝑈 ∈ V) |
| 32 | | tpex 7766 |
. . . 4
⊢
{〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx),
·
〉} ∈ V |
| 33 | 32 | a1i 11 |
. . 3
⊢ (𝜑 → {〈(Base‘ndx),
𝐵〉, 〈(Hom
‘ndx), 𝐻〉,
〈(comp‘ndx), · 〉} ∈
V) |
| 34 | 3, 28, 31, 33 | fvmptd 7023 |
. 2
⊢ (𝜑 → (RingCatALTV‘𝑈) = {〈(Base‘ndx),
𝐵〉, 〈(Hom
‘ndx), 𝐻〉,
〈(comp‘ndx), ·
〉}) |
| 35 | 1, 34 | eqtrid 2789 |
1
⊢ (𝜑 → 𝐶 = {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx),
𝐻〉,
〈(comp‘ndx), ·
〉}) |