Theorem resvid2

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

	Ref	Expression
Hypotheses	resvsca.r	$$⊢R=W{\upharpoonright }_{𝑣}A$$
	resvsca.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	resvsca.b	$$⊢B={\mathrm{Base}}_F$$
Assertion	resvid2	$$⊢\left(B\subseteq A\wedge W\in X\wedge A\in Y\right)\to R=W$$

Proof

Step	Hyp	Ref	Expression
1		resvsca.r	$$⊢R=W{\upharpoonright }_{𝑣}A$$
2		resvsca.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
3		resvsca.b	$$⊢B={\mathrm{Base}}_F$$
4	1 2 3	resvval	$$⊢\left(W\in X\wedge A\in Y\right)\to R=if\left(B\subseteq A,W,W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),F{\upharpoonright }_{𝑠}A⟩\right)$$
5		iftrue	$$⊢B\subseteq A\to if\left(B\subseteq A,W,W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),F{\upharpoonright }_{𝑠}A⟩\right)=W$$
6	4 5	sylan9eqr	$$⊢\left(B\subseteq A\wedge \left(W\in X\wedge A\in Y\right)\right)\to R=W$$
7	6	3impb	$$⊢\left(B\subseteq A\wedge W\in X\wedge A\in Y\right)\to R=W$$