Metamath Proof Explorer

Theorem rnghmsubcsetc

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

Ref Expression
Hypotheses rnghmsubcsetc.c ⊢ 𝐶 = ( ExtStrCat ‘ 𝑈 )
rnghmsubcsetc.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
rnghmsubcsetc.b ⊢ ( 𝜑 → 𝐵 = ( Rng ∩ 𝑈 ) )
rnghmsubcsetc.h ⊢ ( 𝜑 → 𝐻 = ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) )
Assertion rnghmsubcsetc ( 𝜑 → 𝐻 ∈ ( Subcat ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 rnghmsubcsetc.c ⊢ 𝐶 = ( ExtStrCat ‘ 𝑈 )
2 rnghmsubcsetc.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3 rnghmsubcsetc.b ⊢ ( 𝜑 → 𝐵 = ( Rng ∩ 𝑈 ) )
4 rnghmsubcsetc.h ⊢ ( 𝜑 → 𝐻 = ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) )
5 2 3 rnghmsscmap ⊢ ( 𝜑 → ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) ⊆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 rnghmsubcsetclem1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐻 𝑥 ) )
12 1 2 3 4 rnghmsubcsetclem2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( 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 ⊢ ( Rng ∩ 𝑈 ) = ( 𝑈 ∩ Rng )
21 3 20 eqtrdi ⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Rng ) )
22 21 4 rnghmresfn ⊢ ( 𝜑 → 𝐻 Fn ( 𝐵 × 𝐵 ) )
23 15 16 17 19 22 issubc2 ⊢ ( 𝜑 → ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) ↔ ( 𝐻 ⊆cat ( Homf ‘ 𝐶 ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐻 𝑥 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ) ) ) )
24 10 14 23 mpbir2and ⊢ ( 𝜑 → 𝐻 ∈ ( Subcat ‘ 𝐶 ) )