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	$⊢ φ \to I \in W$
	mvrcl.r	$⊢ φ \to R \in Ring$
	mvrcl.x	$⊢ φ \to X \in I$
Assertion	mvrcl	$⊢ φ \to V (X) \in 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	$⊢ φ \to I \in W$
5		mvrcl.r	$⊢ φ \to R \in Ring$
6		mvrcl.x	$⊢ φ \to X \in 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	$⊢ φ \to V (X) \in {Base}_{(I mPwSer R)}$
10		fvexd	$⊢ φ \to V (X) \in V$
11		eqid	$⊢ {Base}_{R} = {Base}_{R}$
12		eqid	$⊢ \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
13	7 11 12 8 9	psrelbas	$⊢ φ \to V (X) : \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟶ {Base}_{R}$
14	13	ffund	$⊢ φ \to Fun V (X)$
15		fvexd	$⊢ φ \to 0_{R} \in V$
16		snfi	$⊢ \{(y \in I ⟼ if (y = X, 1, 0))\} \in Fin$
17	16	a1i	$⊢ φ \to \{(y \in I ⟼ if (y = X, 1, 0))\} \in Fin$
18		eqid	$⊢ 0_{R} = 0_{R}$
19		eqid	$⊢ 1_{R} = 1_{R}$
20	4	adantr	$⊢ (φ \land x \in (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ∖ \{(y \in I ⟼ if (y = X, 1, 0))\})) \to I \in W$
21	5	adantr	$⊢ (φ \land x \in (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ∖ \{(y \in I ⟼ if (y = X, 1, 0))\})) \to R \in Ring$
22	6	adantr	$⊢ (φ \land x \in (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ∖ \{(y \in I ⟼ if (y = X, 1, 0))\})) \to X \in I$
23		simpr	$⊢ (φ \land x \in (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ∖ \{(y \in I ⟼ if (y = X, 1, 0))\})) \to x \in (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ∖ \{(y \in I ⟼ if (y = X, 1, 0))\})$
24		eldifsn	$⊢ x \in (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ∖ \{(y \in I ⟼ if (y = X, 1, 0))\}) \leftrightarrow (x \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \land x \neq (y \in I ⟼ if (y = X, 1, 0)))$
25	23 24	sylib	$⊢ (φ \land x \in (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ∖ \{(y \in I ⟼ if (y = X, 1, 0))\})) \to (x \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \land x \neq (y \in I ⟼ if (y = X, 1, 0)))$
26	25	simpld	$⊢ (φ \land x \in (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ∖ \{(y \in I ⟼ if (y = X, 1, 0))\})) \to x \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
27	2 12 18 19 20 21 22 26	mvrval2	$⊢ (φ \land x \in (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ∖ \{(y \in I ⟼ if (y = X, 1, 0))\})) \to V (X) (x) = if (x = (y \in I ⟼ if (y = X, 1, 0)), 1_{R}, 0_{R})$
28	25	simprd	$⊢ (φ \land x \in (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ∖ \{(y \in I ⟼ if (y = X, 1, 0))\})) \to x \neq (y \in I ⟼ if (y = X, 1, 0))$
29	28	neneqd	$⊢ (φ \land x \in (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ∖ \{(y \in I ⟼ if (y = X, 1, 0))\})) \to \neg x = (y \in I ⟼ if (y = X, 1, 0))$
30	29	iffalsed	$⊢ (φ \land x \in (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ∖ \{(y \in I ⟼ if (y = X, 1, 0))\})) \to if (x = (y \in I ⟼ if (y = X, 1, 0)), 1_{R}, 0_{R}) = 0_{R}$
31	27 30	eqtrd	$⊢ (φ \land x \in (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ∖ \{(y \in I ⟼ if (y = X, 1, 0))\})) \to V (X) (x) = 0_{R}$
32	13 31	suppss	$⊢ φ \to V (X) supp 0_{R} \subseteq \{(y \in I ⟼ if (y = X, 1, 0))\}$
33		suppssfifsupp	$⊢ ((V (X) \in V \land Fun V (X) \land 0_{R} \in V) \land (\{(y \in I ⟼ if (y = X, 1, 0))\} \in Fin \land V (X) supp 0_{R} \subseteq \{(y \in I ⟼ if (y = X, 1, 0))\})) \to {finSupp}_{0_{R}} (V (X))$
34	10 14 15 17 32 33	syl32anc	$⊢ φ \to {finSupp}_{0_{R}} (V (X))$
35	1 7 8 18 3	mplelbas	$⊢ V (X) \in B \leftrightarrow (V (X) \in {Base}_{(I mPwSer R)} \land {finSupp}_{0_{R}} (V (X)))$
36	9 34 35	sylanbrc	$⊢ φ \to V (X) \in B$

Metamath Proof Explorer

Theorem mvrcl

Proof