Metamath Proof Explorer


Theorem rhmpsrlem2

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 rhmpsrlem2 φ k D R x y D | y f k X x R Y k f x Base R

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 eqid Base R = Base R
6 eqid 0 R = 0 R
7 2 ringcmnd φ R CMnd
8 7 adantr φ k D R CMnd
9 1 psrbaglefi k D y D | y f k Fin
10 9 adantl φ k D y D | y f k Fin
11 eqid R = R
12 2 ad2antrr φ k D x y D | y f k R Ring
13 3 ad2antrr φ k D x y D | y f k X : D Base R
14 breq1 y = x y f k x f k
15 14 elrab x y D | y f k x D x f k
16 15 biimpi x y D | y f k x D x f k
17 16 adantl φ k D x y D | y f k x D x f k
18 17 simpld φ k D x y D | y f k x D
19 13 18 ffvelcdmd φ k D x y D | y f k X x Base R
20 4 ad2antrr φ k D x y D | y f k Y : D Base R
21 simplr φ k D x y D | y f k k D
22 1 psrbagf x D x : I 0
23 18 22 syl φ k D x y D | y f k x : I 0
24 17 simprd φ k D x y D | y f k x f k
25 1 psrbagcon k D x : I 0 x f k k f x D k f x f k
26 21 23 24 25 syl3anc φ k D x y D | y f k k f x D k f x f k
27 26 simpld φ k D x y D | y f k k f x D
28 20 27 ffvelcdmd φ k D x y D | y f k Y k f x Base R
29 5 11 12 19 28 ringcld φ k D x y D | y f k X x R Y k f x Base R
30 29 fmpttd φ k D x y D | y f k X x R Y k f x : y D | y f k Base R
31 1 2 3 4 rhmpsrlem1 φ k D finSupp 0 R x y D | y f k X x R Y k f x
32 5 6 8 10 30 31 gsumcl φ k D R x y D | y f k X x R Y k f x Base R