Theorem psrbas

Description: The base set of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by Mario Carneiro, 2-Oct-2015) (Proof shortened by AV, 8-Jul-2019)

	Ref	Expression
Hypotheses	psrbas.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
	psrbas.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	psrbas.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
	psrbas.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	psrbas.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
Assertion	psrbas	⊢ ( 𝜑 → 𝐵 = ( 𝐾 ↑m 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		psrbas.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2		psrbas.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
3		psrbas.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
4		psrbas.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
5		psrbas.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
7		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
8		eqid	⊢ ( TopOpen ‘ 𝑅 ) = ( TopOpen ‘ 𝑅 )
9		eqidd	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( 𝐾 ↑m 𝐷 ) = ( 𝐾 ↑m 𝐷 ) )
10		eqid	⊢ ( ∘f ( +g ‘ 𝑅 ) ↾ ( ( 𝐾 ↑m 𝐷 ) × ( 𝐾 ↑m 𝐷 ) ) ) = ( ∘f ( +g ‘ 𝑅 ) ↾ ( ( 𝐾 ↑m 𝐷 ) × ( 𝐾 ↑m 𝐷 ) ) )
11		eqid	⊢ ( 𝑔 ∈ ( 𝐾 ↑m 𝐷 ) , ℎ ∈ ( 𝐾 ↑m 𝐷 ) ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑔 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ℎ ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) = ( 𝑔 ∈ ( 𝐾 ↑m 𝐷 ) , ℎ ∈ ( 𝐾 ↑m 𝐷 ) ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑔 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ℎ ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )
12		eqid	⊢ ( 𝑥 ∈ 𝐾 , 𝑔 ∈ ( 𝐾 ↑m 𝐷 ) ↦ ( ( 𝐷 × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑔 ) ) = ( 𝑥 ∈ 𝐾 , 𝑔 ∈ ( 𝐾 ↑m 𝐷 ) ↦ ( ( 𝐷 × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑔 ) )
13		eqidd	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( ∏t ‘ ( 𝐷 × { ( TopOpen ‘ 𝑅 ) } ) ) = ( ∏t ‘ ( 𝐷 × { ( TopOpen ‘ 𝑅 ) } ) ) )
14	5	adantr	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → 𝐼 ∈ 𝑉 )
15		simpr	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → 𝑅 ∈ V )
16	1 2 6 7 8 3 9 10 11 12 13 14 15	psrval	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → 𝑆 = ( { ⟨ ( Base ‘ ndx ) , ( 𝐾 ↑m 𝐷 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑅 ) ↾ ( ( 𝐾 ↑m 𝐷 ) × ( 𝐾 ↑m 𝐷 ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑔 ∈ ( 𝐾 ↑m 𝐷 ) , ℎ ∈ ( 𝐾 ↑m 𝐷 ) ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑔 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ℎ ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ 𝐾 , 𝑔 ∈ ( 𝐾 ↑m 𝐷 ) ↦ ( ( 𝐷 × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐷 × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } ) )
17	16	fveq2d	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( Base ‘ 𝑆 ) = ( Base ‘ ( { ⟨ ( Base ‘ ndx ) , ( 𝐾 ↑m 𝐷 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑅 ) ↾ ( ( 𝐾 ↑m 𝐷 ) × ( 𝐾 ↑m 𝐷 ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑔 ∈ ( 𝐾 ↑m 𝐷 ) , ℎ ∈ ( 𝐾 ↑m 𝐷 ) ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑔 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ℎ ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ 𝐾 , 𝑔 ∈ ( 𝐾 ↑m 𝐷 ) ↦ ( ( 𝐷 × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐷 × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } ) ) )
18		ovex	⊢ ( 𝐾 ↑m 𝐷 ) ∈ V
19		psrvalstr	⊢ ( { ⟨ ( Base ‘ ndx ) , ( 𝐾 ↑m 𝐷 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑅 ) ↾ ( ( 𝐾 ↑m 𝐷 ) × ( 𝐾 ↑m 𝐷 ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑔 ∈ ( 𝐾 ↑m 𝐷 ) , ℎ ∈ ( 𝐾 ↑m 𝐷 ) ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑔 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ℎ ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ 𝐾 , 𝑔 ∈ ( 𝐾 ↑m 𝐷 ) ↦ ( ( 𝐷 × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐷 × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } ) Struct ⟨ 1 , 9 ⟩
20		baseid	⊢ Base = Slot ( Base ‘ ndx )
21		snsstp1	⊢ { ⟨ ( Base ‘ ndx ) , ( 𝐾 ↑m 𝐷 ) ⟩ } ⊆ { ⟨ ( Base ‘ ndx ) , ( 𝐾 ↑m 𝐷 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑅 ) ↾ ( ( 𝐾 ↑m 𝐷 ) × ( 𝐾 ↑m 𝐷 ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑔 ∈ ( 𝐾 ↑m 𝐷 ) , ℎ ∈ ( 𝐾 ↑m 𝐷 ) ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑔 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ℎ ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ }
22		ssun1	⊢ { ⟨ ( Base ‘ ndx ) , ( 𝐾 ↑m 𝐷 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑅 ) ↾ ( ( 𝐾 ↑m 𝐷 ) × ( 𝐾 ↑m 𝐷 ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑔 ∈ ( 𝐾 ↑m 𝐷 ) , ℎ ∈ ( 𝐾 ↑m 𝐷 ) ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑔 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ℎ ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , ( 𝐾 ↑m 𝐷 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑅 ) ↾ ( ( 𝐾 ↑m 𝐷 ) × ( 𝐾 ↑m 𝐷 ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑔 ∈ ( 𝐾 ↑m 𝐷 ) , ℎ ∈ ( 𝐾 ↑m 𝐷 ) ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑔 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ℎ ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ 𝐾 , 𝑔 ∈ ( 𝐾 ↑m 𝐷 ) ↦ ( ( 𝐷 × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐷 × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } )
23	21 22	sstri	⊢ { ⟨ ( Base ‘ ndx ) , ( 𝐾 ↑m 𝐷 ) ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , ( 𝐾 ↑m 𝐷 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑅 ) ↾ ( ( 𝐾 ↑m 𝐷 ) × ( 𝐾 ↑m 𝐷 ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑔 ∈ ( 𝐾 ↑m 𝐷 ) , ℎ ∈ ( 𝐾 ↑m 𝐷 ) ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑔 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ℎ ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ 𝐾 , 𝑔 ∈ ( 𝐾 ↑m 𝐷 ) ↦ ( ( 𝐷 × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐷 × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } )
24	19 20 23	strfv	⊢ ( ( 𝐾 ↑m 𝐷 ) ∈ V → ( 𝐾 ↑m 𝐷 ) = ( Base ‘ ( { ⟨ ( Base ‘ ndx ) , ( 𝐾 ↑m 𝐷 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑅 ) ↾ ( ( 𝐾 ↑m 𝐷 ) × ( 𝐾 ↑m 𝐷 ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑔 ∈ ( 𝐾 ↑m 𝐷 ) , ℎ ∈ ( 𝐾 ↑m 𝐷 ) ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑔 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ℎ ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ 𝐾 , 𝑔 ∈ ( 𝐾 ↑m 𝐷 ) ↦ ( ( 𝐷 × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐷 × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } ) ) )
25	18 24	ax-mp	⊢ ( 𝐾 ↑m 𝐷 ) = ( Base ‘ ( { ⟨ ( Base ‘ ndx ) , ( 𝐾 ↑m 𝐷 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑅 ) ↾ ( ( 𝐾 ↑m 𝐷 ) × ( 𝐾 ↑m 𝐷 ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑔 ∈ ( 𝐾 ↑m 𝐷 ) , ℎ ∈ ( 𝐾 ↑m 𝐷 ) ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑔 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ℎ ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ 𝐾 , 𝑔 ∈ ( 𝐾 ↑m 𝐷 ) ↦ ( ( 𝐷 × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐷 × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } ) )
26	17 4 25	3eqtr4g	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → 𝐵 = ( 𝐾 ↑m 𝐷 ) )
27		reldmpsr	⊢ Rel dom mPwSer
28	27	ovprc2	⊢ ( ¬ 𝑅 ∈ V → ( 𝐼 mPwSer 𝑅 ) = ∅ )
29	28	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ∈ V ) → ( 𝐼 mPwSer 𝑅 ) = ∅ )
30	1 29	syl5eq	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ∈ V ) → 𝑆 = ∅ )
31	30	fveq2d	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ∈ V ) → ( Base ‘ 𝑆 ) = ( Base ‘ ∅ ) )
32		base0	⊢ ∅ = ( Base ‘ ∅ )
33	31 4 32	3eqtr4g	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ∈ V ) → 𝐵 = ∅ )
34		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( Base ‘ 𝑅 ) = ∅ )
35	34	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ∈ V ) → ( Base ‘ 𝑅 ) = ∅ )
36	2 35	syl5eq	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ∈ V ) → 𝐾 = ∅ )
37	3	fczpsrbag	⊢ ( 𝐼 ∈ 𝑉 → ( 𝑥 ∈ 𝐼 ↦ 0 ) ∈ 𝐷 )
38	5 37	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 0 ) ∈ 𝐷 )
39	38	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ∈ V ) → ( 𝑥 ∈ 𝐼 ↦ 0 ) ∈ 𝐷 )
40	39	ne0d	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ∈ V ) → 𝐷 ≠ ∅ )
41	2	fvexi	⊢ 𝐾 ∈ V
42		ovex	⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
43	3 42	rabex2	⊢ 𝐷 ∈ V
44	41 43	map0	⊢ ( ( 𝐾 ↑m 𝐷 ) = ∅ ↔ ( 𝐾 = ∅ ∧ 𝐷 ≠ ∅ ) )
45	36 40 44	sylanbrc	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ∈ V ) → ( 𝐾 ↑m 𝐷 ) = ∅ )
46	33 45	eqtr4d	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ∈ V ) → 𝐵 = ( 𝐾 ↑m 𝐷 ) )
47	26 46	pm2.61dan	⊢ ( 𝜑 → 𝐵 = ( 𝐾 ↑m 𝐷 ) )