![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > islvec | Structured version Visualization version GIF version |
Description: The predicate "is a left vector space". (Contributed by NM, 11-Nov-2013.) |
Ref | Expression |
---|---|
islvec.1 | ⊢ 𝐹 = (Scalar‘𝑊) |
Ref | Expression |
---|---|
islvec | ⊢ (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fveq2 6888 | . . . 4 ⊢ (𝑓 = 𝑊 → (Scalar‘𝑓) = (Scalar‘𝑊)) | |
2 | islvec.1 | . . . 4 ⊢ 𝐹 = (Scalar‘𝑊) | |
3 | 1, 2 | eqtr4di 2791 | . . 3 ⊢ (𝑓 = 𝑊 → (Scalar‘𝑓) = 𝐹) |
4 | 3 | eleq1d 2819 | . 2 ⊢ (𝑓 = 𝑊 → ((Scalar‘𝑓) ∈ DivRing ↔ 𝐹 ∈ DivRing)) |
5 | df-lvec 20702 | . 2 ⊢ LVec = {𝑓 ∈ LMod ∣ (Scalar‘𝑓) ∈ DivRing} | |
6 | 4, 5 | elrab2 3685 | 1 ⊢ (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ‘cfv 6540 Scalarcsca 17196 DivRingcdr 20304 LModclmod 20459 LVecclvec 20701 |
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-ext 2704 |
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-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3434 df-v 3477 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-iota 6492 df-fv 6548 df-lvec 20702 |
This theorem is referenced by: lvecdrng 20704 lveclmod 20705 lsslvec 20707 lmhmlvec 20708 lvecprop2d 20767 lvecpropd 20768 rlmlvec 20815 frlmlvec 21300 frlmphl 21320 mpllvec 21561 tvclvec 23685 isnvc2 24198 iscvs 24625 cnstrcvs 24639 zclmncvs 24647 quslvec 32440 ply1lvec 32590 sralvec 32621 matdim 32645 lmhmlvec2 32649 ccfldsrarelvec 32690 bj-isvec 36106 lindsdom 36420 lindsenlbs 36421 lduallvec 37962 dvalveclem 39834 dvhlveclem 39917 lmod1zrnlvec 47077 aacllem 47750 |
Copyright terms: Public domain | W3C validator |