Metamath Proof Explorer


Theorem elrngchom

Description: A morphism of non-unital rings is a function. (Contributed by AV, 27-Feb-2020)

Ref Expression
Hypotheses rngcbas.c C = RngCat U
rngcbas.b B = Base C
rngcbas.u φ U V
rngchomfval.h H = Hom C
rngchom.x φ X B
rngchom.y φ Y B
Assertion elrngchom φ F X H Y F : Base X Base Y

Proof

Step Hyp Ref Expression
1 rngcbas.c C = RngCat U
2 rngcbas.b B = Base C
3 rngcbas.u φ U V
4 rngchomfval.h H = Hom C
5 rngchom.x φ X B
6 rngchom.y φ Y B
7 1 2 3 4 5 6 rngchom φ X H Y = X RngHomo Y
8 7 eleq2d φ F X H Y F X RngHomo Y
9 eqid Base X = Base X
10 eqid Base Y = Base Y
11 9 10 rnghmf F X RngHomo Y F : Base X Base Y
12 8 11 syl6bi φ F X H Y F : Base X Base Y