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	$⊢ ↾_{𝑣} = (w \in V, x \in V ⟼ if ({Base}_{Scalar (w)} \subseteq x, w, w sSet ⟨Scalar (ndx), Scalar (w) ↾_{𝑠} x⟩))$

Step	Hyp	Ref	Expression
0		cresv	$class ↾_{𝑣}$
1		vw	$setvar w$
2		cvv	$class V$
3		vx	$setvar x$
4		cbs	$class Base$
5		csca	$class Scalar$
6	1	cv	$setvar w$
7	6 5	cfv	$class Scalar (w)$
8	7 4	cfv	$class {Base}_{Scalar (w)}$
9	3	cv	$setvar x$
10	8 9	wss	$wff {Base}_{Scalar (w)} \subseteq x$
11		csts	$class sSet$
12		cnx	$class ndx$
13	12 5	cfv	$class Scalar (ndx)$
14		cress	$class ↾_{𝑠}$
15	7 9 14	co	$class (Scalar (w) ↾_{𝑠} x)$
16	13 15	cop	$class ⟨Scalar (ndx), Scalar (w) ↾_{𝑠} x⟩$
17	6 16 11	co	$class (w sSet ⟨Scalar (ndx), Scalar (w) ↾_{𝑠} x⟩)$
18	10 6 17	cif	$class if ({Base}_{Scalar (w)} \subseteq x, w, w sSet ⟨Scalar (ndx), Scalar (w) ↾_{𝑠} x⟩)$
19	1 3 2 2 18	cmpo	$class (w \in V, x \in V ⟼ if ({Base}_{Scalar (w)} \subseteq x, w, w sSet ⟨Scalar (ndx), Scalar (w) ↾_{𝑠} x⟩))$
20	0 19	wceq	$wff ↾_{𝑣} = (w \in V, x \in V ⟼ if ({Base}_{Scalar (w)} \subseteq x, w, w sSet ⟨Scalar (ndx), Scalar (w) ↾_{𝑠} x⟩))$

Metamath Proof Explorer