![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > ltrnat | Structured version Visualization version GIF version |
Description: The lattice translation of an atom is also an atom. TODO: See if this can shorten some ltrnel 36827 uses. (Contributed by NM, 25-May-2012.) |
Ref | Expression |
---|---|
ltrnel.l | ⊢ ≤ = (le‘𝐾) |
ltrnel.a | ⊢ 𝐴 = (Atoms‘𝐾) |
ltrnel.h | ⊢ 𝐻 = (LHyp‘𝐾) |
ltrnel.t | ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
Ref | Expression |
---|---|
ltrnat | ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝐹‘𝑃) ∈ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp3 1131 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → 𝑃 ∈ 𝐴) | |
2 | eqid 2797 | . . . 4 ⊢ (Base‘𝐾) = (Base‘𝐾) | |
3 | ltrnel.a | . . . 4 ⊢ 𝐴 = (Atoms‘𝐾) | |
4 | 2, 3 | atbase 35977 | . . 3 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾)) |
5 | ltrnel.h | . . . 4 ⊢ 𝐻 = (LHyp‘𝐾) | |
6 | ltrnel.t | . . . 4 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) | |
7 | 2, 3, 5, 6 | ltrnatb 36825 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ (Base‘𝐾)) → (𝑃 ∈ 𝐴 ↔ (𝐹‘𝑃) ∈ 𝐴)) |
8 | 4, 7 | syl3an3 1158 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝑃 ∈ 𝐴 ↔ (𝐹‘𝑃) ∈ 𝐴)) |
9 | 1, 8 | mpbid 233 | 1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝐹‘𝑃) ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∧ w3a 1080 = wceq 1525 ∈ wcel 2083 ‘cfv 6232 Basecbs 16316 lecple 16405 Atomscatm 35951 HLchlt 36038 LHypclh 36672 LTrncltrn 36789 |
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-plt 17401 df-glb 17418 df-p0 17482 df-oposet 35864 df-ol 35866 df-oml 35867 df-covers 35954 df-ats 35955 df-hlat 36039 df-lhyp 36676 df-laut 36677 df-ldil 36792 df-ltrn 36793 |
This theorem is referenced by: ltrncoat 36832 trlcnv 36853 trljat2 36855 trlat 36857 trlval3 36875 trlval4 36876 cdlemc3 36881 cdlemc5 36883 cdlemg2kq 37290 cdlemg9a 37320 cdlemg9 37322 cdlemg10bALTN 37324 cdlemg10c 37327 cdlemg10a 37328 cdlemg10 37329 cdlemg12a 37331 cdlemg12c 37333 cdlemg13a 37339 cdlemg17a 37349 cdlemg17g 37355 cdlemg18a 37366 cdlemg18b 37367 cdlemg18c 37368 trlcoabs2N 37410 trlcolem 37414 cdlemg42 37417 cdlemi 37508 cdlemk3 37521 cdlemk4 37522 cdlemk6 37525 cdlemk9 37527 cdlemk9bN 37528 cdlemk10 37531 cdlemksat 37534 cdlemk7 37536 cdlemk12 37538 cdlemkole 37541 cdlemk14 37542 cdlemk15 37543 cdlemk17 37546 cdlemk5u 37549 cdlemk6u 37550 cdlemkuat 37554 cdlemk7u 37558 cdlemk12u 37560 cdlemk37 37602 cdlemk39 37604 cdlemkfid1N 37609 cdlemk47 37637 cdlemk48 37638 cdlemk50 37640 cdlemk51 37641 cdlemk52 37642 cdlemm10N 37806 |
Copyright terms: Public domain | W3C validator |