Theorem fisuppov1

Description: Formula building theorem for finite support: operator with left annihilator. (Contributed by Thierry Arnoux, 5-Oct-2025)

	Ref	Expression
Hypotheses	fisuppov1.1	|- ( ph -> Z e. V )
	fisuppov1.2	|- ( ph -> .0. e. X )
	fisuppov1.3	|- ( ph -> A e. W )
	fisuppov1.4	|- ( ph -> D C_ A )
	fisuppov1.5	|- ( ( ph /\ x e. D ) -> B e. Y )
	fisuppov1.6	|- ( ph -> F : A --> E )
	fisuppov1.7	|- ( ph -> F finSupp .0. )
	fisuppov1.8	|- ( ( ph /\ y e. Y ) -> ( .0. O y ) = Z )
Assertion	fisuppov1	|- ( ph -> ( x e. D |-> ( ( F ` x ) O B ) ) finSupp Z )

Proof

Step	Hyp	Ref	Expression
1		fisuppov1.1	|- ( ph -> Z e. V )
2		fisuppov1.2	|- ( ph -> .0. e. X )
3		fisuppov1.3	|- ( ph -> A e. W )
4		fisuppov1.4	|- ( ph -> D C_ A )
5		fisuppov1.5	|- ( ( ph /\ x e. D ) -> B e. Y )
6		fisuppov1.6	|- ( ph -> F : A --> E )
7		fisuppov1.7	|- ( ph -> F finSupp .0. )
8		fisuppov1.8	|- ( ( ph /\ y e. Y ) -> ( .0. O y ) = Z )
9	3 4	ssexd	|- ( ph -> D e. _V )
10	9	mptexd	|- ( ph -> ( x e. D |-> ( ( F ` x ) O B ) ) e. _V )
11		funmpt	|- Fun ( x e. D |-> ( ( F ` x ) O B ) )
12	11	a1i	|- ( ph -> Fun ( x e. D |-> ( ( F ` x ) O B ) ) )
13	6 4	feqresmpt	|- ( ph -> ( F |` D ) = ( x e. D |-> ( F ` x ) ) )
14	13	oveq1d	|- ( ph -> ( ( F |` D ) supp .0. ) = ( ( x e. D |-> ( F ` x ) ) supp .0. ) )
15	6 3	fexd	|- ( ph -> F e. _V )
16		ressuppss	|- ( ( F e. _V /\ .0. e. X ) -> ( ( F |` D ) supp .0. ) C_ ( F supp .0. ) )
17	15 2 16	syl2anc	|- ( ph -> ( ( F |` D ) supp .0. ) C_ ( F supp .0. ) )
18	14 17	eqsstrrd	|- ( ph -> ( ( x e. D |-> ( F ` x ) ) supp .0. ) C_ ( F supp .0. ) )
19		fvexd	|- ( ( ph /\ x e. D ) -> ( F ` x ) e. _V )
20	18 8 19 5 2	suppssov1	|- ( ph -> ( ( x e. D |-> ( ( F ` x ) O B ) ) supp Z ) C_ ( F supp .0. ) )
21	10 1 12 7 20	fsuppsssuppgd	|- ( ph -> ( x e. D |-> ( ( F ` x ) O B ) ) finSupp Z )