This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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