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

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 ⊢ 𝑊 = { ℎ ∈ 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 ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ 𝐵 )