This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 RngHom 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 RngHom 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 ) = ( RngHom |` ( B X. B ) ) )
13 7 4 10 12 rnghmsubcsetc 
 |-  ( ph -> ( Hom ` R ) e. ( Subcat ` ( ExtStrCat ` U ) ) )
14 eqid 
 |-  ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) = ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) )
15 eqid 
 |-  ( Base ` ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) ) = ( Base ` ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) )
16 1 4 8 12 rngcval 
 |-  ( ph -> R = ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) )
17 16 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) ) )
18 3 17 eqtrid 
 |-  ( ph -> B = ( Base ` ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) ) )
19 18 reseq2d 
 |-  ( ph -> ( _I |` B ) = ( _I |` ( Base ` ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) ) ) )
20 5 19 eqtrd 
 |-  ( ph -> F = ( _I |` ( Base ` ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) ) ) )
21 18 adantr 
 |-  ( ( ph /\ x e. B ) -> B = ( Base ` ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) ) )
22 12 oveqdr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( Hom ` R ) y ) = ( x ( RngHom |` ( B X. B ) ) y ) )
23 ovres 
 |-  ( ( x e. B /\ y e. B ) -> ( x ( RngHom |` ( B X. B ) ) y ) = ( x RngHom y ) )
24 23 adantl 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( RngHom |` ( B X. B ) ) y ) = ( x RngHom y ) )
25 22 24 eqtr2d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x RngHom y ) = ( x ( Hom ` R ) y ) )
26 25 reseq2d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( _I |` ( x RngHom y ) ) = ( _I |` ( x ( Hom ` R ) y ) ) )
27 18 21 26 mpoeq123dva 
 |-  ( ph -> ( x e. B , y e. B |-> ( _I |` ( x RngHom y ) ) ) = ( x e. ( Base ` ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) ) , y e. ( Base ` ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) ) |-> ( _I |` ( x ( Hom ` R ) y ) ) ) )
28 6 27 eqtrd 
 |-  ( ph -> G = ( x e. ( Base ` ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) ) , y e. ( Base ` ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) ) |-> ( _I |` ( x ( Hom ` R ) y ) ) ) )
29 13 14 15 20 28 inclfusubc 
 |-  ( ph -> F ( ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) Func ( ExtStrCat ` U ) ) G )
30 2 a1i 
 |-  ( ph -> E = ( ExtStrCat ` U ) )
31 16 30 oveq12d 
 |-  ( ph -> ( R Func E ) = ( ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) Func ( ExtStrCat ` U ) ) )
32 31 breqd 
 |-  ( ph -> ( F ( R Func E ) G <-> F ( ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) Func ( ExtStrCat ` U ) ) G ) )
33 29 32 mpbird 
 |-  ( ph -> F ( R Func E ) G )