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=BaseF
Assertion resvval ⊢W∈X∧A∈Y→R=ifB⊆AWWsSetScalar⁡ndxF↾𝑠A

Proof

Step Hyp Ref Expression
1 resvsca.r ⊢R=W↾𝑣A
2 resvsca.f ⊢F=Scalar⁡W
3 resvsca.b ⊢B=BaseF
4 elex ⊢W∈X→W∈V
5 elex ⊢A∈Y→A∈V
6 ovex ⊢WsSetScalar⁡ndxF↾𝑠A∈V
7 ifcl ⊢W∈V∧WsSetScalar⁡ndxF↾𝑠A∈V→ifB⊆AWWsSetScalar⁡ndxF↾𝑠A∈V
8 6 7 mpan2 ⊢W∈V→ifB⊆AWWsSetScalar⁡ndxF↾𝑠A∈V
9 8 adantr ⊢W∈V∧A∈V→ifB⊆AWWsSetScalar⁡ndxF↾𝑠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→BaseScalar⁡w=BaseF
14 13 3 eqtr4di ⊢w=W∧x=A→BaseScalar⁡w=B
15 simpr ⊢w=W∧x=A→x=A
16 14 15 sseq12d ⊢w=W∧x=A→BaseScalar⁡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⁡ndxScalar⁡w↾𝑠x=Scalar⁡ndxF↾𝑠A
19 10 18 oveq12d ⊢w=W∧x=A→wsSetScalar⁡ndxScalar⁡w↾𝑠x=WsSetScalar⁡ndxF↾𝑠A
20 16 10 19 ifbieq12d ⊢w=W∧x=A→ifBaseScalar⁡w⊆xwwsSetScalar⁡ndxScalar⁡w↾𝑠x=ifB⊆AWWsSetScalar⁡ndxF↾𝑠A
21 df-resv ⊢↾𝑣=w∈V,x∈V⟼ifBaseScalar⁡w⊆xwwsSetScalar⁡ndxScalar⁡w↾𝑠x
22 20 21 ovmpoga ⊢W∈V∧A∈V∧ifB⊆AWWsSetScalar⁡ndxF↾𝑠A∈V→W↾𝑣A=ifB⊆AWWsSetScalar⁡ndxF↾𝑠A
23 9 22 mpd3an3 ⊢W∈V∧A∈V→W↾𝑣A=ifB⊆AWWsSetScalar⁡ndxF↾𝑠A
24 4 5 23 syl2an ⊢W∈X∧A∈Y→W↾𝑣A=ifB⊆AWWsSetScalar⁡ndxF↾𝑠A
25 1 24 eqtrid ⊢W∈X∧A∈Y→R=ifB⊆AWWsSetScalar⁡ndxF↾𝑠A