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

Metamath Proof Explorer

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 eqtrid ⊢ ( ( 𝜑 ∧ ¬ 𝑅 ∈ 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 eqtrid ⊢ ( ( 𝜑 ∧ ¬ 𝑅 ∈ 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 𝐷 ) )