This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem esplylem

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

Ref Expression
Hypotheses esplympl.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
esplympl.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
esplympl.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
esplympl.k ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
Assertion esplylem ( 𝜑 → ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ⊆ 𝐷 )

Proof

Step Hyp Ref Expression
1 esplympl.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
2 esplympl.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
3 esplympl.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
4 esplympl.k ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
5 nfv ⊢ Ⅎ 𝑑 𝜑
6 indf1o ⊢ ( 𝐼 ∈ Fin → ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 –1-1-onto→ ( { 0 , 1 } ↑m 𝐼 ) )
7 f1of ⊢ ( ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 –1-1-onto→ ( { 0 , 1 } ↑m 𝐼 ) → ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 ⟶ ( { 0 , 1 } ↑m 𝐼 ) )
8 2 6 7 3syl ⊢ ( 𝜑 → ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 ⟶ ( { 0 , 1 } ↑m 𝐼 ) )
9 8 ffund ⊢ ( 𝜑 → Fun ( 𝟭 ‘ 𝐼 ) )
10 breq1 ⊢ ( ℎ = ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) → ( ℎ finSupp 0 ↔ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) finSupp 0 ) )
11 nn0ex ⊢ ℕ0 ∈ V
12 11 a1i ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → ℕ0 ∈ V )
13 2 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → 𝐼 ∈ Fin )
14 ssrab2 ⊢ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ⊆ 𝒫 𝐼
15 14 a1i ⊢ ( 𝜑 → { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ⊆ 𝒫 𝐼 )
16 15 sselda ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → 𝑑 ∈ 𝒫 𝐼 )
17 16 elpwid ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → 𝑑 ⊆ 𝐼 )
18 indf ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑑 ⊆ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) : 𝐼 ⟶ { 0 , 1 } )
19 13 17 18 syl2anc ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) : 𝐼 ⟶ { 0 , 1 } )
20 0nn0 ⊢ 0 ∈ ℕ0
21 20 a1i ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → 0 ∈ ℕ0 )
22 1nn0 ⊢ 1 ∈ ℕ0
23 22 a1i ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → 1 ∈ ℕ0 )
24 21 23 prssd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → { 0 , 1 } ⊆ ℕ0 )
25 19 24 fssd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) : 𝐼 ⟶ ℕ0 )
26 12 13 25 elmapdd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) ∈ ( ℕ0 ↑m 𝐼 ) )
27 19 13 21 fidmfisupp ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) finSupp 0 )
28 10 26 27 elrabd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
29 28 1 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) ∈ 𝐷 )
30 5 9 29 funimassd ⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ⊆ 𝐷 )