Metamath Proof Explorer

Theorem rhmsubc

Description: According to df-subc , the subcategories ( SubcatC ) of a category C are subsets of the homomorphisms of C (see subcssc and subcss2 ). Therefore, the set of unital ring homomorphisms is a "subcategory" of the category of non-unital rings. (Contributed by AV, 2-Mar-2020)

Ref Expression
Hypotheses rngcrescrhm.u ⊢ φ → U ∈ V
rngcrescrhm.c ⊢ C = RngCat ⁡ U
rngcrescrhm.r ⊢ φ → R = Ring ∩ U
rngcrescrhm.h ⊢ H = RingHom ↾ R × R
Assertion rhmsubc ⊢ φ → H ∈ Subcat ⁡ RngCat ⁡ U

Proof

Step Hyp Ref Expression
1 rngcrescrhm.u ⊢ φ → U ∈ V
2 rngcrescrhm.c ⊢ C = RngCat ⁡ U
3 rngcrescrhm.r ⊢ φ → R = Ring ∩ U
4 rngcrescrhm.h ⊢ H = RingHom ↾ R × R
5 eqidd ⊢ φ → Rng ∩ U = Rng ∩ U
6 1 3 5 rhmsscrnghm ⊢ φ → RingHom ↾ R × R ⊆ cat RngHomo ↾ Rng ∩ U × Rng ∩ U
7 4 a1i ⊢ φ → H = RingHom ↾ R × R
8 2 a1i ⊢ φ → C = RngCat ⁡ U
9 8 eqcomd ⊢ φ → RngCat ⁡ U = C
10 9 fveq2d ⊢ φ → Hom 𝑓 ⁡ RngCat ⁡ U = Hom 𝑓 ⁡ C
11 eqid ⊢ Base C = Base C
12 2 11 1 rngchomfeqhom ⊢ φ → Hom 𝑓 ⁡ C = Hom ⁡ C
13 eqid ⊢ Hom ⁡ C = Hom ⁡ C
14 2 11 1 13 rngchomfval ⊢ φ → Hom ⁡ C = RngHomo ↾ Base C × Base C
15 2 11 1 rngcbas ⊢ φ → Base C = U ∩ Rng
16 incom ⊢ U ∩ Rng = Rng ∩ U
17 15 16 eqtrdi ⊢ φ → Base C = Rng ∩ U
18 17 sqxpeqd ⊢ φ → Base C × Base C = Rng ∩ U × Rng ∩ U
19 18 reseq2d ⊢ φ → RngHomo ↾ Base C × Base C = RngHomo ↾ Rng ∩ U × Rng ∩ U
20 14 19 eqtrd ⊢ φ → Hom ⁡ C = RngHomo ↾ Rng ∩ U × Rng ∩ U
21 10 12 20 3eqtrd ⊢ φ → Hom 𝑓 ⁡ RngCat ⁡ U = RngHomo ↾ Rng ∩ U × Rng ∩ U
22 6 7 21 3brtr4d ⊢ φ → H ⊆ cat Hom 𝑓 ⁡ RngCat ⁡ U
23 1 2 3 4 rhmsubclem3 ⊢ φ ∧ x ∈ R → Id ⁡ RngCat ⁡ U ⁡ x ∈ x H x
24 1 2 3 4 rhmsubclem4 ⊢ φ ∧ x ∈ R ∧ y ∈ R ∧ z ∈ R ∧ f ∈ x H y ∧ g ∈ y H z → g x y comp ⁡ RngCat ⁡ U z f ∈ x H z
25 24 ralrimivva ⊢ φ ∧ x ∈ R ∧ y ∈ R ∧ z ∈ R → ∀ f ∈ x H y ∀ g ∈ y H z g x y comp ⁡ RngCat ⁡ U z f ∈ x H z
26 25 ralrimivva ⊢ φ ∧ x ∈ R → ∀ y ∈ R ∀ z ∈ R ∀ f ∈ x H y ∀ g ∈ y H z g x y comp ⁡ RngCat ⁡ U z f ∈ x H z
27 23 26 jca ⊢ φ ∧ x ∈ R → Id ⁡ RngCat ⁡ U ⁡ x ∈ x H x ∧ ∀ y ∈ R ∀ z ∈ R ∀ f ∈ x H y ∀ g ∈ y H z g x y comp ⁡ RngCat ⁡ U z f ∈ x H z
28 27 ralrimiva ⊢ φ → ∀ x ∈ R Id ⁡ RngCat ⁡ U ⁡ x ∈ x H x ∧ ∀ y ∈ R ∀ z ∈ R ∀ f ∈ x H y ∀ g ∈ y H z g x y comp ⁡ RngCat ⁡ U z f ∈ x H z
29 eqid ⊢ Hom 𝑓 ⁡ RngCat ⁡ U = Hom 𝑓 ⁡ RngCat ⁡ U
30 eqid ⊢ Id ⁡ RngCat ⁡ U = Id ⁡ RngCat ⁡ U
31 eqid ⊢ comp ⁡ RngCat ⁡ U = comp ⁡ RngCat ⁡ U
32 eqid ⊢ RngCat ⁡ U = RngCat ⁡ U
33 32 rngccat ⊢ U ∈ V → RngCat ⁡ U ∈ Cat
34 1 33 syl ⊢ φ → RngCat ⁡ U ∈ Cat
35 1 2 3 4 rhmsubclem1 ⊢ φ → H Fn R × R
36 29 30 31 34 35 issubc2 ⊢ φ → H ∈ Subcat ⁡ RngCat ⁡ U ↔ H ⊆ cat Hom 𝑓 ⁡ RngCat ⁡ U ∧ ∀ x ∈ R Id ⁡ RngCat ⁡ U ⁡ x ∈ x H x ∧ ∀ y ∈ R ∀ z ∈ R ∀ f ∈ x H y ∀ g ∈ y H z g x y comp ⁡ RngCat ⁡ U z f ∈ x H z
37 22 28 36 mpbir2and ⊢ φ → H ∈ Subcat ⁡ RngCat ⁡ U