Definition df-mvr 19357

Description: Define the generating elements of the power series algebra. (Contributed by Mario Carneiro, 7-Jan-2015.)

Assertion

Ref	Expression
df-mvr	|- mVar = ( i e. _V , r e. _V |-> ( x e. i |-> ( f e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. i |-> if ( y = x , 1 , 0 ) ) , ( 1r ` r ) , ( 0g ` r ) ) ) ) )

Distinct variable group:   f, h, i, r, x, y

Detailed syntax breakdown of Definition df-mvr

Step	Hyp	Ref	Expression
1		cmvr 19352	. 2 class mVar
2		vi	. . 3 setvar i
3		vr	. . 3 setvar r
4		cvv 3200	. . 3 class _V
5		vx	. . . 4 setvar x
6	2	cv 1482	. . . 4 class i
7		vf	. . . . 5 setvar f
8		vh	. . . . . . . . . 10 setvar h
9	8	cv 1482	. . . . . . . . 9 class h
10	9	ccnv 5113	. . . . . . . 8 class `' h
11		cn 11020	. . . . . . . 8 class NN
12	10, 11	cima 5117	. . . . . . 7 class ( `' h " NN )
13		cfn 7955	. . . . . . 7 class Fin
14	12, 13	wcel 1990	. . . . . 6 wff ( `' h " NN ) e. Fin
15		cn0 11292	. . . . . . 7 class NN0
16		cmap 7857	. . . . . . 7 class ^m
17	15, 6, 16	co 6650	. . . . . 6 class ( NN0 ^m i )
18	14, 8, 17	crab 2916	. . . . 5 class { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin }
19	7	cv 1482	. . . . . . 7 class f
20		vy	. . . . . . . 8 setvar y
21	20, 5	weq 1874	. . . . . . . . 9 wff y = x
22		c1 9937	. . . . . . . . 9 class 1
23		cc0 9936	. . . . . . . . 9 class 0
24	21, 22, 23	cif 4086	. . . . . . . 8 class if ( y = x , 1 , 0 )
25	20, 6, 24	cmpt 4729	. . . . . . 7 class ( y e. i |-> if ( y = x , 1 , 0 ) )
26	19, 25	wceq 1483	. . . . . 6 wff f = ( y e. i |-> if ( y = x , 1 , 0 ) )
27	3	cv 1482	. . . . . . 7 class r
28		cur 18501	. . . . . . 7 class 1r
29	27, 28	cfv 5888	. . . . . 6 class ( 1r ` r )
30		c0g 16100	. . . . . . 7 class 0g
31	27, 30	cfv 5888	. . . . . 6 class ( 0g ` r )
32	26, 29, 31	cif 4086	. . . . 5 class if ( f = ( y e. i |-> if ( y = x , 1 , 0 ) ) , ( 1r ` r ) , ( 0g ` r ) )
33	7, 18, 32	cmpt 4729	. . . 4 class ( f e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. i |-> if ( y = x , 1 , 0 ) ) , ( 1r ` r ) , ( 0g ` r ) ) )
34	5, 6, 33	cmpt 4729	. . 3 class ( x e. i |-> ( f e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. i |-> if ( y = x , 1 , 0 ) ) , ( 1r ` r ) , ( 0g ` r ) ) ) )
35	2, 3, 4, 4, 34	cmpt2 6652	. 2 class ( i e. _V , r e. _V |-> ( x e. i |-> ( f e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. i |-> if ( y = x , 1 , 0 ) ) , ( 1r ` r ) , ( 0g ` r ) ) ) ) )
36	1, 35	wceq 1483	1 wff mVar = ( i e. _V , r e. _V |-> ( x e. i |-> ( f e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. i |-> if ( y = x , 1 , 0 ) ) , ( 1r ` r ) , ( 0g ` r ) ) ) ) )

This definition is referenced by:  mvrfval  19420  vr1val  19562