Metamath Proof Explorer

Theorem rngchomrnghmresALTV

Description: The value of the functionalized Hom-set operation in the category of non-unital rings (in a universe) as restriction of the non-unital ring homomorphisms. (Contributed by AV, 2-Mar-2020) (New usage is discouraged.)

Ref Expression
Hypotheses rngchomrnghmresALTV.c 
|- C = ( RngCatALTV ` U )
rngchomrnghmresALTV.b 
|- B = ( Rng i^i U )
rngchomrnghmresALTV.u 
|- ( ph -> U e. V )
rngchomrnghmresALTV.f 
|- F = ( Homf ` C )
Assertion rngchomrnghmresALTV 
|- ( ph -> F = ( RngHomo |` ( B X. B ) ) )

Proof

Step Hyp Ref Expression
1 rngchomrnghmresALTV.c 
 |-  C = ( RngCatALTV ` U )
2 rngchomrnghmresALTV.b 
 |-  B = ( Rng i^i U )
3 rngchomrnghmresALTV.u 
 |-  ( ph -> U e. V )
4 rngchomrnghmresALTV.f 
 |-  F = ( Homf ` C )
5 eqid 
 |-  ( Base ` C ) = ( Base ` C )
6 1 5 3 rngcbasALTV 
 |-  ( ph -> ( Base ` C ) = ( U i^i Rng ) )
7 inss2 
 |-  ( U i^i Rng ) C_ Rng
8 6 7 eqsstrdi 
 |-  ( ph -> ( Base ` C ) C_ Rng )
9 resmpo 
 |-  ( ( ( Base ` C ) C_ Rng /\ ( Base ` C ) C_ Rng ) -> ( ( x e. Rng , y e. Rng |-> ( x RngHomo y ) ) |` ( ( Base ` C ) X. ( Base ` C ) ) ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x RngHomo y ) ) )
10 8 8 9 syl2anc 
 |-  ( ph -> ( ( x e. Rng , y e. Rng |-> ( x RngHomo y ) ) |` ( ( Base ` C ) X. ( Base ` C ) ) ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x RngHomo y ) ) )
11 df-rnghomo 
 |-  RngHomo = ( r e. Rng , s e. Rng |-> [_ ( Base ` r ) / v ]_ [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | A. x e. v A. y e. v ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) } )
12 ovex 
 |-  ( w ^m v ) e. _V
13 12 rabex 
 |-  { f e. ( w ^m v ) | A. x e. v A. y e. v ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) } e. _V
14 13 csbex 
 |-  [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | A. x e. v A. y e. v ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) } e. _V
15 14 csbex 
 |-  [_ ( Base ` r ) / v ]_ [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | A. x e. v A. y e. v ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) } e. _V
16 11 15 fnmpoi 
 |-  RngHomo Fn ( Rng X. Rng )
17 16 a1i 
 |-  ( ph -> RngHomo Fn ( Rng X. Rng ) )
18 fnov 
 |-  ( RngHomo Fn ( Rng X. Rng ) <-> RngHomo = ( x e. Rng , y e. Rng |-> ( x RngHomo y ) ) )
19 17 18 sylib 
 |-  ( ph -> RngHomo = ( x e. Rng , y e. Rng |-> ( x RngHomo y ) ) )
20 incom 
 |-  ( U i^i Rng ) = ( Rng i^i U )
21 20 a1i 
 |-  ( ph -> ( U i^i Rng ) = ( Rng i^i U ) )
22 2 a1i 
 |-  ( ph -> B = ( Rng i^i U ) )
23 21 6 22 3eqtr4rd 
 |-  ( ph -> B = ( Base ` C ) )
24 23 sqxpeqd 
 |-  ( ph -> ( B X. B ) = ( ( Base ` C ) X. ( Base ` C ) ) )
25 19 24 reseq12d 
 |-  ( ph -> ( RngHomo |` ( B X. B ) ) = ( ( x e. Rng , y e. Rng |-> ( x RngHomo y ) ) |` ( ( Base ` C ) X. ( Base ` C ) ) ) )
26 1 5 3 4 rngchomffvalALTV 
 |-  ( ph -> F = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x RngHomo y ) ) )
27 10 25 26 3eqtr4rd 
 |-  ( ph -> F = ( RngHomo |` ( B X. B ) ) )