resvlem

Description: Other elements of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018)

	Ref	Expression
Hypotheses	resvlem.r	$⊢ R = W ↾_{𝑣} A$
	resvlem.e	$⊢ C = E (W)$
	resvlem.f	$⊢ E = Slot N$
	resvlem.n	$⊢ N \in ℕ$
	resvlem.b	$⊢ N \neq 5$
Assertion	resvlem	$⊢ A \in V \to C = E (R)$

Proof

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

Metamath Proof Explorer

Theorem resvlem

Proof