Theorem fsuppssindlem1

Description: Lemma for fsuppssind . Functions are zero outside of their support. (Contributed by SN, 15-Jul-2024)

	Ref	Expression
Hypotheses	fsuppssindlem1.z	|- ( ph -> .0. e. W )
	fsuppssindlem1.v	|- ( ph -> I e. V )
	fsuppssindlem1.1	|- ( ph -> F : I --> B )
	fsuppssindlem1.2	|- ( ph -> ( F supp .0. ) C_ S )
Assertion	fsuppssindlem1	|- ( ph -> F = ( x e. I |-> if ( x e. S , ( ( F |` S ) ` x ) , .0. ) ) )

Proof

Step	Hyp	Ref	Expression
1		fsuppssindlem1.z	|- ( ph -> .0. e. W )
2		fsuppssindlem1.v	|- ( ph -> I e. V )
3		fsuppssindlem1.1	|- ( ph -> F : I --> B )
4		fsuppssindlem1.2	|- ( ph -> ( F supp .0. ) C_ S )
5	3	feqmptd	|- ( ph -> F = ( x e. I |-> ( F ` x ) ) )
6		fvres	|- ( x e. S -> ( ( F |` S ) ` x ) = ( F ` x ) )
7	6	adantl	|- ( ( ( ph /\ x e. I ) /\ x e. S ) -> ( ( F |` S ) ` x ) = ( F ` x ) )
8		eldif	|- ( x e. ( I \ S ) <-> ( x e. I /\ -. x e. S ) )
9	3 4 2 1	suppssr	|- ( ( ph /\ x e. ( I \ S ) ) -> ( F ` x ) = .0. )
10	9	eqcomd	|- ( ( ph /\ x e. ( I \ S ) ) -> .0. = ( F ` x ) )
11	8 10	sylan2br	|- ( ( ph /\ ( x e. I /\ -. x e. S ) ) -> .0. = ( F ` x ) )
12	11	anassrs	|- ( ( ( ph /\ x e. I ) /\ -. x e. S ) -> .0. = ( F ` x ) )
13	7 12	ifeqda	|- ( ( ph /\ x e. I ) -> if ( x e. S , ( ( F |` S ) ` x ) , .0. ) = ( F ` x ) )
14	13	mpteq2dva	|- ( ph -> ( x e. I |-> if ( x e. S , ( ( F |` S ) ` x ) , .0. ) ) = ( x e. I |-> ( F ` x ) ) )
15	5 14	eqtr4d	|- ( ph -> F = ( x e. I |-> if ( x e. S , ( ( F |` S ) ` x ) , .0. ) ) )