This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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