Definition df-resv 30949

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 30948	. 2 class ↾v
2		vw	. . 3 setvar 𝑤
3		vx	. . 3 setvar 𝑥
4		cvv 3441	. . 3 class V
5	2	cv 1537	. . . . . . 7 class 𝑤
6		csca 16560	. . . . . . 7 class Scalar
7	5, 6	cfv 6324	. . . . . 6 class (Scalar‘𝑤)
8		cbs 16475	. . . . . 6 class Base
9	7, 8	cfv 6324	. . . . 5 class (Base‘(Scalar‘𝑤))
10	3	cv 1537	. . . . 5 class 𝑥
11	9, 10	wss 3881	. . . 4 wff (Base‘(Scalar‘𝑤)) ⊆ 𝑥
12		cnx 16472	. . . . . . 7 class ndx
13	12, 6	cfv 6324	. . . . . 6 class (Scalar‘ndx)
14		cress 16476	. . . . . . 7 class ↾s
15	7, 10, 14	co 7135	. . . . . 6 class ((Scalar‘𝑤) ↾s 𝑥)
16	13, 15	cop 4531	. . . . 5 class ⟨(Scalar‘ndx), ((Scalar‘𝑤) ↾s 𝑥)⟩
17		csts 16473	. . . . 5 class sSet
18	5, 16, 17	co 7135	. . . 4 class (𝑤 sSet ⟨(Scalar‘ndx), ((Scalar‘𝑤) ↾s 𝑥)⟩)
19	11, 5, 18	cif 4425	. . 3 class if((Base‘(Scalar‘𝑤)) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Scalar‘ndx), ((Scalar‘𝑤) ↾s 𝑥)⟩))
20	2, 3, 4, 4, 19	cmpo 7137	. 2 class (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘(Scalar‘𝑤)) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Scalar‘ndx), ((Scalar‘𝑤) ↾s 𝑥)⟩)))
21	1, 20	wceq 1538	1 wff ↾v = (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘(Scalar‘𝑤)) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Scalar‘ndx), ((Scalar‘𝑤) ↾s 𝑥)⟩)))

This definition is referenced by:  reldmresv  30950  resvval  30951