Step | Hyp | Ref
| Expression |
1 | | scaffval.a |
. 2
⊢ ∙ = (
·sf ‘𝑊) |
2 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊)) |
3 | | scaffval.f |
. . . . . . . 8
⊢ 𝐹 = (Scalar‘𝑊) |
4 | 2, 3 | syl6eqr 2674 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝐹) |
5 | 4 | fveq2d 6195 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = (Base‘𝐹)) |
6 | | scaffval.k |
. . . . . 6
⊢ 𝐾 = (Base‘𝐹) |
7 | 5, 6 | syl6eqr 2674 |
. . . . 5
⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = 𝐾) |
8 | | fveq2 6191 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊)) |
9 | | scaffval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑊) |
10 | 8, 9 | syl6eqr 2674 |
. . . . 5
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝐵) |
11 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (
·𝑠 ‘𝑤) = ( ·𝑠
‘𝑊)) |
12 | | scaffval.s |
. . . . . . 7
⊢ · = (
·𝑠 ‘𝑊) |
13 | 11, 12 | syl6eqr 2674 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (
·𝑠 ‘𝑤) = · ) |
14 | 13 | oveqd 6667 |
. . . . 5
⊢ (𝑤 = 𝑊 → (𝑥( ·𝑠
‘𝑤)𝑦) = (𝑥 · 𝑦)) |
15 | 7, 10, 14 | mpt2eq123dv 6717 |
. . . 4
⊢ (𝑤 = 𝑊 → (𝑥 ∈ (Base‘(Scalar‘𝑤)), 𝑦 ∈ (Base‘𝑤) ↦ (𝑥( ·𝑠
‘𝑤)𝑦)) = (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦))) |
16 | | df-scaf 18866 |
. . . 4
⊢
·sf = (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘(Scalar‘𝑤)), 𝑦 ∈ (Base‘𝑤) ↦ (𝑥( ·𝑠
‘𝑤)𝑦))) |
17 | | df-ov 6653 |
. . . . . . . 8
⊢ (𝑥 · 𝑦) = ( · ‘〈𝑥, 𝑦〉) |
18 | | fvrn0 6216 |
. . . . . . . 8
⊢ ( ·
‘〈𝑥, 𝑦〉) ∈ (ran · ∪
{∅}) |
19 | 17, 18 | eqeltri 2697 |
. . . . . . 7
⊢ (𝑥 · 𝑦) ∈ (ran · ∪
{∅}) |
20 | 19 | rgen2w 2925 |
. . . . . 6
⊢
∀𝑥 ∈
𝐾 ∀𝑦 ∈ 𝐵 (𝑥 · 𝑦) ∈ (ran · ∪
{∅}) |
21 | | eqid 2622 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦)) = (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦)) |
22 | 21 | fmpt2 7237 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐾 ∀𝑦 ∈ 𝐵 (𝑥 · 𝑦) ∈ (ran · ∪ {∅})
↔ (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦)):(𝐾 × 𝐵)⟶(ran · ∪
{∅})) |
23 | 20, 22 | mpbi 220 |
. . . . 5
⊢ (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦)):(𝐾 × 𝐵)⟶(ran · ∪
{∅}) |
24 | | fvex 6201 |
. . . . . . 7
⊢
(Base‘𝐹)
∈ V |
25 | 6, 24 | eqeltri 2697 |
. . . . . 6
⊢ 𝐾 ∈ V |
26 | | fvex 6201 |
. . . . . . 7
⊢
(Base‘𝑊)
∈ V |
27 | 9, 26 | eqeltri 2697 |
. . . . . 6
⊢ 𝐵 ∈ V |
28 | 25, 27 | xpex 6962 |
. . . . 5
⊢ (𝐾 × 𝐵) ∈ V |
29 | | fvex 6201 |
. . . . . . . 8
⊢ (
·𝑠 ‘𝑊) ∈ V |
30 | 12, 29 | eqeltri 2697 |
. . . . . . 7
⊢ · ∈
V |
31 | 30 | rnex 7100 |
. . . . . 6
⊢ ran · ∈
V |
32 | | p0ex 4853 |
. . . . . 6
⊢ {∅}
∈ V |
33 | 31, 32 | unex 6956 |
. . . . 5
⊢ (ran
·
∪ {∅}) ∈ V |
34 | | fex2 7121 |
. . . . 5
⊢ (((𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦)):(𝐾 × 𝐵)⟶(ran · ∪ {∅})
∧ (𝐾 × 𝐵) ∈ V ∧ (ran · ∪
{∅}) ∈ V) → (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦)) ∈ V) |
35 | 23, 28, 33, 34 | mp3an 1424 |
. . . 4
⊢ (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦)) ∈ V |
36 | 15, 16, 35 | fvmpt 6282 |
. . 3
⊢ (𝑊 ∈ V → (
·sf ‘𝑊) = (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦))) |
37 | | fvprc 6185 |
. . . . 5
⊢ (¬
𝑊 ∈ V → (
·sf ‘𝑊) = ∅) |
38 | | mpt20 6725 |
. . . . 5
⊢ (𝑥 ∈ ∅, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦)) = ∅ |
39 | 37, 38 | syl6eqr 2674 |
. . . 4
⊢ (¬
𝑊 ∈ V → (
·sf ‘𝑊) = (𝑥 ∈ ∅, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦))) |
40 | | fvprc 6185 |
. . . . . . . . 9
⊢ (¬
𝑊 ∈ V →
(Scalar‘𝑊) =
∅) |
41 | 3, 40 | syl5eq 2668 |
. . . . . . . 8
⊢ (¬
𝑊 ∈ V → 𝐹 = ∅) |
42 | 41 | fveq2d 6195 |
. . . . . . 7
⊢ (¬
𝑊 ∈ V →
(Base‘𝐹) =
(Base‘∅)) |
43 | 6, 42 | syl5eq 2668 |
. . . . . 6
⊢ (¬
𝑊 ∈ V → 𝐾 =
(Base‘∅)) |
44 | | base0 15912 |
. . . . . 6
⊢ ∅ =
(Base‘∅) |
45 | 43, 44 | syl6eqr 2674 |
. . . . 5
⊢ (¬
𝑊 ∈ V → 𝐾 = ∅) |
46 | | eqid 2622 |
. . . . 5
⊢ 𝐵 = 𝐵 |
47 | | mpt2eq12 6715 |
. . . . 5
⊢ ((𝐾 = ∅ ∧ 𝐵 = 𝐵) → (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦)) = (𝑥 ∈ ∅, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦))) |
48 | 45, 46, 47 | sylancl 694 |
. . . 4
⊢ (¬
𝑊 ∈ V → (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦)) = (𝑥 ∈ ∅, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦))) |
49 | 39, 48 | eqtr4d 2659 |
. . 3
⊢ (¬
𝑊 ∈ V → (
·sf ‘𝑊) = (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦))) |
50 | 36, 49 | pm2.61i 176 |
. 2
⊢ (
·sf ‘𝑊) = (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦)) |
51 | 1, 50 | eqtri 2644 |
1
⊢ ∙ =
(𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦)) |