This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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