Theorem resvlemOLD

Description: Obsolete version of resvlem as of 31-Oct-2024. Other elements of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	resvlemOLD.r	$$⊢R=W{\upharpoonright }_{𝑣}A$$
	resvlemOLD.e	$$⊢C=E\left(W\right)$$
	resvlemOLD.f	$$⊢E=\mathrm{Slot}N$$
	resvlemOLD.n	$$⊢N\in \mathbb{N}$$
	resvlemOLD.b	$$⊢N\ne 5$$
Assertion	resvlemOLD	$$⊢A\in V\to C=E\left(R\right)$$

Proof

Step	Hyp	Ref	Expression
1		resvlemOLD.r	$$⊢R=W{\upharpoonright }_{𝑣}A$$
2		resvlemOLD.e	$$⊢C=E\left(W\right)$$
3		resvlemOLD.f	$$⊢E=\mathrm{Slot}N$$
4		resvlemOLD.n	$$⊢N\in \mathbb{N}$$
5		resvlemOLD.b	$$⊢N\ne 5$$
6		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
7		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
8	1 6 7	resvid2	$$⊢\left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\subseteq A\wedge W\in \mathrm{V}\wedge A\in V\right)\to R=W$$
9	8	fveq2d	$$⊢\left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\subseteq A\wedge W\in \mathrm{V}\wedge A\in V\right)\to E\left(R\right)=E\left(W\right)$$
10	9	3expib	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\subseteq A\to \left(\left(W\in \mathrm{V}\wedge A\in V\right)\to E\left(R\right)=E\left(W\right)\right)$$
11	1 6 7	resvval2	$$⊢\left(\neg {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\subseteq A\wedge W\in \mathrm{V}\wedge A\in V\right)\to R=W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(W\right){\upharpoonright }_{𝑠}A⟩$$
12	11	fveq2d	$$⊢\left(\neg {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\subseteq A\wedge W\in \mathrm{V}\wedge A\in V\right)\to E\left(R\right)=E\left(W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(W\right){\upharpoonright }_{𝑠}A⟩\right)$$
13	3 4	ndxid	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
14	3 4	ndxarg	$$⊢E\left(\mathrm{ndx}\right)=N$$
15	14 5	eqnetri	$$⊢E\left(\mathrm{ndx}\right)\ne 5$$
16		scandx	$$⊢\mathrm{Scalar}\left(\mathrm{ndx}\right)=5$$
17	15 16	neeqtrri	$$⊢E\left(\mathrm{ndx}\right)\ne \mathrm{Scalar}\left(\mathrm{ndx}\right)$$
18	13 17	setsnid	$$⊢E\left(W\right)=E\left(W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(W\right){\upharpoonright }_{𝑠}A⟩\right)$$
19	12 18	eqtr4di	$$⊢\left(\neg {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\subseteq A\wedge W\in \mathrm{V}\wedge A\in V\right)\to E\left(R\right)=E\left(W\right)$$
20	19	3expib	$$⊢\neg {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\subseteq A\to \left(\left(W\in \mathrm{V}\wedge A\in V\right)\to E\left(R\right)=E\left(W\right)\right)$$
21	10 20	pm2.61i	$$⊢\left(W\in \mathrm{V}\wedge A\in V\right)\to E\left(R\right)=E\left(W\right)$$
22		reldmresv	$$⊢\mathrm{Rel}\mathrm{dom}{\upharpoonright }_{𝑣}$$
23	22	ovprc1	$$⊢\neg W\in \mathrm{V}\to W{\upharpoonright }_{𝑣}A=\varnothing$$
24	1 23	syl5eq	$$⊢\neg W\in \mathrm{V}\to R=\varnothing$$
25	24	fveq2d	$$⊢\neg W\in \mathrm{V}\to E\left(R\right)=E\left(\varnothing \right)$$
26	3	str0	$$⊢\varnothing =E\left(\varnothing \right)$$
27	25 26	eqtr4di	$$⊢\neg W\in \mathrm{V}\to E\left(R\right)=\varnothing$$
28		fvprc	$$⊢\neg W\in \mathrm{V}\to E\left(W\right)=\varnothing$$
29	27 28	eqtr4d	$$⊢\neg W\in \mathrm{V}\to E\left(R\right)=E\left(W\right)$$
30	29	adantr	$$⊢\left(\neg W\in \mathrm{V}\wedge A\in V\right)\to E\left(R\right)=E\left(W\right)$$
31	21 30	pm2.61ian	$$⊢A\in V\to E\left(R\right)=E\left(W\right)$$
32	2 31	eqtr4id	$$⊢A\in V\to C=E\left(R\right)$$