Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lflvscl Structured version   Visualization version   GIF version

Theorem lflvscl 39033
Description: Closure of a scalar product with a functional. Note that this is the scalar product for a right vector space with the scalar after the vector; reversing these fails closure. (Contributed by NM, 9-Oct-2014.) (Revised by Mario Carneiro, 22-Apr-2015.)
Hypotheses
Ref Expression
lflsccl.v 𝑉 = (Base‘𝑊)
lflsccl.d 𝐷 = (Scalar‘𝑊)
lflsccl.k 𝐾 = (Base‘𝐷)
lflsccl.t · = (.r𝐷)
lflsccl.f 𝐹 = (LFnl‘𝑊)
lflsccl.w (𝜑𝑊 ∈ LMod)
lflsccl.g (𝜑𝐺𝐹)
lflsccl.r (𝜑𝑅𝐾)
Assertion
Ref Expression
lflvscl (𝜑 → (𝐺f · (𝑉 × {𝑅})) ∈ 𝐹)

Proof of Theorem lflvscl
Dummy variables 𝑥 𝑟 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lflsccl.v . . 3 𝑉 = (Base‘𝑊)
21a1i 11 . 2 (𝜑𝑉 = (Base‘𝑊))
3 eqidd 2741 . 2 (𝜑 → (+g𝑊) = (+g𝑊))
4 lflsccl.d . . 3 𝐷 = (Scalar‘𝑊)
54a1i 11 . 2 (𝜑𝐷 = (Scalar‘𝑊))
6 eqidd 2741 . 2 (𝜑 → ( ·𝑠𝑊) = ( ·𝑠𝑊))
7 lflsccl.k . . 3 𝐾 = (Base‘𝐷)
87a1i 11 . 2 (𝜑𝐾 = (Base‘𝐷))
9 eqidd 2741 . 2 (𝜑 → (+g𝐷) = (+g𝐷))
10 lflsccl.t . . 3 · = (.r𝐷)
1110a1i 11 . 2 (𝜑· = (.r𝐷))
12 lflsccl.f . . 3 𝐹 = (LFnl‘𝑊)
1312a1i 11 . 2 (𝜑𝐹 = (LFnl‘𝑊))
14 lflsccl.w . . . . 5 (𝜑𝑊 ∈ LMod)
154lmodring 20888 . . . . 5 (𝑊 ∈ LMod → 𝐷 ∈ Ring)
1614, 15syl 17 . . . 4 (𝜑𝐷 ∈ Ring)
177, 10ringcl 20277 . . . . 5 ((𝐷 ∈ Ring ∧ 𝑥𝐾𝑦𝐾) → (𝑥 · 𝑦) ∈ 𝐾)
18173expb 1120 . . . 4 ((𝐷 ∈ Ring ∧ (𝑥𝐾𝑦𝐾)) → (𝑥 · 𝑦) ∈ 𝐾)
1916, 18sylan 579 . . 3 ((𝜑 ∧ (𝑥𝐾𝑦𝐾)) → (𝑥 · 𝑦) ∈ 𝐾)
20 lflsccl.g . . . 4 (𝜑𝐺𝐹)
214, 7, 1, 12lflf 39019 . . . 4 ((𝑊 ∈ LMod ∧ 𝐺𝐹) → 𝐺:𝑉𝐾)
2214, 20, 21syl2anc 583 . . 3 (𝜑𝐺:𝑉𝐾)
23 lflsccl.r . . . 4 (𝜑𝑅𝐾)
24 fconst6g 6810 . . . 4 (𝑅𝐾 → (𝑉 × {𝑅}):𝑉𝐾)
2523, 24syl 17 . . 3 (𝜑 → (𝑉 × {𝑅}):𝑉𝐾)
261fvexi 6934 . . . 4 𝑉 ∈ V
2726a1i 11 . . 3 (𝜑𝑉 ∈ V)
28 inidm 4248 . . 3 (𝑉𝑉) = 𝑉
2919, 22, 25, 27, 27, 28off 7732 . 2 (𝜑 → (𝐺f · (𝑉 × {𝑅})):𝑉𝐾)
3014adantr 480 . . . . . 6 ((𝜑 ∧ (𝑟𝐾𝑥𝑉𝑦𝑉)) → 𝑊 ∈ LMod)
3120adantr 480 . . . . . 6 ((𝜑 ∧ (𝑟𝐾𝑥𝑉𝑦𝑉)) → 𝐺𝐹)
32 simpr1 1194 . . . . . 6 ((𝜑 ∧ (𝑟𝐾𝑥𝑉𝑦𝑉)) → 𝑟𝐾)
33 simpr2 1195 . . . . . 6 ((𝜑 ∧ (𝑟𝐾𝑥𝑉𝑦𝑉)) → 𝑥𝑉)
34 simpr3 1196 . . . . . 6 ((𝜑 ∧ (𝑟𝐾𝑥𝑉𝑦𝑉)) → 𝑦𝑉)
35 eqid 2740 . . . . . . 7 (+g𝑊) = (+g𝑊)
36 eqid 2740 . . . . . . 7 ( ·𝑠𝑊) = ( ·𝑠𝑊)
37 eqid 2740 . . . . . . 7 (+g𝐷) = (+g𝐷)
381, 35, 4, 36, 7, 37, 10, 12lfli 39017 . . . . . 6 ((𝑊 ∈ LMod ∧ 𝐺𝐹 ∧ (𝑟𝐾𝑥𝑉𝑦𝑉)) → (𝐺‘((𝑟( ·𝑠𝑊)𝑥)(+g𝑊)𝑦)) = ((𝑟 · (𝐺𝑥))(+g𝐷)(𝐺𝑦)))
3930, 31, 32, 33, 34, 38syl113anc 1382 . . . . 5 ((𝜑 ∧ (𝑟𝐾𝑥𝑉𝑦𝑉)) → (𝐺‘((𝑟( ·𝑠𝑊)𝑥)(+g𝑊)𝑦)) = ((𝑟 · (𝐺𝑥))(+g𝐷)(𝐺𝑦)))
4039oveq1d 7463 . . . 4 ((𝜑 ∧ (𝑟𝐾𝑥𝑉𝑦𝑉)) → ((𝐺‘((𝑟( ·𝑠𝑊)𝑥)(+g𝑊)𝑦)) · 𝑅) = (((𝑟 · (𝐺𝑥))(+g𝐷)(𝐺𝑦)) · 𝑅))
4116adantr 480 . . . . 5 ((𝜑 ∧ (𝑟𝐾𝑥𝑉𝑦𝑉)) → 𝐷 ∈ Ring)
424, 7, 1, 12lflcl 39020 . . . . . . 7 ((𝑊 ∈ LMod ∧ 𝐺𝐹𝑥𝑉) → (𝐺𝑥) ∈ 𝐾)
4330, 31, 33, 42syl3anc 1371 . . . . . 6 ((𝜑 ∧ (𝑟𝐾𝑥𝑉𝑦𝑉)) → (𝐺𝑥) ∈ 𝐾)
447, 10ringcl 20277 . . . . . 6 ((𝐷 ∈ Ring ∧ 𝑟𝐾 ∧ (𝐺𝑥) ∈ 𝐾) → (𝑟 · (𝐺𝑥)) ∈ 𝐾)
4541, 32, 43, 44syl3anc 1371 . . . . 5 ((𝜑 ∧ (𝑟𝐾𝑥𝑉𝑦𝑉)) → (𝑟 · (𝐺𝑥)) ∈ 𝐾)
464, 7, 1, 12lflcl 39020 . . . . . 6 ((𝑊 ∈ LMod ∧ 𝐺𝐹𝑦𝑉) → (𝐺𝑦) ∈ 𝐾)
4730, 31, 34, 46syl3anc 1371 . . . . 5 ((𝜑 ∧ (𝑟𝐾𝑥𝑉𝑦𝑉)) → (𝐺𝑦) ∈ 𝐾)
4823adantr 480 . . . . 5 ((𝜑 ∧ (𝑟𝐾𝑥𝑉𝑦𝑉)) → 𝑅𝐾)
497, 37, 10ringdir 20288 . . . . 5 ((𝐷 ∈ Ring ∧ ((𝑟 · (𝐺𝑥)) ∈ 𝐾 ∧ (𝐺𝑦) ∈ 𝐾𝑅𝐾)) → (((𝑟 · (𝐺𝑥))(+g𝐷)(𝐺𝑦)) · 𝑅) = (((𝑟 · (𝐺𝑥)) · 𝑅)(+g𝐷)((𝐺𝑦) · 𝑅)))
5041, 45, 47, 48, 49syl13anc 1372 . . . 4 ((𝜑 ∧ (𝑟𝐾𝑥𝑉𝑦𝑉)) → (((𝑟 · (𝐺𝑥))(+g𝐷)(𝐺𝑦)) · 𝑅) = (((𝑟 · (𝐺𝑥)) · 𝑅)(+g𝐷)((𝐺𝑦) · 𝑅)))
517, 10ringass 20280 . . . . . 6 ((𝐷 ∈ Ring ∧ (𝑟𝐾 ∧ (𝐺𝑥) ∈ 𝐾𝑅𝐾)) → ((𝑟 · (𝐺𝑥)) · 𝑅) = (𝑟 · ((𝐺𝑥) · 𝑅)))
5241, 32, 43, 48, 51syl13anc 1372 . . . . 5 ((𝜑 ∧ (𝑟𝐾𝑥𝑉𝑦𝑉)) → ((𝑟 · (𝐺𝑥)) · 𝑅) = (𝑟 · ((𝐺𝑥) · 𝑅)))
5352oveq1d 7463 . . . 4 ((𝜑 ∧ (𝑟𝐾𝑥𝑉𝑦𝑉)) → (((𝑟 · (𝐺𝑥)) · 𝑅)(+g𝐷)((𝐺𝑦) · 𝑅)) = ((𝑟 · ((𝐺𝑥) · 𝑅))(+g𝐷)((𝐺𝑦) · 𝑅)))
5440, 50, 533eqtrd 2784 . . 3 ((𝜑 ∧ (𝑟𝐾𝑥𝑉𝑦𝑉)) → ((𝐺‘((𝑟( ·𝑠𝑊)𝑥)(+g𝑊)𝑦)) · 𝑅) = ((𝑟 · ((𝐺𝑥) · 𝑅))(+g𝐷)((𝐺𝑦) · 𝑅)))
551, 4, 36, 7lmodvscl 20898 . . . . . 6 ((𝑊 ∈ LMod ∧ 𝑟𝐾𝑥𝑉) → (𝑟( ·𝑠𝑊)𝑥) ∈ 𝑉)
5630, 32, 33, 55syl3anc 1371 . . . . 5 ((𝜑 ∧ (𝑟𝐾𝑥𝑉𝑦𝑉)) → (𝑟( ·𝑠𝑊)𝑥) ∈ 𝑉)
571, 35lmodvacl 20895 . . . . 5 ((𝑊 ∈ LMod ∧ (𝑟( ·𝑠𝑊)𝑥) ∈ 𝑉𝑦𝑉) → ((𝑟( ·𝑠𝑊)𝑥)(+g𝑊)𝑦) ∈ 𝑉)
5830, 56, 34, 57syl3anc 1371 . . . 4 ((𝜑 ∧ (𝑟𝐾𝑥𝑉𝑦𝑉)) → ((𝑟( ·𝑠𝑊)𝑥)(+g𝑊)𝑦) ∈ 𝑉)
5922ffnd 6748 . . . . 5 (𝜑𝐺 Fn 𝑉)
60 eqidd 2741 . . . . 5 ((𝜑 ∧ ((𝑟( ·𝑠𝑊)𝑥)(+g𝑊)𝑦) ∈ 𝑉) → (𝐺‘((𝑟( ·𝑠𝑊)𝑥)(+g𝑊)𝑦)) = (𝐺‘((𝑟( ·𝑠𝑊)𝑥)(+g𝑊)𝑦)))
6127, 23, 59, 60ofc2 7742 . . . 4 ((𝜑 ∧ ((𝑟( ·𝑠𝑊)𝑥)(+g𝑊)𝑦) ∈ 𝑉) → ((𝐺f · (𝑉 × {𝑅}))‘((𝑟( ·𝑠𝑊)𝑥)(+g𝑊)𝑦)) = ((𝐺‘((𝑟( ·𝑠𝑊)𝑥)(+g𝑊)𝑦)) · 𝑅))
6258, 61syldan 590 . . 3 ((𝜑 ∧ (𝑟𝐾𝑥𝑉𝑦𝑉)) → ((𝐺f · (𝑉 × {𝑅}))‘((𝑟( ·𝑠𝑊)𝑥)(+g𝑊)𝑦)) = ((𝐺‘((𝑟( ·𝑠𝑊)𝑥)(+g𝑊)𝑦)) · 𝑅))
63 eqidd 2741 . . . . . . 7 ((𝜑𝑥𝑉) → (𝐺𝑥) = (𝐺𝑥))
6427, 23, 59, 63ofc2 7742 . . . . . 6 ((𝜑𝑥𝑉) → ((𝐺f · (𝑉 × {𝑅}))‘𝑥) = ((𝐺𝑥) · 𝑅))
6533, 64syldan 590 . . . . 5 ((𝜑 ∧ (𝑟𝐾𝑥𝑉𝑦𝑉)) → ((𝐺f · (𝑉 × {𝑅}))‘𝑥) = ((𝐺𝑥) · 𝑅))
6665oveq2d 7464 . . . 4 ((𝜑 ∧ (𝑟𝐾𝑥𝑉𝑦𝑉)) → (𝑟 · ((𝐺f · (𝑉 × {𝑅}))‘𝑥)) = (𝑟 · ((𝐺𝑥) · 𝑅)))
67 eqidd 2741 . . . . . 6 ((𝜑𝑦𝑉) → (𝐺𝑦) = (𝐺𝑦))
6827, 23, 59, 67ofc2 7742 . . . . 5 ((𝜑𝑦𝑉) → ((𝐺f · (𝑉 × {𝑅}))‘𝑦) = ((𝐺𝑦) · 𝑅))
6934, 68syldan 590 . . . 4 ((𝜑 ∧ (𝑟𝐾𝑥𝑉𝑦𝑉)) → ((𝐺f · (𝑉 × {𝑅}))‘𝑦) = ((𝐺𝑦) · 𝑅))
7066, 69oveq12d 7466 . . 3 ((𝜑 ∧ (𝑟𝐾𝑥𝑉𝑦𝑉)) → ((𝑟 · ((𝐺f · (𝑉 × {𝑅}))‘𝑥))(+g𝐷)((𝐺f · (𝑉 × {𝑅}))‘𝑦)) = ((𝑟 · ((𝐺𝑥) · 𝑅))(+g𝐷)((𝐺𝑦) · 𝑅)))
7154, 62, 703eqtr4d 2790 . 2 ((𝜑 ∧ (𝑟𝐾𝑥𝑉𝑦𝑉)) → ((𝐺f · (𝑉 × {𝑅}))‘((𝑟( ·𝑠𝑊)𝑥)(+g𝑊)𝑦)) = ((𝑟 · ((𝐺f · (𝑉 × {𝑅}))‘𝑥))(+g𝐷)((𝐺f · (𝑉 × {𝑅}))‘𝑦)))
722, 3, 5, 6, 8, 9, 11, 13, 29, 71, 14islfld 39018 1 (𝜑 → (𝐺f · (𝑉 × {𝑅})) ∈ 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087   = wceq 1537  wcel 2108  Vcvv 3488  {csn 4648   × cxp 5698  wf 6569  cfv 6573  (class class class)co 7448  f cof 7712  Basecbs 17258  +gcplusg 17311  .rcmulr 17312  Scalarcsca 17314   ·𝑠 cvsca 17315  Ringcrg 20260  LModclmod 20880  LFnlclfn 39013
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-of 7714  df-om 7904  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-er 8763  df-map 8886  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-nn 12294  df-2 12356  df-sets 17211  df-slot 17229  df-ndx 17241  df-base 17259  df-plusg 17324  df-mgm 18678  df-sgrp 18757  df-mnd 18773  df-grp 18976  df-mgp 20162  df-ring 20262  df-lmod 20882  df-lfl 39014
This theorem is referenced by:  lkrsc  39053  lfl1dim  39077  ldualvscl  39095  ldualvsass  39097
  Copyright terms: Public domain W3C validator