rhmmpllem1

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

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		ovexd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X (x) \cdot_{R} Y (k -_{f} x) \in V$
6	5	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\} ⟶ V$
7	1	psrbaglefi	$⊢ k \in D \to \{y \in D \| y \leq_{f} k\} \in Fin$
8	7	adantl	$⊢ (φ \land k \in D) \to \{y \in D \| y \leq_{f} k\} \in Fin$
9		fvexd	$⊢ (φ \land k \in D) \to 0_{R} \in V$
10	6 8 9	fdmfifsupp	$⊢ (φ \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)))$

Metamath Proof Explorer