Metamath Proof Explorer

Theorem mvrcl

Description: A power series variable is a polynomial. (Contributed by Mario Carneiro, 9-Jan-2015)

Ref Expression
Hypotheses mvrcl.s ⊢ P = I mPoly R
mvrcl.v ⊢ V = I mVar R
mvrcl.b ⊢ B = Base P
mvrcl.i ⊢ φ → I ∈ W
mvrcl.r ⊢ φ → R ∈ Ring
mvrcl.x ⊢ φ → X ∈ I
Assertion mvrcl ⊢ φ → V ⁡ X ∈ B

Proof

Step Hyp Ref Expression
1 mvrcl.s ⊢ P = I mPoly R
2 mvrcl.v ⊢ V = I mVar R
3 mvrcl.b ⊢ B = Base P
4 mvrcl.i ⊢ φ → I ∈ W
5 mvrcl.r ⊢ φ → R ∈ Ring
6 mvrcl.x ⊢ φ → X ∈ I
7 eqid ⊢ I mPwSer R = I mPwSer R
8 eqid ⊢ Base I mPwSer R = Base I mPwSer R
9 7 2 8 4 5 6 mvrcl2 ⊢ φ → V ⁡ X ∈ Base I mPwSer R
10 fvexd ⊢ φ → V ⁡ X ∈ V
11 eqid ⊢ Base R = Base R
12 eqid ⊢ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
13 7 11 12 8 9 psrelbas ⊢ φ → V ⁡ X : f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ⟶ Base R
14 13 ffund ⊢ φ → Fun ⁡ V ⁡ X
15 fvexd ⊢ φ → 0 R ∈ V
16 snfi ⊢ y ∈ I ⟼ if y = X 1 0 ∈ Fin
17 16 a1i ⊢ φ → y ∈ I ⟼ if y = X 1 0 ∈ Fin
18 eqid ⊢ 0 R = 0 R
19 eqid ⊢ 1 R = 1 R
20 4 adantr ⊢ φ ∧ x ∈ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ∖ y ∈ I ⟼ if y = X 1 0 → I ∈ W
21 5 adantr ⊢ φ ∧ x ∈ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ∖ y ∈ I ⟼ if y = X 1 0 → R ∈ Ring
22 6 adantr ⊢ φ ∧ x ∈ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ∖ y ∈ I ⟼ if y = X 1 0 → X ∈ I
23 simpr ⊢ φ ∧ x ∈ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ∖ y ∈ I ⟼ if y = X 1 0 → x ∈ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ∖ y ∈ I ⟼ if y = X 1 0
24 eldifsn ⊢ x ∈ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ∖ y ∈ I ⟼ if y = X 1 0 ↔ x ∈ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ∧ x ≠ y ∈ I ⟼ if y = X 1 0
25 23 24 sylib ⊢ φ ∧ x ∈ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ∖ y ∈ I ⟼ if y = X 1 0 → x ∈ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ∧ x ≠ y ∈ I ⟼ if y = X 1 0
26 25 simpld ⊢ φ ∧ x ∈ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ∖ y ∈ I ⟼ if y = X 1 0 → x ∈ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
27 2 12 18 19 20 21 22 26 mvrval2 ⊢ φ ∧ x ∈ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ∖ y ∈ I ⟼ if y = X 1 0 → V ⁡ X ⁡ x = if x = y ∈ I ⟼ if y = X 1 0 1 R 0 R
28 25 simprd ⊢ φ ∧ x ∈ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ∖ y ∈ I ⟼ if y = X 1 0 → x ≠ y ∈ I ⟼ if y = X 1 0
29 28 neneqd ⊢ φ ∧ x ∈ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ∖ y ∈ I ⟼ if y = X 1 0 → ¬ x = y ∈ I ⟼ if y = X 1 0
30 29 iffalsed ⊢ φ ∧ x ∈ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ∖ y ∈ I ⟼ if y = X 1 0 → if x = y ∈ I ⟼ if y = X 1 0 1 R 0 R = 0 R
31 27 30 eqtrd ⊢ φ ∧ x ∈ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ∖ y ∈ I ⟼ if y = X 1 0 → V ⁡ X ⁡ x = 0 R
32 13 31 suppss ⊢ φ → V ⁡ X supp 0 R ⊆ y ∈ I ⟼ if y = X 1 0
33 suppssfifsupp ⊢ V ⁡ X ∈ V ∧ Fun ⁡ V ⁡ X ∧ 0 R ∈ V ∧ y ∈ I ⟼ if y = X 1 0 ∈ Fin ∧ V ⁡ X supp 0 R ⊆ y ∈ I ⟼ if y = X 1 0 → finSupp 0 R⁡ V ⁡ X
34 10 14 15 17 32 33 syl32anc ⊢ φ → finSupp 0 R⁡ V ⁡ X
35 1 7 8 18 3 mplelbas ⊢ V ⁡ X ∈ B ↔ V ⁡ X ∈ Base I mPwSer R ∧ finSupp 0 R⁡ V ⁡ X
36 9 34 35 sylanbrc ⊢ φ → V ⁡ X ∈ B