Metamath Proof Explorer

Theorem esplylem

Description: Lemma for esplyfv and others. (Contributed by Thierry Arnoux, 18-Jan-2026)

Ref Expression
Hypotheses esplympl.d 
|- D = { h e. ( NN0 ^m I ) | h finSupp 0 }
esplympl.i 
|- ( ph -> I e. Fin )
esplympl.r 
|- ( ph -> R e. Ring )
esplympl.k 
|- ( ph -> K e. NN0 )
Assertion esplylem 
|- ( ph -> ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) C_ D )

Proof

Step Hyp Ref Expression
1 esplympl.d 
 |-  D = { h e. ( NN0 ^m I ) | h finSupp 0 }
2 esplympl.i 
 |-  ( ph -> I e. Fin )
3 esplympl.r 
 |-  ( ph -> R e. Ring )
4 esplympl.k 
 |-  ( ph -> K e. NN0 )
5 nfv 
 |-  F/ d ph
6 indf1o 
 |-  ( I e. Fin -> ( _Ind ` I ) : ~P I -1-1-onto-> ( { 0 , 1 } ^m I ) )
7 f1of 
 |-  ( ( _Ind ` I ) : ~P I -1-1-onto-> ( { 0 , 1 } ^m I ) -> ( _Ind ` I ) : ~P I --> ( { 0 , 1 } ^m I ) )
8 2 6 7 3syl 
 |-  ( ph -> ( _Ind ` I ) : ~P I --> ( { 0 , 1 } ^m I ) )
9 8 ffund 
 |-  ( ph -> Fun ( _Ind ` I ) )
10 breq1 
 |-  ( h = ( ( _Ind ` I ) ` d ) -> ( h finSupp 0 <-> ( ( _Ind ` I ) ` d ) finSupp 0 ) )
11 nn0ex 
 |-  NN0 e. _V
12 11 a1i 
 |-  ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> NN0 e. _V )
13 2 adantr 
 |-  ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> I e. Fin )
14 ssrab2 
 |-  { c e. ~P I | ( # ` c ) = K } C_ ~P I
15 14 a1i 
 |-  ( ph -> { c e. ~P I | ( # ` c ) = K } C_ ~P I )
16 15 sselda 
 |-  ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> d e. ~P I )
17 16 elpwid 
 |-  ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> d C_ I )
18 indf 
 |-  ( ( I e. Fin /\ d C_ I ) -> ( ( _Ind ` I ) ` d ) : I --> { 0 , 1 } )
19 13 17 18 syl2anc 
 |-  ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> ( ( _Ind ` I ) ` d ) : I --> { 0 , 1 } )
20 0nn0 
 |-  0 e. NN0
21 20 a1i 
 |-  ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> 0 e. NN0 )
22 1nn0 
 |-  1 e. NN0
23 22 a1i 
 |-  ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> 1 e. NN0 )
24 21 23 prssd 
 |-  ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> { 0 , 1 } C_ NN0 )
25 19 24 fssd 
 |-  ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> ( ( _Ind ` I ) ` d ) : I --> NN0 )
26 12 13 25 elmapdd 
 |-  ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> ( ( _Ind ` I ) ` d ) e. ( NN0 ^m I ) )
27 19 13 21 fidmfisupp 
 |-  ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> ( ( _Ind ` I ) ` d ) finSupp 0 )
28 10 26 27 elrabd 
 |-  ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> ( ( _Ind ` I ) ` d ) e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
29 28 1 eleqtrrdi 
 |-  ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> ( ( _Ind ` I ) ` d ) e. D )
30 5 9 29 funimassd 
 |-  ( ph -> ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) C_ D )