Metamath Proof Explorer


Theorem fisuppov1

Description: Formula building theorem for finite support: operator with left annihilator. (Contributed by Thierry Arnoux, 5-Oct-2025)

Ref Expression
Hypotheses fisuppov1.1 φ Z V
fisuppov1.2 φ 0 ˙ X
fisuppov1.3 φ A W
fisuppov1.4 φ D A
fisuppov1.5 φ x D B Y
fisuppov1.6 φ F : A E
fisuppov1.7 φ finSupp 0 ˙ F
fisuppov1.8 φ y Y 0 ˙ O y = Z
Assertion fisuppov1 φ finSupp Z x D F x O B

Proof

Step Hyp Ref Expression
1 fisuppov1.1 φ Z V
2 fisuppov1.2 φ 0 ˙ X
3 fisuppov1.3 φ A W
4 fisuppov1.4 φ D A
5 fisuppov1.5 φ x D B Y
6 fisuppov1.6 φ F : A E
7 fisuppov1.7 φ finSupp 0 ˙ F
8 fisuppov1.8 φ y Y 0 ˙ O y = Z
9 3 4 ssexd φ D V
10 9 mptexd φ x D F x O B V
11 funmpt Fun x D F x O B
12 11 a1i φ Fun x D F x O B
13 6 4 feqresmpt φ F D = x D F x
14 13 oveq1d φ F D supp 0 ˙ = x D F x supp 0 ˙
15 6 3 fexd φ F V
16 ressuppss F V 0 ˙ X F D supp 0 ˙ F supp 0 ˙
17 15 2 16 syl2anc φ F D supp 0 ˙ F supp 0 ˙
18 14 17 eqsstrrd φ x D F x supp 0 ˙ F supp 0 ˙
19 fvexd φ x D F x V
20 18 8 19 5 2 suppssov1 φ x D F x O B supp Z F supp 0 ˙
21 10 1 12 7 20 fsuppsssuppgd φ finSupp Z x D F x O B