Metamath Proof Explorer


Theorem funcringcsetc

Description: The "natural forgetful functor" from the category of unital rings into the category of sets which sends each ring to its underlying set (base set) and the morphisms (ring homomorphisms) to mappings of the corresponding base sets. (Contributed by AV, 26-Mar-2020)

Ref Expression
Hypotheses funcringcsetc.r
|- R = ( RingCat ` U )
funcringcsetc.s
|- S = ( SetCat ` U )
funcringcsetc.b
|- B = ( Base ` R )
funcringcsetc.u
|- ( ph -> U e. WUni )
funcringcsetc.f
|- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )
funcringcsetc.g
|- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) )
Assertion funcringcsetc
|- ( ph -> F ( R Func S ) G )

Proof

Step Hyp Ref Expression
1 funcringcsetc.r
 |-  R = ( RingCat ` U )
2 funcringcsetc.s
 |-  S = ( SetCat ` U )
3 funcringcsetc.b
 |-  B = ( Base ` R )
4 funcringcsetc.u
 |-  ( ph -> U e. WUni )
5 funcringcsetc.f
 |-  ( ph -> F = ( x e. B |-> ( Base ` x ) ) )
6 funcringcsetc.g
 |-  ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) )
7 eqid
 |-  ( ExtStrCat ` U ) = ( ExtStrCat ` U )
8 eqid
 |-  ( Base ` ( ExtStrCat ` U ) ) = ( Base ` ( ExtStrCat ` U ) )
9 eqid
 |-  ( Base ` S ) = ( Base ` S )
10 7 4 estrcbas
 |-  ( ph -> U = ( Base ` ( ExtStrCat ` U ) ) )
11 10 mpteq1d
 |-  ( ph -> ( x e. U |-> ( Base ` x ) ) = ( x e. ( Base ` ( ExtStrCat ` U ) ) |-> ( Base ` x ) ) )
12 mpoeq12
 |-  ( ( U = ( Base ` ( ExtStrCat ` U ) ) /\ U = ( Base ` ( ExtStrCat ` U ) ) ) -> ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) = ( x e. ( Base ` ( ExtStrCat ` U ) ) , y e. ( Base ` ( ExtStrCat ` U ) ) |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) )
13 10 10 12 syl2anc
 |-  ( ph -> ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) = ( x e. ( Base ` ( ExtStrCat ` U ) ) , y e. ( Base ` ( ExtStrCat ` U ) ) |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) )
14 7 2 8 9 4 11 13 funcestrcsetc
 |-  ( ph -> ( x e. U |-> ( Base ` x ) ) ( ( ExtStrCat ` U ) Func S ) ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) )
15 df-br
 |-  ( ( x e. U |-> ( Base ` x ) ) ( ( ExtStrCat ` U ) Func S ) ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) <-> <. ( x e. U |-> ( Base ` x ) ) , ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) >. e. ( ( ExtStrCat ` U ) Func S ) )
16 14 15 sylib
 |-  ( ph -> <. ( x e. U |-> ( Base ` x ) ) , ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) >. e. ( ( ExtStrCat ` U ) Func S ) )
17 eqid
 |-  ( Base ` R ) = ( Base ` R )
18 1 17 4 ringcbas
 |-  ( ph -> ( Base ` R ) = ( U i^i Ring ) )
19 incom
 |-  ( U i^i Ring ) = ( Ring i^i U )
20 18 19 syl6eq
 |-  ( ph -> ( Base ` R ) = ( Ring i^i U ) )
21 eqid
 |-  ( Hom ` R ) = ( Hom ` R )
22 1 17 4 21 ringchomfval
 |-  ( ph -> ( Hom ` R ) = ( RingHom |` ( ( Base ` R ) X. ( Base ` R ) ) ) )
23 7 4 20 22 rhmsubcsetc
 |-  ( ph -> ( Hom ` R ) e. ( Subcat ` ( ExtStrCat ` U ) ) )
24 16 23 funcres
 |-  ( ph -> ( <. ( x e. U |-> ( Base ` x ) ) , ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) >. |`f ( Hom ` R ) ) e. ( ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) Func S ) )
25 mptexg
 |-  ( U e. WUni -> ( x e. U |-> ( Base ` x ) ) e. _V )
26 4 25 syl
 |-  ( ph -> ( x e. U |-> ( Base ` x ) ) e. _V )
27 fvex
 |-  ( Hom ` R ) e. _V
28 27 a1i
 |-  ( ph -> ( Hom ` R ) e. _V )
29 mpoexga
 |-  ( ( U e. WUni /\ U e. WUni ) -> ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) e. _V )
30 4 4 29 syl2anc
 |-  ( ph -> ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) e. _V )
31 18 22 rhmresfn
 |-  ( ph -> ( Hom ` R ) Fn ( ( Base ` R ) X. ( Base ` R ) ) )
32 26 28 30 31 resfval2
 |-  ( ph -> ( <. ( x e. U |-> ( Base ` x ) ) , ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) >. |`f ( Hom ` R ) ) = <. ( ( x e. U |-> ( Base ` x ) ) |` ( Base ` R ) ) , ( a e. ( Base ` R ) , b e. ( Base ` R ) |-> ( ( a ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) b ) |` ( a ( Hom ` R ) b ) ) ) >. )
33 inss1
 |-  ( U i^i Ring ) C_ U
34 18 33 eqsstrdi
 |-  ( ph -> ( Base ` R ) C_ U )
35 34 resmptd
 |-  ( ph -> ( ( x e. U |-> ( Base ` x ) ) |` ( Base ` R ) ) = ( x e. ( Base ` R ) |-> ( Base ` x ) ) )
36 3 a1i
 |-  ( ph -> B = ( Base ` R ) )
37 36 mpteq1d
 |-  ( ph -> ( x e. B |-> ( Base ` x ) ) = ( x e. ( Base ` R ) |-> ( Base ` x ) ) )
38 5 37 eqtr2d
 |-  ( ph -> ( x e. ( Base ` R ) |-> ( Base ` x ) ) = F )
39 35 38 eqtrd
 |-  ( ph -> ( ( x e. U |-> ( Base ` x ) ) |` ( Base ` R ) ) = F )
40 oveq1
 |-  ( x = a -> ( x RingHom y ) = ( a RingHom y ) )
41 40 reseq2d
 |-  ( x = a -> ( _I |` ( x RingHom y ) ) = ( _I |` ( a RingHom y ) ) )
42 oveq2
 |-  ( y = b -> ( a RingHom y ) = ( a RingHom b ) )
43 42 reseq2d
 |-  ( y = b -> ( _I |` ( a RingHom y ) ) = ( _I |` ( a RingHom b ) ) )
44 41 43 cbvmpov
 |-  ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) = ( a e. B , b e. B |-> ( _I |` ( a RingHom b ) ) )
45 44 a1i
 |-  ( ph -> ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) = ( a e. B , b e. B |-> ( _I |` ( a RingHom b ) ) ) )
46 3 a1i
 |-  ( ( ph /\ a e. B ) -> B = ( Base ` R ) )
47 eqidd
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) = ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) )
48 fveq2
 |-  ( y = b -> ( Base ` y ) = ( Base ` b ) )
49 fveq2
 |-  ( x = a -> ( Base ` x ) = ( Base ` a ) )
50 48 49 oveqan12rd
 |-  ( ( x = a /\ y = b ) -> ( ( Base ` y ) ^m ( Base ` x ) ) = ( ( Base ` b ) ^m ( Base ` a ) ) )
51 50 reseq2d
 |-  ( ( x = a /\ y = b ) -> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) = ( _I |` ( ( Base ` b ) ^m ( Base ` a ) ) ) )
52 51 adantl
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) ) /\ ( x = a /\ y = b ) ) -> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) = ( _I |` ( ( Base ` b ) ^m ( Base ` a ) ) ) )
53 3 34 eqsstrid
 |-  ( ph -> B C_ U )
54 53 sseld
 |-  ( ph -> ( a e. B -> a e. U ) )
55 54 com12
 |-  ( a e. B -> ( ph -> a e. U ) )
56 55 adantr
 |-  ( ( a e. B /\ b e. B ) -> ( ph -> a e. U ) )
57 56 impcom
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> a e. U )
58 53 sseld
 |-  ( ph -> ( b e. B -> b e. U ) )
59 58 adantld
 |-  ( ph -> ( ( a e. B /\ b e. B ) -> b e. U ) )
60 59 imp
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> b e. U )
61 ovexd
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( ( Base ` b ) ^m ( Base ` a ) ) e. _V )
62 61 resiexd
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( _I |` ( ( Base ` b ) ^m ( Base ` a ) ) ) e. _V )
63 47 52 57 60 62 ovmpod
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( a ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) b ) = ( _I |` ( ( Base ` b ) ^m ( Base ` a ) ) ) )
64 63 reseq1d
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( ( a ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) b ) |` ( a ( Hom ` R ) b ) ) = ( ( _I |` ( ( Base ` b ) ^m ( Base ` a ) ) ) |` ( a ( Hom ` R ) b ) ) )
65 4 adantr
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> U e. WUni )
66 simprl
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> a e. B )
67 simprr
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> b e. B )
68 1 3 65 21 66 67 ringchom
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( a ( Hom ` R ) b ) = ( a RingHom b ) )
69 68 reseq2d
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( ( _I |` ( ( Base ` b ) ^m ( Base ` a ) ) ) |` ( a ( Hom ` R ) b ) ) = ( ( _I |` ( ( Base ` b ) ^m ( Base ` a ) ) ) |` ( a RingHom b ) ) )
70 eqid
 |-  ( Base ` a ) = ( Base ` a )
71 eqid
 |-  ( Base ` b ) = ( Base ` b )
72 70 71 rhmf
 |-  ( f e. ( a RingHom b ) -> f : ( Base ` a ) --> ( Base ` b ) )
73 fvex
 |-  ( Base ` b ) e. _V
74 fvex
 |-  ( Base ` a ) e. _V
75 73 74 pm3.2i
 |-  ( ( Base ` b ) e. _V /\ ( Base ` a ) e. _V )
76 75 a1i
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( ( Base ` b ) e. _V /\ ( Base ` a ) e. _V ) )
77 elmapg
 |-  ( ( ( Base ` b ) e. _V /\ ( Base ` a ) e. _V ) -> ( f e. ( ( Base ` b ) ^m ( Base ` a ) ) <-> f : ( Base ` a ) --> ( Base ` b ) ) )
78 76 77 syl
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( f e. ( ( Base ` b ) ^m ( Base ` a ) ) <-> f : ( Base ` a ) --> ( Base ` b ) ) )
79 72 78 syl5ibr
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( f e. ( a RingHom b ) -> f e. ( ( Base ` b ) ^m ( Base ` a ) ) ) )
80 79 ssrdv
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( a RingHom b ) C_ ( ( Base ` b ) ^m ( Base ` a ) ) )
81 80 resabs1d
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( ( _I |` ( ( Base ` b ) ^m ( Base ` a ) ) ) |` ( a RingHom b ) ) = ( _I |` ( a RingHom b ) ) )
82 64 69 81 3eqtrrd
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( _I |` ( a RingHom b ) ) = ( ( a ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) b ) |` ( a ( Hom ` R ) b ) ) )
83 36 46 82 mpoeq123dva
 |-  ( ph -> ( a e. B , b e. B |-> ( _I |` ( a RingHom b ) ) ) = ( a e. ( Base ` R ) , b e. ( Base ` R ) |-> ( ( a ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) b ) |` ( a ( Hom ` R ) b ) ) ) )
84 6 45 83 3eqtrrd
 |-  ( ph -> ( a e. ( Base ` R ) , b e. ( Base ` R ) |-> ( ( a ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) b ) |` ( a ( Hom ` R ) b ) ) ) = G )
85 39 84 opeq12d
 |-  ( ph -> <. ( ( x e. U |-> ( Base ` x ) ) |` ( Base ` R ) ) , ( a e. ( Base ` R ) , b e. ( Base ` R ) |-> ( ( a ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) b ) |` ( a ( Hom ` R ) b ) ) ) >. = <. F , G >. )
86 32 85 eqtr2d
 |-  ( ph -> <. F , G >. = ( <. ( x e. U |-> ( Base ` x ) ) , ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) >. |`f ( Hom ` R ) ) )
87 1 4 18 22 ringcval
 |-  ( ph -> R = ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) )
88 87 oveq1d
 |-  ( ph -> ( R Func S ) = ( ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) Func S ) )
89 24 86 88 3eltr4d
 |-  ( ph -> <. F , G >. e. ( R Func S ) )
90 df-br
 |-  ( F ( R Func S ) G <-> <. F , G >. e. ( R Func S ) )
91 89 90 sylibr
 |-  ( ph -> F ( R Func S ) G )