| Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > Mathboxes > islsat | Structured version Visualization version GIF version | ||
| Description: The predicate "is a 1-dim subspace (atom)" (of a left module or left vector space). (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
| Ref | Expression |
|---|---|
| lsatset.v | ⊢ 𝑉 = (Base‘𝑊) |
| lsatset.n | ⊢ 𝑁 = (LSpan‘𝑊) |
| lsatset.z | ⊢ 0 = (0g‘𝑊) |
| lsatset.a | ⊢ 𝐴 = (LSAtoms‘𝑊) |
| Ref | Expression |
|---|---|
| islsat | ⊢ (𝑊 ∈ 𝑋 → (𝑈 ∈ 𝐴 ↔ ∃𝑥 ∈ (𝑉 ∖ { 0 })𝑈 = (𝑁‘{𝑥}))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | lsatset.v | . . . 4 ⊢ 𝑉 = (Base‘𝑊) | |
| 2 | lsatset.n | . . . 4 ⊢ 𝑁 = (LSpan‘𝑊) | |
| 3 | lsatset.z | . . . 4 ⊢ 0 = (0g‘𝑊) | |
| 4 | lsatset.a | . . . 4 ⊢ 𝐴 = (LSAtoms‘𝑊) | |
| 5 | 1, 2, 3, 4 | lsatset 39621 | . . 3 ⊢ (𝑊 ∈ 𝑋 → 𝐴 = ran (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑥}))) |
| 6 | 5 | eleq2d 2851 | . 2 ⊢ (𝑊 ∈ 𝑋 → (𝑈 ∈ 𝐴 ↔ 𝑈 ∈ ran (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑥})))) |
| 7 | eqid 2765 | . . 3 ⊢ (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑥})) = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑥})) | |
| 8 | fvex 6884 | . . 3 ⊢ (𝑁‘{𝑥}) ∈ V | |
| 9 | 7, 8 | elrnmpti 5942 | . 2 ⊢ (𝑈 ∈ ran (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑥})) ↔ ∃𝑥 ∈ (𝑉 ∖ { 0 })𝑈 = (𝑁‘{𝑥})) |
| 10 | 6, 9 | bitrdi 290 | 1 ⊢ (𝑊 ∈ 𝑋 → (𝑈 ∈ 𝐴 ↔ ∃𝑥 ∈ (𝑉 ∖ { 0 })𝑈 = (𝑁‘{𝑥}))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 209 = wceq 1563 ∈ wcel 2145 ∃wrex 3089 ∖ cdif 3904 {csn 4585 ↦ cmpt 5185 ran crn 5652 ‘cfv 6525 Basecbs 17257 0gc0g 17480 LSpanclspn 21058 LSAtomsclsa 39605 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-sep 5250 ax-nul 5260 ax-pr 5394 ax-un 7722 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3080 df-rex 3090 df-rab 3418 df-v 3459 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-br 5105 df-opab 5167 df-mpt 5186 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-fv 6533 df-lsatoms 39607 |
| This theorem is referenced by: lsatlspsn2 39623 lsatlspsn 39624 islsati 39625 lsateln0 39626 lsatn0 39630 lsatcmp 39634 lsmsat 39639 lsatfixedN 39640 islshpat 39648 lsatcv0 39662 lsat0cv 39664 lcv1 39672 l1cvpat 39685 dih1dimatlem 41960 dihlatat 41968 dochsatshp 42082 |
| Copyright terms: Public domain | W3C validator |