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

Proof

Step Hyp Ref Expression
1 rhmsubcsetc.c ⊢ 𝐶 = ( ExtStrCat ‘ 𝑈 )
2 rhmsubcsetc.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3 rhmsubcsetc.b ⊢ ( 𝜑 → 𝐵 = ( Ring ∩ 𝑈 ) )
4 rhmsubcsetc.h ⊢ ( 𝜑 → 𝐻 = ( RingHom ↾ ( 𝐵 × 𝐵 ) ) )
5 2 3 rhmsscmap ⊢ ( 𝜑 → ( RingHom ↾ ( 𝐵 × 𝐵 ) ) ⊆cat ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) )
6 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
7 1 2 6 estrchomfeqhom ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Hom ‘ 𝐶 ) )
8 1 2 6 estrchomfval ⊢ ( 𝜑 → ( Hom ‘ 𝐶 ) = ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) )
9 7 8 eqtrd ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) )
10 5 4 9 3brtr4d ⊢ ( 𝜑 → 𝐻 ⊆cat ( Homf ‘ 𝐶 ) )
11 1 2 3 4 rhmsubcsetclem1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐻 𝑥 ) )
12 1 2 3 4 rhmsubcsetclem2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
13 11 12 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐻 𝑥 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ) )
14 13 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐻 𝑥 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ) )
15 eqid ⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
16 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
17 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
18 1 estrccat ⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ Cat )
19 2 18 syl ⊢ ( 𝜑 → 𝐶 ∈ Cat )
20 incom ⊢ ( Ring ∩ 𝑈 ) = ( 𝑈 ∩ Ring )
21 3 20 eqtrdi ⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Ring ) )
22 21 4 rhmresfn ⊢ ( 𝜑 → 𝐻 Fn ( 𝐵 × 𝐵 ) )
23 15 16 17 19 22 issubc2 ⊢ ( 𝜑 → ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) ↔ ( 𝐻 ⊆cat ( Homf ‘ 𝐶 ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐻 𝑥 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ) ) ) )
24 10 14 23 mpbir2and ⊢ ( 𝜑 → 𝐻 ∈ ( Subcat ‘ 𝐶 ) )