Definition df-psr 14218

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.)

Assertion

Ref

Expression

df-psr

|- mPwSer = ( i e. _V , r e. _V |-> [_ { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } / d ]_ [_ ( ( Base ` r ) ^m d ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. (Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. (TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. } ) )

Distinct variable group:   b, d, f, g, h, i, k, r, x, y

Detailed syntax breakdown of Definition df-psr

Step	Hyp	Ref	Expression
1		cmps 14217	. 2 class mPwSer
2		vi	. . 3 setvar i
3		vr	. . 3 setvar r
4		cvv 2763	. . 3 class _V
5		vd	. . . 4 setvar d
6		vh	. . . . . . . . 9 setvar h
7	6	cv 1363	. . . . . . . 8 class h
8	7	ccnv 4662	. . . . . . 7 class `' h
9		cn 8990	. . . . . . 7 class NN
10	8, 9	cima 4666	. . . . . 6 class ( `' h " NN )
11		cfn 6799	. . . . . 6 class Fin
12	10, 11	wcel 2167	. . . . 5 wff ( `' h " NN ) e. Fin
13		cn0 9249	. . . . . 6 class NN0
14	2	cv 1363	. . . . . 6 class i
15		cmap 6707	. . . . . 6 class ^m
16	13, 14, 15	co 5922	. . . . 5 class ( NN0 ^m i )
17	12, 6, 16	crab 2479	. . . 4 class { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin }
18		vb	. . . . 5 setvar b
19	3	cv 1363	. . . . . . 7 class r
20		cbs 12678	. . . . . . 7 class Base
21	19, 20	cfv 5258	. . . . . 6 class ( Base ` r )
22	5	cv 1363	. . . . . 6 class d
23	21, 22, 15	co 5922	. . . . 5 class ( ( Base ` r ) ^m d )
24		cnx 12675	. . . . . . . . 9 class ndx
25	24, 20	cfv 5258	. . . . . . . 8 class ( Base ` ndx )
26	18	cv 1363	. . . . . . . 8 class b
27	25, 26	cop 3625	. . . . . . 7 class <. ( Base ` ndx ) , b >.
28		cplusg 12755	. . . . . . . . 9 class +g
29	24, 28	cfv 5258	. . . . . . . 8 class ( +g ` ndx )
30	19, 28	cfv 5258	. . . . . . . . . 10 class ( +g ` r )
31	30	cof 6133	. . . . . . . . 9 class oF ( +g ` r )
32	26, 26	cxp 4661	. . . . . . . . 9 class ( b X. b )
33	31, 32	cres 4665	. . . . . . . 8 class ( oF ( +g ` r ) |` ( b X. b ) )
34	29, 33	cop 3625	. . . . . . 7 class <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >.
35		cmulr 12756	. . . . . . . . 9 class .r
36	24, 35	cfv 5258	. . . . . . . 8 class ( .r ` ndx )
37		vf	. . . . . . . . 9 setvar f
38		vg	. . . . . . . . 9 setvar g
39		vk	. . . . . . . . . 10 setvar k
40		vx	. . . . . . . . . . . 12 setvar x
41		vy	. . . . . . . . . . . . . . 15 setvar y
42	41	cv 1363	. . . . . . . . . . . . . 14 class y
43	39	cv 1363	. . . . . . . . . . . . . 14 class k
44		cle 8062	. . . . . . . . . . . . . . 15 class <_
45	44	cofr 6134	. . . . . . . . . . . . . 14 class oR <_
46	42, 43, 45	wbr 4033	. . . . . . . . . . . . 13 wff y oR <_ k
47	46, 41, 22	crab 2479	. . . . . . . . . . . 12 class { y e. d | y oR <_ k }
48	40	cv 1363	. . . . . . . . . . . . . 14 class x
49	37	cv 1363	. . . . . . . . . . . . . 14 class f
50	48, 49	cfv 5258	. . . . . . . . . . . . 13 class ( f ` x )
51		cmin 8197	. . . . . . . . . . . . . . . 16 class -
52	51	cof 6133	. . . . . . . . . . . . . . 15 class oF -
53	43, 48, 52	co 5922	. . . . . . . . . . . . . 14 class ( k oF - x )
54	38	cv 1363	. . . . . . . . . . . . . 14 class g
55	53, 54	cfv 5258	. . . . . . . . . . . . 13 class ( g ` ( k oF - x ) )
56	19, 35	cfv 5258	. . . . . . . . . . . . 13 class ( .r ` r )
57	50, 55, 56	co 5922	. . . . . . . . . . . 12 class ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) )
58	40, 47, 57	cmpt 4094	. . . . . . . . . . 11 class ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) )
59		cgsu 12928	. . . . . . . . . . 11 class gsumg
60	19, 58, 59	co 5922	. . . . . . . . . 10 class ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) )
61	39, 22, 60	cmpt 4094	. . . . . . . . 9 class ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) )
62	37, 38, 26, 26, 61	cmpo 5924	. . . . . . . 8 class ( f e. b , g e. b |-> ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) )
63	36, 62	cop 3625	. . . . . . 7 class <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >.
64	27, 34, 63	ctp 3624	. . . . . 6 class { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. }
65		csca 12758	. . . . . . . . 9 class Scalar
66	24, 65	cfv 5258	. . . . . . . 8 class (Scalar ` ndx )
67	66, 19	cop 3625	. . . . . . 7 class <. (Scalar ` ndx ) , r >.
68		cvsca 12759	. . . . . . . . 9 class .s
69	24, 68	cfv 5258	. . . . . . . 8 class ( .s ` ndx )
70	48	csn 3622	. . . . . . . . . . 11 class { x }
71	22, 70	cxp 4661	. . . . . . . . . 10 class ( d X. { x } )
72	56	cof 6133	. . . . . . . . . 10 class oF ( .r ` r )
73	71, 49, 72	co 5922	. . . . . . . . 9 class ( ( d X. { x } ) oF ( .r ` r ) f )
74	40, 37, 21, 26, 73	cmpo 5924	. . . . . . . 8 class ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) )
75	69, 74	cop 3625	. . . . . . 7 class <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >.
76		cts 12761	. . . . . . . . 9 class TopSet
77	24, 76	cfv 5258	. . . . . . . 8 class (TopSet ` ndx )
78		ctopn 12911	. . . . . . . . . . . 12 class TopOpen
79	19, 78	cfv 5258	. . . . . . . . . . 11 class ( TopOpen ` r )
80	79	csn 3622	. . . . . . . . . 10 class { ( TopOpen ` r ) }
81	22, 80	cxp 4661	. . . . . . . . 9 class ( d X. { ( TopOpen ` r ) } )
82		cpt 12926	. . . . . . . . 9 class Xt_
83	81, 82	cfv 5258	. . . . . . . 8 class ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) )
84	77, 83	cop 3625	. . . . . . 7 class <. (TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >.
85	67, 75, 84	ctp 3624	. . . . . 6 class { <. (Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. (TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. }
86	64, 85	cun 3155	. . . . 5 class ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. (Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. (TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. } )
87	18, 23, 86	csb 3084	. . . 4 class [_ ( ( Base ` r ) ^m d ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. (Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. (TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. } )
88	5, 17, 87	csb 3084	. . 3 class [_ { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } / d ]_ [_ ( ( Base ` r ) ^m d ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. (Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. (TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. } )
89	2, 3, 4, 4, 88	cmpo 5924	. 2 class ( i e. _V , r e. _V |-> [_ { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } / d ]_ [_ ( ( Base ` r ) ^m d ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. (Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. (TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. } ) )
90	1, 89	wceq 1364	1 wff mPwSer = ( i e. _V , r e. _V |-> [_ { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } / d ]_ [_ ( ( Base ` r ) ^m d ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. (Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. (TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. } ) )

This definition is referenced by:  reldmpsr  14219  psrval  14220  fnpsr  14221