Metamath Proof Explorer

Theorem rhmsscrnghm

Description: The unital ring homomorphisms between unital rings (in a universe) are a subcategory subset of the non-unital ring homomorphisms between non-unital rings (in the same universe). (Contributed by AV, 1-Mar-2020)

Ref Expression
Hypotheses rhmsscrnghm.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
rhmsscrnghm.r ⊢ ( 𝜑 → 𝑅 = ( Ring ∩ 𝑈 ) )
rhmsscrnghm.s ⊢ ( 𝜑 → 𝑆 = ( Rng ∩ 𝑈 ) )
Assertion rhmsscrnghm ( 𝜑 → ( RingHom ↾ ( 𝑅 × 𝑅 ) ) ⊆cat ( RngHomo ↾ ( 𝑆 × 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 rhmsscrnghm.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
2 rhmsscrnghm.r ⊢ ( 𝜑 → 𝑅 = ( Ring ∩ 𝑈 ) )
3 rhmsscrnghm.s ⊢ ( 𝜑 → 𝑆 = ( Rng ∩ 𝑈 ) )
4 ringrng ⊢ ( 𝑟 ∈ Ring → 𝑟 ∈ Rng )
5 4 a1i ⊢ ( 𝜑 → ( 𝑟 ∈ Ring → 𝑟 ∈ Rng ) )
6 5 ssrdv ⊢ ( 𝜑 → Ring ⊆ Rng )
7 6 ssrind ⊢ ( 𝜑 → ( Ring ∩ 𝑈 ) ⊆ ( Rng ∩ 𝑈 ) )
8 7 2 3 3sstr4d ⊢ ( 𝜑 → 𝑅 ⊆ 𝑆 )
9 ovres ⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) → ( 𝑥 ( RingHom ↾ ( 𝑅 × 𝑅 ) ) 𝑦 ) = ( 𝑥 RingHom 𝑦 ) )
10 9 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( 𝑥 ( RingHom ↾ ( 𝑅 × 𝑅 ) ) 𝑦 ) = ( 𝑥 RingHom 𝑦 ) )
11 10 eleq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ℎ ∈ ( 𝑥 ( RingHom ↾ ( 𝑅 × 𝑅 ) ) 𝑦 ) ↔ ℎ ∈ ( 𝑥 RingHom 𝑦 ) ) )
12 rhmisrnghm ⊢ ( ℎ ∈ ( 𝑥 RingHom 𝑦 ) → ℎ ∈ ( 𝑥 RngHomo 𝑦 ) )
13 8 sseld ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑅 → 𝑥 ∈ 𝑆 ) )
14 8 sseld ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑅 → 𝑦 ∈ 𝑆 ) )
15 13 14 anim12d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) → ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) )
16 15 imp ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) )
17 ovres ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 ( RngHomo ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) = ( 𝑥 RngHomo 𝑦 ) )
18 16 17 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( 𝑥 ( RngHomo ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) = ( 𝑥 RngHomo 𝑦 ) )
19 18 eleq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ℎ ∈ ( 𝑥 ( RngHomo ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) ↔ ℎ ∈ ( 𝑥 RngHomo 𝑦 ) ) )
20 12 19 syl5ibr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ℎ ∈ ( 𝑥 RingHom 𝑦 ) → ℎ ∈ ( 𝑥 ( RngHomo ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) ) )
21 11 20 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ℎ ∈ ( 𝑥 ( RingHom ↾ ( 𝑅 × 𝑅 ) ) 𝑦 ) → ℎ ∈ ( 𝑥 ( RngHomo ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) ) )
22 21 ssrdv ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( 𝑥 ( RingHom ↾ ( 𝑅 × 𝑅 ) ) 𝑦 ) ⊆ ( 𝑥 ( RngHomo ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) )
23 22 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝑥 ( RingHom ↾ ( 𝑅 × 𝑅 ) ) 𝑦 ) ⊆ ( 𝑥 ( RngHomo ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) )
24 inss1 ⊢ ( Ring ∩ 𝑈 ) ⊆ Ring
25 2 24 eqsstrdi ⊢ ( 𝜑 → 𝑅 ⊆ Ring )
26 xpss12 ⊢ ( ( 𝑅 ⊆ Ring ∧ 𝑅 ⊆ Ring ) → ( 𝑅 × 𝑅 ) ⊆ ( Ring × Ring ) )
27 25 25 26 syl2anc ⊢ ( 𝜑 → ( 𝑅 × 𝑅 ) ⊆ ( Ring × Ring ) )
28 rhmfn ⊢ RingHom Fn ( Ring × Ring )
29 fnssresb ⊢ ( RingHom Fn ( Ring × Ring ) → ( ( RingHom ↾ ( 𝑅 × 𝑅 ) ) Fn ( 𝑅 × 𝑅 ) ↔ ( 𝑅 × 𝑅 ) ⊆ ( Ring × Ring ) ) )
30 28 29 mp1i ⊢ ( 𝜑 → ( ( RingHom ↾ ( 𝑅 × 𝑅 ) ) Fn ( 𝑅 × 𝑅 ) ↔ ( 𝑅 × 𝑅 ) ⊆ ( Ring × Ring ) ) )
31 27 30 mpbird ⊢ ( 𝜑 → ( RingHom ↾ ( 𝑅 × 𝑅 ) ) Fn ( 𝑅 × 𝑅 ) )
32 inss1 ⊢ ( Rng ∩ 𝑈 ) ⊆ Rng
33 3 32 eqsstrdi ⊢ ( 𝜑 → 𝑆 ⊆ Rng )
34 xpss12 ⊢ ( ( 𝑆 ⊆ Rng ∧ 𝑆 ⊆ Rng ) → ( 𝑆 × 𝑆 ) ⊆ ( Rng × Rng ) )
35 33 33 34 syl2anc ⊢ ( 𝜑 → ( 𝑆 × 𝑆 ) ⊆ ( Rng × Rng ) )
36 rnghmfn ⊢ RngHomo Fn ( Rng × Rng )
37 fnssresb ⊢ ( RngHomo Fn ( Rng × Rng ) → ( ( RngHomo ↾ ( 𝑆 × 𝑆 ) ) Fn ( 𝑆 × 𝑆 ) ↔ ( 𝑆 × 𝑆 ) ⊆ ( Rng × Rng ) ) )
38 36 37 mp1i ⊢ ( 𝜑 → ( ( RngHomo ↾ ( 𝑆 × 𝑆 ) ) Fn ( 𝑆 × 𝑆 ) ↔ ( 𝑆 × 𝑆 ) ⊆ ( Rng × Rng ) ) )
39 35 38 mpbird ⊢ ( 𝜑 → ( RngHomo ↾ ( 𝑆 × 𝑆 ) ) Fn ( 𝑆 × 𝑆 ) )
40 incom ⊢ ( Rng ∩ 𝑈 ) = ( 𝑈 ∩ Rng )
41 inex1g ⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∩ Rng ) ∈ V )
42 40 41 eqeltrid ⊢ ( 𝑈 ∈ 𝑉 → ( Rng ∩ 𝑈 ) ∈ V )
43 1 42 syl ⊢ ( 𝜑 → ( Rng ∩ 𝑈 ) ∈ V )
44 3 43 eqeltrd ⊢ ( 𝜑 → 𝑆 ∈ V )
45 31 39 44 isssc ⊢ ( 𝜑 → ( ( RingHom ↾ ( 𝑅 × 𝑅 ) ) ⊆cat ( RngHomo ↾ ( 𝑆 × 𝑆 ) ) ↔ ( 𝑅 ⊆ 𝑆 ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝑥 ( RingHom ↾ ( 𝑅 × 𝑅 ) ) 𝑦 ) ⊆ ( 𝑥 ( RngHomo ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) ) ) )
46 8 23 45 mpbir2and ⊢ ( 𝜑 → ( RingHom ↾ ( 𝑅 × 𝑅 ) ) ⊆cat ( RngHomo ↾ ( 𝑆 × 𝑆 ) ) )