Theorem resvval2

Description: Value of nontrivial structure 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	resvval2	$$⊢\left(\neg B\subseteq A\wedge W\in X\wedge A\in Y\right)\to R=W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),F{\upharpoonright }_{𝑠}A⟩$$

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		iffalse	$$⊢\neg B\subseteq A\to if\left(B\subseteq A,W,W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),F{\upharpoonright }_{𝑠}A⟩\right)=W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),F{\upharpoonright }_{𝑠}A⟩$$
6	4 5	sylan9eqr	$$⊢\left(\neg B\subseteq A\wedge \left(W\in X\wedge A\in Y\right)\right)\to R=W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),F{\upharpoonright }_{𝑠}A⟩$$
7	6	3impb	$$⊢\left(\neg B\subseteq A\wedge W\in X\wedge A\in Y\right)\to R=W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),F{\upharpoonright }_{𝑠}A⟩$$