Metamath Proof Explorer

Theorem ringchomALTV

Description: Set of arrows of the category of rings (in a universe). (Contributed by AV, 14-Feb-2020) (New usage is discouraged.)

Ref Expression
Hypotheses ringcbasALTV.c 
|- C = ( RingCatALTV ` U )
ringcbasALTV.b 
|- B = ( Base ` C )
ringcbasALTV.u 
|- ( ph -> U e. V )
ringchomfvalALTV.h 
|- H = ( Hom ` C )
ringchomALTV.x 
|- ( ph -> X e. B )
ringchomALTV.y 
|- ( ph -> Y e. B )
Assertion ringchomALTV 
|- ( ph -> ( X H Y ) = ( X RingHom Y ) )

Proof

Step Hyp Ref Expression
1 ringcbasALTV.c 
 |-  C = ( RingCatALTV ` U )
2 ringcbasALTV.b 
 |-  B = ( Base ` C )
3 ringcbasALTV.u 
 |-  ( ph -> U e. V )
4 ringchomfvalALTV.h 
 |-  H = ( Hom ` C )
5 ringchomALTV.x 
 |-  ( ph -> X e. B )
6 ringchomALTV.y 
 |-  ( ph -> Y e. B )
7 1 2 3 4 ringchomfvalALTV 
 |-  ( ph -> H = ( x e. B , y e. B |-> ( x RingHom y ) ) )
8 oveq12 
 |-  ( ( x = X /\ y = Y ) -> ( x RingHom y ) = ( X RingHom Y ) )
9 8 adantl 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> ( x RingHom y ) = ( X RingHom Y ) )
10 ovexd 
 |-  ( ph -> ( X RingHom Y ) e. _V )
11 7 9 5 6 10 ovmpod 
 |-  ( ph -> ( X H Y ) = ( X RingHom Y ) )