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 ⊆ cat x ∈ U , y ∈ U ⟼ Base y Base x
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 ⟼ Base y Base x
9 7 8 eqtrd ⊢ φ → Hom 𝑓 ⁡ C = x ∈ U , y ∈ U ⟼ Base y Base x
10 5 4 9 3brtr4d ⊢ φ → H ⊆ cat Hom 𝑓 ⁡ C
11 1 2 3 4 rhmsubcsetclem1 ⊢ φ ∧ x ∈ B → Id ⁡ C ⁡ x ∈ x H x
12 1 2 3 4 rhmsubcsetclem2 ⊢ φ ∧ x ∈ B → ∀ y ∈ B ∀ z ∈ B ∀ f ∈ x H y ∀ g ∈ y H z g x y comp ⁡ C z f ∈ x H z
13 11 12 jca ⊢ φ ∧ x ∈ B → Id ⁡ C ⁡ x ∈ x H x ∧ ∀ y ∈ B ∀ z ∈ B ∀ f ∈ x H y ∀ g ∈ y H z g x y comp ⁡ C z f ∈ x H z
14 13 ralrimiva ⊢ φ → ∀ x ∈ B Id ⁡ C ⁡ x ∈ x H x ∧ ∀ y ∈ B ∀ z ∈ B ∀ f ∈ x H y ∀ g ∈ y H z g x y comp ⁡ C z f ∈ x H z
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 ⊢ φ → H Fn B × B
23 15 16 17 19 22 issubc2 ⊢ φ → H ∈ Subcat ⁡ C ↔ H ⊆ cat Hom 𝑓 ⁡ C ∧ ∀ x ∈ B Id ⁡ C ⁡ x ∈ x H x ∧ ∀ y ∈ B ∀ z ∈ B ∀ f ∈ x H y ∀ g ∈ y H z g x y comp ⁡ C z f ∈ x H z
24 10 14 23 mpbir2and ⊢ φ → H ∈ Subcat ⁡ C