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 37290 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 1134 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → 𝑃 ∈ 𝐴) | |
2 | eqid 2821 | . . . 4 ⊢ (Base‘𝐾) = (Base‘𝐾) | |
3 | ltrnel.a | . . . 4 ⊢ 𝐴 = (Atoms‘𝐾) | |
4 | 2, 3 | atbase 36440 | . . 3 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾)) |
5 | ltrnel.h | . . . 4 ⊢ 𝐻 = (LHyp‘𝐾) | |
6 | ltrnel.t | . . . 4 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) | |
7 | 2, 3, 5, 6 | ltrnatb 37288 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ (Base‘𝐾)) → (𝑃 ∈ 𝐴 ↔ (𝐹‘𝑃) ∈ 𝐴)) |
8 | 4, 7 | syl3an3 1161 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝑃 ∈ 𝐴 ↔ (𝐹‘𝑃) ∈ 𝐴)) |
9 | 1, 8 | mpbid 234 | 1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝐹‘𝑃) ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1537 ∈ wcel 2114 ‘cfv 6355 Basecbs 16483 lecple 16572 Atomscatm 36414 HLchlt 36501 LHypclh 37135 LTrncltrn 37252 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-rep 5190 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-reu 3145 df-rab 3147 df-v 3496 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4839 df-iun 4921 df-br 5067 df-opab 5129 df-mpt 5147 df-id 5460 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-map 8408 df-plt 17568 df-glb 17585 df-p0 17649 df-oposet 36327 df-ol 36329 df-oml 36330 df-covers 36417 df-ats 36418 df-hlat 36502 df-lhyp 37139 df-laut 37140 df-ldil 37255 df-ltrn 37256 |
This theorem is referenced by: ltrncoat 37295 trlcnv 37316 trljat2 37318 trlat 37320 trlval3 37338 trlval4 37339 cdlemc3 37344 cdlemc5 37346 cdlemg2kq 37753 cdlemg9a 37783 cdlemg9 37785 cdlemg10bALTN 37787 cdlemg10c 37790 cdlemg10a 37791 cdlemg10 37792 cdlemg12a 37794 cdlemg12c 37796 cdlemg13a 37802 cdlemg17a 37812 cdlemg17g 37818 cdlemg18a 37829 cdlemg18b 37830 cdlemg18c 37831 trlcoabs2N 37873 trlcolem 37877 cdlemg42 37880 cdlemi 37971 cdlemk3 37984 cdlemk4 37985 cdlemk6 37988 cdlemk9 37990 cdlemk9bN 37991 cdlemk10 37994 cdlemksat 37997 cdlemk7 37999 cdlemk12 38001 cdlemkole 38004 cdlemk14 38005 cdlemk15 38006 cdlemk17 38009 cdlemk5u 38012 cdlemk6u 38013 cdlemkuat 38017 cdlemk7u 38021 cdlemk12u 38023 cdlemk37 38065 cdlemk39 38067 cdlemkfid1N 38072 cdlemk47 38100 cdlemk48 38101 cdlemk50 38103 cdlemk51 38104 cdlemk52 38105 cdlemm10N 38269 |
Copyright terms: Public domain | W3C validator |