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

Metamath Proof Explorer

Theorem fsuppssov1

Description: Formula building theorem for finite support: operator with left annihilator. Finite support version of suppssov1 . (Contributed by SN, 26-Apr-2025)

Ref Expression
Hypotheses fsuppssov1.s ⊢ φ → finSupp Y⁡ x ∈ D ⟼ A
fsuppssov1.o ⊢ φ ∧ v ∈ R → Y O v = Z
fsuppssov1.a ⊢ φ ∧ x ∈ D → A ∈ V
fsuppssov1.b ⊢ φ ∧ x ∈ D → B ∈ R
fsuppssov1.z ⊢ φ → Z ∈ W
Assertion fsuppssov1 ⊢ φ → finSupp Z⁡ x ∈ D ⟼ A O B

Proof

Step Hyp Ref Expression
1 fsuppssov1.s ⊢ φ → finSupp Y⁡ x ∈ D ⟼ A
2 fsuppssov1.o ⊢ φ ∧ v ∈ R → Y O v = Z
3 fsuppssov1.a ⊢ φ ∧ x ∈ D → A ∈ V
4 fsuppssov1.b ⊢ φ ∧ x ∈ D → B ∈ R
5 fsuppssov1.z ⊢ φ → Z ∈ W
6 relfsupp ⊢ Rel ⁡ finSupp
7 6 brrelex1i ⊢ finSupp Y⁡ x ∈ D ⟼ A → x ∈ D ⟼ A ∈ V
8 1 7 syl ⊢ φ → x ∈ D ⟼ A ∈ V
9 3 fmpttd ⊢ φ → x ∈ D ⟼ A : D ⟶ V
10 dmfex ⊢ x ∈ D ⟼ A ∈ V ∧ x ∈ D ⟼ A : D ⟶ V → D ∈ V
11 8 9 10 syl2anc ⊢ φ → D ∈ V
12 11 mptexd ⊢ φ → x ∈ D ⟼ A O B ∈ V
13 funmpt ⊢ Fun ⁡ x ∈ D ⟼ A O B
14 13 a1i ⊢ φ → Fun ⁡ x ∈ D ⟼ A O B
15 ssidd ⊢ φ → x ∈ D ⟼ A supp Y ⊆ x ∈ D ⟼ A supp Y
16 6 brrelex2i ⊢ finSupp Y⁡ x ∈ D ⟼ A → Y ∈ V
17 1 16 syl ⊢ φ → Y ∈ V
18 15 2 3 4 17 suppssov1 ⊢ φ → x ∈ D ⟼ A O B supp Z ⊆ x ∈ D ⟼ A supp Y
19 12 5 14 1 18 fsuppsssuppgd ⊢ φ → finSupp Z⁡ x ∈ D ⟼ A O B