Metamath Proof Explorer

Theorem funcrngcsetc

Description: The "natural forgetful functor" from the category of non-unital rings into the category of sets which sends each non-unital ring to its underlying set (base set) and the morphisms (non-unital ring homomorphisms) to mappings of the corresponding base sets. An alternate proof is provided in funcrngcsetcALT , using cofuval2 to construct the "natural forgetful functor" from the category of non-unital rings into the category of sets by composing the "inclusion functor" from the category of non-unital rings into the category of extensible structures, see rngcifuestrc , and the "natural forgetful functor" from the category of extensible structures into the category of sets, see funcestrcsetc . (Contributed by AV, 26-Mar-2020)

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

Proof

Step Hyp Ref Expression
1 funcrngcsetc.r 
 |-  R = ( RngCat ` U )
2 funcrngcsetc.s 
 |-  S = ( SetCat ` U )
3 funcrngcsetc.b 
 |-  B = ( Base ` R )
4 funcrngcsetc.u 
 |-  ( ph -> U e. WUni )
5 funcrngcsetc.f 
 |-  ( ph -> F = ( x e. B |-> ( Base ` x ) ) )
6 funcrngcsetc.g 
 |-  ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RngHomo 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 rngcbas 
 |-  ( ph -> ( Base ` R ) = ( U i^i Rng ) )
19 incom 
 |-  ( U i^i Rng ) = ( Rng i^i U )
20 18 19 eqtrdi 
 |-  ( ph -> ( Base ` R ) = ( Rng i^i U ) )
21 eqid 
 |-  ( Hom ` R ) = ( Hom ` R )
22 1 17 4 21 rngchomfval 
 |-  ( ph -> ( Hom ` R ) = ( RngHomo |` ( ( Base ` R ) X. ( Base ` R ) ) ) )
23 7 4 20 22 rnghmsubcsetc 
 |-  ( 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 rnghmresfn 
 |-  ( 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 Rng ) 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 RngHomo y ) = ( a RngHomo y ) )
41 40 reseq2d 
 |-  ( x = a -> ( _I |` ( x RngHomo y ) ) = ( _I |` ( a RngHomo y ) ) )
42 oveq2 
 |-  ( y = b -> ( a RngHomo y ) = ( a RngHomo b ) )
43 42 reseq2d 
 |-  ( y = b -> ( _I |` ( a RngHomo y ) ) = ( _I |` ( a RngHomo b ) ) )
44 41 43 cbvmpov 
 |-  ( x e. B , y e. B |-> ( _I |` ( x RngHomo y ) ) ) = ( a e. B , b e. B |-> ( _I |` ( a RngHomo b ) ) )
45 44 a1i 
 |-  ( ph -> ( x e. B , y e. B |-> ( _I |` ( x RngHomo y ) ) ) = ( a e. B , b e. B |-> ( _I |` ( a RngHomo 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 rngchom 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( a ( Hom ` R ) b ) = ( a RngHomo 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 RngHomo b ) ) )
70 eqid 
 |-  ( Base ` a ) = ( Base ` a )
71 eqid 
 |-  ( Base ` b ) = ( Base ` b )
72 70 71 rnghmf 
 |-  ( f e. ( a RngHomo 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 RngHomo b ) -> f e. ( ( Base ` b ) ^m ( Base ` a ) ) ) )
80 79 ssrdv 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( a RngHomo b ) C_ ( ( Base ` b ) ^m ( Base ` a ) ) )
81 80 resabs1d 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( ( _I |` ( ( Base ` b ) ^m ( Base ` a ) ) ) |` ( a RngHomo b ) ) = ( _I |` ( a RngHomo b ) ) )
82 64 69 81 3eqtrrd 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( _I |` ( a RngHomo 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 RngHomo 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 rngcval 
 |-  ( 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 )