![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > trlnidat | Structured version Visualization version GIF version |
Description: The trace of a lattice translation other than the identity is an atom. Remark above Lemma C in [Crawley] p. 112. (Contributed by NM, 23-May-2012.) |
Ref | Expression |
---|---|
trlnidat.b | ⊢ 𝐵 = (Base‘𝐾) |
trlnidat.a | ⊢ 𝐴 = (Atoms‘𝐾) |
trlnidat.h | ⊢ 𝐻 = (LHyp‘𝐾) |
trlnidat.t | ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
trlnidat.r | ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
Ref | Expression |
---|---|
trlnidat | ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) → (𝑅‘𝐹) ∈ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | trlnidat.b | . . 3 ⊢ 𝐵 = (Base‘𝐾) | |
2 | eqid 2797 | . . 3 ⊢ (le‘𝐾) = (le‘𝐾) | |
3 | trlnidat.a | . . 3 ⊢ 𝐴 = (Atoms‘𝐾) | |
4 | trlnidat.h | . . 3 ⊢ 𝐻 = (LHyp‘𝐾) | |
5 | trlnidat.t | . . 3 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) | |
6 | 1, 2, 3, 4, 5 | ltrnnid 36824 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) → ∃𝑝 ∈ 𝐴 (¬ 𝑝(le‘𝐾)𝑊 ∧ (𝐹‘𝑝) ≠ 𝑝)) |
7 | simp11 1196 | . . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ 𝑝 ∈ 𝐴 ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ (𝐹‘𝑝) ≠ 𝑝)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | |
8 | simp2 1130 | . . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ 𝑝 ∈ 𝐴 ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ (𝐹‘𝑝) ≠ 𝑝)) → 𝑝 ∈ 𝐴) | |
9 | simp3l 1194 | . . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ 𝑝 ∈ 𝐴 ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ (𝐹‘𝑝) ≠ 𝑝)) → ¬ 𝑝(le‘𝐾)𝑊) | |
10 | simp12 1197 | . . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ 𝑝 ∈ 𝐴 ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ (𝐹‘𝑝) ≠ 𝑝)) → 𝐹 ∈ 𝑇) | |
11 | simp3r 1195 | . . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ 𝑝 ∈ 𝐴 ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ (𝐹‘𝑝) ≠ 𝑝)) → (𝐹‘𝑝) ≠ 𝑝) | |
12 | trlnidat.r | . . . . 5 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) | |
13 | 2, 3, 4, 5, 12 | trlat 36857 | . . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ 𝐴 ∧ ¬ 𝑝(le‘𝐾)𝑊) ∧ (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑝) ≠ 𝑝)) → (𝑅‘𝐹) ∈ 𝐴) |
14 | 7, 8, 9, 10, 11, 13 | syl122anc 1372 | . . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ 𝑝 ∈ 𝐴 ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ (𝐹‘𝑝) ≠ 𝑝)) → (𝑅‘𝐹) ∈ 𝐴) |
15 | 14 | rexlimdv3a 3251 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) → (∃𝑝 ∈ 𝐴 (¬ 𝑝(le‘𝐾)𝑊 ∧ (𝐹‘𝑝) ≠ 𝑝) → (𝑅‘𝐹) ∈ 𝐴)) |
16 | 6, 15 | mpd 15 | 1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) → (𝑅‘𝐹) ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∧ w3a 1080 = wceq 1525 ∈ wcel 2083 ≠ wne 2986 ∃wrex 3108 class class class wbr 4968 I cid 5354 ↾ cres 5452 ‘cfv 6232 Basecbs 16316 lecple 16405 Atomscatm 35951 HLchlt 36038 LHypclh 36672 LTrncltrn 36789 trLctrl 36846 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-13 2346 ax-ext 2771 ax-rep 5088 ax-sep 5101 ax-nul 5108 ax-pow 5164 ax-pr 5228 ax-un 7326 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-mo 2578 df-eu 2614 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ne 2987 df-ral 3112 df-rex 3113 df-reu 3114 df-rab 3116 df-v 3442 df-sbc 3712 df-csb 3818 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-nul 4218 df-if 4388 df-pw 4461 df-sn 4479 df-pr 4481 df-op 4485 df-uni 4752 df-iun 4833 df-br 4969 df-opab 5031 df-mpt 5048 df-id 5355 df-xp 5456 df-rel 5457 df-cnv 5458 df-co 5459 df-dm 5460 df-rn 5461 df-res 5462 df-ima 5463 df-iota 6196 df-fun 6234 df-fn 6235 df-f 6236 df-f1 6237 df-fo 6238 df-f1o 6239 df-fv 6240 df-riota 6984 df-ov 7026 df-oprab 7027 df-mpo 7028 df-map 8265 df-proset 17371 df-poset 17389 df-plt 17401 df-lub 17417 df-glb 17418 df-join 17419 df-meet 17420 df-p0 17482 df-p1 17483 df-lat 17489 df-clat 17551 df-oposet 35864 df-ol 35866 df-oml 35867 df-covers 35954 df-ats 35955 df-atl 35986 df-cvlat 36010 df-hlat 36039 df-lhyp 36676 df-laut 36677 df-ldil 36792 df-ltrn 36793 df-trl 36847 |
This theorem is referenced by: ltrnnidn 36862 trlnidatb 36865 trlcone 37416 cdlemg46 37423 trljco 37428 cdlemh2 37504 cdlemh 37505 tendotr 37518 cdlemk3 37521 cdlemk12 37538 cdlemkole 37541 cdlemk14 37542 cdlemk15 37543 cdlemk1u 37547 cdlemk5u 37549 cdlemk12u 37560 cdlemk37 37602 cdlemk39 37604 cdlemkid1 37610 cdlemk47 37637 cdlemk51 37641 cdlemk52 37642 cdleml1N 37664 |
Copyright terms: Public domain | W3C validator |