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 𝑣=wV,xVifBaseScalarwxwwsSetScalarndxScalarw𝑠x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cresv class𝑣
1 vw setvarw
2 cvv classV
3 vx setvarx
4 cbs classBase
5 csca classScalar
6 1 cv setvarw
7 6 5 cfv classScalarw
8 7 4 cfv classBaseScalarw
9 3 cv setvarx
10 8 9 wss wffBaseScalarwx
11 csts classsSet
12 cnx classndx
13 12 5 cfv classScalarndx
14 cress class𝑠
15 7 9 14 co classScalarw𝑠x
16 13 15 cop classScalarndxScalarw𝑠x
17 6 16 11 co classwsSetScalarndxScalarw𝑠x
18 10 6 17 cif classifBaseScalarwxwwsSetScalarndxScalarw𝑠x
19 1 3 2 2 18 cmpo classwV,xVifBaseScalarwxwwsSetScalarndxScalarw𝑠x
20 0 19 wceq wff𝑣=wV,xVifBaseScalarwxwwsSetScalarndxScalarw𝑠x