Metamath Proof Explorer

Theorem rhmsubcrngc

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

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

Proof

Step Hyp Ref Expression
1 rhmsubcrngc.c ⊢ C = RngCat ⁡ U
2 rhmsubcrngc.u ⊢ φ → U ∈ V
3 rhmsubcrngc.b ⊢ φ → B = Ring ∩ U
4 rhmsubcrngc.h ⊢ φ → H = RingHom ↾ B × B
5 eqid ⊢ RngCat ⁡ U = RngCat ⁡ U
6 eqid ⊢ Base RngCat ⁡ U = Base RngCat ⁡ U
7 5 6 2 rngcbas ⊢ φ → Base RngCat ⁡ U = U ∩ Rng
8 incom ⊢ U ∩ Rng = Rng ∩ U
9 7 8 eqtrdi ⊢ φ → Base RngCat ⁡ U = Rng ∩ U
10 2 3 9 rhmsscrnghm ⊢ φ → RingHom ↾ B × B ⊆ cat RngHomo ↾ Base RngCat ⁡ U × Base RngCat ⁡ U
11 1 a1i ⊢ φ → C = RngCat ⁡ U
12 11 fveq2d ⊢ φ → Base C = Base RngCat ⁡ U
13 12 sqxpeqd ⊢ φ → Base C × Base C = Base RngCat ⁡ U × Base RngCat ⁡ U
14 13 reseq2d ⊢ φ → RngHomo ↾ Base C × Base C = RngHomo ↾ Base RngCat ⁡ U × Base RngCat ⁡ U
15 10 14 breqtrrd ⊢ φ → RingHom ↾ B × B ⊆ cat RngHomo ↾ Base C × Base C
16 eqid ⊢ Base C = Base C
17 1 16 2 rngchomfeqhom ⊢ φ → Hom 𝑓 ⁡ C = Hom ⁡ C
18 eqid ⊢ Hom ⁡ C = Hom ⁡ C
19 1 16 2 18 rngchomfval ⊢ φ → Hom ⁡ C = RngHomo ↾ Base C × Base C
20 17 19 eqtrd ⊢ φ → Hom 𝑓 ⁡ C = RngHomo ↾ Base C × Base C
21 15 4 20 3brtr4d ⊢ φ → H ⊆ cat Hom 𝑓 ⁡ C
22 1 2 3 4 rhmsubcrngclem1 ⊢ φ ∧ x ∈ B → Id ⁡ C ⁡ x ∈ x H x
23 1 2 3 4 rhmsubcrngclem2 ⊢ φ ∧ x ∈ B → ∀ y ∈ B ∀ z ∈ B ∀ f ∈ x H y ∀ g ∈ y H z g x y comp ⁡ C z f ∈ x H z
24 22 23 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
25 24 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
26 eqid ⊢ Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ C
27 eqid ⊢ Id ⁡ C = Id ⁡ C
28 eqid ⊢ comp ⁡ C = comp ⁡ C
29 1 rngccat ⊢ U ∈ V → C ∈ Cat
30 2 29 syl ⊢ φ → C ∈ Cat
31 incom ⊢ Ring ∩ U = U ∩ Ring
32 3 31 eqtrdi ⊢ φ → B = U ∩ Ring
33 32 4 rhmresfn ⊢ φ → H Fn B × B
34 26 27 28 30 33 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
35 21 25 34 mpbir2and ⊢ φ → H ∈ Subcat ⁡ C