Metamath Proof Explorer


Theorem ressply1vsca

Description: A restricted power series algebra has the same scalar multiplication operation. (Contributed by Mario Carneiro, 3-Jul-2015)

Ref Expression
Hypotheses ressply1.s 𝑆 = ( Poly1𝑅 )
ressply1.h 𝐻 = ( 𝑅s 𝑇 )
ressply1.u 𝑈 = ( Poly1𝐻 )
ressply1.b 𝐵 = ( Base ‘ 𝑈 )
ressply1.2 ( 𝜑𝑇 ∈ ( SubRing ‘ 𝑅 ) )
ressply1.p 𝑃 = ( 𝑆s 𝐵 )
Assertion ressply1vsca ( ( 𝜑 ∧ ( 𝑋𝑇𝑌𝐵 ) ) → ( 𝑋 ( ·𝑠𝑈 ) 𝑌 ) = ( 𝑋 ( ·𝑠𝑃 ) 𝑌 ) )

Proof

Step Hyp Ref Expression
1 ressply1.s 𝑆 = ( Poly1𝑅 )
2 ressply1.h 𝐻 = ( 𝑅s 𝑇 )
3 ressply1.u 𝑈 = ( Poly1𝐻 )
4 ressply1.b 𝐵 = ( Base ‘ 𝑈 )
5 ressply1.2 ( 𝜑𝑇 ∈ ( SubRing ‘ 𝑅 ) )
6 ressply1.p 𝑃 = ( 𝑆s 𝐵 )
7 eqid ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
8 eqid ( 1o mPoly 𝐻 ) = ( 1o mPoly 𝐻 )
9 eqid ( PwSer1𝐻 ) = ( PwSer1𝐻 )
10 3 9 4 ply1bas 𝐵 = ( Base ‘ ( 1o mPoly 𝐻 ) )
11 1on 1o ∈ On
12 11 a1i ( 𝜑 → 1o ∈ On )
13 eqid ( ( 1o mPoly 𝑅 ) ↾s 𝐵 ) = ( ( 1o mPoly 𝑅 ) ↾s 𝐵 )
14 7 2 8 10 12 5 13 ressmplvsca ( ( 𝜑 ∧ ( 𝑋𝑇𝑌𝐵 ) ) → ( 𝑋 ( ·𝑠 ‘ ( 1o mPoly 𝐻 ) ) 𝑌 ) = ( 𝑋 ( ·𝑠 ‘ ( ( 1o mPoly 𝑅 ) ↾s 𝐵 ) ) 𝑌 ) )
15 eqid ( ·𝑠𝑈 ) = ( ·𝑠𝑈 )
16 3 8 15 ply1vsca ( ·𝑠𝑈 ) = ( ·𝑠 ‘ ( 1o mPoly 𝐻 ) )
17 16 oveqi ( 𝑋 ( ·𝑠𝑈 ) 𝑌 ) = ( 𝑋 ( ·𝑠 ‘ ( 1o mPoly 𝐻 ) ) 𝑌 )
18 eqid ( ·𝑠𝑆 ) = ( ·𝑠𝑆 )
19 1 7 18 ply1vsca ( ·𝑠𝑆 ) = ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) )
20 4 fvexi 𝐵 ∈ V
21 6 18 ressvsca ( 𝐵 ∈ V → ( ·𝑠𝑆 ) = ( ·𝑠𝑃 ) )
22 20 21 ax-mp ( ·𝑠𝑆 ) = ( ·𝑠𝑃 )
23 eqid ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) ) = ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) )
24 13 23 ressvsca ( 𝐵 ∈ V → ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) ) = ( ·𝑠 ‘ ( ( 1o mPoly 𝑅 ) ↾s 𝐵 ) ) )
25 20 24 ax-mp ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) ) = ( ·𝑠 ‘ ( ( 1o mPoly 𝑅 ) ↾s 𝐵 ) )
26 19 22 25 3eqtr3i ( ·𝑠𝑃 ) = ( ·𝑠 ‘ ( ( 1o mPoly 𝑅 ) ↾s 𝐵 ) )
27 26 oveqi ( 𝑋 ( ·𝑠𝑃 ) 𝑌 ) = ( 𝑋 ( ·𝑠 ‘ ( ( 1o mPoly 𝑅 ) ↾s 𝐵 ) ) 𝑌 )
28 14 17 27 3eqtr4g ( ( 𝜑 ∧ ( 𝑋𝑇𝑌𝐵 ) ) → ( 𝑋 ( ·𝑠𝑈 ) 𝑌 ) = ( 𝑋 ( ·𝑠𝑃 ) 𝑌 ) )