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

Metamath Proof Explorer

Theorem dprdw

Description: The property of being a finitely supported function in the family S . (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 𝑆 = 𝐼 )
Assertion dprdw ( 𝜑 → ( 𝐹 ∈ 𝑊 ↔ ( 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ∧ 𝐹 finSupp 0 ) ) )

Proof

Step Hyp Ref Expression
1 dprdff.w ⊢ 𝑊 = { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp 0 }
2 dprdff.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
3 dprdff.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
4 elex ⊢ ( 𝐹 ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) → 𝐹 ∈ V )
5 4 a1i ⊢ ( 𝜑 → ( 𝐹 ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) → 𝐹 ∈ V ) )
6 2 3 dprddomcld ⊢ ( 𝜑 → 𝐼 ∈ V )
7 fnex ⊢ ( ( 𝐹 Fn 𝐼 ∧ 𝐼 ∈ V ) → 𝐹 ∈ V )
8 7 expcom ⊢ ( 𝐼 ∈ V → ( 𝐹 Fn 𝐼 → 𝐹 ∈ V ) )
9 6 8 syl ⊢ ( 𝜑 → ( 𝐹 Fn 𝐼 → 𝐹 ∈ V ) )
10 9 adantrd ⊢ ( 𝜑 → ( ( 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ) → 𝐹 ∈ V ) )
11 fveq2 ⊢ ( 𝑖 = 𝑥 → ( 𝑆 ‘ 𝑖 ) = ( 𝑆 ‘ 𝑥 ) )
12 11 cbvixpv ⊢ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) = X 𝑥 ∈ 𝐼 ( 𝑆 ‘ 𝑥 )
13 12 eleq2i ⊢ ( 𝐹 ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ↔ 𝐹 ∈ X 𝑥 ∈ 𝐼 ( 𝑆 ‘ 𝑥 ) )
14 elixp2 ⊢ ( 𝐹 ∈ X 𝑥 ∈ 𝐼 ( 𝑆 ‘ 𝑥 ) ↔ ( 𝐹 ∈ V ∧ 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ) )
15 3anass ⊢ ( ( 𝐹 ∈ V ∧ 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ) ↔ ( 𝐹 ∈ V ∧ ( 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ) ) )
16 13 14 15 3bitri ⊢ ( 𝐹 ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ↔ ( 𝐹 ∈ V ∧ ( 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ) ) )
17 16 baib ⊢ ( 𝐹 ∈ V → ( 𝐹 ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ↔ ( 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ) ) )
18 17 a1i ⊢ ( 𝜑 → ( 𝐹 ∈ V → ( 𝐹 ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ↔ ( 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ) ) ) )
19 5 10 18 pm5.21ndd ⊢ ( 𝜑 → ( 𝐹 ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ↔ ( 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ) ) )
20 19 anbi1d ⊢ ( 𝜑 → ( ( 𝐹 ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∧ 𝐹 finSupp 0 ) ↔ ( ( 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ) ∧ 𝐹 finSupp 0 ) ) )
21 breq1 ⊢ ( ℎ = 𝐹 → ( ℎ finSupp 0 ↔ 𝐹 finSupp 0 ) )
22 21 1 elrab2 ⊢ ( 𝐹 ∈ 𝑊 ↔ ( 𝐹 ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∧ 𝐹 finSupp 0 ) )
23 df-3an ⊢ ( ( 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ∧ 𝐹 finSupp 0 ) ↔ ( ( 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ) ∧ 𝐹 finSupp 0 ) )
24 20 22 23 3bitr4g ⊢ ( 𝜑 → ( 𝐹 ∈ 𝑊 ↔ ( 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ∧ 𝐹 finSupp 0 ) ) )