vr1val

Description: The value of the generator of the power series algebra (the X in R [ [ X ] ] ). Since all univariate polynomial rings over a fixed base ring R are isomorphic, we don't bother to pass this in as a parameter; internally we are actually using the empty set as this generator and 1o = { (/) } is the index set (but for most purposes this choice should not be visible anyway). (Contributed by Mario Carneiro, 8-Feb-2015) (Revised by Mario Carneiro, 12-Jun-2015)

		Ref	Expression
	Hypothesis	vr1val.1	$⊢ X = {var}_{1} (R)$
	Assertion	vr1val	$⊢ X = (1_{𝑜} mVar R) (\emptyset)$

Proof

Step	Hyp	Ref	Expression
1		vr1val.1	$⊢ X = {var}_{1} (R)$
2		oveq2	$⊢ r = R \to 1_{𝑜} mVar r = 1_{𝑜} mVar R$
3	2	fveq1d	$⊢ r = R \to (1_{𝑜} mVar r) (\emptyset) = (1_{𝑜} mVar R) (\emptyset)$
4		df-vr1	$⊢ {var}_{1} = (r \in V ⟼ (1_{𝑜} mVar r) (\emptyset))$
5		fvex	$⊢ (1_{𝑜} mVar R) (\emptyset) \in V$
6	3 4 5	fvmpt	$⊢ R \in V \to {var}_{1} (R) = (1_{𝑜} mVar R) (\emptyset)$
7	1 6	eqtrid	$⊢ R \in V \to X = (1_{𝑜} mVar R) (\emptyset)$
8		fvprc	$⊢ \neg R \in V \to {var}_{1} (R) = \emptyset$
9		0fv	$⊢ \emptyset (\emptyset) = \emptyset$
10	8 1 9	3eqtr4g	$⊢ \neg R \in V \to X = \emptyset (\emptyset)$
11		df-mvr	$⊢ mVar = (i \in V, r \in V ⟼ (x \in i ⟼ (f \in \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (f = (y \in i ⟼ if (y = x, 1, 0)), 1_{r}, 0_{r}))))$
12	11	reldmmpo	$⊢ Rel dom mVar$
13	12	ovprc2	$⊢ \neg R \in V \to 1_{𝑜} mVar R = \emptyset$
14	13	fveq1d	$⊢ \neg R \in V \to (1_{𝑜} mVar R) (\emptyset) = \emptyset (\emptyset)$
15	10 14	eqtr4d	$⊢ \neg R \in V \to X = (1_{𝑜} mVar R) (\emptyset)$
16	7 15	pm2.61i	$⊢ X = (1_{𝑜} mVar R) (\emptyset)$

Metamath Proof Explorer

Theorem vr1val

Proof