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 ⊢ S = I mPwSer R
psrmon.b ⊢ B = Base S
psrmon.z ⊢ 0 ˙ = 0 R
psrmon.o ⊢ 1 ˙ = 1 R
psrmon.d ⊢ D = h ∈ ℕ 0 I | finSupp 0 ⁡ h
psrmon.i ⊢ φ → I ∈ W
psrmon.r ⊢ φ → R ∈ Ring
psrmon.x ⊢ φ → X ∈ D
Assertion psrmon ⊢ φ → y ∈ D ⟼ if y = X 1 ˙ 0 ˙ ∈ B

Proof

Step Hyp Ref Expression
1 psrmon.s ⊢ S = I mPwSer R
2 psrmon.b ⊢ B = Base S
3 psrmon.z ⊢ 0 ˙ = 0 R
4 psrmon.o ⊢ 1 ˙ = 1 R
5 psrmon.d ⊢ D = h ∈ ℕ 0 I | finSupp 0 ⁡ h
6 psrmon.i ⊢ φ → I ∈ W
7 psrmon.r ⊢ φ → R ∈ Ring
8 psrmon.x ⊢ φ → X ∈ D
9 eqid ⊢ Base R = Base R
10 9 4 ringidcl ⊢ R ∈ Ring → 1 ˙ ∈ Base R
11 9 3 ring0cl ⊢ R ∈ Ring → 0 ˙ ∈ Base R
12 10 11 ifcld ⊢ R ∈ Ring → if y = X 1 ˙ 0 ˙ ∈ Base R
13 7 12 syl ⊢ φ → if y = X 1 ˙ 0 ˙ ∈ Base R
14 13 adantr ⊢ φ ∧ y ∈ D → if y = X 1 ˙ 0 ˙ ∈ Base R
15 14 fmpttd ⊢ φ → y ∈ D ⟼ if y = X 1 ˙ 0 ˙ : D ⟶ Base R
16 fvex ⊢ Base R ∈ V
17 ovex ⊢ ℕ 0 I ∈ V
18 5 17 rabex2 ⊢ D ∈ V
19 16 18 elmap ⊢ y ∈ D ⟼ if y = X 1 ˙ 0 ˙ ∈ Base R D ↔ y ∈ D ⟼ if y = X 1 ˙ 0 ˙ : D ⟶ Base R
20 15 19 sylibr ⊢ φ → y ∈ D ⟼ if y = X 1 ˙ 0 ˙ ∈ Base R D
21 5 psrbasfsupp ⊢ D = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
22 eqid ⊢ Base S = Base S
23 1 9 21 22 6 psrbas ⊢ φ → Base S = Base R D
24 20 23 eleqtrrd ⊢ φ → y ∈ D ⟼ if y = X 1 ˙ 0 ˙ ∈ Base S
25 24 2 eleqtrrdi ⊢ φ → y ∈ D ⟼ if y = X 1 ˙ 0 ˙ ∈ B