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