Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  scaffval Structured version   Visualization version   GIF version

Theorem scaffval 19368
 Description: The scalar multiplication operation as a function. (Contributed by Mario Carneiro, 5-Oct-2015.)
Hypotheses
Ref Expression
scaffval.b 𝐵 = (Base‘𝑊)
scaffval.f 𝐹 = (Scalar‘𝑊)
scaffval.k 𝐾 = (Base‘𝐹)
scaffval.a = ( ·sf𝑊)
scaffval.s · = ( ·𝑠𝑊)
Assertion
Ref Expression
scaffval = (𝑥𝐾, 𝑦𝐵 ↦ (𝑥 · 𝑦))
Distinct variable groups:   𝑥,𝑦,𝐵   𝑥,𝐾,𝑦   𝑥, · ,𝑦   𝑥,𝑊,𝑦
Allowed substitution hints:   (𝑥,𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem scaffval
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 scaffval.a . 2 = ( ·sf𝑊)
2 fveq2 6493 . . . . . . . 8 (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊))
3 scaffval.f . . . . . . . 8 𝐹 = (Scalar‘𝑊)
42, 3syl6eqr 2826 . . . . . . 7 (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝐹)
54fveq2d 6497 . . . . . 6 (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = (Base‘𝐹))
6 scaffval.k . . . . . 6 𝐾 = (Base‘𝐹)
75, 6syl6eqr 2826 . . . . 5 (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = 𝐾)
8 fveq2 6493 . . . . . 6 (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊))
9 scaffval.b . . . . . 6 𝐵 = (Base‘𝑊)
108, 9syl6eqr 2826 . . . . 5 (𝑤 = 𝑊 → (Base‘𝑤) = 𝐵)
11 fveq2 6493 . . . . . . 7 (𝑤 = 𝑊 → ( ·𝑠𝑤) = ( ·𝑠𝑊))
12 scaffval.s . . . . . . 7 · = ( ·𝑠𝑊)
1311, 12syl6eqr 2826 . . . . . 6 (𝑤 = 𝑊 → ( ·𝑠𝑤) = · )
1413oveqd 6987 . . . . 5 (𝑤 = 𝑊 → (𝑥( ·𝑠𝑤)𝑦) = (𝑥 · 𝑦))
157, 10, 14mpoeq123dv 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 · ∪ {∅})
1917, 18eqeltri 2856 . . . . . . 7 (𝑥 · 𝑦) ∈ (ran · ∪ {∅})
2019rgen2w 3095 . . . . . 6 𝑥𝐾𝑦𝐵 (𝑥 · 𝑦) ∈ (ran · ∪ {∅})
21 eqid 2772 . . . . . . 7 (𝑥𝐾, 𝑦𝐵 ↦ (𝑥 · 𝑦)) = (𝑥𝐾, 𝑦𝐵 ↦ (𝑥 · 𝑦))
2221fmpo 7568 . . . . . 6 (∀𝑥𝐾𝑦𝐵 (𝑥 · 𝑦) ∈ (ran · ∪ {∅}) ↔ (𝑥𝐾, 𝑦𝐵 ↦ (𝑥 · 𝑦)):(𝐾 × 𝐵)⟶(ran · ∪ {∅}))
2320, 22mpbi 222 . . . . 5 (𝑥𝐾, 𝑦𝐵 ↦ (𝑥 · 𝑦)):(𝐾 × 𝐵)⟶(ran · ∪ {∅})
246fvexi 6507 . . . . . 6 𝐾 ∈ V
259fvexi 6507 . . . . . 6 𝐵 ∈ V
2624, 25xpex 7287 . . . . 5 (𝐾 × 𝐵) ∈ V
2712fvexi 6507 . . . . . . 7 · ∈ V
2827rnex 7426 . . . . . 6 ran · ∈ V
29 p0ex 5131 . . . . . 6 {∅} ∈ V
3028, 29unex 7280 . . . . 5 (ran · ∪ {∅}) ∈ V
31 fex2 7447 . . . . 5 (((𝑥𝐾, 𝑦𝐵 ↦ (𝑥 · 𝑦)):(𝐾 × 𝐵)⟶(ran · ∪ {∅}) ∧ (𝐾 × 𝐵) ∈ V ∧ (ran · ∪ {∅}) ∈ V) → (𝑥𝐾, 𝑦𝐵 ↦ (𝑥 · 𝑦)) ∈ V)
3223, 26, 30, 31mp3an 1440 . . . 4 (𝑥𝐾, 𝑦𝐵 ↦ (𝑥 · 𝑦)) ∈ V
3315, 16, 32fvmpt 6589 . . 3 (𝑊 ∈ V → ( ·sf𝑊) = (𝑥𝐾, 𝑦𝐵 ↦ (𝑥 · 𝑦)))
34 fvprc 6486 . . . . 5 𝑊 ∈ V → ( ·sf𝑊) = ∅)
35 mpo0 7049 . . . . 5 (𝑥 ∈ ∅, 𝑦𝐵 ↦ (𝑥 · 𝑦)) = ∅
3634, 35syl6eqr 2826 . . . 4 𝑊 ∈ V → ( ·sf𝑊) = (𝑥 ∈ ∅, 𝑦𝐵 ↦ (𝑥 · 𝑦)))
37 fvprc 6486 . . . . . . . . 9 𝑊 ∈ V → (Scalar‘𝑊) = ∅)
383, 37syl5eq 2820 . . . . . . . 8 𝑊 ∈ V → 𝐹 = ∅)
3938fveq2d 6497 . . . . . . 7 𝑊 ∈ V → (Base‘𝐹) = (Base‘∅))
406, 39syl5eq 2820 . . . . . 6 𝑊 ∈ V → 𝐾 = (Base‘∅))
41 base0 16386 . . . . . 6 ∅ = (Base‘∅)
4240, 41syl6eqr 2826 . . . . 5 𝑊 ∈ V → 𝐾 = ∅)
43 eqid 2772 . . . . 5 𝐵 = 𝐵
44 mpoeq12 7039 . . . . 5 ((𝐾 = ∅ ∧ 𝐵 = 𝐵) → (𝑥𝐾, 𝑦𝐵 ↦ (𝑥 · 𝑦)) = (𝑥 ∈ ∅, 𝑦𝐵 ↦ (𝑥 · 𝑦)))
4542, 43, 44sylancl 577 . . . 4 𝑊 ∈ V → (𝑥𝐾, 𝑦𝐵 ↦ (𝑥 · 𝑦)) = (𝑥 ∈ ∅, 𝑦𝐵 ↦ (𝑥 · 𝑦)))
4636, 45eqtr4d 2811 . . 3 𝑊 ∈ V → ( ·sf𝑊) = (𝑥𝐾, 𝑦𝐵 ↦ (𝑥 · 𝑦)))
4733, 46pm2.61i 177 . 2 ( ·sf𝑊) = (𝑥𝐾, 𝑦𝐵 ↦ (𝑥 · 𝑦))
481, 47eqtri 2796 1 = (𝑥𝐾, 𝑦𝐵 ↦ (𝑥 · 𝑦))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   = wceq 1507   ∈ wcel 2050  ∀wral 3082  Vcvv 3409   ∪ cun 3821  ∅c0 4172  {csn 4435  ⟨cop 4441   × cxp 5399  ran crn 5402  ⟶wf 6178  ‘cfv 6182  (class class class)co 6970   ∈ cmpo 6972  Basecbs 16333  Scalarcsca 16418   ·𝑠 cvsca 16419   ·sf cscaf 19351 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2744  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-ral 3087  df-rex 3088  df-rab 3091  df-v 3411  df-sbc 3676  df-csb 3781  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4707  df-iun 4788  df-br 4924  df-opab 4986  df-mpt 5003  df-id 5306  df-xp 5407  df-rel 5408  df-cnv 5409  df-co 5410  df-dm 5411  df-rn 5412  df-res 5413  df-ima 5414  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-fv 6190  df-ov 6973  df-oprab 6974  df-mpo 6975  df-1st 7495  df-2nd 7496  df-slot 16337  df-base 16339  df-scaf 19353 This theorem is referenced by:  scafval  19369  scafeq  19370  scaffn  19371  lmodscaf  19372  rlmscaf  19696
 Copyright terms: Public domain W3C validator