Metamath Proof Explorer

Theorem rngcresringcat

Description: The restriction of the category of non-unital rings to the set of unital ring homomorphisms is the category of unital rings. (Contributed by AV, 16-Mar-2020)

Ref Expression
Hypotheses rhmsubcrngc.c ⊢ 𝐶 = ( RngCat ‘ 𝑈 )
rhmsubcrngc.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
rhmsubcrngc.b ⊢ ( 𝜑 → 𝐵 = ( Ring ∩ 𝑈 ) )
rhmsubcrngc.h ⊢ ( 𝜑 → 𝐻 = ( RingHom ↾ ( 𝐵 × 𝐵 ) ) )
Assertion rngcresringcat ( 𝜑 → ( 𝐶 ↾cat 𝐻 ) = ( RingCat ‘ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 rhmsubcrngc.c ⊢ 𝐶 = ( RngCat ‘ 𝑈 )
2 rhmsubcrngc.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3 rhmsubcrngc.b ⊢ ( 𝜑 → 𝐵 = ( Ring ∩ 𝑈 ) )
4 rhmsubcrngc.h ⊢ ( 𝜑 → 𝐻 = ( RingHom ↾ ( 𝐵 × 𝐵 ) ) )
5 eqidd ⊢ ( 𝜑 → ( 𝑈 ∩ Rng ) = ( 𝑈 ∩ Rng ) )
6 eqidd ⊢ ( 𝜑 → ( RngHomo ↾ ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) ) = ( RngHomo ↾ ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) ) )
7 eqidd ⊢ ( 𝜑 → ( comp ‘ ( ExtStrCat ‘ 𝑈 ) ) = ( comp ‘ ( ExtStrCat ‘ 𝑈 ) ) )
8 1 2 5 6 7 dfrngc2 ⊢ ( 𝜑 → 𝐶 = { ⟨ ( Base ‘ ndx ) , ( 𝑈 ∩ Rng ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( RngHomo ↾ ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( comp ‘ ( ExtStrCat ‘ 𝑈 ) ) ⟩ } )
9 inex1g ⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∩ Rng ) ∈ V )
10 2 9 syl ⊢ ( 𝜑 → ( 𝑈 ∩ Rng ) ∈ V )
11 rnghmfn ⊢ RngHomo Fn ( Rng × Rng )
12 fnfun ⊢ ( RngHomo Fn ( Rng × Rng ) → Fun RngHomo )
13 11 12 mp1i ⊢ ( 𝜑 → Fun RngHomo )
14 sqxpexg ⊢ ( ( 𝑈 ∩ Rng ) ∈ V → ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) ∈ V )
15 10 14 syl ⊢ ( 𝜑 → ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) ∈ V )
16 resfunexg ⊢ ( ( Fun RngHomo ∧ ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) ∈ V ) → ( RngHomo ↾ ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) ) ∈ V )
17 13 15 16 syl2anc ⊢ ( 𝜑 → ( RngHomo ↾ ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) ) ∈ V )
18 fvexd ⊢ ( 𝜑 → ( comp ‘ ( ExtStrCat ‘ 𝑈 ) ) ∈ V )
19 rhmfn ⊢ RingHom Fn ( Ring × Ring )
20 fnfun ⊢ ( RingHom Fn ( Ring × Ring ) → Fun RingHom )
21 19 20 mp1i ⊢ ( 𝜑 → Fun RingHom )
22 incom ⊢ ( Ring ∩ 𝑈 ) = ( 𝑈 ∩ Ring )
23 3 22 eqtrdi ⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Ring ) )
24 inex1g ⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∩ Ring ) ∈ V )
25 2 24 syl ⊢ ( 𝜑 → ( 𝑈 ∩ Ring ) ∈ V )
26 23 25 eqeltrd ⊢ ( 𝜑 → 𝐵 ∈ V )
27 sqxpexg ⊢ ( 𝐵 ∈ V → ( 𝐵 × 𝐵 ) ∈ V )
28 26 27 syl ⊢ ( 𝜑 → ( 𝐵 × 𝐵 ) ∈ V )
29 resfunexg ⊢ ( ( Fun RingHom ∧ ( 𝐵 × 𝐵 ) ∈ V ) → ( RingHom ↾ ( 𝐵 × 𝐵 ) ) ∈ V )
30 21 28 29 syl2anc ⊢ ( 𝜑 → ( RingHom ↾ ( 𝐵 × 𝐵 ) ) ∈ V )
31 4 30 eqeltrd ⊢ ( 𝜑 → 𝐻 ∈ V )
32 ringrng ⊢ ( 𝑟 ∈ Ring → 𝑟 ∈ Rng )
33 32 a1i ⊢ ( 𝜑 → ( 𝑟 ∈ Ring → 𝑟 ∈ Rng ) )
34 33 ssrdv ⊢ ( 𝜑 → Ring ⊆ Rng )
35 34 ssrind ⊢ ( 𝜑 → ( Ring ∩ 𝑈 ) ⊆ ( Rng ∩ 𝑈 ) )
36 incom ⊢ ( 𝑈 ∩ Rng ) = ( Rng ∩ 𝑈 )
37 36 a1i ⊢ ( 𝜑 → ( 𝑈 ∩ Rng ) = ( Rng ∩ 𝑈 ) )
38 35 3 37 3sstr4d ⊢ ( 𝜑 → 𝐵 ⊆ ( 𝑈 ∩ Rng ) )
39 8 10 17 18 31 38 estrres ⊢ ( 𝜑 → ( ( 𝐶 ↾s 𝐵 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ( comp ‘ ( ExtStrCat ‘ 𝑈 ) ) ⟩ } )
40 eqid ⊢ ( 𝐶 ↾cat 𝐻 ) = ( 𝐶 ↾cat 𝐻 )
41 fvexd ⊢ ( 𝜑 → ( RngCat ‘ 𝑈 ) ∈ V )
42 1 41 eqeltrid ⊢ ( 𝜑 → 𝐶 ∈ V )
43 23 4 rhmresfn ⊢ ( 𝜑 → 𝐻 Fn ( 𝐵 × 𝐵 ) )
44 40 42 26 43 rescval2 ⊢ ( 𝜑 → ( 𝐶 ↾cat 𝐻 ) = ( ( 𝐶 ↾s 𝐵 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
45 eqid ⊢ ( RingCat ‘ 𝑈 ) = ( RingCat ‘ 𝑈 )
46 45 2 23 4 7 dfringc2 ⊢ ( 𝜑 → ( RingCat ‘ 𝑈 ) = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ( comp ‘ ( ExtStrCat ‘ 𝑈 ) ) ⟩ } )
47 39 44 46 3eqtr4d ⊢ ( 𝜑 → ( 𝐶 ↾cat 𝐻 ) = ( RingCat ‘ 𝑈 ) )