Metamath Proof Explorer

Theorem rhmsscmap2

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

Ref Expression
Hypotheses rhmsscmap.u 
|- ( ph -> U e. V )
rhmsscmap.r 
|- ( ph -> R = ( Ring i^i U ) )
Assertion rhmsscmap2 
|- ( ph -> ( RingHom |` ( R X. R ) ) C_cat ( x e. R , y e. R |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) )

Proof

Step Hyp Ref Expression
1 rhmsscmap.u 
 |-  ( ph -> U e. V )
2 rhmsscmap.r 
 |-  ( ph -> R = ( Ring i^i U ) )
3 ssidd 
 |-  ( ph -> R C_ R )
4 eqid 
 |-  ( Base ` a ) = ( Base ` a )
5 eqid 
 |-  ( Base ` b ) = ( Base ` b )
6 4 5 rhmf 
 |-  ( h e. ( a RingHom b ) -> h : ( Base ` a ) --> ( Base ` b ) )
7 simpr 
 |-  ( ( ( ph /\ ( a e. R /\ b e. R ) ) /\ h : ( Base ` a ) --> ( Base ` b ) ) -> h : ( Base ` a ) --> ( Base ` b ) )
8 fvex 
 |-  ( Base ` b ) e. _V
9 fvex 
 |-  ( Base ` a ) e. _V
10 8 9 pm3.2i 
 |-  ( ( Base ` b ) e. _V /\ ( Base ` a ) e. _V )
11 elmapg 
 |-  ( ( ( Base ` b ) e. _V /\ ( Base ` a ) e. _V ) -> ( h e. ( ( Base ` b ) ^m ( Base ` a ) ) <-> h : ( Base ` a ) --> ( Base ` b ) ) )
12 10 11 mp1i 
 |-  ( ( ( ph /\ ( a e. R /\ b e. R ) ) /\ h : ( Base ` a ) --> ( Base ` b ) ) -> ( h e. ( ( Base ` b ) ^m ( Base ` a ) ) <-> h : ( Base ` a ) --> ( Base ` b ) ) )
13 7 12 mpbird 
 |-  ( ( ( ph /\ ( a e. R /\ b e. R ) ) /\ h : ( Base ` a ) --> ( Base ` b ) ) -> h e. ( ( Base ` b ) ^m ( Base ` a ) ) )
14 13 ex 
 |-  ( ( ph /\ ( a e. R /\ b e. R ) ) -> ( h : ( Base ` a ) --> ( Base ` b ) -> h e. ( ( Base ` b ) ^m ( Base ` a ) ) ) )
15 6 14 syl5 
 |-  ( ( ph /\ ( a e. R /\ b e. R ) ) -> ( h e. ( a RingHom b ) -> h e. ( ( Base ` b ) ^m ( Base ` a ) ) ) )
16 15 ssrdv 
 |-  ( ( ph /\ ( a e. R /\ b e. R ) ) -> ( a RingHom b ) C_ ( ( Base ` b ) ^m ( Base ` a ) ) )
17 ovres 
 |-  ( ( a e. R /\ b e. R ) -> ( a ( RingHom |` ( R X. R ) ) b ) = ( a RingHom b ) )
18 17 adantl 
 |-  ( ( ph /\ ( a e. R /\ b e. R ) ) -> ( a ( RingHom |` ( R X. R ) ) b ) = ( a RingHom b ) )
19 eqidd 
 |-  ( ( a e. R /\ b e. R ) -> ( x e. R , y e. R |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) = ( x e. R , y e. R |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) )
20 fveq2 
 |-  ( y = b -> ( Base ` y ) = ( Base ` b ) )
21 fveq2 
 |-  ( x = a -> ( Base ` x ) = ( Base ` a ) )
22 20 21 oveqan12rd 
 |-  ( ( x = a /\ y = b ) -> ( ( Base ` y ) ^m ( Base ` x ) ) = ( ( Base ` b ) ^m ( Base ` a ) ) )
23 22 adantl 
 |-  ( ( ( a e. R /\ b e. R ) /\ ( x = a /\ y = b ) ) -> ( ( Base ` y ) ^m ( Base ` x ) ) = ( ( Base ` b ) ^m ( Base ` a ) ) )
24 simpl 
 |-  ( ( a e. R /\ b e. R ) -> a e. R )
25 simpr 
 |-  ( ( a e. R /\ b e. R ) -> b e. R )
26 ovexd 
 |-  ( ( a e. R /\ b e. R ) -> ( ( Base ` b ) ^m ( Base ` a ) ) e. _V )
27 19 23 24 25 26 ovmpod 
 |-  ( ( a e. R /\ b e. R ) -> ( a ( x e. R , y e. R |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) b ) = ( ( Base ` b ) ^m ( Base ` a ) ) )
28 27 adantl 
 |-  ( ( ph /\ ( a e. R /\ b e. R ) ) -> ( a ( x e. R , y e. R |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) b ) = ( ( Base ` b ) ^m ( Base ` a ) ) )
29 16 18 28 3sstr4d 
 |-  ( ( ph /\ ( a e. R /\ b e. R ) ) -> ( a ( RingHom |` ( R X. R ) ) b ) C_ ( a ( x e. R , y e. R |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) b ) )
30 29 ralrimivva 
 |-  ( ph -> A. a e. R A. b e. R ( a ( RingHom |` ( R X. R ) ) b ) C_ ( a ( x e. R , y e. R |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) b ) )
31 rhmfn 
 |-  RingHom Fn ( Ring X. Ring )
32 31 a1i 
 |-  ( ph -> RingHom Fn ( Ring X. Ring ) )
33 inss1 
 |-  ( Ring i^i U ) C_ Ring
34 2 33 eqsstrdi 
 |-  ( ph -> R C_ Ring )
35 xpss12 
 |-  ( ( R C_ Ring /\ R C_ Ring ) -> ( R X. R ) C_ ( Ring X. Ring ) )
36 34 34 35 syl2anc 
 |-  ( ph -> ( R X. R ) C_ ( Ring X. Ring ) )
37 fnssres 
 |-  ( ( RingHom Fn ( Ring X. Ring ) /\ ( R X. R ) C_ ( Ring X. Ring ) ) -> ( RingHom |` ( R X. R ) ) Fn ( R X. R ) )
38 32 36 37 syl2anc 
 |-  ( ph -> ( RingHom |` ( R X. R ) ) Fn ( R X. R ) )
39 eqid 
 |-  ( x e. R , y e. R |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) = ( x e. R , y e. R |-> ( ( Base ` y ) ^m ( Base ` x ) ) )
40 ovex 
 |-  ( ( Base ` y ) ^m ( Base ` x ) ) e. _V
41 39 40 fnmpoi 
 |-  ( x e. R , y e. R |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) Fn ( R X. R )
42 41 a1i 
 |-  ( ph -> ( x e. R , y e. R |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) Fn ( R X. R ) )
43 incom 
 |-  ( Ring i^i U ) = ( U i^i Ring )
44 inex1g 
 |-  ( U e. V -> ( U i^i Ring ) e. _V )
45 1 44 syl 
 |-  ( ph -> ( U i^i Ring ) e. _V )
46 43 45 eqeltrid 
 |-  ( ph -> ( Ring i^i U ) e. _V )
47 2 46 eqeltrd 
 |-  ( ph -> R e. _V )
48 38 42 47 isssc 
 |-  ( ph -> ( ( RingHom |` ( R X. R ) ) C_cat ( x e. R , y e. R |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) <-> ( R C_ R /\ A. a e. R A. b e. R ( a ( RingHom |` ( R X. R ) ) b ) C_ ( a ( x e. R , y e. R |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) b ) ) ) )
49 3 30 48 mpbir2and 
 |-  ( ph -> ( RingHom |` ( R X. R ) ) C_cat ( x e. R , y e. R |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) )