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 𝑌 ) ) |