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

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 { 𝑓 ∈ ( ℕ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 ‘ 𝑃 ) 𝑌 ) )