dfrngc2

Description: Alternate definition of the category of non-unital rings (in a universe). (Contributed by AV, 16-Mar-2020)

	Ref	Expression
Hypotheses	dfrngc2.c	⊢ 𝐶 = ( RngCat ‘ 𝑈 )
	dfrngc2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	dfrngc2.b	⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Rng ) )
	dfrngc2.h	⊢ ( 𝜑 → 𝐻 = ( RngHom ↾ ( 𝐵 × 𝐵 ) ) )
	dfrngc2.o	⊢ ( 𝜑 → · = ( comp ‘ ( ExtStrCat ‘ 𝑈 ) ) )
Assertion	dfrngc2	⊢ ( 𝜑 → 𝐶 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		dfrngc2.c	⊢ 𝐶 = ( RngCat ‘ 𝑈 )
2		dfrngc2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3		dfrngc2.b	⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Rng ) )
4		dfrngc2.h	⊢ ( 𝜑 → 𝐻 = ( RngHom ↾ ( 𝐵 × 𝐵 ) ) )
5		dfrngc2.o	⊢ ( 𝜑 → · = ( comp ‘ ( ExtStrCat ‘ 𝑈 ) ) )
6	1 2 3 4	rngcval	⊢ ( 𝜑 → 𝐶 = ( ( ExtStrCat ‘ 𝑈 ) ↾_cat 𝐻 ) )
7		eqid	⊢ ( ( ExtStrCat ‘ 𝑈 ) ↾_cat 𝐻 ) = ( ( ExtStrCat ‘ 𝑈 ) ↾_cat 𝐻 )
8		fvexd	⊢ ( 𝜑 → ( ExtStrCat ‘ 𝑈 ) ∈ V )
9		inex1g	⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∩ Rng ) ∈ V )
10	2 9	syl	⊢ ( 𝜑 → ( 𝑈 ∩ Rng ) ∈ V )
11	3 10	eqeltrd	⊢ ( 𝜑 → 𝐵 ∈ V )
12	3 4	rnghmresfn	⊢ ( 𝜑 → 𝐻 Fn ( 𝐵 × 𝐵 ) )
13	7 8 11 12	rescval2	⊢ ( 𝜑 → ( ( ExtStrCat ‘ 𝑈 ) ↾_cat 𝐻 ) = ( ( ( ExtStrCat ‘ 𝑈 ) ↾_s 𝐵 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
14		eqid	⊢ ( ExtStrCat ‘ 𝑈 ) = ( ExtStrCat ‘ 𝑈 )
15		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) )
16		eqid	⊢ ( comp ‘ ( ExtStrCat ‘ 𝑈 ) ) = ( comp ‘ ( ExtStrCat ‘ 𝑈 ) )
17	14 2 16	estrccofval	⊢ ( 𝜑 → ( comp ‘ ( ExtStrCat ‘ 𝑈 ) ) = ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧 ∈ 𝑈 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑧 ) ↑_m ( Base ‘ ( 2^nd ‘ 𝑣 ) ) ) , 𝑓 ∈ ( ( Base ‘ ( 2^nd ‘ 𝑣 ) ) ↑_m ( Base ‘ ( 1^st ‘ 𝑣 ) ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) )
18	5 17	eqtrd	⊢ ( 𝜑 → · = ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧 ∈ 𝑈 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑧 ) ↑_m ( Base ‘ ( 2^nd ‘ 𝑣 ) ) ) , 𝑓 ∈ ( ( Base ‘ ( 2^nd ‘ 𝑣 ) ) ↑_m ( Base ‘ ( 1^st ‘ 𝑣 ) ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) )
19	14 2 15 18	estrcval	⊢ ( 𝜑 → ( ExtStrCat ‘ 𝑈 ) = { ⟨ ( Base ‘ ndx ) , 𝑈 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )
20		mpoexga	⊢ ( ( 𝑈 ∈ 𝑉 ∧ 𝑈 ∈ 𝑉 ) → ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) ∈ V )
21	2 2 20	syl2anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) ∈ V )
22		fvexd	⊢ ( 𝜑 → ( comp ‘ ( ExtStrCat ‘ 𝑈 ) ) ∈ V )
23	5 22	eqeltrd	⊢ ( 𝜑 → · ∈ V )
24		rnghmfn	⊢ RngHom Fn ( Rng × Rng )
25		fnfun	⊢ ( RngHom Fn ( Rng × Rng ) → Fun RngHom )
26	24 25	mp1i	⊢ ( 𝜑 → Fun RngHom )
27		sqxpexg	⊢ ( 𝐵 ∈ V → ( 𝐵 × 𝐵 ) ∈ V )
28	11 27	syl	⊢ ( 𝜑 → ( 𝐵 × 𝐵 ) ∈ V )
29		resfunexg	⊢ ( ( Fun RngHom ∧ ( 𝐵 × 𝐵 ) ∈ V ) → ( RngHom ↾ ( 𝐵 × 𝐵 ) ) ∈ V )
30	26 28 29	syl2anc	⊢ ( 𝜑 → ( RngHom ↾ ( 𝐵 × 𝐵 ) ) ∈ V )
31	4 30	eqeltrd	⊢ ( 𝜑 → 𝐻 ∈ V )
32		inss1	⊢ ( 𝑈 ∩ Rng ) ⊆ 𝑈
33	3 32	eqsstrdi	⊢ ( 𝜑 → 𝐵 ⊆ 𝑈 )
34	19 2 21 23 31 33	estrres	⊢ ( 𝜑 → ( ( ( ExtStrCat ‘ 𝑈 ) ↾_s 𝐵 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )
35	6 13 34	3eqtrd	⊢ ( 𝜑 → 𝐶 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )

Metamath Proof Explorer

Theorem dfrngc2

Proof