Metamath Proof Explorer


Theorem resspsrbas

Description: A restricted power series algebra has the same base set. (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 resspsrbas ( 𝜑𝐵 = ( Base ‘ 𝑃 ) )

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 fvex ( Base ‘ 𝑅 ) ∈ V
8 2 subrgbas ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝑇 = ( Base ‘ 𝐻 ) )
9 6 8 syl ( 𝜑𝑇 = ( Base ‘ 𝐻 ) )
10 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
11 10 subrgss ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝑇 ⊆ ( Base ‘ 𝑅 ) )
12 6 11 syl ( 𝜑𝑇 ⊆ ( Base ‘ 𝑅 ) )
13 9 12 eqsstrrd ( 𝜑 → ( Base ‘ 𝐻 ) ⊆ ( Base ‘ 𝑅 ) )
14 13 adantr ( ( 𝜑𝐼 ∈ V ) → ( Base ‘ 𝐻 ) ⊆ ( Base ‘ 𝑅 ) )
15 mapss ( ( ( Base ‘ 𝑅 ) ∈ V ∧ ( Base ‘ 𝐻 ) ⊆ ( Base ‘ 𝑅 ) ) → ( ( Base ‘ 𝐻 ) ↑m { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ⊆ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) )
16 7 14 15 sylancr ( ( 𝜑𝐼 ∈ V ) → ( ( Base ‘ 𝐻 ) ↑m { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ⊆ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) )
17 eqid ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
18 eqid { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
19 simpr ( ( 𝜑𝐼 ∈ V ) → 𝐼 ∈ V )
20 3 17 18 4 19 psrbas ( ( 𝜑𝐼 ∈ V ) → 𝐵 = ( ( Base ‘ 𝐻 ) ↑m { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) )
21 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
22 1 10 18 21 19 psrbas ( ( 𝜑𝐼 ∈ V ) → ( Base ‘ 𝑆 ) = ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) )
23 16 20 22 3sstr4d ( ( 𝜑𝐼 ∈ V ) → 𝐵 ⊆ ( Base ‘ 𝑆 ) )
24 reldmpsr Rel dom mPwSer
25 24 ovprc1 ( ¬ 𝐼 ∈ V → ( 𝐼 mPwSer 𝐻 ) = ∅ )
26 3 25 syl5eq ( ¬ 𝐼 ∈ V → 𝑈 = ∅ )
27 26 adantl ( ( 𝜑 ∧ ¬ 𝐼 ∈ V ) → 𝑈 = ∅ )
28 27 fveq2d ( ( 𝜑 ∧ ¬ 𝐼 ∈ V ) → ( Base ‘ 𝑈 ) = ( Base ‘ ∅ ) )
29 base0 ∅ = ( Base ‘ ∅ )
30 28 4 29 3eqtr4g ( ( 𝜑 ∧ ¬ 𝐼 ∈ V ) → 𝐵 = ∅ )
31 0ss ∅ ⊆ ( Base ‘ 𝑆 )
32 30 31 eqsstrdi ( ( 𝜑 ∧ ¬ 𝐼 ∈ V ) → 𝐵 ⊆ ( Base ‘ 𝑆 ) )
33 23 32 pm2.61dan ( 𝜑𝐵 ⊆ ( Base ‘ 𝑆 ) )
34 5 21 ressbas2 ( 𝐵 ⊆ ( Base ‘ 𝑆 ) → 𝐵 = ( Base ‘ 𝑃 ) )
35 33 34 syl ( 𝜑𝐵 = ( Base ‘ 𝑃 ) )