This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑋 = ( var1 ‘ 𝑅 )
vr1cl2.2 ⊢ 𝑆 = ( PwSer1 ‘ 𝑅 )
vr1cl2.3 ⊢ 𝐵 = ( Base ‘ 𝑆 )
Assertion vr1cl2 ( 𝑅 ∈ Ring → 𝑋 ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 vr1val.1 ⊢ 𝑋 = ( var1 ‘ 𝑅 )
2 vr1cl2.2 ⊢ 𝑆 = ( PwSer1 ‘ 𝑅 )
3 vr1cl2.3 ⊢ 𝐵 = ( Base ‘ 𝑆 )
4 1 vr1val ⊢ 𝑋 = ( ( 1o mVar 𝑅 ) ‘ ∅ )
5 eqid ⊢ ( 1o mPwSer 𝑅 ) = ( 1o mPwSer 𝑅 )
6 eqid ⊢ ( 1o mVar 𝑅 ) = ( 1o mVar 𝑅 )
7 eqid ⊢ ( Base ‘ ( 1o mPwSer 𝑅 ) ) = ( Base ‘ ( 1o mPwSer 𝑅 ) )
8 1on ⊢ 1o ∈ On
9 8 a1i ⊢ ( 𝑅 ∈ Ring → 1o ∈ On )
10 id ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Ring )
11 0lt1o ⊢ ∅ ∈ 1o
12 11 a1i ⊢ ( 𝑅 ∈ Ring → ∅ ∈ 1o )
13 5 6 7 9 10 12 mvrcl2 ⊢ ( 𝑅 ∈ Ring → ( ( 1o mVar 𝑅 ) ‘ ∅ ) ∈ ( Base ‘ ( 1o mPwSer 𝑅 ) ) )
14 2 psr1val ⊢ 𝑆 = ( ( 1o ordPwSer 𝑅 ) ‘ ∅ )
15 0ss ⊢ ∅ ⊆ ( 1o × 1o )
16 15 a1i ⊢ ( 𝑅 ∈ Ring → ∅ ⊆ ( 1o × 1o ) )
17 5 14 16 opsrbas ⊢ ( 𝑅 ∈ Ring → ( Base ‘ ( 1o mPwSer 𝑅 ) ) = ( Base ‘ 𝑆 ) )
18 17 3 eqtr4di ⊢ ( 𝑅 ∈ Ring → ( Base ‘ ( 1o mPwSer 𝑅 ) ) = 𝐵 )
19 13 18 eleqtrd ⊢ ( 𝑅 ∈ Ring → ( ( 1o mVar 𝑅 ) ‘ ∅ ) ∈ 𝐵 )
20 4 19 eqeltrid ⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ 𝐵 )