Metamath Proof Explorer

Theorem rhmsubcsetc

Description: The unital ring homomorphisms between unital rings (in a universe) are a subcategory of the category of extensible structures. (Contributed by AV, 9-Mar-2020)

Ref Expression
Hypotheses rhmsubcsetc.c ⊢C=ExtStrCat⁡U
rhmsubcsetc.u ⊢φ→U∈V
rhmsubcsetc.b ⊢φ→B=Ring∩U
rhmsubcsetc.h ⊢φ→H=RingHom↾B×B
Assertion rhmsubcsetc ⊢φ→H∈Subcat⁡C

Proof

Step Hyp Ref Expression
1 rhmsubcsetc.c ⊢C=ExtStrCat⁡U
2 rhmsubcsetc.u ⊢φ→U∈V
3 rhmsubcsetc.b ⊢φ→B=Ring∩U
4 rhmsubcsetc.h ⊢φ→H=RingHom↾B×B
5 2 3 rhmsscmap ⊢φ→RingHom↾B×B⊆catx∈U,y∈U⟼BaseyBasex
6 eqid ⊢Hom⁡C=Hom⁡C
7 1 2 6 estrchomfeqhom ⊢φ→Hom𝑓⁡C=Hom⁡C
8 1 2 6 estrchomfval ⊢φ→Hom⁡C=x∈U,y∈U⟼BaseyBasex
9 7 8 eqtrd ⊢φ→Hom𝑓⁡C=x∈U,y∈U⟼BaseyBasex
10 5 4 9 3brtr4d ⊢φ→H⊆catHom𝑓⁡C
11 1 2 3 4 rhmsubcsetclem1 ⊢φ∧x∈B→Id⁡C⁡x∈xHx
12 1 2 3 4 rhmsubcsetclem2 ⊢φ∧x∈B→∀y∈B∀z∈B∀f∈xHy∀g∈yHzgxycomp⁡Czf∈xHz
13 11 12 jca ⊢φ∧x∈B→Id⁡C⁡x∈xHx∧∀y∈B∀z∈B∀f∈xHy∀g∈yHzgxycomp⁡Czf∈xHz
14 13 ralrimiva ⊢φ→∀x∈BId⁡C⁡x∈xHx∧∀y∈B∀z∈B∀f∈xHy∀g∈yHzgxycomp⁡Czf∈xHz
15 eqid ⊢Hom𝑓⁡C=Hom𝑓⁡C
16 eqid ⊢Id⁡C=Id⁡C
17 eqid ⊢comp⁡C=comp⁡C
18 1 estrccat ⊢U∈V→C∈Cat
19 2 18 syl ⊢φ→C∈Cat
20 incom ⊢Ring∩U=U∩Ring
21 3 20 eqtrdi ⊢φ→B=U∩Ring
22 21 4 rhmresfn ⊢φ→HFnB×B
23 15 16 17 19 22 issubc2 ⊢φ→H∈Subcat⁡C↔H⊆catHom𝑓⁡C∧∀x∈BId⁡C⁡x∈xHx∧∀y∈B∀z∈B∀f∈xHy∀g∈yHzgxycomp⁡Czf∈xHz
24 10 14 23 mpbir2and ⊢φ→H∈Subcat⁡C