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 φ U V
ringchomfvalALTV.h H = Hom C
ringchomALTV.x φ X B
ringchomALTV.y φ Y B
Assertion elringchomALTV φ F 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 φ U V
4 ringchomfvalALTV.h H = Hom C
5 ringchomALTV.x φ X B
6 ringchomALTV.y φ Y B
7 1 2 3 4 5 6 ringchomALTV φ X H Y = X RingHom Y
8 7 eleq2d φ F X H Y F X RingHom Y
9 eqid Base X = Base X
10 eqid Base Y = Base Y
11 9 10 rhmf F X RingHom Y F : Base X Base Y
12 8 11 syl6bi φ F X H Y F : Base X Base Y