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 eqtrid ⊢ W ∈ X ∧ A ∈ Y → R = if B ⊆ A W W sSet Scalar ⁡ ndx F ↾ 𝑠 A