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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cresv	⊢ ↾v
1		vw	⊢ 𝑤
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		cbs	⊢ Base
5		csca	⊢ Scalar
6	1	cv	⊢ 𝑤
7	6 5	cfv	⊢ ( Scalar ‘ 𝑤 )
8	7 4	cfv	⊢ ( Base ‘ ( Scalar ‘ 𝑤 ) )
9	3	cv	⊢ 𝑥
10	8 9	wss	⊢ ( Base ‘ ( Scalar ‘ 𝑤 ) ) ⊆ 𝑥
11		csts	⊢ sSet
12		cnx	⊢ ndx
13	12 5	cfv	⊢ ( Scalar ‘ ndx )
14		cress	⊢ ↾s
15	7 9 14	co	⊢ ( ( Scalar ‘ 𝑤 ) ↾s 𝑥 )
16	13 15	cop	⊢ ⟨ ( Scalar ‘ ndx ) , ( ( Scalar ‘ 𝑤 ) ↾s 𝑥 ) ⟩
17	6 16 11	co	⊢ ( 𝑤 sSet ⟨ ( Scalar ‘ ndx ) , ( ( Scalar ‘ 𝑤 ) ↾s 𝑥 ) ⟩ )
18	10 6 17	cif	⊢ if ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ⊆ 𝑥 , 𝑤 , ( 𝑤 sSet ⟨ ( Scalar ‘ ndx ) , ( ( Scalar ‘ 𝑤 ) ↾s 𝑥 ) ⟩ ) )
19	1 3 2 2 18	cmpo	⊢ ( 𝑤 ∈ V , 𝑥 ∈ V ↦ if ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ⊆ 𝑥 , 𝑤 , ( 𝑤 sSet ⟨ ( Scalar ‘ ndx ) , ( ( Scalar ‘ 𝑤 ) ↾s 𝑥 ) ⟩ ) ) )
20	0 19	wceq	⊢ ↾v = ( 𝑤 ∈ V , 𝑥 ∈ V ↦ if ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ⊆ 𝑥 , 𝑤 , ( 𝑤 sSet ⟨ ( Scalar ‘ ndx ) , ( ( Scalar ‘ 𝑤 ) ↾s 𝑥 ) ⟩ ) ) )