Theorem resvval2

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

	Ref	Expression
Hypotheses	resvsca.r	|- R = ( W |`v A )
	resvsca.f	|- F = ( Scalar ` W )
	resvsca.b	|- B = ( Base ` F )
Assertion	resvval2	|- ( ( -. B C_ A /\ W e. X /\ A e. Y ) -> R = ( W sSet <. ( Scalar ` ndx ) , ( F |`s A ) >. ) )

Proof

Step	Hyp	Ref	Expression
1		resvsca.r	|- R = ( W |`v A )
2		resvsca.f	|- F = ( Scalar ` W )
3		resvsca.b	|- B = ( Base ` F )
4	1 2 3	resvval	|- ( ( W e. X /\ A e. Y ) -> R = if ( B C_ A , W , ( W sSet <. ( Scalar ` ndx ) , ( F |`s A ) >. ) ) )
5		iffalse	|- ( -. B C_ A -> if ( B C_ A , W , ( W sSet <. ( Scalar ` ndx ) , ( F |`s A ) >. ) ) = ( W sSet <. ( Scalar ` ndx ) , ( F |`s A ) >. ) )
6	4 5	sylan9eqr	|- ( ( -. B C_ A /\ ( W e. X /\ A e. Y ) ) -> R = ( W sSet <. ( Scalar ` ndx ) , ( F |`s A ) >. ) )
7	6	3impb	|- ( ( -. B C_ A /\ W e. X /\ A e. Y ) -> R = ( W sSet <. ( Scalar ` ndx ) , ( F |`s A ) >. ) )