Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > lvecpsslmod | Structured version Visualization version GIF version |
Description: The class of all (left) vector spaces is a proper subclass of the class of all (left) modules. Although it is obvious (and proven by lveclmod 20156) that every left vector space is a left module, there is (at least) one left module which is no left vector space, for example the zero module over the zero ring, see lmod1zrnlvec 45523. (Contributed by AV, 29-Apr-2019.) |
Ref | Expression |
---|---|
lvecpsslmod | ⊢ LVec ⊊ LMod |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lveclmod 20156 | . . 3 ⊢ (𝑣 ∈ LVec → 𝑣 ∈ LMod) | |
2 | 1 | ssriv 3914 | . 2 ⊢ LVec ⊆ LMod |
3 | vex 3419 | . . . 4 ⊢ 𝑖 ∈ V | |
4 | vex 3419 | . . . 4 ⊢ 𝑧 ∈ V | |
5 | 3, 4 | pm3.2i 474 | . . 3 ⊢ (𝑖 ∈ V ∧ 𝑧 ∈ V) |
6 | eqid 2738 | . . . . 5 ⊢ {〈(Base‘ndx), {𝑧}〉, 〈(+g‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉, 〈(.r‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉} = {〈(Base‘ndx), {𝑧}〉, 〈(+g‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉, 〈(.r‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉} | |
7 | eqid 2738 | . . . . 5 ⊢ ({〈(Base‘ndx), {𝑖}〉, 〈(+g‘ndx), {〈〈𝑖, 𝑖〉, 𝑖〉}〉, 〈(Scalar‘ndx), {〈(Base‘ndx), {𝑧}〉, 〈(+g‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉, 〈(.r‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉}〉} ∪ {〈( ·𝑠 ‘ndx), {〈〈𝑧, 𝑖〉, 𝑖〉}〉}) = ({〈(Base‘ndx), {𝑖}〉, 〈(+g‘ndx), {〈〈𝑖, 𝑖〉, 𝑖〉}〉, 〈(Scalar‘ndx), {〈(Base‘ndx), {𝑧}〉, 〈(+g‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉, 〈(.r‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉}〉} ∪ {〈( ·𝑠 ‘ndx), {〈〈𝑧, 𝑖〉, 𝑖〉}〉}) | |
8 | 6, 7 | lmod1zr 45522 | . . . 4 ⊢ ((𝑖 ∈ V ∧ 𝑧 ∈ V) → ({〈(Base‘ndx), {𝑖}〉, 〈(+g‘ndx), {〈〈𝑖, 𝑖〉, 𝑖〉}〉, 〈(Scalar‘ndx), {〈(Base‘ndx), {𝑧}〉, 〈(+g‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉, 〈(.r‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉}〉} ∪ {〈( ·𝑠 ‘ndx), {〈〈𝑧, 𝑖〉, 𝑖〉}〉}) ∈ LMod) |
9 | 6, 7 | lmod1zrnlvec 45523 | . . . . 5 ⊢ ((𝑖 ∈ V ∧ 𝑧 ∈ V) → ({〈(Base‘ndx), {𝑖}〉, 〈(+g‘ndx), {〈〈𝑖, 𝑖〉, 𝑖〉}〉, 〈(Scalar‘ndx), {〈(Base‘ndx), {𝑧}〉, 〈(+g‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉, 〈(.r‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉}〉} ∪ {〈( ·𝑠 ‘ndx), {〈〈𝑧, 𝑖〉, 𝑖〉}〉}) ∉ LVec) |
10 | df-nel 3048 | . . . . 5 ⊢ (({〈(Base‘ndx), {𝑖}〉, 〈(+g‘ndx), {〈〈𝑖, 𝑖〉, 𝑖〉}〉, 〈(Scalar‘ndx), {〈(Base‘ndx), {𝑧}〉, 〈(+g‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉, 〈(.r‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉}〉} ∪ {〈( ·𝑠 ‘ndx), {〈〈𝑧, 𝑖〉, 𝑖〉}〉}) ∉ LVec ↔ ¬ ({〈(Base‘ndx), {𝑖}〉, 〈(+g‘ndx), {〈〈𝑖, 𝑖〉, 𝑖〉}〉, 〈(Scalar‘ndx), {〈(Base‘ndx), {𝑧}〉, 〈(+g‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉, 〈(.r‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉}〉} ∪ {〈( ·𝑠 ‘ndx), {〈〈𝑧, 𝑖〉, 𝑖〉}〉}) ∈ LVec) | |
11 | 9, 10 | sylib 221 | . . . 4 ⊢ ((𝑖 ∈ V ∧ 𝑧 ∈ V) → ¬ ({〈(Base‘ndx), {𝑖}〉, 〈(+g‘ndx), {〈〈𝑖, 𝑖〉, 𝑖〉}〉, 〈(Scalar‘ndx), {〈(Base‘ndx), {𝑧}〉, 〈(+g‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉, 〈(.r‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉}〉} ∪ {〈( ·𝑠 ‘ndx), {〈〈𝑧, 𝑖〉, 𝑖〉}〉}) ∈ LVec) |
12 | 8, 11 | jca 515 | . . 3 ⊢ ((𝑖 ∈ V ∧ 𝑧 ∈ V) → (({〈(Base‘ndx), {𝑖}〉, 〈(+g‘ndx), {〈〈𝑖, 𝑖〉, 𝑖〉}〉, 〈(Scalar‘ndx), {〈(Base‘ndx), {𝑧}〉, 〈(+g‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉, 〈(.r‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉}〉} ∪ {〈( ·𝑠 ‘ndx), {〈〈𝑧, 𝑖〉, 𝑖〉}〉}) ∈ LMod ∧ ¬ ({〈(Base‘ndx), {𝑖}〉, 〈(+g‘ndx), {〈〈𝑖, 𝑖〉, 𝑖〉}〉, 〈(Scalar‘ndx), {〈(Base‘ndx), {𝑧}〉, 〈(+g‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉, 〈(.r‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉}〉} ∪ {〈( ·𝑠 ‘ndx), {〈〈𝑧, 𝑖〉, 𝑖〉}〉}) ∈ LVec)) |
13 | nelne1 3039 | . . . 4 ⊢ ((({〈(Base‘ndx), {𝑖}〉, 〈(+g‘ndx), {〈〈𝑖, 𝑖〉, 𝑖〉}〉, 〈(Scalar‘ndx), {〈(Base‘ndx), {𝑧}〉, 〈(+g‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉, 〈(.r‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉}〉} ∪ {〈( ·𝑠 ‘ndx), {〈〈𝑧, 𝑖〉, 𝑖〉}〉}) ∈ LMod ∧ ¬ ({〈(Base‘ndx), {𝑖}〉, 〈(+g‘ndx), {〈〈𝑖, 𝑖〉, 𝑖〉}〉, 〈(Scalar‘ndx), {〈(Base‘ndx), {𝑧}〉, 〈(+g‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉, 〈(.r‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉}〉} ∪ {〈( ·𝑠 ‘ndx), {〈〈𝑧, 𝑖〉, 𝑖〉}〉}) ∈ LVec) → LMod ≠ LVec) | |
14 | 13 | necomd 2997 | . . 3 ⊢ ((({〈(Base‘ndx), {𝑖}〉, 〈(+g‘ndx), {〈〈𝑖, 𝑖〉, 𝑖〉}〉, 〈(Scalar‘ndx), {〈(Base‘ndx), {𝑧}〉, 〈(+g‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉, 〈(.r‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉}〉} ∪ {〈( ·𝑠 ‘ndx), {〈〈𝑧, 𝑖〉, 𝑖〉}〉}) ∈ LMod ∧ ¬ ({〈(Base‘ndx), {𝑖}〉, 〈(+g‘ndx), {〈〈𝑖, 𝑖〉, 𝑖〉}〉, 〈(Scalar‘ndx), {〈(Base‘ndx), {𝑧}〉, 〈(+g‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉, 〈(.r‘ndx), {〈〈𝑧, 𝑧〉, 𝑧〉}〉}〉} ∪ {〈( ·𝑠 ‘ndx), {〈〈𝑧, 𝑖〉, 𝑖〉}〉}) ∈ LVec) → LVec ≠ LMod) |
15 | 5, 12, 14 | mp2b 10 | . 2 ⊢ LVec ≠ LMod |
16 | df-pss 3894 | . 2 ⊢ (LVec ⊊ LMod ↔ (LVec ⊆ LMod ∧ LVec ≠ LMod)) | |
17 | 2, 15, 16 | mpbir2an 711 | 1 ⊢ LVec ⊊ LMod |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 399 ∈ wcel 2111 ≠ wne 2941 ∉ wnel 3047 Vcvv 3415 ∪ cun 3873 ⊆ wss 3875 ⊊ wpss 3876 {csn 4550 {ctp 4554 〈cop 4556 ‘cfv 6389 ndxcnx 16757 Basecbs 16773 +gcplusg 16815 .rcmulr 16816 Scalarcsca 16818 ·𝑠 cvsca 16819 LModclmod 19912 LVecclvec 20152 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2159 ax-12 2176 ax-ext 2709 ax-rep 5188 ax-sep 5201 ax-nul 5208 ax-pow 5267 ax-pr 5331 ax-un 7532 ax-cnex 10798 ax-resscn 10799 ax-1cn 10800 ax-icn 10801 ax-addcl 10802 ax-addrcl 10803 ax-mulcl 10804 ax-mulrcl 10805 ax-mulcom 10806 ax-addass 10807 ax-mulass 10808 ax-distr 10809 ax-i2m1 10810 ax-1ne0 10811 ax-1rid 10812 ax-rnegex 10813 ax-rrecex 10814 ax-cnre 10815 ax-pre-lttri 10816 ax-pre-lttrn 10817 ax-pre-ltadd 10818 ax-pre-mulgt0 10819 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2072 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3067 df-rex 3068 df-reu 3069 df-rmo 3070 df-rab 3071 df-v 3417 df-sbc 3704 df-csb 3821 df-dif 3878 df-un 3880 df-in 3882 df-ss 3892 df-pss 3894 df-nul 4247 df-if 4449 df-pw 4524 df-sn 4551 df-pr 4553 df-tp 4555 df-op 4557 df-uni 4829 df-int 4869 df-iun 4915 df-br 5063 df-opab 5125 df-mpt 5145 df-tr 5171 df-id 5464 df-eprel 5469 df-po 5477 df-so 5478 df-fr 5518 df-we 5520 df-xp 5566 df-rel 5567 df-cnv 5568 df-co 5569 df-dm 5570 df-rn 5571 df-res 5572 df-ima 5573 df-pred 6169 df-ord 6225 df-on 6226 df-lim 6227 df-suc 6228 df-iota 6347 df-fun 6391 df-fn 6392 df-f 6393 df-f1 6394 df-fo 6395 df-f1o 6396 df-fv 6397 df-riota 7179 df-ov 7225 df-oprab 7226 df-mpo 7227 df-om 7654 df-1st 7770 df-2nd 7771 df-tpos 7977 df-wrecs 8056 df-recs 8117 df-rdg 8155 df-1o 8211 df-oadd 8215 df-er 8400 df-en 8636 df-dom 8637 df-sdom 8638 df-fin 8639 df-dju 9530 df-card 9568 df-pnf 10882 df-mnf 10883 df-xr 10884 df-ltxr 10885 df-le 10886 df-sub 11077 df-neg 11078 df-nn 11844 df-2 11906 df-3 11907 df-4 11908 df-5 11909 df-6 11910 df-n0 12104 df-xnn0 12176 df-z 12190 df-uz 12452 df-fz 13109 df-hash 13910 df-struct 16713 df-sets 16730 df-slot 16748 df-ndx 16758 df-base 16774 df-plusg 16828 df-mulr 16829 df-sca 16831 df-vsca 16832 df-0g 16959 df-mgm 18127 df-sgrp 18176 df-mnd 18187 df-grp 18381 df-minusg 18382 df-mgp 19518 df-ur 19530 df-ring 19577 df-oppr 19654 df-dvdsr 19672 df-unit 19673 df-drng 19782 df-lmod 19914 df-lvec 20153 df-nzr 20309 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |