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	$$⊢\phi \to {finSupp}_Y\left(\left(x\in D⟼A\right)\right)$$
	fsuppssov1.o	$$⊢\left(\phi \wedge v\in R\right)\to YOv=Z$$
	fsuppssov1.a	$$⊢\left(\phi \wedge x\in D\right)\to A\in V$$
	fsuppssov1.b	$$⊢\left(\phi \wedge x\in D\right)\to B\in R$$
	fsuppssov1.z	$$⊢\phi \to Z\in W$$
Assertion	fsuppssov1	$$⊢\phi \to {finSupp}_Z\left(\left(x\in D⟼AOB\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fsuppssov1.s	$$⊢\phi \to {finSupp}_Y\left(\left(x\in D⟼A\right)\right)$$
2		fsuppssov1.o	$$⊢\left(\phi \wedge v\in R\right)\to YOv=Z$$
3		fsuppssov1.a	$$⊢\left(\phi \wedge x\in D\right)\to A\in V$$
4		fsuppssov1.b	$$⊢\left(\phi \wedge x\in D\right)\to B\in R$$
5		fsuppssov1.z	$$⊢\phi \to Z\in W$$
6		relfsupp	$$⊢\mathrm{Rel}\mathrm{finSupp}$$
7	6	brrelex1i	$$⊢{finSupp}_Y\left(\left(x\in D⟼A\right)\right)\to \left(x\in D⟼A\right)\in \mathrm{V}$$
8	1 7	syl	$$⊢\phi \to \left(x\in D⟼A\right)\in \mathrm{V}$$
9	3	fmpttd	$$⊢\phi \to \left(x\in D⟼A\right):D⟶V$$
10		dmfex	$$⊢\left(\left(x\in D⟼A\right)\in \mathrm{V}\wedge \left(x\in D⟼A\right):D⟶V\right)\to D\in \mathrm{V}$$
11	8 9 10	syl2anc	$$⊢\phi \to D\in \mathrm{V}$$
12	11	mptexd	$$⊢\phi \to \left(x\in D⟼AOB\right)\in \mathrm{V}$$
13		funmpt	$$⊢\mathrm{Fun}\left(x\in D⟼AOB\right)$$
14	13	a1i	$$⊢\phi \to \mathrm{Fun}\left(x\in D⟼AOB\right)$$
15		ssidd	$$⊢\phi \to \left(x\in D⟼A\right)\mathrm{supp}Y\subseteq \left(x\in D⟼A\right)\mathrm{supp}Y$$
16	6	brrelex2i	$$⊢{finSupp}_Y\left(\left(x\in D⟼A\right)\right)\to Y\in \mathrm{V}$$
17	1 16	syl	$$⊢\phi \to Y\in \mathrm{V}$$
18	15 2 3 4 17	suppssov1	$$⊢\phi \to \left(x\in D⟼AOB\right)\mathrm{supp}Z\subseteq \left(x\in D⟼A\right)\mathrm{supp}Y$$
19	12 5 14 1 18	fsuppsssuppgd	$$⊢\phi \to {finSupp}_Z\left(\left(x\in D⟼AOB\right)\right)$$