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