Metamath Proof Explorer

Theorem rhmpsrlem2

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 rhmpsrlem2 
|- ( ( ph /\ k e. D ) -> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) e. ( Base ` 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 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
7 2 ringcmnd 
 |-  ( ph -> R e. CMnd )
8 7 adantr 
 |-  ( ( ph /\ k e. D ) -> R e. CMnd )
9 1 psrbaglefi 
 |-  ( k e. D -> { y e. D | y oR <_ k } e. Fin )
10 9 adantl 
 |-  ( ( ph /\ k e. D ) -> { y e. D | y oR <_ k } e. Fin )
11 eqid 
 |-  ( .r ` R ) = ( .r ` R )
12 2 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> R e. Ring )
13 3 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> X : D --> ( Base ` R ) )
14 breq1 
 |-  ( y = x -> ( y oR <_ k <-> x oR <_ k ) )
15 14 elrab 
 |-  ( x e. { y e. D | y oR <_ k } <-> ( x e. D /\ x oR <_ k ) )
16 15 biimpi 
 |-  ( x e. { y e. D | y oR <_ k } -> ( x e. D /\ x oR <_ k ) )
17 16 adantl 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( x e. D /\ x oR <_ k ) )
18 17 simpld 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> x e. D )
19 13 18 ffvelcdmd 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( X ` x ) e. ( Base ` R ) )
20 4 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> Y : D --> ( Base ` R ) )
21 simplr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> k e. D )
22 1 psrbagf 
 |-  ( x e. D -> x : I --> NN0 )
23 18 22 syl 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> x : I --> NN0 )
24 17 simprd 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> x oR <_ k )
25 1 psrbagcon 
 |-  ( ( k e. D /\ x : I --> NN0 /\ x oR <_ k ) -> ( ( k oF - x ) e. D /\ ( k oF - x ) oR <_ k ) )
26 21 23 24 25 syl3anc 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( k oF - x ) e. D /\ ( k oF - x ) oR <_ k ) )
27 26 simpld 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( k oF - x ) e. D )
28 20 27 ffvelcdmd 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( Y ` ( k oF - x ) ) e. ( Base ` R ) )
29 5 11 12 19 28 ringcld 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) e. ( Base ` R ) )
30 29 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 } --> ( Base ` R ) )
31 1 2 3 4 rhmpsrlem1 
 |-  ( ( ph /\ k e. D ) -> ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) finSupp ( 0g ` R ) )
32 5 6 8 10 30 31 gsumcl 
 |-  ( ( ph /\ k e. D ) -> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) e. ( Base ` R ) )