Metamath Proof Explorer


Theorem resvid2

Description: General behavior of trivial restriction. (Contributed by Thierry Arnoux, 6-Sep-2018)

Ref Expression
Hypotheses resvsca.r 𝑅 = ( 𝑊v 𝐴 )
resvsca.f 𝐹 = ( Scalar ‘ 𝑊 )
resvsca.b 𝐵 = ( Base ‘ 𝐹 )
Assertion resvid2 ( ( 𝐵𝐴𝑊𝑋𝐴𝑌 ) → 𝑅 = 𝑊 )

Proof

Step Hyp Ref Expression
1 resvsca.r 𝑅 = ( 𝑊v 𝐴 )
2 resvsca.f 𝐹 = ( Scalar ‘ 𝑊 )
3 resvsca.b 𝐵 = ( Base ‘ 𝐹 )
4 1 2 3 resvval ( ( 𝑊𝑋𝐴𝑌 ) → 𝑅 = if ( 𝐵𝐴 , 𝑊 , ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝐹s 𝐴 ) ⟩ ) ) )
5 iftrue ( 𝐵𝐴 → if ( 𝐵𝐴 , 𝑊 , ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝐹s 𝐴 ) ⟩ ) ) = 𝑊 )
6 4 5 sylan9eqr ( ( 𝐵𝐴 ∧ ( 𝑊𝑋𝐴𝑌 ) ) → 𝑅 = 𝑊 )
7 6 3impb ( ( 𝐵𝐴𝑊𝑋𝐴𝑌 ) → 𝑅 = 𝑊 )