Metamath Proof Explorer


Theorem rhmpsrlem1

Description: Lemma for rhmpsr et al. (Contributed by SN, 8-Feb-2025)

Ref Expression
Hypotheses rhmpsrlem1.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
rhmpsrlem1.r ( 𝜑𝑅 ∈ Ring )
rhmpsrlem1.x ( 𝜑𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
rhmpsrlem1.y ( 𝜑𝑌 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
Assertion rhmpsrlem1 ( ( 𝜑𝑘𝐷 ) → ( 𝑥 ∈ { 𝑦𝐷𝑦r𝑘 } ↦ ( ( 𝑋𝑥 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ) ) finSupp ( 0g𝑅 ) )

Proof

Step Hyp Ref Expression
1 rhmpsrlem1.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
2 rhmpsrlem1.r ( 𝜑𝑅 ∈ Ring )
3 rhmpsrlem1.x ( 𝜑𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
4 rhmpsrlem1.y ( 𝜑𝑌 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
5 ovexd ( ( ( 𝜑𝑘𝐷 ) ∧ 𝑥 ∈ { 𝑦𝐷𝑦r𝑘 } ) → ( ( 𝑋𝑥 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ) ∈ V )
6 5 fmpttd ( ( 𝜑𝑘𝐷 ) → ( 𝑥 ∈ { 𝑦𝐷𝑦r𝑘 } ↦ ( ( 𝑋𝑥 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ) ) : { 𝑦𝐷𝑦r𝑘 } ⟶ V )
7 1 psrbaglefi ( 𝑘𝐷 → { 𝑦𝐷𝑦r𝑘 } ∈ Fin )
8 7 adantl ( ( 𝜑𝑘𝐷 ) → { 𝑦𝐷𝑦r𝑘 } ∈ Fin )
9 fvexd ( ( 𝜑𝑘𝐷 ) → ( 0g𝑅 ) ∈ V )
10 6 8 9 fdmfifsupp ( ( 𝜑𝑘𝐷 ) → ( 𝑥 ∈ { 𝑦𝐷𝑦r𝑘 } ↦ ( ( 𝑋𝑥 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ) ) finSupp ( 0g𝑅 ) )