rngcval

Description: Value of the category of non-unital rings (in a universe). (Contributed by AV, 27-Feb-2020) (Revised by AV, 8-Mar-2020)

	Ref	Expression
Hypotheses	rngcval.c	⊢ 𝐶 = ( RngCat ‘ 𝑈 )
	rngcval.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	rngcval.b	⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Rng ) )
	rngcval.h	⊢ ( 𝜑 → 𝐻 = ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) )
Assertion	rngcval	⊢ ( 𝜑 → 𝐶 = ( ( ExtStrCat ‘ 𝑈 ) ↾_cat 𝐻 ) )

Proof

Step	Hyp	Ref	Expression
1		rngcval.c	⊢ 𝐶 = ( RngCat ‘ 𝑈 )
2		rngcval.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3		rngcval.b	⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Rng ) )
4		rngcval.h	⊢ ( 𝜑 → 𝐻 = ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) )
5		df-rngc	⊢ RngCat = ( 𝑢 ∈ V ↦ ( ( ExtStrCat ‘ 𝑢 ) ↾_cat ( RngHomo ↾ ( ( 𝑢 ∩ Rng ) × ( 𝑢 ∩ Rng ) ) ) ) )
6		fveq2	⊢ ( 𝑢 = 𝑈 → ( ExtStrCat ‘ 𝑢 ) = ( ExtStrCat ‘ 𝑈 ) )
7	6	adantl	⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( ExtStrCat ‘ 𝑢 ) = ( ExtStrCat ‘ 𝑈 ) )
8		ineq1	⊢ ( 𝑢 = 𝑈 → ( 𝑢 ∩ Rng ) = ( 𝑈 ∩ Rng ) )
9	8	sqxpeqd	⊢ ( 𝑢 = 𝑈 → ( ( 𝑢 ∩ Rng ) × ( 𝑢 ∩ Rng ) ) = ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) )
10	3	sqxpeqd	⊢ ( 𝜑 → ( 𝐵 × 𝐵 ) = ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) )
11	10	eqcomd	⊢ ( 𝜑 → ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) = ( 𝐵 × 𝐵 ) )
12	9 11	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( ( 𝑢 ∩ Rng ) × ( 𝑢 ∩ Rng ) ) = ( 𝐵 × 𝐵 ) )
13	12	reseq2d	⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( RngHomo ↾ ( ( 𝑢 ∩ Rng ) × ( 𝑢 ∩ Rng ) ) ) = ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) )
14	4	eqcomd	⊢ ( 𝜑 → ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) = 𝐻 )
15	14	adantr	⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) = 𝐻 )
16	13 15	eqtrd	⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( RngHomo ↾ ( ( 𝑢 ∩ Rng ) × ( 𝑢 ∩ Rng ) ) ) = 𝐻 )
17	7 16	oveq12d	⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( ( ExtStrCat ‘ 𝑢 ) ↾_cat ( RngHomo ↾ ( ( 𝑢 ∩ Rng ) × ( 𝑢 ∩ Rng ) ) ) ) = ( ( ExtStrCat ‘ 𝑈 ) ↾_cat 𝐻 ) )
18	2	elexd	⊢ ( 𝜑 → 𝑈 ∈ V )
19		ovexd	⊢ ( 𝜑 → ( ( ExtStrCat ‘ 𝑈 ) ↾_cat 𝐻 ) ∈ V )
20	5 17 18 19	fvmptd2	⊢ ( 𝜑 → ( RngCat ‘ 𝑈 ) = ( ( ExtStrCat ‘ 𝑈 ) ↾_cat 𝐻 ) )
21	1 20	syl5eq	⊢ ( 𝜑 → 𝐶 = ( ( ExtStrCat ‘ 𝑈 ) ↾_cat 𝐻 ) )

Metamath Proof Explorer

Theorem rngcval

Proof