Metamath Proof Explorer

Theorem funcrngcsetcALT

Description: Alternate proof of funcrngcsetc , 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 . Surprisingly, this proof is longer than the direct proof given in funcrngcsetc . (Contributed by AV, 30-Mar-2020) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 funcrngcsetcALT.r 
 |-  R = ( RngCat ` U )
2 funcrngcsetcALT.s 
 |-  S = ( SetCat ` U )
3 funcrngcsetcALT.b 
 |-  B = ( Base ` R )
4 funcrngcsetcALT.u 
 |-  ( ph -> U e. WUni )
5 funcrngcsetcALT.f 
 |-  ( ph -> F = ( x e. B |-> ( Base ` x ) ) )
6 funcrngcsetcALT.g 
 |-  ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RngHom y ) ) ) )
7 fveq2 
 |-  ( x = u -> ( Base ` x ) = ( Base ` u ) )
8 7 cbvmptv 
 |-  ( x e. B |-> ( Base ` x ) ) = ( u e. B |-> ( Base ` u ) )
9 5 8 eqtrdi 
 |-  ( ph -> F = ( u e. B |-> ( Base ` u ) ) )
10 coires1 
 |-  ( ( u e. U |-> ( Base ` u ) ) o. ( _I |` B ) ) = ( ( u e. U |-> ( Base ` u ) ) |` B )
11 1 3 4 rngcbas 
 |-  ( ph -> B = ( U i^i Rng ) )
12 11 eleq2d 
 |-  ( ph -> ( x e. B <-> x e. ( U i^i Rng ) ) )
13 elin 
 |-  ( x e. ( U i^i Rng ) <-> ( x e. U /\ x e. Rng ) )
14 13 simplbi 
 |-  ( x e. ( U i^i Rng ) -> x e. U )
15 12 14 biimtrdi 
 |-  ( ph -> ( x e. B -> x e. U ) )
16 15 ssrdv 
 |-  ( ph -> B C_ U )
17 16 resmptd 
 |-  ( ph -> ( ( u e. U |-> ( Base ` u ) ) |` B ) = ( u e. B |-> ( Base ` u ) ) )
18 10 17 eqtr2id 
 |-  ( ph -> ( u e. B |-> ( Base ` u ) ) = ( ( u e. U |-> ( Base ` u ) ) o. ( _I |` B ) ) )
19 9 18 eqtrd 
 |-  ( ph -> F = ( ( u e. U |-> ( Base ` u ) ) o. ( _I |` B ) ) )
20 coires1 
 |-  ( ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) o. ( _I |` ( x RngHom y ) ) ) = ( ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) |` ( x RngHom y ) )
21 eqid 
 |-  ( Base ` x ) = ( Base ` x )
22 eqid 
 |-  ( Base ` y ) = ( Base ` y )
23 21 22 rnghmf 
 |-  ( z e. ( x RngHom y ) -> z : ( Base ` x ) --> ( Base ` y ) )
24 fvex 
 |-  ( Base ` y ) e. _V
25 fvex 
 |-  ( Base ` x ) e. _V
26 24 25 pm3.2i 
 |-  ( ( Base ` y ) e. _V /\ ( Base ` x ) e. _V )
27 elmapg 
 |-  ( ( ( Base ` y ) e. _V /\ ( Base ` x ) e. _V ) -> ( z e. ( ( Base ` y ) ^m ( Base ` x ) ) <-> z : ( Base ` x ) --> ( Base ` y ) ) )
28 26 27 mp1i 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( z e. ( ( Base ` y ) ^m ( Base ` x ) ) <-> z : ( Base ` x ) --> ( Base ` y ) ) )
29 23 28 imbitrrid 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( z e. ( x RngHom y ) -> z e. ( ( Base ` y ) ^m ( Base ` x ) ) ) )
30 29 ssrdv 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( x RngHom y ) C_ ( ( Base ` y ) ^m ( Base ` x ) ) )
31 30 resabs1d 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) |` ( x RngHom y ) ) = ( _I |` ( x RngHom y ) ) )
32 20 31 eqtr2id 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( _I |` ( x RngHom y ) ) = ( ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) o. ( _I |` ( x RngHom y ) ) ) )
33 32 mpoeq3dva 
 |-  ( ph -> ( x e. B , y e. B |-> ( _I |` ( x RngHom y ) ) ) = ( x e. B , y e. B |-> ( ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) o. ( _I |` ( x RngHom y ) ) ) ) )
34 6 33 eqtrd 
 |-  ( ph -> G = ( x e. B , y e. B |-> ( ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) o. ( _I |` ( x RngHom y ) ) ) ) )
35 3 a1i 
 |-  ( ph -> B = ( Base ` R ) )
36 3 a1i 
 |-  ( ( ph /\ x e. B ) -> B = ( Base ` R ) )
37 fvresi 
 |-  ( x e. B -> ( ( _I |` B ) ` x ) = x )
38 37 adantr 
 |-  ( ( x e. B /\ y e. B ) -> ( ( _I |` B ) ` x ) = x )
39 38 adantl 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( _I |` B ) ` x ) = x )
40 fvresi 
 |-  ( y e. B -> ( ( _I |` B ) ` y ) = y )
41 40 adantl 
 |-  ( ( x e. B /\ y e. B ) -> ( ( _I |` B ) ` y ) = y )
42 41 adantl 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( _I |` B ) ` y ) = y )
43 39 42 oveq12d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( ( _I |` B ) ` x ) ( w e. U , z e. U |-> ( _I |` ( ( Base ` z ) ^m ( Base ` w ) ) ) ) ( ( _I |` B ) ` y ) ) = ( x ( w e. U , z e. U |-> ( _I |` ( ( Base ` z ) ^m ( Base ` w ) ) ) ) y ) )
44 eqidd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( w e. U , z e. U |-> ( _I |` ( ( Base ` z ) ^m ( Base ` w ) ) ) ) = ( w e. U , z e. U |-> ( _I |` ( ( Base ` z ) ^m ( Base ` w ) ) ) ) )
45 simprr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( w = x /\ z = y ) ) -> z = y )
46 45 fveq2d 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( w = x /\ z = y ) ) -> ( Base ` z ) = ( Base ` y ) )
47 simprl 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( w = x /\ z = y ) ) -> w = x )
48 47 fveq2d 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( w = x /\ z = y ) ) -> ( Base ` w ) = ( Base ` x ) )
49 46 48 oveq12d 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( w = x /\ z = y ) ) -> ( ( Base ` z ) ^m ( Base ` w ) ) = ( ( Base ` y ) ^m ( Base ` x ) ) )
50 49 reseq2d 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( w = x /\ z = y ) ) -> ( _I |` ( ( Base ` z ) ^m ( Base ` w ) ) ) = ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) )
51 15 com12 
 |-  ( x e. B -> ( ph -> x e. U ) )
52 51 adantr 
 |-  ( ( x e. B /\ y e. B ) -> ( ph -> x e. U ) )
53 52 impcom 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> x e. U )
54 11 eleq2d 
 |-  ( ph -> ( y e. B <-> y e. ( U i^i Rng ) ) )
55 elin 
 |-  ( y e. ( U i^i Rng ) <-> ( y e. U /\ y e. Rng ) )
56 55 simplbi 
 |-  ( y e. ( U i^i Rng ) -> y e. U )
57 54 56 biimtrdi 
 |-  ( ph -> ( y e. B -> y e. U ) )
58 57 a1d 
 |-  ( ph -> ( x e. B -> ( y e. B -> y e. U ) ) )
59 58 imp32 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> y e. U )
60 ovex 
 |-  ( ( Base ` y ) ^m ( Base ` x ) ) e. _V
61 60 a1i 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( Base ` y ) ^m ( Base ` x ) ) e. _V )
62 61 resiexd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) e. _V )
63 44 50 53 59 62 ovmpod 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( w e. U , z e. U |-> ( _I |` ( ( Base ` z ) ^m ( Base ` w ) ) ) ) y ) = ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) )
64 43 63 eqtr2d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) = ( ( ( _I |` B ) ` x ) ( w e. U , z e. U |-> ( _I |` ( ( Base ` z ) ^m ( Base ` w ) ) ) ) ( ( _I |` B ) ` y ) ) )
65 eqidd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( f e. B , g e. B |-> ( _I |` ( f RngHom g ) ) ) = ( f e. B , g e. B |-> ( _I |` ( f RngHom g ) ) ) )
66 oveq12 
 |-  ( ( f = x /\ g = y ) -> ( f RngHom g ) = ( x RngHom y ) )
67 66 reseq2d 
 |-  ( ( f = x /\ g = y ) -> ( _I |` ( f RngHom g ) ) = ( _I |` ( x RngHom y ) ) )
68 67 adantl 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( f = x /\ g = y ) ) -> ( _I |` ( f RngHom g ) ) = ( _I |` ( x RngHom y ) ) )
69 simprl 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> x e. B )
70 simprr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> y e. B )
71 ovex 
 |-  ( x RngHom y ) e. _V
72 71 a1i 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x RngHom y ) e. _V )
73 72 resiexd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( _I |` ( x RngHom y ) ) e. _V )
74 65 68 69 70 73 ovmpod 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( f e. B , g e. B |-> ( _I |` ( f RngHom g ) ) ) y ) = ( _I |` ( x RngHom y ) ) )
75 74 eqcomd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( _I |` ( x RngHom y ) ) = ( x ( f e. B , g e. B |-> ( _I |` ( f RngHom g ) ) ) y ) )
76 64 75 coeq12d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) o. ( _I |` ( x RngHom y ) ) ) = ( ( ( ( _I |` B ) ` x ) ( w e. U , z e. U |-> ( _I |` ( ( Base ` z ) ^m ( Base ` w ) ) ) ) ( ( _I |` B ) ` y ) ) o. ( x ( f e. B , g e. B |-> ( _I |` ( f RngHom g ) ) ) y ) ) )
77 35 36 76 mpoeq123dva 
 |-  ( ph -> ( x e. B , y e. B |-> ( ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) o. ( _I |` ( x RngHom y ) ) ) ) = ( x e. ( Base ` R ) , y e. ( Base ` R ) |-> ( ( ( ( _I |` B ) ` x ) ( w e. U , z e. U |-> ( _I |` ( ( Base ` z ) ^m ( Base ` w ) ) ) ) ( ( _I |` B ) ` y ) ) o. ( x ( f e. B , g e. B |-> ( _I |` ( f RngHom g ) ) ) y ) ) ) )
78 34 77 eqtrd 
 |-  ( ph -> G = ( x e. ( Base ` R ) , y e. ( Base ` R ) |-> ( ( ( ( _I |` B ) ` x ) ( w e. U , z e. U |-> ( _I |` ( ( Base ` z ) ^m ( Base ` w ) ) ) ) ( ( _I |` B ) ` y ) ) o. ( x ( f e. B , g e. B |-> ( _I |` ( f RngHom g ) ) ) y ) ) ) )
79 19 78 opeq12d 
 |-  ( ph -> <. F , G >. = <. ( ( u e. U |-> ( Base ` u ) ) o. ( _I |` B ) ) , ( x e. ( Base ` R ) , y e. ( Base ` R ) |-> ( ( ( ( _I |` B ) ` x ) ( w e. U , z e. U |-> ( _I |` ( ( Base ` z ) ^m ( Base ` w ) ) ) ) ( ( _I |` B ) ` y ) ) o. ( x ( f e. B , g e. B |-> ( _I |` ( f RngHom g ) ) ) y ) ) ) >. )
80 eqid 
 |-  ( Base ` R ) = ( Base ` R )
81 eqid 
 |-  ( ExtStrCat ` U ) = ( ExtStrCat ` U )
82 eqidd 
 |-  ( ph -> ( _I |` B ) = ( _I |` B ) )
83 eqidd 
 |-  ( ph -> ( f e. B , g e. B |-> ( _I |` ( f RngHom g ) ) ) = ( f e. B , g e. B |-> ( _I |` ( f RngHom g ) ) ) )
84 1 81 3 4 82 83 rngcifuestrc 
 |-  ( ph -> ( _I |` B ) ( R Func ( ExtStrCat ` U ) ) ( f e. B , g e. B |-> ( _I |` ( f RngHom g ) ) ) )
85 eqid 
 |-  ( Base ` ( ExtStrCat ` U ) ) = ( Base ` ( ExtStrCat ` U ) )
86 eqid 
 |-  ( Base ` S ) = ( Base ` S )
87 81 4 estrcbas 
 |-  ( ph -> U = ( Base ` ( ExtStrCat ` U ) ) )
88 87 mpteq1d 
 |-  ( ph -> ( u e. U |-> ( Base ` u ) ) = ( u e. ( Base ` ( ExtStrCat ` U ) ) |-> ( Base ` u ) ) )
89 fveq2 
 |-  ( w = u -> ( Base ` w ) = ( Base ` u ) )
90 89 oveq2d 
 |-  ( w = u -> ( ( Base ` z ) ^m ( Base ` w ) ) = ( ( Base ` z ) ^m ( Base ` u ) ) )
91 90 reseq2d 
 |-  ( w = u -> ( _I |` ( ( Base ` z ) ^m ( Base ` w ) ) ) = ( _I |` ( ( Base ` z ) ^m ( Base ` u ) ) ) )
92 fveq2 
 |-  ( z = v -> ( Base ` z ) = ( Base ` v ) )
93 92 oveq1d 
 |-  ( z = v -> ( ( Base ` z ) ^m ( Base ` u ) ) = ( ( Base ` v ) ^m ( Base ` u ) ) )
94 93 reseq2d 
 |-  ( z = v -> ( _I |` ( ( Base ` z ) ^m ( Base ` u ) ) ) = ( _I |` ( ( Base ` v ) ^m ( Base ` u ) ) ) )
95 91 94 cbvmpov 
 |-  ( w e. U , z e. U |-> ( _I |` ( ( Base ` z ) ^m ( Base ` w ) ) ) ) = ( u e. U , v e. U |-> ( _I |` ( ( Base ` v ) ^m ( Base ` u ) ) ) )
96 95 a1i 
 |-  ( ph -> ( w e. U , z e. U |-> ( _I |` ( ( Base ` z ) ^m ( Base ` w ) ) ) ) = ( u e. U , v e. U |-> ( _I |` ( ( Base ` v ) ^m ( Base ` u ) ) ) ) )
97 eqidd 
 |-  ( ph -> ( _I |` ( ( Base ` v ) ^m ( Base ` u ) ) ) = ( _I |` ( ( Base ` v ) ^m ( Base ` u ) ) ) )
98 87 87 97 mpoeq123dv 
 |-  ( ph -> ( u e. U , v e. U |-> ( _I |` ( ( Base ` v ) ^m ( Base ` u ) ) ) ) = ( u e. ( Base ` ( ExtStrCat ` U ) ) , v e. ( Base ` ( ExtStrCat ` U ) ) |-> ( _I |` ( ( Base ` v ) ^m ( Base ` u ) ) ) ) )
99 96 98 eqtrd 
 |-  ( ph -> ( w e. U , z e. U |-> ( _I |` ( ( Base ` z ) ^m ( Base ` w ) ) ) ) = ( u e. ( Base ` ( ExtStrCat ` U ) ) , v e. ( Base ` ( ExtStrCat ` U ) ) |-> ( _I |` ( ( Base ` v ) ^m ( Base ` u ) ) ) ) )
100 81 2 85 86 4 88 99 funcestrcsetc 
 |-  ( ph -> ( u e. U |-> ( Base ` u ) ) ( ( ExtStrCat ` U ) Func S ) ( w e. U , z e. U |-> ( _I |` ( ( Base ` z ) ^m ( Base ` w ) ) ) ) )
101 80 84 100 cofuval2 
 |-  ( ph -> ( <. ( u e. U |-> ( Base ` u ) ) , ( w e. U , z e. U |-> ( _I |` ( ( Base ` z ) ^m ( Base ` w ) ) ) ) >. o.func <. ( _I |` B ) , ( f e. B , g e. B |-> ( _I |` ( f RngHom g ) ) ) >. ) = <. ( ( u e. U |-> ( Base ` u ) ) o. ( _I |` B ) ) , ( x e. ( Base ` R ) , y e. ( Base ` R ) |-> ( ( ( ( _I |` B ) ` x ) ( w e. U , z e. U |-> ( _I |` ( ( Base ` z ) ^m ( Base ` w ) ) ) ) ( ( _I |` B ) ` y ) ) o. ( x ( f e. B , g e. B |-> ( _I |` ( f RngHom g ) ) ) y ) ) ) >. )
102 79 101 eqtr4d 
 |-  ( ph -> <. F , G >. = ( <. ( u e. U |-> ( Base ` u ) ) , ( w e. U , z e. U |-> ( _I |` ( ( Base ` z ) ^m ( Base ` w ) ) ) ) >. o.func <. ( _I |` B ) , ( f e. B , g e. B |-> ( _I |` ( f RngHom g ) ) ) >. ) )
103 df-br 
 |-  ( ( _I |` B ) ( R Func ( ExtStrCat ` U ) ) ( f e. B , g e. B |-> ( _I |` ( f RngHom g ) ) ) <-> <. ( _I |` B ) , ( f e. B , g e. B |-> ( _I |` ( f RngHom g ) ) ) >. e. ( R Func ( ExtStrCat ` U ) ) )
104 84 103 sylib 
 |-  ( ph -> <. ( _I |` B ) , ( f e. B , g e. B |-> ( _I |` ( f RngHom g ) ) ) >. e. ( R Func ( ExtStrCat ` U ) ) )
105 df-br 
 |-  ( ( u e. U |-> ( Base ` u ) ) ( ( ExtStrCat ` U ) Func S ) ( w e. U , z e. U |-> ( _I |` ( ( Base ` z ) ^m ( Base ` w ) ) ) ) <-> <. ( u e. U |-> ( Base ` u ) ) , ( w e. U , z e. U |-> ( _I |` ( ( Base ` z ) ^m ( Base ` w ) ) ) ) >. e. ( ( ExtStrCat ` U ) Func S ) )
106 100 105 sylib 
 |-  ( ph -> <. ( u e. U |-> ( Base ` u ) ) , ( w e. U , z e. U |-> ( _I |` ( ( Base ` z ) ^m ( Base ` w ) ) ) ) >. e. ( ( ExtStrCat ` U ) Func S ) )
107 104 106 cofucl 
 |-  ( ph -> ( <. ( u e. U |-> ( Base ` u ) ) , ( w e. U , z e. U |-> ( _I |` ( ( Base ` z ) ^m ( Base ` w ) ) ) ) >. o.func <. ( _I |` B ) , ( f e. B , g e. B |-> ( _I |` ( f RngHom g ) ) ) >. ) e. ( R Func S ) )
108 102 107 eqeltrd 
 |-  ( ph -> <. F , G >. e. ( R Func S ) )
109 df-br 
 |-  ( F ( R Func S ) G <-> <. F , G >. e. ( R Func S ) )
110 108 109 sylibr 
 |-  ( ph -> F ( R Func S ) G )