Theorem dprdff

Description: A finitely supported function in S is a function into the base. (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	⊢ ( 𝜑 → 𝐹 ∈ 𝑊 )
	dprdff.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion	dprdff	⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		dprdff.w	⊢ 𝑊 = { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp 0 }
2		dprdff.1	⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
3		dprdff.2	⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
4		dprdff.3	⊢ ( 𝜑 → 𝐹 ∈ 𝑊 )
5		dprdff.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
6	1 2 3	dprdw	⊢ ( 𝜑 → ( 𝐹 ∈ 𝑊 ↔ ( 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ∧ 𝐹 finSupp 0 ) ) )
7	4 6	mpbid	⊢ ( 𝜑 → ( 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ∧ 𝐹 finSupp 0 ) )
8	7	simp1d	⊢ ( 𝜑 → 𝐹 Fn 𝐼 )
9	7	simp2d	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) )
10	2 3	dprdf2	⊢ ( 𝜑 → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
11	10	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑆 ‘ 𝑥 ) ∈ ( SubGrp ‘ 𝐺 ) )
12	5	subgss	⊢ ( ( 𝑆 ‘ 𝑥 ) ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑆 ‘ 𝑥 ) ⊆ 𝐵 )
13	11 12	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑆 ‘ 𝑥 ) ⊆ 𝐵 )
14	13	sseld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )
15	14	ralimdva	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) → ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )
16	9 15	mpd	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
17		ffnfv	⊢ ( 𝐹 : 𝐼 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )
18	8 16 17	sylanbrc	⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ 𝐵 )