Metamath Proof Explorer


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 { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ⊆ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) )
23 15 21 22 sylancr ( 𝜑 → ( ( Base ‘ 𝐻 ) ↑m { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ⊆ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) )
24 23 adantr ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( ( Base ‘ 𝐻 ) ↑m { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ⊆ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) )
25 eqid ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
26 eqid { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ 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 { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) )
32 1 18 26 12 30 psrbas ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( Base ‘ 𝑆 ) = ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ 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 ofeq ( ( +g𝑅 ) = ( +g𝐻 ) → ∘f ( +g𝑅 ) = ∘f ( +g𝐻 ) )
41 39 40 syl ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ∘f ( +g𝑅 ) = ∘f ( +g𝐻 ) )
42 41 oveqd ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( 𝑋f ( +g𝑅 ) 𝑌 ) = ( 𝑋f ( +g𝐻 ) 𝑌 ) )
43 36 42 eqtrd ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( 𝑋 ( +g𝑆 ) 𝑌 ) = ( 𝑋f ( +g𝐻 ) 𝑌 ) )
44 4 fvexi 𝐵 ∈ V
45 5 14 ressplusg ( 𝐵 ∈ V → ( +g𝑆 ) = ( +g𝑃 ) )
46 44 45 mp1i ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( +g𝑆 ) = ( +g𝑃 ) )
47 46 oveqd ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( 𝑋 ( +g𝑆 ) 𝑌 ) = ( 𝑋 ( +g𝑃 ) 𝑌 ) )
48 11 43 47 3eqtr2d ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( 𝑋 ( +g𝑈 ) 𝑌 ) = ( 𝑋 ( +g𝑃 ) 𝑌 ) )