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 𝑌 )
fsuppssov1.o ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑅 ) → ( 𝑌 𝑂 𝑣 ) = 𝑍 )
fsuppssov1.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐴 ∈ 𝑉 )
fsuppssov1.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐵 ∈ 𝑅 )
fsuppssov1.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
Assertion fsuppssov1 ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) finSupp 𝑍 )

Proof

Step Hyp Ref Expression
1 fsuppssov1.s ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) finSupp 𝑌 )
2 fsuppssov1.o ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑅 ) → ( 𝑌 𝑂 𝑣 ) = 𝑍 )
3 fsuppssov1.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐴 ∈ 𝑉 )
4 fsuppssov1.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐵 ∈ 𝑅 )
5 fsuppssov1.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
6 relfsupp ⊢ Rel finSupp
7 6 brrelex1i ⊢ ( ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) finSupp 𝑌 → ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) ∈ V )
8 1 7 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) ∈ V )
9 3 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) : 𝐷 ⟶ 𝑉 )
10 dmfex ⊢ ( ( ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) ∈ V ∧ ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) : 𝐷 ⟶ 𝑉 ) → 𝐷 ∈ V )
11 8 9 10 syl2anc ⊢ ( 𝜑 → 𝐷 ∈ V )
12 11 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) ∈ V )
13 funmpt ⊢ Fun ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) )
14 13 a1i ⊢ ( 𝜑 → Fun ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) )
15 ssidd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) supp 𝑌 ) ⊆ ( ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) supp 𝑌 ) )
16 6 brrelex2i ⊢ ( ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) finSupp 𝑌 → 𝑌 ∈ V )
17 1 16 syl ⊢ ( 𝜑 → 𝑌 ∈ V )
18 15 2 3 4 17 suppssov1 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) supp 𝑍 ) ⊆ ( ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) supp 𝑌 ) )
19 12 5 14 1 18 fsuppsssuppgd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) finSupp 𝑍 )