Definition df-resv 29825

Description: Define an operator to restrict the scalar field component of an extended structure. (Contributed by Thierry Arnoux, 5-Sep-2018.)

Assertion

Ref	Expression
df-resv	|- ↾v = ( w e. _V , x e. _V |-> if ( ( Base ` (Scalar ` w ) ) C_ x , w , ( w sSet <. (Scalar ` ndx ) , ( (Scalar ` w ) ↾s x ) >. ) ) )

Distinct variable group:   x, w

Detailed syntax breakdown of Definition df-resv

Step	Hyp	Ref	Expression
1		cresv 29824	. 2 class ↾v
2		vw	. . 3 setvar w
3		vx	. . 3 setvar x
4		cvv 3200	. . 3 class _V
5	2	cv 1482	. . . . . . 7 class w
6		csca 15944	. . . . . . 7 class Scalar
7	5, 6	cfv 5888	. . . . . 6 class (Scalar ` w )
8		cbs 15857	. . . . . 6 class Base
9	7, 8	cfv 5888	. . . . 5 class ( Base ` (Scalar ` w ) )
10	3	cv 1482	. . . . 5 class x
11	9, 10	wss 3574	. . . 4 wff ( Base ` (Scalar ` w ) ) C_ x
12		cnx 15854	. . . . . . 7 class ndx
13	12, 6	cfv 5888	. . . . . 6 class (Scalar ` ndx )
14		cress 15858	. . . . . . 7 class ↾s
15	7, 10, 14	co 6650	. . . . . 6 class ( (Scalar ` w ) ↾s x )
16	13, 15	cop 4183	. . . . 5 class <. (Scalar ` ndx ) , ( (Scalar ` w ) ↾s x ) >.
17		csts 15855	. . . . 5 class sSet
18	5, 16, 17	co 6650	. . . 4 class ( w sSet <. (Scalar ` ndx ) , ( (Scalar ` w ) ↾s x ) >. )
19	11, 5, 18	cif 4086	. . 3 class if ( ( Base ` (Scalar ` w ) ) C_ x , w , ( w sSet <. (Scalar ` ndx ) , ( (Scalar ` w ) ↾s x ) >. ) )
20	2, 3, 4, 4, 19	cmpt2 6652	. 2 class ( w e. _V , x e. _V |-> if ( ( Base ` (Scalar ` w ) ) C_ x , w , ( w sSet <. (Scalar ` ndx ) , ( (Scalar ` w ) ↾s x ) >. ) ) )
21	1, 20	wceq 1483	1 wff ↾v = ( w e. _V , x e. _V |-> if ( ( Base ` (Scalar ` w ) ) C_ x , w , ( w sSet <. (Scalar ` ndx ) , ( (Scalar ` w ) ↾s x ) >. ) ) )

This definition is referenced by:  reldmresv  29826  resvval  29827