Theorem resspsradd

Description: A restricted power series algebra has the same addition 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	resspsradd	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( +g ‘ 𝑈 ) 𝑌 ) = ( 𝑋 ( +g ‘ 𝑃 ) 𝑌 ) )

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	⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 )
8		eqid	⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
9		simprl	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
10		simprr	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
11	3 4 7 8 9 10	psradd	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( +g ‘ 𝑈 ) 𝑌 ) = ( 𝑋 ∘f ( +g ‘ 𝐻 ) 𝑌 ) )
12		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
13		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
14		eqid	⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
15		fvex	⊢ ( Base ‘ 𝑅 ) ∈ V
16	2	subrgbas	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝑇 = ( Base ‘ 𝐻 ) )
17	6 16	syl	⊢ ( 𝜑 → 𝑇 = ( Base ‘ 𝐻 ) )
18		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
19	18	subrgss	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝑇 ⊆ ( Base ‘ 𝑅 ) )
20	6 19	syl	⊢ ( 𝜑 → 𝑇 ⊆ ( Base ‘ 𝑅 ) )
21	17 20	eqsstrrd	⊢ ( 𝜑 → ( Base ‘ 𝐻 ) ⊆ ( Base ‘ 𝑅 ) )
22		mapss	⊢ ( ( ( Base ‘ 𝑅 ) ∈ V ∧ ( Base ‘ 𝐻 ) ⊆ ( Base ‘ 𝑅 ) ) → ( ( Base ‘ 𝐻 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ⊆ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
23	15 21 22	sylancr	⊢ ( 𝜑 → ( ( Base ‘ 𝐻 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ⊆ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
24	23	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( Base ‘ 𝐻 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ⊆ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
25		eqid	⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
26		eqid	⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
27		reldmpsr	⊢ Rel dom mPwSer
28	27 3 4	elbasov	⊢ ( 𝑋 ∈ 𝐵 → ( 𝐼 ∈ V ∧ 𝐻 ∈ V ) )
29	28	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐼 ∈ V ∧ 𝐻 ∈ V ) )
30	29	simpld	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐼 ∈ V )
31	3 25 26 4 30	psrbas	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐵 = ( ( Base ‘ 𝐻 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
32	1 18 26 12 30	psrbas	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( Base ‘ 𝑆 ) = ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
33	24 31 32	3sstr4d	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐵 ⊆ ( Base ‘ 𝑆 ) )
34	33 9	sseldd	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 ∈ ( Base ‘ 𝑆 ) )
35	33 10	sseldd	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑌 ∈ ( Base ‘ 𝑆 ) )
36	1 12 13 14 34 35	psradd	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( +g ‘ 𝑆 ) 𝑌 ) = ( 𝑋 ∘f ( +g ‘ 𝑅 ) 𝑌 ) )
37	2 13	ressplusg	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → ( +g ‘ 𝑅 ) = ( +g ‘ 𝐻 ) )
38	6 37	syl	⊢ ( 𝜑 → ( +g ‘ 𝑅 ) = ( +g ‘ 𝐻 ) )
39	38	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( +g ‘ 𝑅 ) = ( +g ‘ 𝐻 ) )
40	39	ofeqd	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ∘f ( +g ‘ 𝑅 ) = ∘f ( +g ‘ 𝐻 ) )
41	40	oveqd	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ∘f ( +g ‘ 𝑅 ) 𝑌 ) = ( 𝑋 ∘f ( +g ‘ 𝐻 ) 𝑌 ) )
42	36 41	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( +g ‘ 𝑆 ) 𝑌 ) = ( 𝑋 ∘f ( +g ‘ 𝐻 ) 𝑌 ) )
43	4	fvexi	⊢ 𝐵 ∈ V
44	5 14	ressplusg	⊢ ( 𝐵 ∈ V → ( +g ‘ 𝑆 ) = ( +g ‘ 𝑃 ) )
45	43 44	mp1i	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( +g ‘ 𝑆 ) = ( +g ‘ 𝑃 ) )
46	45	oveqd	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( +g ‘ 𝑆 ) 𝑌 ) = ( 𝑋 ( +g ‘ 𝑃 ) 𝑌 ) )
47	11 42 46	3eqtr2d	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( +g ‘ 𝑈 ) 𝑌 ) = ( 𝑋 ( +g ‘ 𝑃 ) 𝑌 ) )