Metamath Proof Explorer


Theorem rngcvalALTV

Description: Value of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020)

Ref Expression
Hypotheses rngcvalALTV.c 𝐶 = ( RngCatALTV ‘ 𝑈 )
rngcvalALTV.u ( 𝜑𝑈𝑉 )
rngcvalALTV.b ( 𝜑𝐵 = ( 𝑈 ∩ Rng ) )
rngcvalALTV.h ( 𝜑𝐻 = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥 RngHomo 𝑦 ) ) )
rngcvalALTV.o ( 𝜑· = ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧𝐵 ↦ ( 𝑔 ∈ ( ( 2nd𝑣 ) RngHomo 𝑧 ) , 𝑓 ∈ ( ( 1st𝑣 ) RngHomo ( 2nd𝑣 ) ) ↦ ( 𝑔𝑓 ) ) ) )
Assertion rngcvalALTV ( 𝜑𝐶 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )

Proof

Step Hyp Ref Expression
1 rngcvalALTV.c 𝐶 = ( RngCatALTV ‘ 𝑈 )
2 rngcvalALTV.u ( 𝜑𝑈𝑉 )
3 rngcvalALTV.b ( 𝜑𝐵 = ( 𝑈 ∩ Rng ) )
4 rngcvalALTV.h ( 𝜑𝐻 = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥 RngHomo 𝑦 ) ) )
5 rngcvalALTV.o ( 𝜑· = ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧𝐵 ↦ ( 𝑔 ∈ ( ( 2nd𝑣 ) RngHomo 𝑧 ) , 𝑓 ∈ ( ( 1st𝑣 ) RngHomo ( 2nd𝑣 ) ) ↦ ( 𝑔𝑓 ) ) ) )
6 df-rngcALTV RngCatALTV = ( 𝑢 ∈ V ↦ ( 𝑢 ∩ Rng ) / 𝑏 { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥𝑏 , 𝑦𝑏 ↦ ( 𝑥 RngHomo 𝑦 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧𝑏 ↦ ( 𝑔 ∈ ( ( 2nd𝑣 ) RngHomo 𝑧 ) , 𝑓 ∈ ( ( 1st𝑣 ) RngHomo ( 2nd𝑣 ) ) ↦ ( 𝑔𝑓 ) ) ) ⟩ } )
7 6 a1i ( 𝜑 → RngCatALTV = ( 𝑢 ∈ V ↦ ( 𝑢 ∩ Rng ) / 𝑏 { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥𝑏 , 𝑦𝑏 ↦ ( 𝑥 RngHomo 𝑦 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧𝑏 ↦ ( 𝑔 ∈ ( ( 2nd𝑣 ) RngHomo 𝑧 ) , 𝑓 ∈ ( ( 1st𝑣 ) RngHomo ( 2nd𝑣 ) ) ↦ ( 𝑔𝑓 ) ) ) ⟩ } ) )
8 vex 𝑢 ∈ V
9 8 inex1 ( 𝑢 ∩ Rng ) ∈ V
10 9 a1i ( ( 𝜑𝑢 = 𝑈 ) → ( 𝑢 ∩ Rng ) ∈ V )
11 ineq1 ( 𝑢 = 𝑈 → ( 𝑢 ∩ Rng ) = ( 𝑈 ∩ Rng ) )
12 11 adantl ( ( 𝜑𝑢 = 𝑈 ) → ( 𝑢 ∩ Rng ) = ( 𝑈 ∩ Rng ) )
13 3 adantr ( ( 𝜑𝑢 = 𝑈 ) → 𝐵 = ( 𝑈 ∩ Rng ) )
14 12 13 eqtr4d ( ( 𝜑𝑢 = 𝑈 ) → ( 𝑢 ∩ Rng ) = 𝐵 )
15 simpr ( ( ( 𝜑𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → 𝑏 = 𝐵 )
16 15 opeq2d ( ( ( 𝜑𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ = ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ )
17 eqidd ( ( ( 𝜑𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ( 𝑥 RngHomo 𝑦 ) = ( 𝑥 RngHomo 𝑦 ) )
18 15 15 17 mpoeq123dv ( ( ( 𝜑𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ( 𝑥𝑏 , 𝑦𝑏 ↦ ( 𝑥 RngHomo 𝑦 ) ) = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥 RngHomo 𝑦 ) ) )
19 4 ad2antrr ( ( ( 𝜑𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → 𝐻 = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥 RngHomo 𝑦 ) ) )
20 18 19 eqtr4d ( ( ( 𝜑𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ( 𝑥𝑏 , 𝑦𝑏 ↦ ( 𝑥 RngHomo 𝑦 ) ) = 𝐻 )
21 20 opeq2d ( ( ( 𝜑𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ⟨ ( Hom ‘ ndx ) , ( 𝑥𝑏 , 𝑦𝑏 ↦ ( 𝑥 RngHomo 𝑦 ) ) ⟩ = ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ )
22 15 sqxpeqd ( ( ( 𝜑𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ( 𝑏 × 𝑏 ) = ( 𝐵 × 𝐵 ) )
23 eqidd ( ( ( 𝜑𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ( 𝑔 ∈ ( ( 2nd𝑣 ) RngHomo 𝑧 ) , 𝑓 ∈ ( ( 1st𝑣 ) RngHomo ( 2nd𝑣 ) ) ↦ ( 𝑔𝑓 ) ) = ( 𝑔 ∈ ( ( 2nd𝑣 ) RngHomo 𝑧 ) , 𝑓 ∈ ( ( 1st𝑣 ) RngHomo ( 2nd𝑣 ) ) ↦ ( 𝑔𝑓 ) ) )
24 22 15 23 mpoeq123dv ( ( ( 𝜑𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧𝑏 ↦ ( 𝑔 ∈ ( ( 2nd𝑣 ) RngHomo 𝑧 ) , 𝑓 ∈ ( ( 1st𝑣 ) RngHomo ( 2nd𝑣 ) ) ↦ ( 𝑔𝑓 ) ) ) = ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧𝐵 ↦ ( 𝑔 ∈ ( ( 2nd𝑣 ) RngHomo 𝑧 ) , 𝑓 ∈ ( ( 1st𝑣 ) RngHomo ( 2nd𝑣 ) ) ↦ ( 𝑔𝑓 ) ) ) )
25 5 ad2antrr ( ( ( 𝜑𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → · = ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧𝐵 ↦ ( 𝑔 ∈ ( ( 2nd𝑣 ) RngHomo 𝑧 ) , 𝑓 ∈ ( ( 1st𝑣 ) RngHomo ( 2nd𝑣 ) ) ↦ ( 𝑔𝑓 ) ) ) )
26 24 25 eqtr4d ( ( ( 𝜑𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧𝑏 ↦ ( 𝑔 ∈ ( ( 2nd𝑣 ) RngHomo 𝑧 ) , 𝑓 ∈ ( ( 1st𝑣 ) RngHomo ( 2nd𝑣 ) ) ↦ ( 𝑔𝑓 ) ) ) = · )
27 26 opeq2d ( ( ( 𝜑𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧𝑏 ↦ ( 𝑔 ∈ ( ( 2nd𝑣 ) RngHomo 𝑧 ) , 𝑓 ∈ ( ( 1st𝑣 ) RngHomo ( 2nd𝑣 ) ) ↦ ( 𝑔𝑓 ) ) ) ⟩ = ⟨ ( comp ‘ ndx ) , · ⟩ )
28 16 21 27 tpeq123d ( ( ( 𝜑𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥𝑏 , 𝑦𝑏 ↦ ( 𝑥 RngHomo 𝑦 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧𝑏 ↦ ( 𝑔 ∈ ( ( 2nd𝑣 ) RngHomo 𝑧 ) , 𝑓 ∈ ( ( 1st𝑣 ) RngHomo ( 2nd𝑣 ) ) ↦ ( 𝑔𝑓 ) ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )
29 10 14 28 csbied2 ( ( 𝜑𝑢 = 𝑈 ) → ( 𝑢 ∩ Rng ) / 𝑏 { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥𝑏 , 𝑦𝑏 ↦ ( 𝑥 RngHomo 𝑦 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧𝑏 ↦ ( 𝑔 ∈ ( ( 2nd𝑣 ) RngHomo 𝑧 ) , 𝑓 ∈ ( ( 1st𝑣 ) RngHomo ( 2nd𝑣 ) ) ↦ ( 𝑔𝑓 ) ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )
30 elex ( 𝑈𝑉𝑈 ∈ V )
31 2 30 syl ( 𝜑𝑈 ∈ V )
32 tpex { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ∈ V
33 32 a1i ( 𝜑 → { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ∈ V )
34 7 29 31 33 fvmptd ( 𝜑 → ( RngCatALTV ‘ 𝑈 ) = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )
35 1 34 syl5eq ( 𝜑𝐶 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )