Theorem dprdffsupp

Description: A finitely supported function in S is a finitely supported function. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 11-Jul-2019)

	Ref	Expression
Hypotheses	dprdff.w	⊢ 𝑊 = { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp 0 }
	dprdff.1	⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
	dprdff.2	⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
	dprdff.3	⊢ ( 𝜑 → 𝐹 ∈ 𝑊 )
Assertion	dprdffsupp	⊢ ( 𝜑 → 𝐹 finSupp 0 )

Proof

Step	Hyp	Ref	Expression
1		dprdff.w	⊢ 𝑊 = { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp 0 }
2		dprdff.1	⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
3		dprdff.2	⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
4		dprdff.3	⊢ ( 𝜑 → 𝐹 ∈ 𝑊 )
5	1 2 3	dprdw	⊢ ( 𝜑 → ( 𝐹 ∈ 𝑊 ↔ ( 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ∧ 𝐹 finSupp 0 ) ) )
6	4 5	mpbid	⊢ ( 𝜑 → ( 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ∧ 𝐹 finSupp 0 ) )
7	6	simp3d	⊢ ( 𝜑 → 𝐹 finSupp 0 )