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 ∈ ℕ 0 I | f -1 ℕ ∈ Fin
rhmpsrlem1.r ⊢ φ → R ∈ Ring
rhmpsrlem1.x ⊢ φ → X : D ⟶ Base R
rhmpsrlem1.y ⊢ φ → Y : D ⟶ Base R
Assertion rhmpsrlem1 ⊢ φ ∧ k ∈ D → finSupp 0 R⁡ x ∈ y ∈ D | y ≤ f k ⟼ X ⁡ x ⋅ R Y ⁡ k − f x

Proof

Step Hyp Ref Expression
1 rhmpsrlem1.d ⊢ D = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
2 rhmpsrlem1.r ⊢ φ → R ∈ Ring
3 rhmpsrlem1.x ⊢ φ → X : D ⟶ Base R
4 rhmpsrlem1.y ⊢ φ → Y : D ⟶ Base R
5 ovexd ⊢ φ ∧ k ∈ D ∧ x ∈ y ∈ D | y ≤ f k → X ⁡ x ⋅ R Y ⁡ k − f x ∈ V
6 5 fmpttd ⊢ φ ∧ k ∈ D → x ∈ y ∈ D | y ≤ f k ⟼ X ⁡ x ⋅ R Y ⁡ k − f x : y ∈ D | y ≤ f k ⟶ V
7 1 psrbaglefi ⊢ k ∈ D → y ∈ D | y ≤ f k ∈ Fin
8 7 adantl ⊢ φ ∧ k ∈ D → y ∈ D | y ≤ f k ∈ Fin
9 fvexd ⊢ φ ∧ k ∈ D → 0 R ∈ V
10 6 8 9 fdmfifsupp ⊢ φ ∧ k ∈ D → finSupp 0 R⁡ x ∈ y ∈ D | y ≤ f k ⟼ X ⁡ x ⋅ R Y ⁡ k − f x