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 ) ) ) )