Step | Hyp | Ref
| Expression |
1 | | scaffval.a |
. 2
⊢ ∙ = (
·sf ‘𝑊) |
2 | | fveq2 6493 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊)) |
3 | | scaffval.f |
. . . . . . . 8
⊢ 𝐹 = (Scalar‘𝑊) |
4 | 2, 3 | syl6eqr 2826 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝐹) |
5 | 4 | fveq2d 6497 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = (Base‘𝐹)) |
6 | | scaffval.k |
. . . . . 6
⊢ 𝐾 = (Base‘𝐹) |
7 | 5, 6 | syl6eqr 2826 |
. . . . 5
⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = 𝐾) |
8 | | fveq2 6493 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊)) |
9 | | scaffval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑊) |
10 | 8, 9 | syl6eqr 2826 |
. . . . 5
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝐵) |
11 | | fveq2 6493 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (
·𝑠 ‘𝑤) = ( ·𝑠
‘𝑊)) |
12 | | scaffval.s |
. . . . . . 7
⊢ · = (
·𝑠 ‘𝑊) |
13 | 11, 12 | syl6eqr 2826 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (
·𝑠 ‘𝑤) = · ) |
14 | 13 | oveqd 6987 |
. . . . 5
⊢ (𝑤 = 𝑊 → (𝑥( ·𝑠
‘𝑤)𝑦) = (𝑥 · 𝑦)) |
15 | 7, 10, 14 | mpoeq123dv 7041 |
. . . 4
⊢ (𝑤 = 𝑊 → (𝑥 ∈ (Base‘(Scalar‘𝑤)), 𝑦 ∈ (Base‘𝑤) ↦ (𝑥( ·𝑠
‘𝑤)𝑦)) = (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦))) |
16 | | df-scaf 19353 |
. . . 4
⊢
·sf = (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘(Scalar‘𝑤)), 𝑦 ∈ (Base‘𝑤) ↦ (𝑥( ·𝑠
‘𝑤)𝑦))) |
17 | | df-ov 6973 |
. . . . . . . 8
⊢ (𝑥 · 𝑦) = ( · ‘〈𝑥, 𝑦〉) |
18 | | fvrn0 6521 |
. . . . . . . 8
⊢ ( ·
‘〈𝑥, 𝑦〉) ∈ (ran · ∪
{∅}) |
19 | 17, 18 | eqeltri 2856 |
. . . . . . 7
⊢ (𝑥 · 𝑦) ∈ (ran · ∪
{∅}) |
20 | 19 | rgen2w 3095 |
. . . . . 6
⊢
∀𝑥 ∈
𝐾 ∀𝑦 ∈ 𝐵 (𝑥 · 𝑦) ∈ (ran · ∪
{∅}) |
21 | | eqid 2772 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦)) = (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦)) |
22 | 21 | fmpo 7568 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐾 ∀𝑦 ∈ 𝐵 (𝑥 · 𝑦) ∈ (ran · ∪ {∅})
↔ (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦)):(𝐾 × 𝐵)⟶(ran · ∪
{∅})) |
23 | 20, 22 | mpbi 222 |
. . . . 5
⊢ (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦)):(𝐾 × 𝐵)⟶(ran · ∪
{∅}) |
24 | 6 | fvexi 6507 |
. . . . . 6
⊢ 𝐾 ∈ V |
25 | 9 | fvexi 6507 |
. . . . . 6
⊢ 𝐵 ∈ V |
26 | 24, 25 | xpex 7287 |
. . . . 5
⊢ (𝐾 × 𝐵) ∈ V |
27 | 12 | fvexi 6507 |
. . . . . . 7
⊢ · ∈
V |
28 | 27 | rnex 7426 |
. . . . . 6
⊢ ran · ∈
V |
29 | | p0ex 5131 |
. . . . . 6
⊢ {∅}
∈ V |
30 | 28, 29 | unex 7280 |
. . . . 5
⊢ (ran
·
∪ {∅}) ∈ V |
31 | | fex2 7447 |
. . . . 5
⊢ (((𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦)):(𝐾 × 𝐵)⟶(ran · ∪ {∅})
∧ (𝐾 × 𝐵) ∈ V ∧ (ran · ∪
{∅}) ∈ V) → (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦)) ∈ V) |
32 | 23, 26, 30, 31 | mp3an 1440 |
. . . 4
⊢ (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦)) ∈ V |
33 | 15, 16, 32 | fvmpt 6589 |
. . 3
⊢ (𝑊 ∈ V → (
·sf ‘𝑊) = (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦))) |
34 | | fvprc 6486 |
. . . . 5
⊢ (¬
𝑊 ∈ V → (
·sf ‘𝑊) = ∅) |
35 | | mpo0 7049 |
. . . . 5
⊢ (𝑥 ∈ ∅, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦)) = ∅ |
36 | 34, 35 | syl6eqr 2826 |
. . . 4
⊢ (¬
𝑊 ∈ V → (
·sf ‘𝑊) = (𝑥 ∈ ∅, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦))) |
37 | | fvprc 6486 |
. . . . . . . . 9
⊢ (¬
𝑊 ∈ V →
(Scalar‘𝑊) =
∅) |
38 | 3, 37 | syl5eq 2820 |
. . . . . . . 8
⊢ (¬
𝑊 ∈ V → 𝐹 = ∅) |
39 | 38 | fveq2d 6497 |
. . . . . . 7
⊢ (¬
𝑊 ∈ V →
(Base‘𝐹) =
(Base‘∅)) |
40 | 6, 39 | syl5eq 2820 |
. . . . . 6
⊢ (¬
𝑊 ∈ V → 𝐾 =
(Base‘∅)) |
41 | | base0 16386 |
. . . . . 6
⊢ ∅ =
(Base‘∅) |
42 | 40, 41 | syl6eqr 2826 |
. . . . 5
⊢ (¬
𝑊 ∈ V → 𝐾 = ∅) |
43 | | eqid 2772 |
. . . . 5
⊢ 𝐵 = 𝐵 |
44 | | mpoeq12 7039 |
. . . . 5
⊢ ((𝐾 = ∅ ∧ 𝐵 = 𝐵) → (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦)) = (𝑥 ∈ ∅, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦))) |
45 | 42, 43, 44 | sylancl 577 |
. . . 4
⊢ (¬
𝑊 ∈ V → (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦)) = (𝑥 ∈ ∅, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦))) |
46 | 36, 45 | eqtr4d 2811 |
. . 3
⊢ (¬
𝑊 ∈ V → (
·sf ‘𝑊) = (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦))) |
47 | 33, 46 | pm2.61i 177 |
. 2
⊢ (
·sf ‘𝑊) = (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦)) |
48 | 1, 47 | eqtri 2796 |
1
⊢ ∙ =
(𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦)) |