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 
|- ( ph -> U e. V )
rhmsscrnghm.r 
|- ( ph -> R = ( Ring i^i U ) )
rhmsscrnghm.s 
|- ( ph -> S = ( Rng i^i U ) )
Assertion rhmsscrnghm 
|- ( ph -> ( RingHom |` ( R X. R ) ) C_cat ( RngHomo |` ( S X. S ) ) )

Proof

Step Hyp Ref Expression
1 rhmsscrnghm.u 
 |-  ( ph -> U e. V )
2 rhmsscrnghm.r 
 |-  ( ph -> R = ( Ring i^i U ) )
3 rhmsscrnghm.s 
 |-  ( ph -> S = ( Rng i^i U ) )
4 ringrng 
 |-  ( r e. Ring -> r e. Rng )
5 4 a1i 
 |-  ( ph -> ( r e. Ring -> r e. Rng ) )
6 5 ssrdv 
 |-  ( ph -> Ring C_ Rng )
7 6 ssrind 
 |-  ( ph -> ( Ring i^i U ) C_ ( Rng i^i U ) )
8 7 2 3 3sstr4d 
 |-  ( ph -> R C_ S )
9 ovres 
 |-  ( ( x e. R /\ y e. R ) -> ( x ( RingHom |` ( R X. R ) ) y ) = ( x RingHom y ) )
10 9 adantl 
 |-  ( ( ph /\ ( x e. R /\ y e. R ) ) -> ( x ( RingHom |` ( R X. R ) ) y ) = ( x RingHom y ) )
11 10 eleq2d 
 |-  ( ( ph /\ ( x e. R /\ y e. R ) ) -> ( h e. ( x ( RingHom |` ( R X. R ) ) y ) <-> h e. ( x RingHom y ) ) )
12 rhmisrnghm 
 |-  ( h e. ( x RingHom y ) -> h e. ( x RngHomo y ) )
13 8 sseld 
 |-  ( ph -> ( x e. R -> x e. S ) )
14 8 sseld 
 |-  ( ph -> ( y e. R -> y e. S ) )
15 13 14 anim12d 
 |-  ( ph -> ( ( x e. R /\ y e. R ) -> ( x e. S /\ y e. S ) ) )
16 15 imp 
 |-  ( ( ph /\ ( x e. R /\ y e. R ) ) -> ( x e. S /\ y e. S ) )
17 ovres 
 |-  ( ( x e. S /\ y e. S ) -> ( x ( RngHomo |` ( S X. S ) ) y ) = ( x RngHomo y ) )
18 16 17 syl 
 |-  ( ( ph /\ ( x e. R /\ y e. R ) ) -> ( x ( RngHomo |` ( S X. S ) ) y ) = ( x RngHomo y ) )
19 18 eleq2d 
 |-  ( ( ph /\ ( x e. R /\ y e. R ) ) -> ( h e. ( x ( RngHomo |` ( S X. S ) ) y ) <-> h e. ( x RngHomo y ) ) )
20 12 19 syl5ibr 
 |-  ( ( ph /\ ( x e. R /\ y e. R ) ) -> ( h e. ( x RingHom y ) -> h e. ( x ( RngHomo |` ( S X. S ) ) y ) ) )
21 11 20 sylbid 
 |-  ( ( ph /\ ( x e. R /\ y e. R ) ) -> ( h e. ( x ( RingHom |` ( R X. R ) ) y ) -> h e. ( x ( RngHomo |` ( S X. S ) ) y ) ) )
22 21 ssrdv 
 |-  ( ( ph /\ ( x e. R /\ y e. R ) ) -> ( x ( RingHom |` ( R X. R ) ) y ) C_ ( x ( RngHomo |` ( S X. S ) ) y ) )
23 22 ralrimivva 
 |-  ( ph -> A. x e. R A. y e. R ( x ( RingHom |` ( R X. R ) ) y ) C_ ( x ( RngHomo |` ( S X. S ) ) y ) )
24 inss1 
 |-  ( Ring i^i U ) C_ Ring
25 2 24 eqsstrdi 
 |-  ( ph -> R C_ Ring )
26 xpss12 
 |-  ( ( R C_ Ring /\ R C_ Ring ) -> ( R X. R ) C_ ( Ring X. Ring ) )
27 25 25 26 syl2anc 
 |-  ( ph -> ( R X. R ) C_ ( Ring X. Ring ) )
28 rhmfn 
 |-  RingHom Fn ( Ring X. Ring )
29 fnssresb 
 |-  ( RingHom Fn ( Ring X. Ring ) -> ( ( RingHom |` ( R X. R ) ) Fn ( R X. R ) <-> ( R X. R ) C_ ( Ring X. Ring ) ) )
30 28 29 mp1i 
 |-  ( ph -> ( ( RingHom |` ( R X. R ) ) Fn ( R X. R ) <-> ( R X. R ) C_ ( Ring X. Ring ) ) )
31 27 30 mpbird 
 |-  ( ph -> ( RingHom |` ( R X. R ) ) Fn ( R X. R ) )
32 inss1 
 |-  ( Rng i^i U ) C_ Rng
33 3 32 eqsstrdi 
 |-  ( ph -> S C_ Rng )
34 xpss12 
 |-  ( ( S C_ Rng /\ S C_ Rng ) -> ( S X. S ) C_ ( Rng X. Rng ) )
35 33 33 34 syl2anc 
 |-  ( ph -> ( S X. S ) C_ ( Rng X. Rng ) )
36 rnghmfn 
 |-  RngHomo Fn ( Rng X. Rng )
37 fnssresb 
 |-  ( RngHomo Fn ( Rng X. Rng ) -> ( ( RngHomo |` ( S X. S ) ) Fn ( S X. S ) <-> ( S X. S ) C_ ( Rng X. Rng ) ) )
38 36 37 mp1i 
 |-  ( ph -> ( ( RngHomo |` ( S X. S ) ) Fn ( S X. S ) <-> ( S X. S ) C_ ( Rng X. Rng ) ) )
39 35 38 mpbird 
 |-  ( ph -> ( RngHomo |` ( S X. S ) ) Fn ( S X. S ) )
40 incom 
 |-  ( Rng i^i U ) = ( U i^i Rng )
41 inex1g 
 |-  ( U e. V -> ( U i^i Rng ) e. _V )
42 40 41 eqeltrid 
 |-  ( U e. V -> ( Rng i^i U ) e. _V )
43 1 42 syl 
 |-  ( ph -> ( Rng i^i U ) e. _V )
44 3 43 eqeltrd 
 |-  ( ph -> S e. _V )
45 31 39 44 isssc 
 |-  ( ph -> ( ( RingHom |` ( R X. R ) ) C_cat ( RngHomo |` ( S X. S ) ) <-> ( R C_ S /\ A. x e. R A. y e. R ( x ( RingHom |` ( R X. R ) ) y ) C_ ( x ( RngHomo |` ( S X. S ) ) y ) ) ) )
46 8 23 45 mpbir2and 
 |-  ( ph -> ( RingHom |` ( R X. R ) ) C_cat ( RngHomo |` ( S X. S ) ) )