This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dprdfcl

Description: A finitely supported function in S has its X -th element in S ( X ) . (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	dprdfcl	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑋 ) ∈ ( 𝑆 ‘ 𝑋 ) )

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	simp2d	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) )
8		fveq2	⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
9		fveq2	⊢ ( 𝑥 = 𝑋 → ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑋 ) )
10	8 9	eleq12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑋 ) ∈ ( 𝑆 ‘ 𝑋 ) ) )
11	10	rspccva	⊢ ( ( ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ∧ 𝑋 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑋 ) ∈ ( 𝑆 ‘ 𝑋 ) )
12	7 11	sylan	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑋 ) ∈ ( 𝑆 ‘ 𝑋 ) )