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	|- ( ph -> ( x e. D |-> A ) finSupp Y )
	fsuppssov1.o	|- ( ( ph /\ v e. R ) -> ( Y O v ) = Z )
	fsuppssov1.a	|- ( ( ph /\ x e. D ) -> A e. V )
	fsuppssov1.b	|- ( ( ph /\ x e. D ) -> B e. R )
	fsuppssov1.z	|- ( ph -> Z e. W )
Assertion	fsuppssov1	|- ( ph -> ( x e. D |-> ( A O B ) ) finSupp Z )

Proof

Step	Hyp	Ref	Expression
1		fsuppssov1.s	|- ( ph -> ( x e. D |-> A ) finSupp Y )
2		fsuppssov1.o	|- ( ( ph /\ v e. R ) -> ( Y O v ) = Z )
3		fsuppssov1.a	|- ( ( ph /\ x e. D ) -> A e. V )
4		fsuppssov1.b	|- ( ( ph /\ x e. D ) -> B e. R )
5		fsuppssov1.z	|- ( ph -> Z e. W )
6		relfsupp	|- Rel finSupp
7	6	brrelex1i	|- ( ( x e. D |-> A ) finSupp Y -> ( x e. D |-> A ) e. _V )
8	1 7	syl	|- ( ph -> ( x e. D |-> A ) e. _V )
9	3	fmpttd	|- ( ph -> ( x e. D |-> A ) : D --> V )
10		dmfex	|- ( ( ( x e. D |-> A ) e. _V /\ ( x e. D |-> A ) : D --> V ) -> D e. _V )
11	8 9 10	syl2anc	|- ( ph -> D e. _V )
12	11	mptexd	|- ( ph -> ( x e. D |-> ( A O B ) ) e. _V )
13		funmpt	|- Fun ( x e. D |-> ( A O B ) )
14	13	a1i	|- ( ph -> Fun ( x e. D |-> ( A O B ) ) )
15		ssidd	|- ( ph -> ( ( x e. D |-> A ) supp Y ) C_ ( ( x e. D |-> A ) supp Y ) )
16	6	brrelex2i	|- ( ( x e. D |-> A ) finSupp Y -> Y e. _V )
17	1 16	syl	|- ( ph -> Y e. _V )
18	15 2 3 4 17	suppssov1	|- ( ph -> ( ( x e. D |-> ( A O B ) ) supp Z ) C_ ( ( x e. D |-> A ) supp Y ) )
19	12 5 14 1 18	fsuppsssuppgd	|- ( ph -> ( x e. D |-> ( A O B ) ) finSupp Z )