Metamath Proof Explorer

Theorem fsuppssindlem2

Description: Lemma for fsuppssind . Write a function as a union. (Contributed by SN, 15-Jul-2024)

Ref Expression
Hypotheses fsuppssindlem2.b 
|- ( ph -> B e. W )
fsuppssindlem2.v 
|- ( ph -> I e. V )
fsuppssindlem2.s 
|- ( ph -> S C_ I )
Assertion fsuppssindlem2 
|- ( ph -> ( F e. { f e. ( B ^m S ) | ( x e. I |-> if ( x e. S , ( f ` x ) , .0. ) ) e. H } <-> ( F : S --> B /\ ( F u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) )

Proof

Step Hyp Ref Expression
1 fsuppssindlem2.b 
 |-  ( ph -> B e. W )
2 fsuppssindlem2.v 
 |-  ( ph -> I e. V )
3 fsuppssindlem2.s 
 |-  ( ph -> S C_ I )
4 fveq1 
 |-  ( f = F -> ( f ` x ) = ( F ` x ) )
5 4 ifeq1d 
 |-  ( f = F -> if ( x e. S , ( f ` x ) , .0. ) = if ( x e. S , ( F ` x ) , .0. ) )
6 5 mpteq2dv 
 |-  ( f = F -> ( x e. I |-> if ( x e. S , ( f ` x ) , .0. ) ) = ( x e. I |-> if ( x e. S , ( F ` x ) , .0. ) ) )
7 6 eleq1d 
 |-  ( f = F -> ( ( x e. I |-> if ( x e. S , ( f ` x ) , .0. ) ) e. H <-> ( x e. I |-> if ( x e. S , ( F ` x ) , .0. ) ) e. H ) )
8 7 elrab 
 |-  ( F e. { f e. ( B ^m S ) | ( x e. I |-> if ( x e. S , ( f ` x ) , .0. ) ) e. H } <-> ( F e. ( B ^m S ) /\ ( x e. I |-> if ( x e. S , ( F ` x ) , .0. ) ) e. H ) )
9 2 3 ssexd 
 |-  ( ph -> S e. _V )
10 1 9 elmapd 
 |-  ( ph -> ( F e. ( B ^m S ) <-> F : S --> B ) )
11 10 anbi1d 
 |-  ( ph -> ( ( F e. ( B ^m S ) /\ ( x e. I |-> if ( x e. S , ( F ` x ) , .0. ) ) e. H ) <-> ( F : S --> B /\ ( x e. I |-> if ( x e. S , ( F ` x ) , .0. ) ) e. H ) ) )
12 partfun 
 |-  ( x e. I |-> if ( x e. S , ( F ` x ) , .0. ) ) = ( ( x e. ( I i^i S ) |-> ( F ` x ) ) u. ( x e. ( I \ S ) |-> .0. ) )
13 sseqin2 
 |-  ( S C_ I <-> ( I i^i S ) = S )
14 3 13 sylib 
 |-  ( ph -> ( I i^i S ) = S )
15 14 mpteq1d 
 |-  ( ph -> ( x e. ( I i^i S ) |-> ( F ` x ) ) = ( x e. S |-> ( F ` x ) ) )
16 15 adantr 
 |-  ( ( ph /\ F : S --> B ) -> ( x e. ( I i^i S ) |-> ( F ` x ) ) = ( x e. S |-> ( F ` x ) ) )
17 simpr 
 |-  ( ( ph /\ F : S --> B ) -> F : S --> B )
18 17 feqmptd 
 |-  ( ( ph /\ F : S --> B ) -> F = ( x e. S |-> ( F ` x ) ) )
19 16 18 eqtr4d 
 |-  ( ( ph /\ F : S --> B ) -> ( x e. ( I i^i S ) |-> ( F ` x ) ) = F )
20 fconstmpt 
 |-  ( ( I \ S ) X. { .0. } ) = ( x e. ( I \ S ) |-> .0. )
21 20 eqcomi 
 |-  ( x e. ( I \ S ) |-> .0. ) = ( ( I \ S ) X. { .0. } )
22 21 a1i 
 |-  ( ( ph /\ F : S --> B ) -> ( x e. ( I \ S ) |-> .0. ) = ( ( I \ S ) X. { .0. } ) )
23 19 22 uneq12d 
 |-  ( ( ph /\ F : S --> B ) -> ( ( x e. ( I i^i S ) |-> ( F ` x ) ) u. ( x e. ( I \ S ) |-> .0. ) ) = ( F u. ( ( I \ S ) X. { .0. } ) ) )
24 12 23 syl5eq 
 |-  ( ( ph /\ F : S --> B ) -> ( x e. I |-> if ( x e. S , ( F ` x ) , .0. ) ) = ( F u. ( ( I \ S ) X. { .0. } ) ) )
25 24 eleq1d 
 |-  ( ( ph /\ F : S --> B ) -> ( ( x e. I |-> if ( x e. S , ( F ` x ) , .0. ) ) e. H <-> ( F u. ( ( I \ S ) X. { .0. } ) ) e. H ) )
26 25 pm5.32da 
 |-  ( ph -> ( ( F : S --> B /\ ( x e. I |-> if ( x e. S , ( F ` x ) , .0. ) ) e. H ) <-> ( F : S --> B /\ ( F u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) )
27 11 26 bitrd 
 |-  ( ph -> ( ( F e. ( B ^m S ) /\ ( x e. I |-> if ( x e. S , ( F ` x ) , .0. ) ) e. H ) <-> ( F : S --> B /\ ( F u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) )
28 8 27 syl5bb 
 |-  ( ph -> ( F e. { f e. ( B ^m S ) | ( x e. I |-> if ( x e. S , ( f ` x ) , .0. ) ) e. H } <-> ( F : S --> B /\ ( F u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) )