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

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 { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ⊆ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
16 7 14 15 sylancr ⊢ ( ( 𝜑 ∧ 𝐼 ∈ V ) → ( ( Base ‘ 𝐻 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ⊆ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
17 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
18 eqid ⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
19 simpr ⊢ ( ( 𝜑 ∧ 𝐼 ∈ V ) → 𝐼 ∈ V )
20 3 17 18 4 19 psrbas ⊢ ( ( 𝜑 ∧ 𝐼 ∈ V ) → 𝐵 = ( ( Base ‘ 𝐻 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
21 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
22 1 10 18 21 19 psrbas ⊢ ( ( 𝜑 ∧ 𝐼 ∈ V ) → ( Base ‘ 𝑆 ) = ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
23 16 20 22 3sstr4d ⊢ ( ( 𝜑 ∧ 𝐼 ∈ V ) → 𝐵 ⊆ ( Base ‘ 𝑆 ) )
24 reldmpsr ⊢ Rel dom mPwSer
25 24 ovprc1 ⊢ ( ¬ 𝐼 ∈ V → ( 𝐼 mPwSer 𝐻 ) = ∅ )
26 3 25 eqtrid ⊢ ( ¬ 𝐼 ∈ 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 ‘ 𝑃 ) )