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

Metamath Proof Explorer

Definition df-psr

Description: Define the algebra of power series over the index set i and with coefficients from the ring r . (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion df-psr mPwSer = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ⦋ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } / 𝑑 ⦌ ⦋ ( ( Base ‘ 𝑟 ) ↑m 𝑑 ) / 𝑏 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑟 ) ↾ ( 𝑏 × 𝑏 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑟 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑓 ∈ 𝑏 ↦ ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) ) ⟩ } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmps ⊢ mPwSer
1 vi ⊢ 𝑖
2 cvv ⊢ V
3 vr ⊢ 𝑟
4 vh ⊢ ℎ
5 cn0 ⊢ ℕ0
6 cmap ⊢ ↑m
7 1 cv ⊢ 𝑖
8 5 7 6 co ⊢ ( ℕ0 ↑m 𝑖 )
9 4 cv ⊢ ℎ
10 9 ccnv ⊢ ◡ ℎ
11 cn ⊢ ℕ
12 10 11 cima ⊢ ( ◡ ℎ “ ℕ )
13 cfn ⊢ Fin
14 12 13 wcel ⊢ ( ◡ ℎ “ ℕ ) ∈ Fin
15 14 4 8 crab ⊢ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
16 vd ⊢ 𝑑
17 cbs ⊢ Base
18 3 cv ⊢ 𝑟
19 18 17 cfv ⊢ ( Base ‘ 𝑟 )
20 16 cv ⊢ 𝑑
21 19 20 6 co ⊢ ( ( Base ‘ 𝑟 ) ↑m 𝑑 )
22 vb ⊢ 𝑏
23 cnx ⊢ ndx
24 23 17 cfv ⊢ ( Base ‘ ndx )
25 22 cv ⊢ 𝑏
26 24 25 cop ⊢ ⟨ ( Base ‘ ndx ) , 𝑏 ⟩
27 cplusg ⊢ +g
28 23 27 cfv ⊢ ( +g ‘ ndx )
29 18 27 cfv ⊢ ( +g ‘ 𝑟 )
30 29 cof ⊢ ∘f ( +g ‘ 𝑟 )
31 25 25 cxp ⊢ ( 𝑏 × 𝑏 )
32 30 31 cres ⊢ ( ∘f ( +g ‘ 𝑟 ) ↾ ( 𝑏 × 𝑏 ) )
33 28 32 cop ⊢ ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑟 ) ↾ ( 𝑏 × 𝑏 ) ) ⟩
34 cmulr ⊢ .r
35 23 34 cfv ⊢ ( .r ‘ ndx )
36 vf ⊢ 𝑓
37 vg ⊢ 𝑔
38 vk ⊢ 𝑘
39 cgsu ⊢ Σg
40 vx ⊢ 𝑥
41 vy ⊢ 𝑦
42 41 cv ⊢ 𝑦
43 cle ⊢ ≤
44 43 cofr ⊢ ∘r ≤
45 38 cv ⊢ 𝑘
46 42 45 44 wbr ⊢ 𝑦 ∘r ≤ 𝑘
47 46 41 20 crab ⊢ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 }
48 36 cv ⊢ 𝑓
49 40 cv ⊢ 𝑥
50 49 48 cfv ⊢ ( 𝑓 ‘ 𝑥 )
51 18 34 cfv ⊢ ( .r ‘ 𝑟 )
52 37 cv ⊢ 𝑔
53 cmin ⊢ −
54 53 cof ⊢ ∘f −
55 45 49 54 co ⊢ ( 𝑘 ∘f − 𝑥 )
56 55 52 cfv ⊢ ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) )
57 50 56 51 co ⊢ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) )
58 40 47 57 cmpt ⊢ ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) )
59 18 58 39 co ⊢ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) )
60 38 20 59 cmpt ⊢ ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) )
61 36 37 25 25 60 cmpo ⊢ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )
62 35 61 cop ⊢ ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩
63 26 33 62 ctp ⊢ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑟 ) ↾ ( 𝑏 × 𝑏 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ }
64 csca ⊢ Scalar
65 23 64 cfv ⊢ ( Scalar ‘ ndx )
66 65 18 cop ⊢ ⟨ ( Scalar ‘ ndx ) , 𝑟 ⟩
67 cvsca ⊢ ·𝑠
68 23 67 cfv ⊢ ( ·𝑠 ‘ ndx )
69 49 csn ⊢ { 𝑥 }
70 20 69 cxp ⊢ ( 𝑑 × { 𝑥 } )
71 51 cof ⊢ ∘f ( .r ‘ 𝑟 )
72 70 48 71 co ⊢ ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 )
73 40 36 19 25 72 cmpo ⊢ ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑓 ∈ 𝑏 ↦ ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) )
74 68 73 cop ⊢ ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑓 ∈ 𝑏 ↦ ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) ) ⟩
75 cts ⊢ TopSet
76 23 75 cfv ⊢ ( TopSet ‘ ndx )
77 cpt ⊢ ∏t
78 ctopn ⊢ TopOpen
79 18 78 cfv ⊢ ( TopOpen ‘ 𝑟 )
80 79 csn ⊢ { ( TopOpen ‘ 𝑟 ) }
81 20 80 cxp ⊢ ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } )
82 81 77 cfv ⊢ ( ∏t ‘ ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) )
83 76 82 cop ⊢ ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) ) ⟩
84 66 74 83 ctp ⊢ { ⟨ ( Scalar ‘ ndx ) , 𝑟 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑓 ∈ 𝑏 ↦ ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) ) ⟩ }
85 63 84 cun ⊢ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑟 ) ↾ ( 𝑏 × 𝑏 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑟 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑓 ∈ 𝑏 ↦ ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) ) ⟩ } )
86 22 21 85 csb ⊢ ⦋ ( ( Base ‘ 𝑟 ) ↑m 𝑑 ) / 𝑏 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑟 ) ↾ ( 𝑏 × 𝑏 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑟 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑓 ∈ 𝑏 ↦ ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) ) ⟩ } )
87 16 15 86 csb ⊢ ⦋ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } / 𝑑 ⦌ ⦋ ( ( Base ‘ 𝑟 ) ↑m 𝑑 ) / 𝑏 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑟 ) ↾ ( 𝑏 × 𝑏 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑟 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑓 ∈ 𝑏 ↦ ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) ) ⟩ } )
88 1 3 2 2 87 cmpo ⊢ ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ⦋ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } / 𝑑 ⦌ ⦋ ( ( Base ‘ 𝑟 ) ↑m 𝑑 ) / 𝑏 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑟 ) ↾ ( 𝑏 × 𝑏 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑟 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑓 ∈ 𝑏 ↦ ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) ) ⟩ } ) )
89 0 88 wceq ⊢ mPwSer = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ⦋ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } / 𝑑 ⦌ ⦋ ( ( Base ‘ 𝑟 ) ↑m 𝑑 ) / 𝑏 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑟 ) ↾ ( 𝑏 × 𝑏 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑟 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑓 ∈ 𝑏 ↦ ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) ) ⟩ } ) )