rhmmpllem2

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

	Ref	Expression
Hypotheses	rhmmpllem1.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	rhmmpllem1.r	$⊢ φ \to R \in Ring$
	rhmmpllem1.x	$⊢ φ \to X : D ⟶ {Base}_{R}$
	rhmmpllem1.y	$⊢ φ \to Y : D ⟶ {Base}_{R}$
Assertion	rhmmpllem2	$⊢ (φ \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		rhmmpllem1.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
2		rhmmpllem1.r	$⊢ φ \to R \in Ring$
3		rhmmpllem1.x	$⊢ φ \to X : D ⟶ {Base}_{R}$
4		rhmmpllem1.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	biimpi	$⊢ x \in \{y \in D \| y \leq_{f} k\} \to (x \in D \land x \leq_{f} k)$
17	16	adantl	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to (x \in D \land x \leq_{f} k)$
18	17	simpld	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to x \in D$
19	13 18	ffvelcdmd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X (x) \in {Base}_{R}$
20	4	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Y : D ⟶ {Base}_{R}$
21		simplr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to k \in D$
22	1	psrbagf	$⊢ x \in D \to x : I ⟶ ℕ_{0}$
23	18 22	syl	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to x : I ⟶ ℕ_{0}$
24	17	simprd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to x \leq_{f} k$
25	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)$
26	21 23 24 25	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)$
27	26	simpld	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to k -_{f} x \in D$
28	20 27	ffvelcdmd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Y (k -_{f} x) \in {Base}_{R}$
29	5 11 12 19 28	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}$
30	29	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}$
31	1 2 3 4	rhmmpllem1	$⊢ (φ \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)))$
32	5 6 8 10 30 31	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 rhmmpllem2

Proof