Theorem 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	⊢ 𝑋 = ( var1 ‘ 𝑅 )
Assertion	vr1val	⊢ 𝑋 = ( ( 1o mVar 𝑅 ) ‘ ∅ )

Proof

Step	Hyp	Ref	Expression
1		vr1val.1	⊢ 𝑋 = ( var1 ‘ 𝑅 )
2		oveq2	⊢ ( 𝑟 = 𝑅 → ( 1o mVar 𝑟 ) = ( 1o mVar 𝑅 ) )
3	2	fveq1d	⊢ ( 𝑟 = 𝑅 → ( ( 1o mVar 𝑟 ) ‘ ∅ ) = ( ( 1o mVar 𝑅 ) ‘ ∅ ) )
4		df-vr1	⊢ var1 = ( 𝑟 ∈ V ↦ ( ( 1o mVar 𝑟 ) ‘ ∅ ) )
5		fvex	⊢ ( ( 1o mVar 𝑅 ) ‘ ∅ ) ∈ V
6	3 4 5	fvmpt	⊢ ( 𝑅 ∈ V → ( var1 ‘ 𝑅 ) = ( ( 1o mVar 𝑅 ) ‘ ∅ ) )
7	1 6	syl5eq	⊢ ( 𝑅 ∈ V → 𝑋 = ( ( 1o mVar 𝑅 ) ‘ ∅ ) )
8		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( var1 ‘ 𝑅 ) = ∅ )
9		0fv	⊢ ( ∅ ‘ ∅ ) = ∅
10	8 1 9	3eqtr4g	⊢ ( ¬ 𝑅 ∈ V → 𝑋 = ( ∅ ‘ ∅ ) )
11		df-mvr	⊢ mVar = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑥 ∈ 𝑖 ↦ ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) ) ) )
12	11	reldmmpo	⊢ Rel dom mVar
13	12	ovprc2	⊢ ( ¬ 𝑅 ∈ V → ( 1o mVar 𝑅 ) = ∅ )
14	13	fveq1d	⊢ ( ¬ 𝑅 ∈ V → ( ( 1o mVar 𝑅 ) ‘ ∅ ) = ( ∅ ‘ ∅ ) )
15	10 14	eqtr4d	⊢ ( ¬ 𝑅 ∈ V → 𝑋 = ( ( 1o mVar 𝑅 ) ‘ ∅ ) )
16	7 15	pm2.61i	⊢ 𝑋 = ( ( 1o mVar 𝑅 ) ‘ ∅ )