Metamath Proof Explorer

Theorem 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 ∈ V → 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 ∈ V
5 eqid ⊢ F ↾ 𝑠 A = F ↾ 𝑠 A
6 5 3 ressid2 ⊢ B ⊆ A ∧ F ∈ V ∧ A ∈ V → F ↾ 𝑠 A = F
7 4 6 mp3an2 ⊢ B ⊆ A ∧ A ∈ V → F ↾ 𝑠 A = F
8 7 3adant2 ⊢ B ⊆ A ∧ W ∈ V ∧ A ∈ V → F ↾ 𝑠 A = F
9 1 2 3 resvid2 ⊢ B ⊆ A ∧ W ∈ V ∧ A ∈ V → R = W
10 9 fveq2d ⊢ B ⊆ A ∧ W ∈ V ∧ A ∈ V → Scalar ⁡ R = Scalar ⁡ W
11 2 8 10 3eqtr4a ⊢ B ⊆ A ∧ W ∈ V ∧ A ∈ V → F ↾ 𝑠 A = Scalar ⁡ R
12 11 3expib ⊢ B ⊆ A → W ∈ V ∧ A ∈ V → F ↾ 𝑠 A = Scalar ⁡ R
13 simp2 ⊢ ¬ B ⊆ A ∧ W ∈ V ∧ A ∈ V → W ∈ V
14 ovex ⊢ F ↾ 𝑠 A ∈ V
15 scaid ⊢ Scalar = Slot Scalar ⁡ ndx
16 15 setsid ⊢ W ∈ V ∧ F ↾ 𝑠 A ∈ V → F ↾ 𝑠 A = Scalar ⁡ W sSet Scalar ⁡ ndx F ↾ 𝑠 A
17 13 14 16 sylancl ⊢ ¬ B ⊆ A ∧ W ∈ V ∧ A ∈ V → F ↾ 𝑠 A = Scalar ⁡ W sSet Scalar ⁡ ndx F ↾ 𝑠 A
18 1 2 3 resvval2 ⊢ ¬ B ⊆ A ∧ W ∈ V ∧ A ∈ V → R = W sSet Scalar ⁡ ndx F ↾ 𝑠 A
19 18 fveq2d ⊢ ¬ B ⊆ A ∧ W ∈ V ∧ A ∈ V → Scalar ⁡ R = Scalar ⁡ W sSet Scalar ⁡ ndx F ↾ 𝑠 A
20 17 19 eqtr4d ⊢ ¬ B ⊆ A ∧ W ∈ V ∧ A ∈ V → F ↾ 𝑠 A = Scalar ⁡ R
21 20 3expib ⊢ ¬ B ⊆ A → W ∈ V ∧ A ∈ V → F ↾ 𝑠 A = Scalar ⁡ R
22 12 21 pm2.61i ⊢ W ∈ V ∧ A ∈ V → F ↾ 𝑠 A = Scalar ⁡ R
23 0fv ⊢ ∅ ⁡ Scalar ⁡ ndx = ∅
24 0ex ⊢ ∅ ∈ V
25 24 15 strfvn ⊢ Scalar ⁡ ∅ = ∅ ⁡ Scalar ⁡ ndx
26 ress0 ⊢ ∅ ↾ 𝑠 A = ∅
27 23 25 26 3eqtr4ri ⊢ ∅ ↾ 𝑠 A = Scalar ⁡ ∅
28 fvprc ⊢ ¬ W ∈ V → Scalar ⁡ W = ∅
29 2 28 eqtrid ⊢ ¬ W ∈ V → F = ∅
30 29 oveq1d ⊢ ¬ W ∈ V → F ↾ 𝑠 A = ∅ ↾ 𝑠 A
31 reldmresv ⊢ Rel ⁡ dom ⁡ ↾ 𝑣
32 31 ovprc1 ⊢ ¬ W ∈ V → W ↾ 𝑣 A = ∅
33 1 32 eqtrid ⊢ ¬ W ∈ V → R = ∅
34 33 fveq2d ⊢ ¬ W ∈ V → Scalar ⁡ R = Scalar ⁡ ∅
35 27 30 34 3eqtr4a ⊢ ¬ W ∈ V → F ↾ 𝑠 A = Scalar ⁡ R
36 35 adantr ⊢ ¬ W ∈ V ∧ A ∈ V → F ↾ 𝑠 A = Scalar ⁡ R
37 22 36 pm2.61ian ⊢ A ∈ V → F ↾ 𝑠 A = Scalar ⁡ R