resvsca

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

	Ref	Expression
Hypotheses	resvsca.r	$⊢ R = W ↾_{𝑣} A$
	resvsca.f	$⊢ F = Scalar (W)$
	resvsca.b	$⊢ B = {Base}_{F}$
Assertion	resvsca	$⊢ A \in V \to F ↾_{𝑠} A = Scalar (R)$

Proof

Step	Hyp	Ref	Expression
1		resvsca.r	$⊢ R = W ↾_{𝑣} A$
2		resvsca.f	$⊢ F = Scalar (W)$
3		resvsca.b	$⊢ B = {Base}_{F}$
4	2	fvexi	$⊢ F \in V$
5		eqid	$⊢ F ↾_{𝑠} A = F ↾_{𝑠} A$
6	5 3	ressid2	$⊢ (B \subseteq A \land F \in V \land A \in V) \to F ↾_{𝑠} A = F$
7	4 6	mp3an2	$⊢ (B \subseteq A \land A \in V) \to F ↾_{𝑠} A = F$
8	7	3adant2	$⊢ (B \subseteq A \land W \in V \land A \in V) \to F ↾_{𝑠} A = F$
9	1 2 3	resvid2	$⊢ (B \subseteq A \land W \in V \land A \in V) \to R = W$
10	9	fveq2d	$⊢ (B \subseteq A \land W \in V \land A \in V) \to Scalar (R) = Scalar (W)$
11	2 8 10	3eqtr4a	$⊢ (B \subseteq A \land W \in V \land A \in V) \to F ↾_{𝑠} A = Scalar (R)$
12	11	3expib	$⊢ B \subseteq A \to ((W \in V \land A \in V) \to F ↾_{𝑠} A = Scalar (R))$
13		simp2	$⊢ (\neg B \subseteq A \land W \in V \land A \in V) \to W \in V$
14		ovex	$⊢ F ↾_{𝑠} A \in V$
15		scaid	$⊢ Scalar = Slot Scalar (ndx)$
16	15	setsid	$⊢ (W \in V \land F ↾_{𝑠} A \in V) \to F ↾_{𝑠} A = Scalar (W sSet ⟨Scalar (ndx), F ↾_{𝑠} A⟩)$
17	13 14 16	sylancl	$⊢ (\neg B \subseteq A \land W \in V \land A \in V) \to F ↾_{𝑠} A = Scalar (W sSet ⟨Scalar (ndx), F ↾_{𝑠} A⟩)$
18	1 2 3	resvval2	$⊢ (\neg B \subseteq A \land W \in V \land A \in V) \to R = W sSet ⟨Scalar (ndx), F ↾_{𝑠} A⟩$
19	18	fveq2d	$⊢ (\neg B \subseteq A \land W \in V \land A \in V) \to Scalar (R) = Scalar (W sSet ⟨Scalar (ndx), F ↾_{𝑠} A⟩)$
20	17 19	eqtr4d	$⊢ (\neg B \subseteq A \land W \in V \land A \in V) \to F ↾_{𝑠} A = Scalar (R)$
21	20	3expib	$⊢ \neg B \subseteq A \to ((W \in V \land A \in V) \to F ↾_{𝑠} A = Scalar (R))$
22	12 21	pm2.61i	$⊢ (W \in V \land A \in V) \to F ↾_{𝑠} A = Scalar (R)$
23		0fv	$⊢ \emptyset (Scalar (ndx)) = \emptyset$
24		0ex	$⊢ \emptyset \in V$
25	24 15	strfvn	$⊢ Scalar (\emptyset) = \emptyset (Scalar (ndx))$
26		ress0	$⊢ \emptyset ↾_{𝑠} A = \emptyset$
27	23 25 26	3eqtr4ri	$⊢ \emptyset ↾_{𝑠} A = Scalar (\emptyset)$
28		fvprc	$⊢ \neg W \in V \to Scalar (W) = \emptyset$
29	2 28	eqtrid	$⊢ \neg W \in V \to F = \emptyset$
30	29	oveq1d	$⊢ \neg W \in V \to F ↾_{𝑠} A = \emptyset ↾_{𝑠} A$
31		reldmresv	$⊢ Rel dom ↾_{𝑣}$
32	31	ovprc1	$⊢ \neg W \in V \to W ↾_{𝑣} A = \emptyset$
33	1 32	eqtrid	$⊢ \neg W \in V \to R = \emptyset$
34	33	fveq2d	$⊢ \neg W \in V \to Scalar (R) = Scalar (\emptyset)$
35	27 30 34	3eqtr4a	$⊢ \neg W \in V \to F ↾_{𝑠} A = Scalar (R)$
36	35	adantr	$⊢ (\neg W \in V \land A \in V) \to F ↾_{𝑠} A = Scalar (R)$
37	22 36	pm2.61ian	$⊢ A \in V \to F ↾_{𝑠} A = Scalar (R)$

Metamath Proof Explorer

Theorem resvsca

Proof