Definition df-resv 31503

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 = (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘(Scalar‘𝑤)) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Scalar‘ndx), ((Scalar‘𝑤) ↾s 𝑥)⟩)))

Distinct variable group:   𝑥,𝑤

Detailed syntax breakdown of Definition df-resv

Step	Hyp	Ref	Expression
1		cresv 31502	. 2 class ↾v
2		vw	. . 3 setvar 𝑤
3		vx	. . 3 setvar 𝑥
4		cvv 3430	. . 3 class V
5	2	cv 1540	. . . . . . 7 class 𝑤
6		csca 16946	. . . . . . 7 class Scalar
7	5, 6	cfv 6430	. . . . . 6 class (Scalar‘𝑤)
8		cbs 16893	. . . . . 6 class Base
9	7, 8	cfv 6430	. . . . 5 class (Base‘(Scalar‘𝑤))
10	3	cv 1540	. . . . 5 class 𝑥
11	9, 10	wss 3891	. . . 4 wff (Base‘(Scalar‘𝑤)) ⊆ 𝑥
12		cnx 16875	. . . . . . 7 class ndx
13	12, 6	cfv 6430	. . . . . 6 class (Scalar‘ndx)
14		cress 16922	. . . . . . 7 class ↾s
15	7, 10, 14	co 7268	. . . . . 6 class ((Scalar‘𝑤) ↾s 𝑥)
16	13, 15	cop 4572	. . . . 5 class ⟨(Scalar‘ndx), ((Scalar‘𝑤) ↾s 𝑥)⟩
17		csts 16845	. . . . 5 class sSet
18	5, 16, 17	co 7268	. . . 4 class (𝑤 sSet ⟨(Scalar‘ndx), ((Scalar‘𝑤) ↾s 𝑥)⟩)
19	11, 5, 18	cif 4464	. . 3 class if((Base‘(Scalar‘𝑤)) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Scalar‘ndx), ((Scalar‘𝑤) ↾s 𝑥)⟩))
20	2, 3, 4, 4, 19	cmpo 7270	. 2 class (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘(Scalar‘𝑤)) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Scalar‘ndx), ((Scalar‘𝑤) ↾s 𝑥)⟩)))
21	1, 20	wceq 1541	1 wff ↾v = (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘(Scalar‘𝑤)) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Scalar‘ndx), ((Scalar‘𝑤) ↾s 𝑥)⟩)))

This definition is referenced by:  reldmresv  31504  resvval  31505