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 W = h i I S i | finSupp 0 ˙ h
dprdff.1 φ G dom DProd S
dprdff.2 φ dom S = I
Assertion dprdw φ F W F Fn I x I F x S x finSupp 0 ˙ F

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 elex F i I S i F V
5 4 a1i φ F i I S i F V
6 2 3 dprddomcld φ I V
7 fnex F Fn I I V F V
8 7 expcom I V F Fn I F V
9 6 8 syl φ F Fn I F V
10 9 adantrd φ F Fn I x I F x S x F V
11 fveq2 i = x S i = S x
12 11 cbvixpv i I S i = x I S x
13 12 eleq2i F i I S i F x I S x
14 elixp2 F x I S x F V F Fn I x I F x S x
15 3anass F V F Fn I x I F x S x F V F Fn I x I F x S x
16 13 14 15 3bitri F i I S i F V F Fn I x I F x S x
17 16 baib F V F i I S i F Fn I x I F x S x
18 17 a1i φ F V F i I S i F Fn I x I F x S x
19 5 10 18 pm5.21ndd φ F i I S i F Fn I x I F x S x
20 19 anbi1d φ F i I S i finSupp 0 ˙ F F Fn I x I F x S x finSupp 0 ˙ F
21 breq1 h = F finSupp 0 ˙ h finSupp 0 ˙ F
22 21 1 elrab2 F W F i I S i finSupp 0 ˙ F
23 df-3an F Fn I x I F x S x finSupp 0 ˙ F F Fn I x I F x S x finSupp 0 ˙ F
24 20 22 23 3bitr4g φ F W F Fn I x I F x S x finSupp 0 ˙ F