Metamath Proof Explorer

Theorem resvval

Description: Value of structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018)

Ref Expression
Hypotheses resvsca.r ⊢ 𝑅 = ( 𝑊 ↾v 𝐴 )
resvsca.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
resvsca.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
Assertion resvval ( ( 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌 ) → 𝑅 = if ( 𝐵 ⊆ 𝐴 , 𝑊 , ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝐹 ↾s 𝐴 ) ⟩ ) ) )

Proof

Step Hyp Ref Expression
1 resvsca.r ⊢ 𝑅 = ( 𝑊 ↾v 𝐴 )
2 resvsca.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3 resvsca.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
4 elex ⊢ ( 𝑊 ∈ 𝑋 → 𝑊 ∈ V )
5 elex ⊢ ( 𝐴 ∈ 𝑌 → 𝐴 ∈ V )
6 ovex ⊢ ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝐹 ↾s 𝐴 ) ⟩ ) ∈ V
7 ifcl ⊢ ( ( 𝑊 ∈ V ∧ ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝐹 ↾s 𝐴 ) ⟩ ) ∈ V ) → if ( 𝐵 ⊆ 𝐴 , 𝑊 , ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝐹 ↾s 𝐴 ) ⟩ ) ) ∈ V )
8 6 7 mpan2 ⊢ ( 𝑊 ∈ V → if ( 𝐵 ⊆ 𝐴 , 𝑊 , ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝐹 ↾s 𝐴 ) ⟩ ) ) ∈ V )
9 8 adantr ⊢ ( ( 𝑊 ∈ V ∧ 𝐴 ∈ V ) → if ( 𝐵 ⊆ 𝐴 , 𝑊 , ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝐹 ↾s 𝐴 ) ⟩ ) ) ∈ V )
10 simpl ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑥 = 𝐴 ) → 𝑤 = 𝑊 )
11 10 fveq2d ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑥 = 𝐴 ) → ( Scalar ‘ 𝑤 ) = ( Scalar ‘ 𝑊 ) )
12 11 2 eqtr4di ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑥 = 𝐴 ) → ( Scalar ‘ 𝑤 ) = 𝐹 )
13 12 fveq2d ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑥 = 𝐴 ) → ( Base ‘ ( Scalar ‘ 𝑤 ) ) = ( Base ‘ 𝐹 ) )
14 13 3 eqtr4di ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑥 = 𝐴 ) → ( Base ‘ ( Scalar ‘ 𝑤 ) ) = 𝐵 )
15 simpr ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑥 = 𝐴 ) → 𝑥 = 𝐴 )
16 14 15 sseq12d ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑥 = 𝐴 ) → ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ⊆ 𝑥 ↔ 𝐵 ⊆ 𝐴 ) )
17 12 15 oveq12d ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑥 = 𝐴 ) → ( ( Scalar ‘ 𝑤 ) ↾s 𝑥 ) = ( 𝐹 ↾s 𝐴 ) )
18 17 opeq2d ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑥 = 𝐴 ) → ⟨ ( Scalar ‘ ndx ) , ( ( Scalar ‘ 𝑤 ) ↾s 𝑥 ) ⟩ = ⟨ ( Scalar ‘ ndx ) , ( 𝐹 ↾s 𝐴 ) ⟩ )
19 10 18 oveq12d ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑥 = 𝐴 ) → ( 𝑤 sSet ⟨ ( Scalar ‘ ndx ) , ( ( Scalar ‘ 𝑤 ) ↾s 𝑥 ) ⟩ ) = ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝐹 ↾s 𝐴 ) ⟩ ) )
20 16 10 19 ifbieq12d ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑥 = 𝐴 ) → if ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ⊆ 𝑥 , 𝑤 , ( 𝑤 sSet ⟨ ( Scalar ‘ ndx ) , ( ( Scalar ‘ 𝑤 ) ↾s 𝑥 ) ⟩ ) ) = if ( 𝐵 ⊆ 𝐴 , 𝑊 , ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝐹 ↾s 𝐴 ) ⟩ ) ) )
21 df-resv ⊢ ↾v = ( 𝑤 ∈ V , 𝑥 ∈ V ↦ if ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ⊆ 𝑥 , 𝑤 , ( 𝑤 sSet ⟨ ( Scalar ‘ ndx ) , ( ( Scalar ‘ 𝑤 ) ↾s 𝑥 ) ⟩ ) ) )
22 20 21 ovmpoga ⊢ ( ( 𝑊 ∈ V ∧ 𝐴 ∈ V ∧ if ( 𝐵 ⊆ 𝐴 , 𝑊 , ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝐹 ↾s 𝐴 ) ⟩ ) ) ∈ V ) → ( 𝑊 ↾v 𝐴 ) = if ( 𝐵 ⊆ 𝐴 , 𝑊 , ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝐹 ↾s 𝐴 ) ⟩ ) ) )
23 9 22 mpd3an3 ⊢ ( ( 𝑊 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑊 ↾v 𝐴 ) = if ( 𝐵 ⊆ 𝐴 , 𝑊 , ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝐹 ↾s 𝐴 ) ⟩ ) ) )
24 4 5 23 syl2an ⊢ ( ( 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌 ) → ( 𝑊 ↾v 𝐴 ) = if ( 𝐵 ⊆ 𝐴 , 𝑊 , ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝐹 ↾s 𝐴 ) ⟩ ) ) )
25 1 24 syl5eq ⊢ ( ( 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌 ) → 𝑅 = if ( 𝐵 ⊆ 𝐴 , 𝑊 , ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝐹 ↾s 𝐴 ) ⟩ ) ) )