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 ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
rngcrescrhm.c ⊢ 𝐶 = ( RngCat ‘ 𝑈 )
rngcrescrhm.r ⊢ ( 𝜑 → 𝑅 = ( Ring ∩ 𝑈 ) )
rngcrescrhm.h ⊢ 𝐻 = ( RingHom ↾ ( 𝑅 × 𝑅 ) )
Assertion rhmsubc ( 𝜑 → 𝐻 ∈ ( Subcat ‘ ( RngCat ‘ 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 rngcrescrhm.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
2 rngcrescrhm.c ⊢ 𝐶 = ( RngCat ‘ 𝑈 )
3 rngcrescrhm.r ⊢ ( 𝜑 → 𝑅 = ( Ring ∩ 𝑈 ) )
4 rngcrescrhm.h ⊢ 𝐻 = ( RingHom ↾ ( 𝑅 × 𝑅 ) )
5 eqidd ⊢ ( 𝜑 → ( Rng ∩ 𝑈 ) = ( Rng ∩ 𝑈 ) )
6 1 3 5 rhmsscrnghm ⊢ ( 𝜑 → ( RingHom ↾ ( 𝑅 × 𝑅 ) ) ⊆cat ( RngHomo ↾ ( ( Rng ∩ 𝑈 ) × ( Rng ∩ 𝑈 ) ) ) )
7 4 a1i ⊢ ( 𝜑 → 𝐻 = ( RingHom ↾ ( 𝑅 × 𝑅 ) ) )
8 2 a1i ⊢ ( 𝜑 → 𝐶 = ( RngCat ‘ 𝑈 ) )
9 8 eqcomd ⊢ ( 𝜑 → ( RngCat ‘ 𝑈 ) = 𝐶 )
10 9 fveq2d ⊢ ( 𝜑 → ( Homf ‘ ( RngCat ‘ 𝑈 ) ) = ( Homf ‘ 𝐶 ) )
11 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
12 2 11 1 rngchomfeqhom ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Hom ‘ 𝐶 ) )
13 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
14 2 11 1 13 rngchomfval ⊢ ( 𝜑 → ( Hom ‘ 𝐶 ) = ( RngHomo ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) )
15 2 11 1 rngcbas ⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( 𝑈 ∩ Rng ) )
16 incom ⊢ ( 𝑈 ∩ Rng ) = ( Rng ∩ 𝑈 )
17 15 16 eqtrdi ⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( Rng ∩ 𝑈 ) )
18 17 sqxpeqd ⊢ ( 𝜑 → ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) = ( ( Rng ∩ 𝑈 ) × ( Rng ∩ 𝑈 ) ) )
19 18 reseq2d ⊢ ( 𝜑 → ( RngHomo ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) = ( RngHomo ↾ ( ( Rng ∩ 𝑈 ) × ( Rng ∩ 𝑈 ) ) ) )
20 14 19 eqtrd ⊢ ( 𝜑 → ( Hom ‘ 𝐶 ) = ( RngHomo ↾ ( ( Rng ∩ 𝑈 ) × ( Rng ∩ 𝑈 ) ) ) )
21 10 12 20 3eqtrd ⊢ ( 𝜑 → ( Homf ‘ ( RngCat ‘ 𝑈 ) ) = ( RngHomo ↾ ( ( Rng ∩ 𝑈 ) × ( Rng ∩ 𝑈 ) ) ) )
22 6 7 21 3brtr4d ⊢ ( 𝜑 → 𝐻 ⊆cat ( Homf ‘ ( RngCat ‘ 𝑈 ) ) )
23 1 2 3 4 rhmsubclem3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → ( ( Id ‘ ( RngCat ‘ 𝑈 ) ) ‘ 𝑥 ) ∈ ( 𝑥 𝐻 𝑥 ) )
24 1 2 3 4 rhmsubclem4 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( RngCat ‘ 𝑈 ) ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
25 24 ralrimivva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( RngCat ‘ 𝑈 ) ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
26 25 ralrimivva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → ∀ 𝑦 ∈ 𝑅 ∀ 𝑧 ∈ 𝑅 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( RngCat ‘ 𝑈 ) ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
27 23 26 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → ( ( ( Id ‘ ( RngCat ‘ 𝑈 ) ) ‘ 𝑥 ) ∈ ( 𝑥 𝐻 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑅 ∀ 𝑧 ∈ 𝑅 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( RngCat ‘ 𝑈 ) ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ) )
28 27 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑅 ( ( ( Id ‘ ( RngCat ‘ 𝑈 ) ) ‘ 𝑥 ) ∈ ( 𝑥 𝐻 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑅 ∀ 𝑧 ∈ 𝑅 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( RngCat ‘ 𝑈 ) ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ) )
29 eqid ⊢ ( Homf ‘ ( RngCat ‘ 𝑈 ) ) = ( Homf ‘ ( RngCat ‘ 𝑈 ) )
30 eqid ⊢ ( Id ‘ ( RngCat ‘ 𝑈 ) ) = ( Id ‘ ( RngCat ‘ 𝑈 ) )
31 eqid ⊢ ( comp ‘ ( RngCat ‘ 𝑈 ) ) = ( comp ‘ ( RngCat ‘ 𝑈 ) )
32 eqid ⊢ ( RngCat ‘ 𝑈 ) = ( RngCat ‘ 𝑈 )
33 32 rngccat ⊢ ( 𝑈 ∈ 𝑉 → ( RngCat ‘ 𝑈 ) ∈ Cat )
34 1 33 syl ⊢ ( 𝜑 → ( RngCat ‘ 𝑈 ) ∈ Cat )
35 1 2 3 4 rhmsubclem1 ⊢ ( 𝜑 → 𝐻 Fn ( 𝑅 × 𝑅 ) )
36 29 30 31 34 35 issubc2 ⊢ ( 𝜑 → ( 𝐻 ∈ ( Subcat ‘ ( RngCat ‘ 𝑈 ) ) ↔ ( 𝐻 ⊆cat ( Homf ‘ ( RngCat ‘ 𝑈 ) ) ∧ ∀ 𝑥 ∈ 𝑅 ( ( ( Id ‘ ( RngCat ‘ 𝑈 ) ) ‘ 𝑥 ) ∈ ( 𝑥 𝐻 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑅 ∀ 𝑧 ∈ 𝑅 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( RngCat ‘ 𝑈 ) ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ) ) ) )
37 22 28 36 mpbir2and ⊢ ( 𝜑 → 𝐻 ∈ ( Subcat ‘ ( RngCat ‘ 𝑈 ) ) )