Theorem resvid2

Description: General behavior of trivial 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	resvid2	|- ( ( B C_ A /\ W e. X /\ A e. Y ) -> R = W )

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		iftrue	|- ( B C_ A -> if ( B C_ A , W , ( W sSet <. ( Scalar ` ndx ) , ( F |`s A ) >. ) ) = W )
6	4 5	sylan9eqr	|- ( ( B C_ A /\ ( W e. X /\ A e. Y ) ) -> R = W )
7	6	3impb	|- ( ( B C_ A /\ W e. X /\ A e. Y ) -> R = W )