Metamath Proof Explorer


Theorem resvval

Description: Value of 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 resvval W X A Y R = if B A W W sSet Scalar ndx F 𝑠 A

Proof

Step Hyp Ref Expression
1 resvsca.r R = W 𝑣 A
2 resvsca.f F = Scalar W
3 resvsca.b B = Base F
4 elex W X W V
5 elex A Y A V
6 ovex W sSet Scalar ndx F 𝑠 A V
7 ifcl W V W sSet Scalar ndx F 𝑠 A V if B A W W sSet Scalar ndx F 𝑠 A V
8 6 7 mpan2 W V if B A W W sSet Scalar ndx F 𝑠 A V
9 8 adantr W V A V if B A W W sSet Scalar ndx F 𝑠 A V
10 simpl w = W x = A w = W
11 10 fveq2d w = W x = A Scalar w = Scalar W
12 11 2 eqtr4di w = W x = A Scalar w = F
13 12 fveq2d w = W x = A Base Scalar w = Base F
14 13 3 eqtr4di w = W x = A Base Scalar w = B
15 simpr w = W x = A x = A
16 14 15 sseq12d w = W x = A Base Scalar w x B A
17 12 15 oveq12d w = W x = A Scalar w 𝑠 x = F 𝑠 A
18 17 opeq2d w = W x = A Scalar ndx Scalar w 𝑠 x = Scalar ndx F 𝑠 A
19 10 18 oveq12d w = W x = A w sSet Scalar ndx Scalar w 𝑠 x = W sSet Scalar ndx F 𝑠 A
20 16 10 19 ifbieq12d w = W x = A if Base Scalar w x w w sSet Scalar ndx Scalar w 𝑠 x = if B A W W sSet Scalar ndx F 𝑠 A
21 df-resv 𝑣 = w V , x V if Base Scalar w x w w sSet Scalar ndx Scalar w 𝑠 x
22 20 21 ovmpoga W V A V if B A W W sSet Scalar ndx F 𝑠 A V W 𝑣 A = if B A W W sSet Scalar ndx F 𝑠 A
23 9 22 mpd3an3 W V A V W 𝑣 A = if B A W W sSet Scalar ndx F 𝑠 A
24 4 5 23 syl2an W X A Y W 𝑣 A = if B A W W sSet Scalar ndx F 𝑠 A
25 1 24 syl5eq W X A Y R = if B A W W sSet Scalar ndx F 𝑠 A