Metamath Proof Explorer

Theorem rngcifuestrc

Description: The "inclusion functor" from the category of non-unital rings into the category of extensible structures. (Contributed by AV, 30-Mar-2020)

Ref Expression
Hypotheses rngcifuestrc.r 
|- R = ( RngCat ` U )
rngcifuestrc.e 
|- E = ( ExtStrCat ` U )
rngcifuestrc.b 
|- B = ( Base ` R )
rngcifuestrc.u 
|- ( ph -> U e. V )
rngcifuestrc.f 
|- ( ph -> F = ( _I |` B ) )
rngcifuestrc.g 
|- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RngHomo y ) ) ) )
Assertion rngcifuestrc 
|- ( ph -> F ( R Func E ) G )

Proof

Step Hyp Ref Expression
1 rngcifuestrc.r 
 |-  R = ( RngCat ` U )
2 rngcifuestrc.e 
 |-  E = ( ExtStrCat ` U )
3 rngcifuestrc.b 
 |-  B = ( Base ` R )
4 rngcifuestrc.u 
 |-  ( ph -> U e. V )
5 rngcifuestrc.f 
 |-  ( ph -> F = ( _I |` B ) )
6 rngcifuestrc.g 
 |-  ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RngHomo y ) ) ) )
7 eqid 
 |-  ( ExtStrCat ` U ) = ( ExtStrCat ` U )
8 1 3 4 rngcbas 
 |-  ( ph -> B = ( U i^i Rng ) )
9 incom 
 |-  ( U i^i Rng ) = ( Rng i^i U )
10 8 9 eqtrdi 
 |-  ( ph -> B = ( Rng i^i U ) )
11 eqid 
 |-  ( Hom ` R ) = ( Hom ` R )
12 1 3 4 11 rngchomfval 
 |-  ( ph -> ( Hom ` R ) = ( RngHomo |` ( B X. B ) ) )
13 7 4 10 12 rnghmsubcsetc 
 |-  ( ph -> ( Hom ` R ) e. ( Subcat ` ( ExtStrCat ` U ) ) )
14 13 idi 
 |-  ( ph -> ( Hom ` R ) e. ( Subcat ` ( ExtStrCat ` U ) ) )
15 eqid 
 |-  ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) = ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) )
16 eqid 
 |-  ( Base ` ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) ) = ( Base ` ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) )
17 1 4 8 12 rngcval 
 |-  ( ph -> R = ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) )
18 17 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) ) )
19 3 18 syl5eq 
 |-  ( ph -> B = ( Base ` ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) ) )
20 19 reseq2d 
 |-  ( ph -> ( _I |` B ) = ( _I |` ( Base ` ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) ) ) )
21 5 20 eqtrd 
 |-  ( ph -> F = ( _I |` ( Base ` ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) ) ) )
22 19 adantr 
 |-  ( ( ph /\ x e. B ) -> B = ( Base ` ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) ) )
23 12 oveqdr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( Hom ` R ) y ) = ( x ( RngHomo |` ( B X. B ) ) y ) )
24 ovres 
 |-  ( ( x e. B /\ y e. B ) -> ( x ( RngHomo |` ( B X. B ) ) y ) = ( x RngHomo y ) )
25 24 adantl 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( RngHomo |` ( B X. B ) ) y ) = ( x RngHomo y ) )
26 23 25 eqtr2d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x RngHomo y ) = ( x ( Hom ` R ) y ) )
27 26 reseq2d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( _I |` ( x RngHomo y ) ) = ( _I |` ( x ( Hom ` R ) y ) ) )
28 19 22 27 mpoeq123dva 
 |-  ( ph -> ( x e. B , y e. B |-> ( _I |` ( x RngHomo y ) ) ) = ( x e. ( Base ` ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) ) , y e. ( Base ` ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) ) |-> ( _I |` ( x ( Hom ` R ) y ) ) ) )
29 6 28 eqtrd 
 |-  ( ph -> G = ( x e. ( Base ` ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) ) , y e. ( Base ` ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) ) |-> ( _I |` ( x ( Hom ` R ) y ) ) ) )
30 14 15 16 21 29 inclfusubc 
 |-  ( ph -> F ( ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) Func ( ExtStrCat ` U ) ) G )
31 2 a1i 
 |-  ( ph -> E = ( ExtStrCat ` U ) )
32 17 31 oveq12d 
 |-  ( ph -> ( R Func E ) = ( ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) Func ( ExtStrCat ` U ) ) )
33 32 breqd 
 |-  ( ph -> ( F ( R Func E ) G <-> F ( ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) Func ( ExtStrCat ` U ) ) G ) )
34 30 33 mpbird 
 |-  ( ph -> F ( R Func E ) G )