Definition df-resv 33336

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 33335	. 2 class ↾v
2		vw	. . 3 setvar 𝑤
3		vx	. . 3 setvar 𝑥
4		cvv 3437	. . 3 class V
5	2	cv 1540	. . . . . . 7 class 𝑤
6		csca 17171	. . . . . . 7 class Scalar
7	5, 6	cfv 6489	. . . . . 6 class (Scalar‘𝑤)
8		cbs 17127	. . . . . 6 class Base
9	7, 8	cfv 6489	. . . . 5 class (Base‘(Scalar‘𝑤))
10	3	cv 1540	. . . . 5 class 𝑥
11	9, 10	wss 3898	. . . 4 wff (Base‘(Scalar‘𝑤)) ⊆ 𝑥
12		cnx 17111	. . . . . . 7 class ndx
13	12, 6	cfv 6489	. . . . . 6 class (Scalar‘ndx)
14		cress 17148	. . . . . . 7 class ↾s
15	7, 10, 14	co 7355	. . . . . 6 class ((Scalar‘𝑤) ↾s 𝑥)
16	13, 15	cop 4583	. . . . 5 class ⟨(Scalar‘ndx), ((Scalar‘𝑤) ↾s 𝑥)⟩
17		csts 17081	. . . . 5 class sSet
18	5, 16, 17	co 7355	. . . 4 class (𝑤 sSet ⟨(Scalar‘ndx), ((Scalar‘𝑤) ↾s 𝑥)⟩)
19	11, 5, 18	cif 4476	. . 3 class if((Base‘(Scalar‘𝑤)) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Scalar‘ndx), ((Scalar‘𝑤) ↾s 𝑥)⟩))
20	2, 3, 4, 4, 19	cmpo 7357	. 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  33337  resvval  33338