rhmpsrlem2

	Ref	Expression
Hypotheses	rhmpsrlem1.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	rhmpsrlem1.r	$⊢ φ \to R \in Ring$
	rhmpsrlem1.x	$⊢ φ \to X : D ⟶ {Base}_{R}$
	rhmpsrlem1.y	$⊢ φ \to Y : D ⟶ {Base}_{R}$
Assertion	rhmpsrlem2	$⊢ (φ \land k \in D) \to \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (X (x) \cdot_{R} Y (k -_{f} x)) \in {Base}_{R}$

Proof

Step	Hyp	Ref	Expression
1		rhmpsrlem1.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
2		rhmpsrlem1.r	$⊢ φ \to R \in Ring$
3		rhmpsrlem1.x	$⊢ φ \to X : D ⟶ {Base}_{R}$
4		rhmpsrlem1.y	$⊢ φ \to Y : D ⟶ {Base}_{R}$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6		eqid	$⊢ 0_{R} = 0_{R}$
7	2	ringcmnd	$⊢ φ \to R \in CMnd$
8	7	adantr	$⊢ (φ \land k \in D) \to R \in CMnd$
9	1	psrbaglefi	$⊢ k \in D \to \{y \in D \| y \leq_{f} k\} \in Fin$
10	9	adantl	$⊢ (φ \land k \in D) \to \{y \in D \| y \leq_{f} k\} \in Fin$
11		eqid	$⊢ \cdot_{R} = \cdot_{R}$
12	2	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to R \in Ring$
13	3	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X : D ⟶ {Base}_{R}$
14		breq1	$⊢ y = x \to (y \leq_{f} k \leftrightarrow x \leq_{f} k)$
15	14	elrab	$⊢ x \in \{y \in D \| y \leq_{f} k\} \leftrightarrow (x \in D \land x \leq_{f} k)$
16	15	bilani	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to (x \in D \land x \leq_{f} k)$
17	16	simpld	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to x \in D$
18	13 17	ffvelcdmd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X (x) \in {Base}_{R}$
19	4	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Y : D ⟶ {Base}_{R}$
20		simplr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to k \in D$
21	1	psrbagf	$⊢ x \in D \to x : I ⟶ ℕ_{0}$
22	17 21	syl	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to x : I ⟶ ℕ_{0}$
23	16	simprd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to x \leq_{f} k$
24	1	psrbagcon	$⊢ (k \in D \land x : I ⟶ ℕ_{0} \land x \leq_{f} k) \to (k -_{f} x \in D \land (k -_{f} x) \leq_{f} k)$
25	20 22 23 24	syl3anc	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to (k -_{f} x \in D \land (k -_{f} x) \leq_{f} k)$
26	25	simpld	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to k -_{f} x \in D$
27	19 26	ffvelcdmd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Y (k -_{f} x) \in {Base}_{R}$
28	5 11 12 18 27	ringcld	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X (x) \cdot_{R} Y (k -_{f} x) \in {Base}_{R}$
29	28	fmpttd	$⊢ (φ \land k \in D) \to (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x)) : \{y \in D \| y \leq_{f} k\} ⟶ {Base}_{R}$
30	1 2 3 4	rhmpsrlem1	$⊢ (φ \land k \in D) \to {finSupp}_{0_{R}} ((x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x)))$
31	5 6 8 10 29 30	gsumcl	$⊢ (φ \land k \in D) \to \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (X (x) \cdot_{R} Y (k -_{f} x)) \in {Base}_{R}$

Metamath Proof Explorer

Theorem rhmpsrlem2

Proof