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 ‘ 𝑃 ) )