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 ⊢ 𝐶 = ( RngCat ‘ 𝑈 )
rhmsubcrngc.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
rhmsubcrngc.b ⊢ ( 𝜑 → 𝐵 = ( Ring ∩ 𝑈 ) )
rhmsubcrngc.h ⊢ ( 𝜑 → 𝐻 = ( RingHom ↾ ( 𝐵 × 𝐵 ) ) )
Assertion rhmsubcrngc ( 𝜑 → 𝐻 ∈ ( Subcat ‘ 𝐶 ) )

Proof

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