Metamath Proof Explorer


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 𝑥 ) ⟩ ) ) )