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

Metamath Proof Explorer

Theorem psrmon

Description: A monomial is a power series. (Contributed by Thierry Arnoux, 16-Mar-2026)

Ref Expression
Hypotheses psrmon.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
psrmon.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
psrmon.z ⊢ 0 = ( 0g ‘ 𝑅 )
psrmon.o ⊢ 1 = ( 1r ‘ 𝑅 )
psrmon.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
psrmon.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
psrmon.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
psrmon.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
Assertion psrmon ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 psrmon.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psrmon.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
3 psrmon.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 psrmon.o ⊢ 1 = ( 1r ‘ 𝑅 )
5 psrmon.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
6 psrmon.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
7 psrmon.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
8 psrmon.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
9 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10 9 4 ringidcl ⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Base ‘ 𝑅 ) )
11 9 3 ring0cl ⊢ ( 𝑅 ∈ Ring → 0 ∈ ( Base ‘ 𝑅 ) )
12 10 11 ifcld ⊢ ( 𝑅 ∈ Ring → if ( 𝑦 = 𝑋 , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
13 7 12 syl ⊢ ( 𝜑 → if ( 𝑦 = 𝑋 , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → if ( 𝑦 = 𝑋 , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
15 14 fmpttd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
16 fvex ⊢ ( Base ‘ 𝑅 ) ∈ V
17 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
18 5 17 rabex2 ⊢ 𝐷 ∈ V
19 16 18 elmap ⊢ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) ↔ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
20 15 19 sylibr ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
21 5 psrbasfsupp ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
22 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
23 1 9 21 22 6 psrbas ⊢ ( 𝜑 → ( Base ‘ 𝑆 ) = ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
24 20 23 eleqtrrd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ ( Base ‘ 𝑆 ) )
25 24 2 eleqtrrdi ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ 𝐵 )