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	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( ·𝑠 ‘ 𝑈 ) 𝑌 ) = ( 𝑋 ( ·𝑠 ‘ 𝑃 ) 𝑌 ) )