Metamath Proof Explorer


Theorem resvval2

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

Ref Expression
Hypotheses resvsca.r 𝑅 = ( 𝑊v 𝐴 )
resvsca.f 𝐹 = ( Scalar ‘ 𝑊 )
resvsca.b 𝐵 = ( Base ‘ 𝐹 )
Assertion resvval2 ( ( ¬ 𝐵𝐴𝑊𝑋𝐴𝑌 ) → 𝑅 = ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝐹s 𝐴 ) ⟩ ) )

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 iffalse ( ¬ 𝐵𝐴 → if ( 𝐵𝐴 , 𝑊 , ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝐹s 𝐴 ) ⟩ ) ) = ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝐹s 𝐴 ) ⟩ ) )
6 4 5 sylan9eqr ( ( ¬ 𝐵𝐴 ∧ ( 𝑊𝑋𝐴𝑌 ) ) → 𝑅 = ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝐹s 𝐴 ) ⟩ ) )
7 6 3impb ( ( ¬ 𝐵𝐴𝑊𝑋𝐴𝑌 ) → 𝑅 = ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝐹s 𝐴 ) ⟩ ) )