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

Theorem islfl 37572
Description: The predicate "is a linear functional". (Contributed by NM, 15-Apr-2014.)
Hypotheses
Ref Expression
lflset.v 𝑉 = (Baseβ€˜π‘Š)
lflset.a + = (+gβ€˜π‘Š)
lflset.d 𝐷 = (Scalarβ€˜π‘Š)
lflset.s Β· = ( ·𝑠 β€˜π‘Š)
lflset.k 𝐾 = (Baseβ€˜π·)
lflset.p ⨣ = (+gβ€˜π·)
lflset.t Γ— = (.rβ€˜π·)
lflset.f 𝐹 = (LFnlβ€˜π‘Š)
Assertion
Ref Expression
islfl (π‘Š ∈ 𝑋 β†’ (𝐺 ∈ 𝐹 ↔ (𝐺:π‘‰βŸΆπΎ ∧ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘¦ ∈ 𝑉 (πΊβ€˜((π‘Ÿ Β· π‘₯) + 𝑦)) = ((π‘Ÿ Γ— (πΊβ€˜π‘₯)) ⨣ (πΊβ€˜π‘¦)))))
Distinct variable groups:   𝐾,π‘Ÿ   π‘₯,𝑦,𝑉   π‘₯,π‘Ÿ,𝑦,π‘Š   𝐺,π‘Ÿ,π‘₯,𝑦
Allowed substitution hints:   𝐷(π‘₯,𝑦,π‘Ÿ)   + (π‘₯,𝑦,π‘Ÿ)   ⨣ (π‘₯,𝑦,π‘Ÿ)   Β· (π‘₯,𝑦,π‘Ÿ)   Γ— (π‘₯,𝑦,π‘Ÿ)   𝐹(π‘₯,𝑦,π‘Ÿ)   𝐾(π‘₯,𝑦)   𝑉(π‘Ÿ)   𝑋(π‘₯,𝑦,π‘Ÿ)

Proof of Theorem islfl
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 lflset.v . . . 4 𝑉 = (Baseβ€˜π‘Š)
2 lflset.a . . . 4 + = (+gβ€˜π‘Š)
3 lflset.d . . . 4 𝐷 = (Scalarβ€˜π‘Š)
4 lflset.s . . . 4 Β· = ( ·𝑠 β€˜π‘Š)
5 lflset.k . . . 4 𝐾 = (Baseβ€˜π·)
6 lflset.p . . . 4 ⨣ = (+gβ€˜π·)
7 lflset.t . . . 4 Γ— = (.rβ€˜π·)
8 lflset.f . . . 4 𝐹 = (LFnlβ€˜π‘Š)
91, 2, 3, 4, 5, 6, 7, 8lflset 37571 . . 3 (π‘Š ∈ 𝑋 β†’ 𝐹 = {𝑓 ∈ (𝐾 ↑m 𝑉) ∣ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘¦ ∈ 𝑉 (π‘“β€˜((π‘Ÿ Β· π‘₯) + 𝑦)) = ((π‘Ÿ Γ— (π‘“β€˜π‘₯)) ⨣ (π‘“β€˜π‘¦))})
109eleq2d 2820 . 2 (π‘Š ∈ 𝑋 β†’ (𝐺 ∈ 𝐹 ↔ 𝐺 ∈ {𝑓 ∈ (𝐾 ↑m 𝑉) ∣ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘¦ ∈ 𝑉 (π‘“β€˜((π‘Ÿ Β· π‘₯) + 𝑦)) = ((π‘Ÿ Γ— (π‘“β€˜π‘₯)) ⨣ (π‘“β€˜π‘¦))}))
11 fveq1 6845 . . . . . . 7 (𝑓 = 𝐺 β†’ (π‘“β€˜((π‘Ÿ Β· π‘₯) + 𝑦)) = (πΊβ€˜((π‘Ÿ Β· π‘₯) + 𝑦)))
12 fveq1 6845 . . . . . . . . 9 (𝑓 = 𝐺 β†’ (π‘“β€˜π‘₯) = (πΊβ€˜π‘₯))
1312oveq2d 7377 . . . . . . . 8 (𝑓 = 𝐺 β†’ (π‘Ÿ Γ— (π‘“β€˜π‘₯)) = (π‘Ÿ Γ— (πΊβ€˜π‘₯)))
14 fveq1 6845 . . . . . . . 8 (𝑓 = 𝐺 β†’ (π‘“β€˜π‘¦) = (πΊβ€˜π‘¦))
1513, 14oveq12d 7379 . . . . . . 7 (𝑓 = 𝐺 β†’ ((π‘Ÿ Γ— (π‘“β€˜π‘₯)) ⨣ (π‘“β€˜π‘¦)) = ((π‘Ÿ Γ— (πΊβ€˜π‘₯)) ⨣ (πΊβ€˜π‘¦)))
1611, 15eqeq12d 2749 . . . . . 6 (𝑓 = 𝐺 β†’ ((π‘“β€˜((π‘Ÿ Β· π‘₯) + 𝑦)) = ((π‘Ÿ Γ— (π‘“β€˜π‘₯)) ⨣ (π‘“β€˜π‘¦)) ↔ (πΊβ€˜((π‘Ÿ Β· π‘₯) + 𝑦)) = ((π‘Ÿ Γ— (πΊβ€˜π‘₯)) ⨣ (πΊβ€˜π‘¦))))
17162ralbidv 3209 . . . . 5 (𝑓 = 𝐺 β†’ (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘¦ ∈ 𝑉 (π‘“β€˜((π‘Ÿ Β· π‘₯) + 𝑦)) = ((π‘Ÿ Γ— (π‘“β€˜π‘₯)) ⨣ (π‘“β€˜π‘¦)) ↔ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘¦ ∈ 𝑉 (πΊβ€˜((π‘Ÿ Β· π‘₯) + 𝑦)) = ((π‘Ÿ Γ— (πΊβ€˜π‘₯)) ⨣ (πΊβ€˜π‘¦))))
1817ralbidv 3171 . . . 4 (𝑓 = 𝐺 β†’ (βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘¦ ∈ 𝑉 (π‘“β€˜((π‘Ÿ Β· π‘₯) + 𝑦)) = ((π‘Ÿ Γ— (π‘“β€˜π‘₯)) ⨣ (π‘“β€˜π‘¦)) ↔ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘¦ ∈ 𝑉 (πΊβ€˜((π‘Ÿ Β· π‘₯) + 𝑦)) = ((π‘Ÿ Γ— (πΊβ€˜π‘₯)) ⨣ (πΊβ€˜π‘¦))))
1918elrab 3649 . . 3 (𝐺 ∈ {𝑓 ∈ (𝐾 ↑m 𝑉) ∣ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘¦ ∈ 𝑉 (π‘“β€˜((π‘Ÿ Β· π‘₯) + 𝑦)) = ((π‘Ÿ Γ— (π‘“β€˜π‘₯)) ⨣ (π‘“β€˜π‘¦))} ↔ (𝐺 ∈ (𝐾 ↑m 𝑉) ∧ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘¦ ∈ 𝑉 (πΊβ€˜((π‘Ÿ Β· π‘₯) + 𝑦)) = ((π‘Ÿ Γ— (πΊβ€˜π‘₯)) ⨣ (πΊβ€˜π‘¦))))
205fvexi 6860 . . . . 5 𝐾 ∈ V
211fvexi 6860 . . . . 5 𝑉 ∈ V
2220, 21elmap 8815 . . . 4 (𝐺 ∈ (𝐾 ↑m 𝑉) ↔ 𝐺:π‘‰βŸΆπΎ)
2322anbi1i 625 . . 3 ((𝐺 ∈ (𝐾 ↑m 𝑉) ∧ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘¦ ∈ 𝑉 (πΊβ€˜((π‘Ÿ Β· π‘₯) + 𝑦)) = ((π‘Ÿ Γ— (πΊβ€˜π‘₯)) ⨣ (πΊβ€˜π‘¦))) ↔ (𝐺:π‘‰βŸΆπΎ ∧ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘¦ ∈ 𝑉 (πΊβ€˜((π‘Ÿ Β· π‘₯) + 𝑦)) = ((π‘Ÿ Γ— (πΊβ€˜π‘₯)) ⨣ (πΊβ€˜π‘¦))))
2419, 23bitri 275 . 2 (𝐺 ∈ {𝑓 ∈ (𝐾 ↑m 𝑉) ∣ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘¦ ∈ 𝑉 (π‘“β€˜((π‘Ÿ Β· π‘₯) + 𝑦)) = ((π‘Ÿ Γ— (π‘“β€˜π‘₯)) ⨣ (π‘“β€˜π‘¦))} ↔ (𝐺:π‘‰βŸΆπΎ ∧ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘¦ ∈ 𝑉 (πΊβ€˜((π‘Ÿ Β· π‘₯) + 𝑦)) = ((π‘Ÿ Γ— (πΊβ€˜π‘₯)) ⨣ (πΊβ€˜π‘¦))))
2510, 24bitrdi 287 1 (π‘Š ∈ 𝑋 β†’ (𝐺 ∈ 𝐹 ↔ (𝐺:π‘‰βŸΆπΎ ∧ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘¦ ∈ 𝑉 (πΊβ€˜((π‘Ÿ Β· π‘₯) + 𝑦)) = ((π‘Ÿ Γ— (πΊβ€˜π‘₯)) ⨣ (πΊβ€˜π‘¦)))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  βˆ€wral 3061  {crab 3406  βŸΆwf 6496  β€˜cfv 6500  (class class class)co 7361   ↑m cmap 8771  Basecbs 17091  +gcplusg 17141  .rcmulr 17142  Scalarcsca 17144   ·𝑠 cvsca 17145  LFnlclfn 37569
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3449  df-sbc 3744  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-br 5110  df-opab 5172  df-mpt 5193  df-id 5535  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-ov 7364  df-oprab 7365  df-mpo 7366  df-map 8773  df-lfl 37570
This theorem is referenced by:  lfli  37573  islfld  37574  lflf  37575  lfl0f  37581  lfladdcl  37583  lflnegcl  37587  lshpkrcl  37628
  Copyright terms: Public domain W3C validator