Theorem ringcvalALTV

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

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

Proof

Step	Hyp	Ref	Expression
1		ringcvalALTV.c	⊢ 𝐶 = ( RingCatALTV ‘ 𝑈 )
2		ringcvalALTV.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3		ringcvalALTV.b	⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Ring ) )
4		ringcvalALTV.h	⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 RingHom 𝑦 ) ) )
5		ringcvalALTV.o	⊢ ( 𝜑 → · = ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) RingHom 𝑧 ) , 𝑓 ∈ ( ( 1st ‘ 𝑣 ) RingHom ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) )
6		df-ringcALTV	⊢ RingCatALTV = ( 𝑢 ∈ V ↦ ⦋ ( 𝑢 ∩ Ring ) / 𝑏 ⦌ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 RingHom 𝑦 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) RingHom 𝑧 ) , 𝑓 ∈ ( ( 1st ‘ 𝑣 ) RingHom ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) ⟩ } )
7	6	a1i	⊢ ( 𝜑 → RingCatALTV = ( 𝑢 ∈ V ↦ ⦋ ( 𝑢 ∩ Ring ) / 𝑏 ⦌ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 RingHom 𝑦 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) RingHom 𝑧 ) , 𝑓 ∈ ( ( 1st ‘ 𝑣 ) RingHom ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) ⟩ } ) )
8		vex	⊢ 𝑢 ∈ V
9	8	inex1	⊢ ( 𝑢 ∩ Ring ) ∈ V
10	9	a1i	⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( 𝑢 ∩ Ring ) ∈ V )
11		ineq1	⊢ ( 𝑢 = 𝑈 → ( 𝑢 ∩ Ring ) = ( 𝑈 ∩ Ring ) )
12	11	adantl	⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( 𝑢 ∩ Ring ) = ( 𝑈 ∩ Ring ) )
13	3	adantr	⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → 𝐵 = ( 𝑈 ∩ Ring ) )
14	12 13	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( 𝑢 ∩ Ring ) = 𝐵 )
15		simpr	⊢ ( ( ( 𝜑 ∧ 𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → 𝑏 = 𝐵 )
16	15	opeq2d	⊢ ( ( ( 𝜑 ∧ 𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ = ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ )
17		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ( 𝑥 RingHom 𝑦 ) = ( 𝑥 RingHom 𝑦 ) )
18	15 15 17	mpoeq123dv	⊢ ( ( ( 𝜑 ∧ 𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 RingHom 𝑦 ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 RingHom 𝑦 ) ) )
19	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 RingHom 𝑦 ) ) )
20	18 19	eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 RingHom 𝑦 ) ) = 𝐻 )
21	20	opeq2d	⊢ ( ( ( 𝜑 ∧ 𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 RingHom 𝑦 ) ) ⟩ = ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ )
22	15	sqxpeqd	⊢ ( ( ( 𝜑 ∧ 𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ( 𝑏 × 𝑏 ) = ( 𝐵 × 𝐵 ) )
23		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) RingHom 𝑧 ) , 𝑓 ∈ ( ( 1st ‘ 𝑣 ) RingHom ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) = ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) RingHom 𝑧 ) , 𝑓 ∈ ( ( 1st ‘ 𝑣 ) RingHom ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) )
24	22 15 23	mpoeq123dv	⊢ ( ( ( 𝜑 ∧ 𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) RingHom 𝑧 ) , 𝑓 ∈ ( ( 1st ‘ 𝑣 ) RingHom ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) = ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) RingHom 𝑧 ) , 𝑓 ∈ ( ( 1st ‘ 𝑣 ) RingHom ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) )
25	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → · = ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) RingHom 𝑧 ) , 𝑓 ∈ ( ( 1st ‘ 𝑣 ) RingHom ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) )
26	24 25	eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) RingHom 𝑧 ) , 𝑓 ∈ ( ( 1st ‘ 𝑣 ) RingHom ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) = · )
27	26	opeq2d	⊢ ( ( ( 𝜑 ∧ 𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) RingHom 𝑧 ) , 𝑓 ∈ ( ( 1st ‘ 𝑣 ) RingHom ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) ⟩ = ⟨ ( comp ‘ ndx ) , · ⟩ )
28	16 21 27	tpeq123d	⊢ ( ( ( 𝜑 ∧ 𝑢 = 𝑈 ) ∧ 𝑏 = 𝐵 ) → { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 RingHom 𝑦 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) RingHom 𝑧 ) , 𝑓 ∈ ( ( 1st ‘ 𝑣 ) RingHom ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )
29	10 14 28	csbied2	⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ⦋ ( 𝑢 ∩ Ring ) / 𝑏 ⦌ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 RingHom 𝑦 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) RingHom 𝑧 ) , 𝑓 ∈ ( ( 1st ‘ 𝑣 ) RingHom ( 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	⊢ ( 𝜑 → ( RingCatALTV ‘ 𝑈 ) = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )
35	1 34	eqtrid	⊢ ( 𝜑 → 𝐶 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )