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

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