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 syl5eq ¬ 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 syl5eq ¬ 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