Metamath Proof Explorer

Theorem rhmsscmap

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

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