mplvrpmlem

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

	Ref	Expression
Hypotheses	mplvrpmlem.s	⊢ 𝑆 = ( SymGrp ‘ 𝐼 )
	mplvrpmlem.p	⊢ 𝑃 = ( Base ‘ 𝑆 )
	mplvrpmlem.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	mplvrpmlem.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
	mplvrpmlem.1	⊢ ( 𝜑 → 𝑋 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } )
Assertion	mplvrpmlem	⊢ ( 𝜑 → ( 𝑋 ∘ 𝐷 ) ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } )

Proof

Step	Hyp	Ref	Expression
1		mplvrpmlem.s	⊢ 𝑆 = ( SymGrp ‘ 𝐼 )
2		mplvrpmlem.p	⊢ 𝑃 = ( Base ‘ 𝑆 )
3		mplvrpmlem.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4		mplvrpmlem.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
5		mplvrpmlem.1	⊢ ( 𝜑 → 𝑋 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } )
6		breq1	⊢ ( ℎ = ( 𝑋 ∘ 𝐷 ) → ( ℎ finSupp 0 ↔ ( 𝑋 ∘ 𝐷 ) finSupp 0 ) )
7		nn0ex	⊢ ℕ₀ ∈ V
8	7	a1i	⊢ ( 𝜑 → ℕ₀ ∈ V )
9		ssrab2	⊢ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ⊆ ( ℕ₀ ↑_m 𝐼 )
10	9 5	sselid	⊢ ( 𝜑 → 𝑋 ∈ ( ℕ₀ ↑_m 𝐼 ) )
11	3 8 10	elmaprd	⊢ ( 𝜑 → 𝑋 : 𝐼 ⟶ ℕ₀ )
12	1 2	symgbasf1o	⊢ ( 𝐷 ∈ 𝑃 → 𝐷 : 𝐼 –1-1-onto→ 𝐼 )
13	4 12	syl	⊢ ( 𝜑 → 𝐷 : 𝐼 –1-1-onto→ 𝐼 )
14		f1of	⊢ ( 𝐷 : 𝐼 –1-1-onto→ 𝐼 → 𝐷 : 𝐼 ⟶ 𝐼 )
15	13 14	syl	⊢ ( 𝜑 → 𝐷 : 𝐼 ⟶ 𝐼 )
16	11 15	fcod	⊢ ( 𝜑 → ( 𝑋 ∘ 𝐷 ) : 𝐼 ⟶ ℕ₀ )
17	8 3 16	elmapdd	⊢ ( 𝜑 → ( 𝑋 ∘ 𝐷 ) ∈ ( ℕ₀ ↑_m 𝐼 ) )
18		breq1	⊢ ( ℎ = 𝑋 → ( ℎ finSupp 0 ↔ 𝑋 finSupp 0 ) )
19	18	elrab	⊢ ( 𝑋 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↔ ( 𝑋 ∈ ( ℕ₀ ↑_m 𝐼 ) ∧ 𝑋 finSupp 0 ) )
20	19	simprbi	⊢ ( 𝑋 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } → 𝑋 finSupp 0 )
21	5 20	syl	⊢ ( 𝜑 → 𝑋 finSupp 0 )
22		f1of1	⊢ ( 𝐷 : 𝐼 –1-1-onto→ 𝐼 → 𝐷 : 𝐼 –1-1→ 𝐼 )
23	13 22	syl	⊢ ( 𝜑 → 𝐷 : 𝐼 –1-1→ 𝐼 )
24		0nn0	⊢ 0 ∈ ℕ₀
25	24	a1i	⊢ ( 𝜑 → 0 ∈ ℕ₀ )
26	21 23 25 5	fsuppco	⊢ ( 𝜑 → ( 𝑋 ∘ 𝐷 ) finSupp 0 )
27	6 17 26	elrabd	⊢ ( 𝜑 → ( 𝑋 ∘ 𝐷 ) ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } )

Metamath Proof Explorer

Theorem mplvrpmlem

Proof