Metamath Proof Explorer


Theorem ressmplvsca

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

Ref Expression
Hypotheses ressmpl.s 𝑆 = ( 𝐼 mPoly 𝑅 )
ressmpl.h 𝐻 = ( 𝑅s 𝑇 )
ressmpl.u 𝑈 = ( 𝐼 mPoly 𝐻 )
ressmpl.b 𝐵 = ( Base ‘ 𝑈 )
ressmpl.1 ( 𝜑𝐼𝑉 )
ressmpl.2 ( 𝜑𝑇 ∈ ( SubRing ‘ 𝑅 ) )
ressmpl.p 𝑃 = ( 𝑆s 𝐵 )
Assertion ressmplvsca ( ( 𝜑 ∧ ( 𝑋𝑇𝑌𝐵 ) ) → ( 𝑋 ( ·𝑠𝑈 ) 𝑌 ) = ( 𝑋 ( ·𝑠𝑃 ) 𝑌 ) )

Proof

Step Hyp Ref Expression
1 ressmpl.s 𝑆 = ( 𝐼 mPoly 𝑅 )
2 ressmpl.h 𝐻 = ( 𝑅s 𝑇 )
3 ressmpl.u 𝑈 = ( 𝐼 mPoly 𝐻 )
4 ressmpl.b 𝐵 = ( Base ‘ 𝑈 )
5 ressmpl.1 ( 𝜑𝐼𝑉 )
6 ressmpl.2 ( 𝜑𝑇 ∈ ( SubRing ‘ 𝑅 ) )
7 ressmpl.p 𝑃 = ( 𝑆s 𝐵 )
8 eqid ( 𝐼 mPwSer 𝐻 ) = ( 𝐼 mPwSer 𝐻 )
9 eqid ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝐻 ) )
10 3 8 4 9 mplbasss 𝐵 ⊆ ( Base ‘ ( 𝐼 mPwSer 𝐻 ) )
11 10 sseli ( 𝑌𝐵𝑌 ∈ ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) )
12 eqid ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
13 eqid ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ) = ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) )
14 12 2 8 9 13 6 resspsrvsca ( ( 𝜑 ∧ ( 𝑋𝑇𝑌 ∈ ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ) ) → ( 𝑋 ( ·𝑠 ‘ ( 𝐼 mPwSer 𝐻 ) ) 𝑌 ) = ( 𝑋 ( ·𝑠 ‘ ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ) ) 𝑌 ) )
15 11 14 sylanr2 ( ( 𝜑 ∧ ( 𝑋𝑇𝑌𝐵 ) ) → ( 𝑋 ( ·𝑠 ‘ ( 𝐼 mPwSer 𝐻 ) ) 𝑌 ) = ( 𝑋 ( ·𝑠 ‘ ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ) ) 𝑌 ) )
16 4 fvexi 𝐵 ∈ V
17 3 8 4 mplval2 𝑈 = ( ( 𝐼 mPwSer 𝐻 ) ↾s 𝐵 )
18 eqid ( ·𝑠 ‘ ( 𝐼 mPwSer 𝐻 ) ) = ( ·𝑠 ‘ ( 𝐼 mPwSer 𝐻 ) )
19 17 18 ressvsca ( 𝐵 ∈ V → ( ·𝑠 ‘ ( 𝐼 mPwSer 𝐻 ) ) = ( ·𝑠𝑈 ) )
20 16 19 ax-mp ( ·𝑠 ‘ ( 𝐼 mPwSer 𝐻 ) ) = ( ·𝑠𝑈 )
21 20 oveqi ( 𝑋 ( ·𝑠 ‘ ( 𝐼 mPwSer 𝐻 ) ) 𝑌 ) = ( 𝑋 ( ·𝑠𝑈 ) 𝑌 )
22 fvex ( Base ‘ 𝑆 ) ∈ V
23 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
24 1 12 23 mplval2 𝑆 = ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ 𝑆 ) )
25 eqid ( ·𝑠 ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( ·𝑠 ‘ ( 𝐼 mPwSer 𝑅 ) )
26 24 25 ressvsca ( ( Base ‘ 𝑆 ) ∈ V → ( ·𝑠 ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( ·𝑠𝑆 ) )
27 22 26 ax-mp ( ·𝑠 ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( ·𝑠𝑆 )
28 fvex ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ∈ V
29 13 25 ressvsca ( ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ∈ V → ( ·𝑠 ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( ·𝑠 ‘ ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ) ) )
30 28 29 ax-mp ( ·𝑠 ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( ·𝑠 ‘ ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ) )
31 eqid ( ·𝑠𝑆 ) = ( ·𝑠𝑆 )
32 7 31 ressvsca ( 𝐵 ∈ V → ( ·𝑠𝑆 ) = ( ·𝑠𝑃 ) )
33 16 32 ax-mp ( ·𝑠𝑆 ) = ( ·𝑠𝑃 )
34 27 30 33 3eqtr3i ( ·𝑠 ‘ ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ) ) = ( ·𝑠𝑃 )
35 34 oveqi ( 𝑋 ( ·𝑠 ‘ ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ) ) 𝑌 ) = ( 𝑋 ( ·𝑠𝑃 ) 𝑌 )
36 15 21 35 3eqtr3g ( ( 𝜑 ∧ ( 𝑋𝑇𝑌𝐵 ) ) → ( 𝑋 ( ·𝑠𝑈 ) 𝑌 ) = ( 𝑋 ( ·𝑠𝑃 ) 𝑌 ) )