Definition df-resv 29825

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 29824	. 2 class ↾v
2		vw	. . 3 setvar 𝑤
3		vx	. . 3 setvar 𝑥
4		cvv 3200	. . 3 class V
5	2	cv 1482	. . . . . . 7 class 𝑤
6		csca 15944	. . . . . . 7 class Scalar
7	5, 6	cfv 5888	. . . . . 6 class (Scalar‘𝑤)
8		cbs 15857	. . . . . 6 class Base
9	7, 8	cfv 5888	. . . . 5 class (Base‘(Scalar‘𝑤))
10	3	cv 1482	. . . . 5 class 𝑥
11	9, 10	wss 3574	. . . 4 wff (Base‘(Scalar‘𝑤)) ⊆ 𝑥
12		cnx 15854	. . . . . . 7 class ndx
13	12, 6	cfv 5888	. . . . . 6 class (Scalar‘ndx)
14		cress 15858	. . . . . . 7 class ↾s
15	7, 10, 14	co 6650	. . . . . 6 class ((Scalar‘𝑤) ↾s 𝑥)
16	13, 15	cop 4183	. . . . 5 class ⟨(Scalar‘ndx), ((Scalar‘𝑤) ↾s 𝑥)⟩
17		csts 15855	. . . . 5 class sSet
18	5, 16, 17	co 6650	. . . 4 class (𝑤 sSet ⟨(Scalar‘ndx), ((Scalar‘𝑤) ↾s 𝑥)⟩)
19	11, 5, 18	cif 4086	. . 3 class if((Base‘(Scalar‘𝑤)) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Scalar‘ndx), ((Scalar‘𝑤) ↾s 𝑥)⟩))
20	2, 3, 4, 4, 19	cmpt2 6652	. 2 class (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘(Scalar‘𝑤)) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Scalar‘ndx), ((Scalar‘𝑤) ↾s 𝑥)⟩)))
21	1, 20	wceq 1483	1 wff ↾v = (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘(Scalar‘𝑤)) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Scalar‘ndx), ((Scalar‘𝑤) ↾s 𝑥)⟩)))

This definition is referenced by:  reldmresv  29826  resvval  29827