Metamath Proof Explorer

Theorem rhmsubcALTV

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) (New usage is discouraged.)

Ref Expression
Hypotheses rngcrescrhmALTV.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
rngcrescrhmALTV.c ⊢ 𝐶 = ( RngCatALTV ‘ 𝑈 )
rngcrescrhmALTV.r ⊢ ( 𝜑 → 𝑅 = ( Ring ∩ 𝑈 ) )
rngcrescrhmALTV.h ⊢ 𝐻 = ( RingHom ↾ ( 𝑅 × 𝑅 ) )
Assertion rhmsubcALTV ( 𝜑 → 𝐻 ∈ ( Subcat ‘ ( RngCatALTV ‘ 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 rngcrescrhmALTV.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
2 rngcrescrhmALTV.c ⊢ 𝐶 = ( RngCatALTV ‘ 𝑈 )
3 rngcrescrhmALTV.r ⊢ ( 𝜑 → 𝑅 = ( Ring ∩ 𝑈 ) )
4 rngcrescrhmALTV.h ⊢ 𝐻 = ( RingHom ↾ ( 𝑅 × 𝑅 ) )
5 eqidd ⊢ ( 𝜑 → ( Rng ∩ 𝑈 ) = ( Rng ∩ 𝑈 ) )
6 1 3 5 rhmsscrnghm ⊢ ( 𝜑 → ( RingHom ↾ ( 𝑅 × 𝑅 ) ) ⊆cat ( RngHomo ↾ ( ( Rng ∩ 𝑈 ) × ( Rng ∩ 𝑈 ) ) ) )
7 4 a1i ⊢ ( 𝜑 → 𝐻 = ( RingHom ↾ ( 𝑅 × 𝑅 ) ) )
8 eqid ⊢ ( RngCatALTV ‘ 𝑈 ) = ( RngCatALTV ‘ 𝑈 )
9 eqid ⊢ ( Rng ∩ 𝑈 ) = ( Rng ∩ 𝑈 )
10 eqid ⊢ ( Homf ‘ ( RngCatALTV ‘ 𝑈 ) ) = ( Homf ‘ ( RngCatALTV ‘ 𝑈 ) )
11 8 9 1 10 rngchomrnghmresALTV ⊢ ( 𝜑 → ( Homf ‘ ( RngCatALTV ‘ 𝑈 ) ) = ( RngHomo ↾ ( ( Rng ∩ 𝑈 ) × ( Rng ∩ 𝑈 ) ) ) )
12 6 7 11 3brtr4d ⊢ ( 𝜑 → 𝐻 ⊆cat ( Homf ‘ ( RngCatALTV ‘ 𝑈 ) ) )
13 1 2 3 4 rhmsubcALTVlem3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → ( ( Id ‘ ( RngCatALTV ‘ 𝑈 ) ) ‘ 𝑥 ) ∈ ( 𝑥 𝐻 𝑥 ) )
14 1 2 3 4 rhmsubcALTVlem4 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( RngCatALTV ‘ 𝑈 ) ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
15 14 ralrimivva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( RngCatALTV ‘ 𝑈 ) ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
16 15 ralrimivva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → ∀ 𝑦 ∈ 𝑅 ∀ 𝑧 ∈ 𝑅 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( RngCatALTV ‘ 𝑈 ) ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
17 13 16 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → ( ( ( Id ‘ ( RngCatALTV ‘ 𝑈 ) ) ‘ 𝑥 ) ∈ ( 𝑥 𝐻 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑅 ∀ 𝑧 ∈ 𝑅 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( RngCatALTV ‘ 𝑈 ) ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ) )
18 17 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑅 ( ( ( Id ‘ ( RngCatALTV ‘ 𝑈 ) ) ‘ 𝑥 ) ∈ ( 𝑥 𝐻 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑅 ∀ 𝑧 ∈ 𝑅 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( RngCatALTV ‘ 𝑈 ) ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ) )
19 eqid ⊢ ( Id ‘ ( RngCatALTV ‘ 𝑈 ) ) = ( Id ‘ ( RngCatALTV ‘ 𝑈 ) )
20 eqid ⊢ ( comp ‘ ( RngCatALTV ‘ 𝑈 ) ) = ( comp ‘ ( RngCatALTV ‘ 𝑈 ) )
21 8 rngccatALTV ⊢ ( 𝑈 ∈ 𝑉 → ( RngCatALTV ‘ 𝑈 ) ∈ Cat )
22 1 21 syl ⊢ ( 𝜑 → ( RngCatALTV ‘ 𝑈 ) ∈ Cat )
23 1 2 3 4 rhmsubcALTVlem1 ⊢ ( 𝜑 → 𝐻 Fn ( 𝑅 × 𝑅 ) )
24 10 19 20 22 23 issubc2 ⊢ ( 𝜑 → ( 𝐻 ∈ ( Subcat ‘ ( RngCatALTV ‘ 𝑈 ) ) ↔ ( 𝐻 ⊆cat ( Homf ‘ ( RngCatALTV ‘ 𝑈 ) ) ∧ ∀ 𝑥 ∈ 𝑅 ( ( ( Id ‘ ( RngCatALTV ‘ 𝑈 ) ) ‘ 𝑥 ) ∈ ( 𝑥 𝐻 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑅 ∀ 𝑧 ∈ 𝑅 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( RngCatALTV ‘ 𝑈 ) ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ) ) ) )
25 12 18 24 mpbir2and ⊢ ( 𝜑 → 𝐻 ∈ ( Subcat ‘ ( RngCatALTV ‘ 𝑈 ) ) )