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 𝐶 = ( RingCatALTV ‘ 𝑈 )
ringcbasALTV.b 𝐵 = ( Base ‘ 𝐶 )
ringcbasALTV.u ( 𝜑𝑈𝑉 )
ringchomfvalALTV.h 𝐻 = ( Hom ‘ 𝐶 )
ringchomALTV.x ( 𝜑𝑋𝐵 )
ringchomALTV.y ( 𝜑𝑌𝐵 )
Assertion ringchomALTV ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( 𝑋 RingHom 𝑌 ) )

Proof

Step Hyp Ref Expression
1 ringcbasALTV.c 𝐶 = ( RingCatALTV ‘ 𝑈 )
2 ringcbasALTV.b 𝐵 = ( Base ‘ 𝐶 )
3 ringcbasALTV.u ( 𝜑𝑈𝑉 )
4 ringchomfvalALTV.h 𝐻 = ( Hom ‘ 𝐶 )
5 ringchomALTV.x ( 𝜑𝑋𝐵 )
6 ringchomALTV.y ( 𝜑𝑌𝐵 )
7 1 2 3 4 ringchomfvalALTV ( 𝜑𝐻 = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥 RingHom 𝑦 ) ) )
8 oveq12 ( ( 𝑥 = 𝑋𝑦 = 𝑌 ) → ( 𝑥 RingHom 𝑦 ) = ( 𝑋 RingHom 𝑌 ) )
9 8 adantl ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → ( 𝑥 RingHom 𝑦 ) = ( 𝑋 RingHom 𝑌 ) )
10 ovexd ( 𝜑 → ( 𝑋 RingHom 𝑌 ) ∈ V )
11 7 9 5 6 10 ovmpod ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( 𝑋 RingHom 𝑌 ) )