Proof of Theorem resvsca
Step | Hyp | Ref
| Expression |
1 | | resvsca.f |
. . . . 5
⊢ 𝐹 = (Scalar‘𝑊) |
2 | | fvex 6201 |
. . . . . . . 8
⊢
(Scalar‘𝑊)
∈ V |
3 | 1, 2 | eqeltri 2697 |
. . . . . . 7
⊢ 𝐹 ∈ V |
4 | | eqid 2622 |
. . . . . . . 8
⊢ (𝐹 ↾s 𝐴) = (𝐹 ↾s 𝐴) |
5 | | resvsca.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐹) |
6 | 4, 5 | ressid2 15928 |
. . . . . . 7
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐹 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐹 ↾s 𝐴) = 𝐹) |
7 | 3, 6 | mp3an2 1412 |
. . . . . 6
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → (𝐹 ↾s 𝐴) = 𝐹) |
8 | 7 | 3adant2 1080 |
. . . . 5
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐹 ↾s 𝐴) = 𝐹) |
9 | | resvsca.r |
. . . . . . 7
⊢ 𝑅 = (𝑊 ↾v 𝐴) |
10 | 9, 1, 5 | resvid2 29828 |
. . . . . 6
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → 𝑅 = 𝑊) |
11 | 10 | fveq2d 6195 |
. . . . 5
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (Scalar‘𝑅) = (Scalar‘𝑊)) |
12 | 1, 8, 11 | 3eqtr4a 2682 |
. . . 4
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐹 ↾s 𝐴) = (Scalar‘𝑅)) |
13 | 12 | 3expib 1268 |
. . 3
⊢ (𝐵 ⊆ 𝐴 → ((𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐹 ↾s 𝐴) = (Scalar‘𝑅))) |
14 | | simp2 1062 |
. . . . . 6
⊢ ((¬
𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → 𝑊 ∈ V) |
15 | | ovex 6678 |
. . . . . 6
⊢ (𝐹 ↾s 𝐴) ∈ V |
16 | | scaid 16014 |
. . . . . . 7
⊢ Scalar =
Slot (Scalar‘ndx) |
17 | 16 | setsid 15914 |
. . . . . 6
⊢ ((𝑊 ∈ V ∧ (𝐹 ↾s 𝐴) ∈ V) → (𝐹 ↾s 𝐴) = (Scalar‘(𝑊 sSet 〈(Scalar‘ndx),
(𝐹 ↾s
𝐴)〉))) |
18 | 14, 15, 17 | sylancl 694 |
. . . . 5
⊢ ((¬
𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐹 ↾s 𝐴) = (Scalar‘(𝑊 sSet 〈(Scalar‘ndx), (𝐹 ↾s 𝐴)〉))) |
19 | 9, 1, 5 | resvval2 29829 |
. . . . . 6
⊢ ((¬
𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → 𝑅 = (𝑊 sSet 〈(Scalar‘ndx), (𝐹 ↾s 𝐴)〉)) |
20 | 19 | fveq2d 6195 |
. . . . 5
⊢ ((¬
𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (Scalar‘𝑅) = (Scalar‘(𝑊 sSet 〈(Scalar‘ndx), (𝐹 ↾s 𝐴)〉))) |
21 | 18, 20 | eqtr4d 2659 |
. . . 4
⊢ ((¬
𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐹 ↾s 𝐴) = (Scalar‘𝑅)) |
22 | 21 | 3expib 1268 |
. . 3
⊢ (¬
𝐵 ⊆ 𝐴 → ((𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐹 ↾s 𝐴) = (Scalar‘𝑅))) |
23 | 13, 22 | pm2.61i 176 |
. 2
⊢ ((𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐹 ↾s 𝐴) = (Scalar‘𝑅)) |
24 | | 0fv 6227 |
. . . . 5
⊢
(∅‘(Scalar‘ndx)) = ∅ |
25 | | 0ex 4790 |
. . . . . 6
⊢ ∅
∈ V |
26 | 25, 16 | strfvn 15879 |
. . . . 5
⊢
(Scalar‘∅) =
(∅‘(Scalar‘ndx)) |
27 | | ress0 15934 |
. . . . 5
⊢ (∅
↾s 𝐴) =
∅ |
28 | 24, 26, 27 | 3eqtr4ri 2655 |
. . . 4
⊢ (∅
↾s 𝐴) =
(Scalar‘∅) |
29 | | fvprc 6185 |
. . . . . 6
⊢ (¬
𝑊 ∈ V →
(Scalar‘𝑊) =
∅) |
30 | 1, 29 | syl5eq 2668 |
. . . . 5
⊢ (¬
𝑊 ∈ V → 𝐹 = ∅) |
31 | 30 | oveq1d 6665 |
. . . 4
⊢ (¬
𝑊 ∈ V → (𝐹 ↾s 𝐴) = (∅ ↾s
𝐴)) |
32 | | reldmresv 29826 |
. . . . . . 7
⊢ Rel dom
↾v |
33 | 32 | ovprc1 6684 |
. . . . . 6
⊢ (¬
𝑊 ∈ V → (𝑊 ↾v 𝐴) = ∅) |
34 | 9, 33 | syl5eq 2668 |
. . . . 5
⊢ (¬
𝑊 ∈ V → 𝑅 = ∅) |
35 | 34 | fveq2d 6195 |
. . . 4
⊢ (¬
𝑊 ∈ V →
(Scalar‘𝑅) =
(Scalar‘∅)) |
36 | 28, 31, 35 | 3eqtr4a 2682 |
. . 3
⊢ (¬
𝑊 ∈ V → (𝐹 ↾s 𝐴) = (Scalar‘𝑅)) |
37 | 36 | adantr 481 |
. 2
⊢ ((¬
𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐹 ↾s 𝐴) = (Scalar‘𝑅)) |
38 | 23, 37 | pm2.61ian 831 |
1
⊢ (𝐴 ∈ 𝑉 → (𝐹 ↾s 𝐴) = (Scalar‘𝑅)) |