Theorem rhmpsrlem1

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

	Ref	Expression
Hypotheses	rhmpsrlem1.d	|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
	rhmpsrlem1.r	|- ( ph -> R e. Ring )
	rhmpsrlem1.x	|- ( ph -> X : D --> ( Base ` R ) )
	rhmpsrlem1.y	|- ( ph -> Y : D --> ( Base ` R ) )
Assertion	rhmpsrlem1	|- ( ( ph /\ k e. D ) -> ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) finSupp ( 0g ` R ) )

Proof

Step	Hyp	Ref	Expression
1		rhmpsrlem1.d	|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
2		rhmpsrlem1.r	|- ( ph -> R e. Ring )
3		rhmpsrlem1.x	|- ( ph -> X : D --> ( Base ` R ) )
4		rhmpsrlem1.y	|- ( ph -> Y : D --> ( Base ` R ) )
5		ovexd	|- ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) e. _V )
6	5	fmpttd	|- ( ( ph /\ k e. D ) -> ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) : { y e. D | y oR <_ k } --> _V )
7	1	psrbaglefi	|- ( k e. D -> { y e. D | y oR <_ k } e. Fin )
8	7	adantl	|- ( ( ph /\ k e. D ) -> { y e. D | y oR <_ k } e. Fin )
9		fvexd	|- ( ( ph /\ k e. D ) -> ( 0g ` R ) e. _V )
10	6 8 9	fdmfifsupp	|- ( ( ph /\ k e. D ) -> ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) finSupp ( 0g ` R ) )