resvlem

Description: Other elements of a scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018) (Revised by AV, 31-Oct-2024)

	Ref	Expression
Hypotheses	resvlem.r	$⊢ R = W ↾_{𝑣} A$
	resvlem.e	$⊢ C = E (W)$
	resvlem.f	$⊢ E = Slot E (ndx)$
	resvlem.n	$⊢ E (ndx) \neq Scalar (ndx)$
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 E (ndx)$
4		resvlem.n	$⊢ E (ndx) \neq Scalar (ndx)$
5		eqid	$⊢ Scalar (W) = Scalar (W)$
6		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
7	1 5 6	resvid2	$⊢ ({Base}_{Scalar (W)} \subseteq A \land W \in V \land A \in V) \to R = W$
8	7	fveq2d	$⊢ ({Base}_{Scalar (W)} \subseteq A \land W \in V \land A \in V) \to E (R) = E (W)$
9	8	3expib	$⊢ {Base}_{Scalar (W)} \subseteq A \to ((W \in V \land A \in V) \to E (R) = E (W))$
10	1 5 6	resvval2	$⊢ (\neg {Base}_{Scalar (W)} \subseteq A \land W \in V \land A \in V) \to R = W sSet ⟨Scalar (ndx), Scalar (W) ↾_{𝑠} A⟩$
11	10	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⟩)$
12	3 4	setsnid	$⊢ E (W) = E (W sSet ⟨Scalar (ndx), Scalar (W) ↾_{𝑠} A⟩)$
13	11 12	eqtr4di	$⊢ (\neg {Base}_{Scalar (W)} \subseteq A \land W \in V \land A \in V) \to E (R) = E (W)$
14	13	3expib	$⊢ \neg {Base}_{Scalar (W)} \subseteq A \to ((W \in V \land A \in V) \to E (R) = E (W))$
15	9 14	pm2.61i	$⊢ (W \in V \land A \in V) \to E (R) = E (W)$
16	3	str0	$⊢ \emptyset = E (\emptyset)$
17	16	eqcomi	$⊢ E (\emptyset) = \emptyset$
18		reldmresv	$⊢ Rel dom ↾_{𝑣}$
19	17 1 18	oveqprc	$⊢ \neg W \in V \to E (W) = E (R)$
20	19	eqcomd	$⊢ \neg W \in V \to E (R) = E (W)$
21	20	adantr	$⊢ (\neg W \in V \land A \in V) \to E (R) = E (W)$
22	15 21	pm2.61ian	$⊢ A \in V \to E (R) = E (W)$
23	2 22	eqtr4id	$⊢ A \in V \to C = E (R)$

Metamath Proof Explorer

Theorem resvlem

Proof