Step | Hyp | Ref
| Expression |
1 | | asclfval.a |
. 2
⊢ 𝐴 = (algSc‘𝑊) |
2 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊)) |
3 | | asclfval.f |
. . . . . . . 8
⊢ 𝐹 = (Scalar‘𝑊) |
4 | 2, 3 | syl6eqr 2662 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝐹) |
5 | 4 | fveq2d 6107 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = (Base‘𝐹)) |
6 | | asclfval.k |
. . . . . 6
⊢ 𝐾 = (Base‘𝐹) |
7 | 5, 6 | syl6eqr 2662 |
. . . . 5
⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = 𝐾) |
8 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (
·𝑠 ‘𝑤) = ( ·𝑠
‘𝑊)) |
9 | | asclfval.s |
. . . . . . 7
⊢ · = (
·𝑠 ‘𝑊) |
10 | 8, 9 | syl6eqr 2662 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (
·𝑠 ‘𝑤) = · ) |
11 | | eqidd 2611 |
. . . . . 6
⊢ (𝑤 = 𝑊 → 𝑥 = 𝑥) |
12 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (1r‘𝑤) = (1r‘𝑊)) |
13 | | asclfval.o |
. . . . . . 7
⊢ 1 =
(1r‘𝑊) |
14 | 12, 13 | syl6eqr 2662 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (1r‘𝑤) = 1 ) |
15 | 10, 11, 14 | oveq123d 6570 |
. . . . 5
⊢ (𝑤 = 𝑊 → (𝑥( ·𝑠
‘𝑤)(1r‘𝑤)) = (𝑥 · 1 )) |
16 | 7, 15 | mpteq12dv 4663 |
. . . 4
⊢ (𝑤 = 𝑊 → (𝑥 ∈ (Base‘(Scalar‘𝑤)) ↦ (𝑥( ·𝑠
‘𝑤)(1r‘𝑤))) = (𝑥 ∈ 𝐾 ↦ (𝑥 · 1 ))) |
17 | | df-ascl 19135 |
. . . 4
⊢ algSc =
(𝑤 ∈ V ↦ (𝑥 ∈
(Base‘(Scalar‘𝑤)) ↦ (𝑥( ·𝑠
‘𝑤)(1r‘𝑤)))) |
18 | 3 | fveq2i 6106 |
. . . . . . 7
⊢
(Base‘𝐹) =
(Base‘(Scalar‘𝑊)) |
19 | 6, 18 | eqtri 2632 |
. . . . . 6
⊢ 𝐾 =
(Base‘(Scalar‘𝑊)) |
20 | | fvex 6113 |
. . . . . 6
⊢
(Base‘(Scalar‘𝑊)) ∈ V |
21 | 19, 20 | eqeltri 2684 |
. . . . 5
⊢ 𝐾 ∈ V |
22 | 21 | mptex 6390 |
. . . 4
⊢ (𝑥 ∈ 𝐾 ↦ (𝑥 · 1 )) ∈
V |
23 | 16, 17, 22 | fvmpt 6191 |
. . 3
⊢ (𝑊 ∈ V →
(algSc‘𝑊) = (𝑥 ∈ 𝐾 ↦ (𝑥 · 1 ))) |
24 | | fvprc 6097 |
. . . . 5
⊢ (¬
𝑊 ∈ V →
(algSc‘𝑊) =
∅) |
25 | | mpt0 5934 |
. . . . 5
⊢ (𝑥 ∈ ∅ ↦ (𝑥 · 1 )) =
∅ |
26 | 24, 25 | syl6eqr 2662 |
. . . 4
⊢ (¬
𝑊 ∈ V →
(algSc‘𝑊) = (𝑥 ∈ ∅ ↦ (𝑥 · 1 ))) |
27 | | fvprc 6097 |
. . . . . . . . 9
⊢ (¬
𝑊 ∈ V →
(Scalar‘𝑊) =
∅) |
28 | 3, 27 | syl5eq 2656 |
. . . . . . . 8
⊢ (¬
𝑊 ∈ V → 𝐹 = ∅) |
29 | 28 | fveq2d 6107 |
. . . . . . 7
⊢ (¬
𝑊 ∈ V →
(Base‘𝐹) =
(Base‘∅)) |
30 | | base0 15740 |
. . . . . . 7
⊢ ∅ =
(Base‘∅) |
31 | 29, 30 | syl6eqr 2662 |
. . . . . 6
⊢ (¬
𝑊 ∈ V →
(Base‘𝐹) =
∅) |
32 | 6, 31 | syl5eq 2656 |
. . . . 5
⊢ (¬
𝑊 ∈ V → 𝐾 = ∅) |
33 | 32 | mpteq1d 4666 |
. . . 4
⊢ (¬
𝑊 ∈ V → (𝑥 ∈ 𝐾 ↦ (𝑥 · 1 )) = (𝑥 ∈ ∅ ↦ (𝑥 · 1 ))) |
34 | 26, 33 | eqtr4d 2647 |
. . 3
⊢ (¬
𝑊 ∈ V →
(algSc‘𝑊) = (𝑥 ∈ 𝐾 ↦ (𝑥 · 1 ))) |
35 | 23, 34 | pm2.61i 175 |
. 2
⊢
(algSc‘𝑊) =
(𝑥 ∈ 𝐾 ↦ (𝑥 · 1 )) |
36 | 1, 35 | eqtri 2632 |
1
⊢ 𝐴 = (𝑥 ∈ 𝐾 ↦ (𝑥 · 1 )) |