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 )

Metamath Proof Explorer

Theorem esplylem

Proof