Theorem mplvrpmlem

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

	Ref	Expression
Hypotheses	mplvrpmlem.s	|- S = ( SymGrp ` I )
	mplvrpmlem.p	|- P = ( Base ` S )
	mplvrpmlem.i	|- ( ph -> I e. V )
	mplvrpmlem.d	|- ( ph -> D e. P )
	mplvrpmlem.1	|- ( ph -> X e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
Assertion	mplvrpmlem	|- ( ph -> ( X o. D ) e. { h e. ( NN0 ^m I ) | h finSupp 0 } )

Proof

Step	Hyp	Ref	Expression
1		mplvrpmlem.s	|- S = ( SymGrp ` I )
2		mplvrpmlem.p	|- P = ( Base ` S )
3		mplvrpmlem.i	|- ( ph -> I e. V )
4		mplvrpmlem.d	|- ( ph -> D e. P )
5		mplvrpmlem.1	|- ( ph -> X e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
6		breq1	|- ( h = ( X o. D ) -> ( h finSupp 0 <-> ( X o. D ) finSupp 0 ) )
7		nn0ex	|- NN0 e. _V
8	7	a1i	|- ( ph -> NN0 e. _V )
9		ssrab2	|- { h e. ( NN0 ^m I ) | h finSupp 0 } C_ ( NN0 ^m I )
10	9 5	sselid	|- ( ph -> X e. ( NN0 ^m I ) )
11	3 8 10	elmaprd	|- ( ph -> X : I --> NN0 )
12	1 2	symgbasf1o	|- ( D e. P -> D : I -1-1-onto-> I )
13	4 12	syl	|- ( ph -> D : I -1-1-onto-> I )
14		f1of	|- ( D : I -1-1-onto-> I -> D : I --> I )
15	13 14	syl	|- ( ph -> D : I --> I )
16	11 15	fcod	|- ( ph -> ( X o. D ) : I --> NN0 )
17	8 3 16	elmapdd	|- ( ph -> ( X o. D ) e. ( NN0 ^m I ) )
18		breq1	|- ( h = X -> ( h finSupp 0 <-> X finSupp 0 ) )
19	18	elrab	|- ( X e. { h e. ( NN0 ^m I ) | h finSupp 0 } <-> ( X e. ( NN0 ^m I ) /\ X finSupp 0 ) )
20	19	simprbi	|- ( X e. { h e. ( NN0 ^m I ) | h finSupp 0 } -> X finSupp 0 )
21	5 20	syl	|- ( ph -> X finSupp 0 )
22		f1of1	|- ( D : I -1-1-onto-> I -> D : I -1-1-> I )
23	13 22	syl	|- ( ph -> D : I -1-1-> I )
24		0nn0	|- 0 e. NN0
25	24	a1i	|- ( ph -> 0 e. NN0 )
26	21 23 25 5	fsuppco	|- ( ph -> ( X o. D ) finSupp 0 )
27	6 17 26	elrabd	|- ( ph -> ( X o. D ) e. { h e. ( NN0 ^m I ) | h finSupp 0 } )