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

Metamath Proof Explorer

Theorem resspsrvsca

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

Ref Expression
Hypotheses resspsr.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
resspsr.h ⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
resspsr.u ⊢ 𝑈 = ( 𝐼 mPwSer 𝐻 )
resspsr.b ⊢ 𝐵 = ( Base ‘ 𝑈 )
resspsr.p ⊢ 𝑃 = ( 𝑆 ↾s 𝐵 )
resspsr.2 ⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
Assertion resspsrvsca ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( ·𝑠 ‘ 𝑈 ) 𝑌 ) = ( 𝑋 ( ·𝑠 ‘ 𝑃 ) 𝑌 ) )

Proof

Step Hyp Ref Expression
1 resspsr.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 resspsr.h ⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
3 resspsr.u ⊢ 𝑈 = ( 𝐼 mPwSer 𝐻 )
4 resspsr.b ⊢ 𝐵 = ( Base ‘ 𝑈 )
5 resspsr.p ⊢ 𝑃 = ( 𝑆 ↾s 𝐵 )
6 resspsr.2 ⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
7 eqid ⊢ ( ·𝑠 ‘ 𝑈 ) = ( ·𝑠 ‘ 𝑈 )
8 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
9 eqid ⊢ ( .r ‘ 𝐻 ) = ( .r ‘ 𝐻 )
10 eqid ⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
11 simprl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 ∈ 𝑇 )
12 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
13 2 subrgbas ⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝑇 = ( Base ‘ 𝐻 ) )
14 12 13 syl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑇 = ( Base ‘ 𝐻 ) )
15 11 14 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 ∈ ( Base ‘ 𝐻 ) )
16 simprr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
17 3 7 8 4 9 10 15 16 psrvsca ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( ·𝑠 ‘ 𝑈 ) 𝑌 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑋 } ) ∘f ( .r ‘ 𝐻 ) 𝑌 ) )
18 eqid ⊢ ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑆 )
19 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
20 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
21 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
22 19 subrgss ⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝑇 ⊆ ( Base ‘ 𝑅 ) )
23 12 22 syl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑇 ⊆ ( Base ‘ 𝑅 ) )
24 23 11 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 ∈ ( Base ‘ 𝑅 ) )
25 1 2 3 4 5 6 resspsrbas ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑃 ) )
26 5 20 ressbasss ⊢ ( Base ‘ 𝑃 ) ⊆ ( Base ‘ 𝑆 )
27 25 26 eqsstrdi ⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ 𝑆 ) )
28 27 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐵 ⊆ ( Base ‘ 𝑆 ) )
29 28 16 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑌 ∈ ( Base ‘ 𝑆 ) )
30 1 18 19 20 21 10 24 29 psrvsca ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( ·𝑠 ‘ 𝑆 ) 𝑌 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) 𝑌 ) )
31 2 21 ressmulr ⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → ( .r ‘ 𝑅 ) = ( .r ‘ 𝐻 ) )
32 ofeq ⊢ ( ( .r ‘ 𝑅 ) = ( .r ‘ 𝐻 ) → ∘f ( .r ‘ 𝑅 ) = ∘f ( .r ‘ 𝐻 ) )
33 12 31 32 3syl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → ∘f ( .r ‘ 𝑅 ) = ∘f ( .r ‘ 𝐻 ) )
34 33 oveqd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) 𝑌 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑋 } ) ∘f ( .r ‘ 𝐻 ) 𝑌 ) )
35 30 34 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( ·𝑠 ‘ 𝑆 ) 𝑌 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑋 } ) ∘f ( .r ‘ 𝐻 ) 𝑌 ) )
36 4 fvexi ⊢ 𝐵 ∈ V
37 5 18 ressvsca ⊢ ( 𝐵 ∈ V → ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑃 ) )
38 36 37 mp1i ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑃 ) )
39 38 oveqd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( ·𝑠 ‘ 𝑆 ) 𝑌 ) = ( 𝑋 ( ·𝑠 ‘ 𝑃 ) 𝑌 ) )
40 17 35 39 3eqtr2d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( ·𝑠 ‘ 𝑈 ) 𝑌 ) = ( 𝑋 ( ·𝑠 ‘ 𝑃 ) 𝑌 ) )