Metamath Proof Explorer

Definition df-resv

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

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cresv 
 |-  |`v
1 vw 
 |-  w
2 cvv 
 |-  _V
3 vx 
 |-  x
4 cbs 
 |-  Base
5 csca 
 |-  Scalar
6 1 cv 
 |-  w
7 6 5 cfv 
 |-  ( Scalar ` w )
8 7 4 cfv 
 |-  ( Base ` ( Scalar ` w ) )
9 3 cv 
 |-  x
10 8 9 wss 
 |-  ( Base ` ( Scalar ` w ) ) C_ x
11 csts 
 |-  sSet
12 cnx 
 |-  ndx
13 12 5 cfv 
 |-  ( Scalar ` ndx )
14 cress 
 |-  |`s
15 7 9 14 co 
 |-  ( ( Scalar ` w ) |`s x )
16 13 15 cop 
 |-  <. ( Scalar ` ndx ) , ( ( Scalar ` w ) |`s x ) >.
17 6 16 11 co 
 |-  ( w sSet <. ( Scalar ` ndx ) , ( ( Scalar ` w ) |`s x ) >. )
18 10 6 17 cif 
 |-  if ( ( Base ` ( Scalar ` w ) ) C_ x , w , ( w sSet <. ( Scalar ` ndx ) , ( ( Scalar ` w ) |`s x ) >. ) )
19 1 3 2 2 18 cmpo 
 |-  ( w e. _V , x e. _V |-> if ( ( Base ` ( Scalar ` w ) ) C_ x , w , ( w sSet <. ( Scalar ` ndx ) , ( ( Scalar ` w ) |`s x ) >. ) ) )
20 0 19 wceq 
 |-  |`v = ( w e. _V , x e. _V |-> if ( ( Base ` ( Scalar ` w ) ) C_ x , w , ( w sSet <. ( Scalar ` ndx ) , ( ( Scalar ` w ) |`s x ) >. ) ) )