Metamath Proof Explorer


Theorem elringchomALTV

Description: A morphism of rings is a function. (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 elringchomALTV
|- ( ph -> ( F e. ( X H Y ) -> F : ( Base ` X ) --> ( Base ` 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 5 6 ringchomALTV
 |-  ( ph -> ( X H Y ) = ( X RingHom Y ) )
8 7 eleq2d
 |-  ( ph -> ( F e. ( X H Y ) <-> F e. ( X RingHom Y ) ) )
9 eqid
 |-  ( Base ` X ) = ( Base ` X )
10 eqid
 |-  ( Base ` Y ) = ( Base ` Y )
11 9 10 rhmf
 |-  ( F e. ( X RingHom Y ) -> F : ( Base ` X ) --> ( Base ` Y ) )
12 8 11 syl6bi
 |-  ( ph -> ( F e. ( X H Y ) -> F : ( Base ` X ) --> ( Base ` Y ) ) )