Metamath Proof Explorer


Theorem rhmpsrlem1

Description: Lemma for rhmpsr et al. (Contributed by SN, 8-Feb-2025)

Ref Expression
Hypotheses rhmpsrlem1.d D = f 0 I | f -1 Fin
rhmpsrlem1.r φ R Ring
rhmpsrlem1.x φ X : D Base R
rhmpsrlem1.y φ Y : D Base R
Assertion rhmpsrlem1 φ k D finSupp 0 R x y D | y f k X x R Y k f x

Proof

Step Hyp Ref Expression
1 rhmpsrlem1.d D = f 0 I | f -1 Fin
2 rhmpsrlem1.r φ R Ring
3 rhmpsrlem1.x φ X : D Base R
4 rhmpsrlem1.y φ Y : D Base R
5 ovexd φ k D x y D | y f k X x R Y k f x V
6 5 fmpttd φ k D x y D | y f k X x R Y k f x : y D | y f k V
7 1 psrbaglefi k D y D | y f k Fin
8 7 adantl φ k D y D | y f k Fin
9 fvexd φ k D 0 R V
10 6 8 9 fdmfifsupp φ k D finSupp 0 R x y D | y f k X x R Y k f x