Metamath Proof Explorer

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 ⊢ W = h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h
dprdff.1 ⊢ φ → G dom ⁡ DProd S
dprdff.2 ⊢ φ → dom ⁡ S = I
dprdff.3 ⊢ φ → F ∈ W
dprdff.b ⊢ B = Base G
Assertion dprdff ⊢ φ → F : I ⟶ B

Proof

Step Hyp Ref Expression
1 dprdff.w ⊢ W = h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h
2 dprdff.1 ⊢ φ → G dom ⁡ DProd S
3 dprdff.2 ⊢ φ → dom ⁡ S = I
4 dprdff.3 ⊢ φ → F ∈ W
5 dprdff.b ⊢ B = Base G
6 1 2 3 dprdw ⊢ φ → F ∈ W ↔ F Fn I ∧ ∀ x ∈ I F ⁡ x ∈ S ⁡ x ∧ finSupp 0 ˙⁡ F
7 4 6 mpbid ⊢ φ → F Fn I ∧ ∀ x ∈ I F ⁡ x ∈ S ⁡ x ∧ finSupp 0 ˙⁡ F
8 7 simp1d ⊢ φ → F Fn I
9 7 simp2d ⊢ φ → ∀ x ∈ I F ⁡ x ∈ S ⁡ x
10 2 3 dprdf2 ⊢ φ → S : I ⟶ SubGrp ⁡ G
11 10 ffvelrnda ⊢ φ ∧ x ∈ I → S ⁡ x ∈ SubGrp ⁡ G
12 5 subgss ⊢ S ⁡ x ∈ SubGrp ⁡ G → S ⁡ x ⊆ B
13 11 12 syl ⊢ φ ∧ x ∈ I → S ⁡ x ⊆ B
14 13 sseld ⊢ φ ∧ x ∈ I → F ⁡ x ∈ S ⁡ x → F ⁡ x ∈ B
15 14 ralimdva ⊢ φ → ∀ x ∈ I F ⁡ x ∈ S ⁡ x → ∀ x ∈ I F ⁡ x ∈ B
16 9 15 mpd ⊢ φ → ∀ x ∈ I F ⁡ x ∈ B
17 ffnfv ⊢ F : I ⟶ B ↔ F Fn I ∧ ∀ x ∈ I F ⁡ x ∈ B
18 8 16 17 sylanbrc ⊢ φ → F : I ⟶ B