Metamath Proof Explorer


Theorem mvrcl2

Description: A power series variable is an element of the base set. (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypotheses mvrf.s 𝑆 = ( 𝐼 mPwSer 𝑅 )
mvrf.v 𝑉 = ( 𝐼 mVar 𝑅 )
mvrf.b 𝐵 = ( Base ‘ 𝑆 )
mvrf.i ( 𝜑𝐼𝑊 )
mvrf.r ( 𝜑𝑅 ∈ Ring )
mvrcl2.x ( 𝜑𝑋𝐼 )
Assertion mvrcl2 ( 𝜑 → ( 𝑉𝑋 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 mvrf.s 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 mvrf.v 𝑉 = ( 𝐼 mVar 𝑅 )
3 mvrf.b 𝐵 = ( Base ‘ 𝑆 )
4 mvrf.i ( 𝜑𝐼𝑊 )
5 mvrf.r ( 𝜑𝑅 ∈ Ring )
6 mvrcl2.x ( 𝜑𝑋𝐼 )
7 1 2 3 4 5 mvrf ( 𝜑𝑉 : 𝐼𝐵 )
8 7 6 ffvelrnd ( 𝜑 → ( 𝑉𝑋 ) ∈ 𝐵 )