Step | Hyp | Ref
| Expression |
1 | | imasvscaf.u |
. . . . . . 7
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) |
2 | | imasvscaf.v |
. . . . . . 7
⊢ (𝜑 → 𝑉 = (Base‘𝑅)) |
3 | | imasvscaf.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) |
4 | | imasvscaf.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ 𝑍) |
5 | | imasvscaf.g |
. . . . . . 7
⊢ 𝐺 = (Scalar‘𝑅) |
6 | | imasvscaf.k |
. . . . . . 7
⊢ 𝐾 = (Base‘𝐺) |
7 | | imasvscaf.q |
. . . . . . 7
⊢ · = (
·𝑠 ‘𝑅) |
8 | | imasvscaf.s |
. . . . . . 7
⊢ ∙ = (
·𝑠 ‘𝑈) |
9 | | imasvscaf.e |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘𝑎) = (𝐹‘𝑞) → (𝐹‘(𝑝 · 𝑎)) = (𝐹‘(𝑝 · 𝑞)))) |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | imasvscafn 17229 |
. . . . . 6
⊢ (𝜑 → ∙ Fn (𝐾 × 𝐵)) |
11 | | fnfun 6529 |
. . . . . 6
⊢ ( ∙ Fn
(𝐾 × 𝐵) → Fun ∙ ) |
12 | 10, 11 | syl 17 |
. . . . 5
⊢ (𝜑 → Fun ∙ ) |
13 | 12 | 3ad2ant1 1131 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → Fun ∙ ) |
14 | | eqidd 2740 |
. . . . . . . 8
⊢ (𝑞 = 𝑌 → 𝐾 = 𝐾) |
15 | | fveq2 6768 |
. . . . . . . . 9
⊢ (𝑞 = 𝑌 → (𝐹‘𝑞) = (𝐹‘𝑌)) |
16 | 15 | sneqd 4578 |
. . . . . . . 8
⊢ (𝑞 = 𝑌 → {(𝐹‘𝑞)} = {(𝐹‘𝑌)}) |
17 | | oveq2 7276 |
. . . . . . . . 9
⊢ (𝑞 = 𝑌 → (𝑝 · 𝑞) = (𝑝 · 𝑌)) |
18 | 17 | fveq2d 6772 |
. . . . . . . 8
⊢ (𝑞 = 𝑌 → (𝐹‘(𝑝 · 𝑞)) = (𝐹‘(𝑝 · 𝑌))) |
19 | 14, 16, 18 | mpoeq123dv 7341 |
. . . . . . 7
⊢ (𝑞 = 𝑌 → (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))) = (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑌)} ↦ (𝐹‘(𝑝 · 𝑌)))) |
20 | 19 | ssiun2s 4982 |
. . . . . 6
⊢ (𝑌 ∈ 𝑉 → (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑌)} ↦ (𝐹‘(𝑝 · 𝑌))) ⊆ ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))) |
21 | 20 | 3ad2ant3 1133 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑌)} ↦ (𝐹‘(𝑝 · 𝑌))) ⊆ ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))) |
22 | 1, 2, 3, 4, 5, 6, 7, 8 | imasvsca 17212 |
. . . . . 6
⊢ (𝜑 → ∙ = ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))) |
23 | 22 | 3ad2ant1 1131 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → ∙ = ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞)))) |
24 | 21, 23 | sseqtrrd 3966 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑌)} ↦ (𝐹‘(𝑝 · 𝑌))) ⊆ ∙ ) |
25 | | simp2 1135 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → 𝑋 ∈ 𝐾) |
26 | | fvex 6781 |
. . . . . . 7
⊢ (𝐹‘𝑌) ∈ V |
27 | 26 | snid 4602 |
. . . . . 6
⊢ (𝐹‘𝑌) ∈ {(𝐹‘𝑌)} |
28 | | opelxpi 5625 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐾 ∧ (𝐹‘𝑌) ∈ {(𝐹‘𝑌)}) → 〈𝑋, (𝐹‘𝑌)〉 ∈ (𝐾 × {(𝐹‘𝑌)})) |
29 | 25, 27, 28 | sylancl 585 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → 〈𝑋, (𝐹‘𝑌)〉 ∈ (𝐾 × {(𝐹‘𝑌)})) |
30 | | eqid 2739 |
. . . . . 6
⊢ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑌)} ↦ (𝐹‘(𝑝 · 𝑌))) = (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑌)} ↦ (𝐹‘(𝑝 · 𝑌))) |
31 | | fvex 6781 |
. . . . . 6
⊢ (𝐹‘(𝑝 · 𝑌)) ∈ V |
32 | 30, 31 | dmmpo 7897 |
. . . . 5
⊢ dom
(𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑌)} ↦ (𝐹‘(𝑝 · 𝑌))) = (𝐾 × {(𝐹‘𝑌)}) |
33 | 29, 32 | eleqtrrdi 2851 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → 〈𝑋, (𝐹‘𝑌)〉 ∈ dom (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑌)} ↦ (𝐹‘(𝑝 · 𝑌)))) |
34 | | funssfv 6789 |
. . . 4
⊢ ((Fun
∙
∧ (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑌)} ↦ (𝐹‘(𝑝 · 𝑌))) ⊆ ∙ ∧ 〈𝑋, (𝐹‘𝑌)〉 ∈ dom (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑌)} ↦ (𝐹‘(𝑝 · 𝑌)))) → ( ∙ ‘〈𝑋, (𝐹‘𝑌)〉) = ((𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑌)} ↦ (𝐹‘(𝑝 · 𝑌)))‘〈𝑋, (𝐹‘𝑌)〉)) |
35 | 13, 24, 33, 34 | syl3anc 1369 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → ( ∙ ‘〈𝑋, (𝐹‘𝑌)〉) = ((𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑌)} ↦ (𝐹‘(𝑝 · 𝑌)))‘〈𝑋, (𝐹‘𝑌)〉)) |
36 | | df-ov 7271 |
. . 3
⊢ (𝑋 ∙ (𝐹‘𝑌)) = ( ∙ ‘〈𝑋, (𝐹‘𝑌)〉) |
37 | | df-ov 7271 |
. . 3
⊢ (𝑋(𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑌)} ↦ (𝐹‘(𝑝 · 𝑌)))(𝐹‘𝑌)) = ((𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑌)} ↦ (𝐹‘(𝑝 · 𝑌)))‘〈𝑋, (𝐹‘𝑌)〉) |
38 | 35, 36, 37 | 3eqtr4g 2804 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → (𝑋 ∙ (𝐹‘𝑌)) = (𝑋(𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑌)} ↦ (𝐹‘(𝑝 · 𝑌)))(𝐹‘𝑌))) |
39 | | fvoveq1 7291 |
. . . 4
⊢ (𝑝 = 𝑋 → (𝐹‘(𝑝 · 𝑌)) = (𝐹‘(𝑋 · 𝑌))) |
40 | | eqidd 2740 |
. . . 4
⊢ (𝑥 = (𝐹‘𝑌) → (𝐹‘(𝑋 · 𝑌)) = (𝐹‘(𝑋 · 𝑌))) |
41 | | fvex 6781 |
. . . 4
⊢ (𝐹‘(𝑋 · 𝑌)) ∈ V |
42 | 39, 40, 30, 41 | ovmpo 7424 |
. . 3
⊢ ((𝑋 ∈ 𝐾 ∧ (𝐹‘𝑌) ∈ {(𝐹‘𝑌)}) → (𝑋(𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑌)} ↦ (𝐹‘(𝑝 · 𝑌)))(𝐹‘𝑌)) = (𝐹‘(𝑋 · 𝑌))) |
43 | 25, 27, 42 | sylancl 585 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → (𝑋(𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑌)} ↦ (𝐹‘(𝑝 · 𝑌)))(𝐹‘𝑌)) = (𝐹‘(𝑋 · 𝑌))) |
44 | 38, 43 | eqtrd 2779 |
1
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → (𝑋 ∙ (𝐹‘𝑌)) = (𝐹‘(𝑋 · 𝑌))) |