Theorem rhmmpllem1

Description: Lemma for rhmmpl . A subproof of psrmulcllem . (Contributed by SN, 8-Feb-2025)

	Ref	Expression
Hypotheses	rhmmpllem1.d	|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
	rhmmpllem1.r	|- ( ph -> R e. Ring )
	rhmmpllem1.x	|- ( ph -> X : D --> ( Base ` R ) )
	rhmmpllem1.y	|- ( ph -> Y : D --> ( Base ` R ) )
Assertion	rhmmpllem1	|- ( ( 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		rhmmpllem1.d	|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
2		rhmmpllem1.r	|- ( ph -> R e. Ring )
3		rhmmpllem1.x	|- ( ph -> X : D --> ( Base ` R ) )
4		rhmmpllem1.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 ) )