Metamath Proof Explorer


Theorem vr1cl2

Description: The variable X is a member of the power series algebra R [ [ X ] ] . (Contributed by Mario Carneiro, 8-Feb-2015)

Ref Expression
Hypotheses vr1val.1 X = var 1 R
vr1cl2.2 S = PwSer 1 R
vr1cl2.3 B = Base S
Assertion vr1cl2 R Ring X B

Proof

Step Hyp Ref Expression
1 vr1val.1 X = var 1 R
2 vr1cl2.2 S = PwSer 1 R
3 vr1cl2.3 B = Base S
4 1 vr1val X = 1 𝑜 mVar R
5 eqid 1 𝑜 mPwSer R = 1 𝑜 mPwSer R
6 eqid 1 𝑜 mVar R = 1 𝑜 mVar R
7 eqid Base 1 𝑜 mPwSer R = Base 1 𝑜 mPwSer R
8 1on 1 𝑜 On
9 8 a1i R Ring 1 𝑜 On
10 id R Ring R Ring
11 0lt1o 1 𝑜
12 11 a1i R Ring 1 𝑜
13 5 6 7 9 10 12 mvrcl2 R Ring 1 𝑜 mVar R Base 1 𝑜 mPwSer R
14 2 psr1val S = 1 𝑜 ordPwSer R
15 0ss 1 𝑜 × 1 𝑜
16 15 a1i R Ring 1 𝑜 × 1 𝑜
17 5 14 16 opsrbas R Ring Base 1 𝑜 mPwSer R = Base S
18 17 3 eqtr4di R Ring Base 1 𝑜 mPwSer R = B
19 13 18 eleqtrd R Ring 1 𝑜 mVar R B
20 4 19 eqeltrid R Ring X B