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 𝑍 )