![]() |
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 36160 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 1169 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → 𝑃 ∈ 𝐴) | |
2 | eqid 2799 | . . . 4 ⊢ (Base‘𝐾) = (Base‘𝐾) | |
3 | ltrnel.a | . . . 4 ⊢ 𝐴 = (Atoms‘𝐾) | |
4 | 2, 3 | atbase 35310 | . . 3 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾)) |
5 | ltrnel.h | . . . 4 ⊢ 𝐻 = (LHyp‘𝐾) | |
6 | ltrnel.t | . . . 4 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) | |
7 | 2, 3, 5, 6 | ltrnatb 36158 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ (Base‘𝐾)) → (𝑃 ∈ 𝐴 ↔ (𝐹‘𝑃) ∈ 𝐴)) |
8 | 4, 7 | syl3an3 1206 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝑃 ∈ 𝐴 ↔ (𝐹‘𝑃) ∈ 𝐴)) |
9 | 1, 8 | mpbid 224 | 1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝐹‘𝑃) ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 385 ∧ w3a 1108 = wceq 1653 ∈ wcel 2157 ‘cfv 6101 Basecbs 16184 lecple 16274 Atomscatm 35284 HLchlt 35371 LHypclh 36005 LTrncltrn 36122 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 ax-rep 4964 ax-sep 4975 ax-nul 4983 ax-pow 5035 ax-pr 5097 ax-un 7183 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ne 2972 df-ral 3094 df-rex 3095 df-reu 3096 df-rab 3098 df-v 3387 df-sbc 3634 df-csb 3729 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-nul 4116 df-if 4278 df-pw 4351 df-sn 4369 df-pr 4371 df-op 4375 df-uni 4629 df-iun 4712 df-br 4844 df-opab 4906 df-mpt 4923 df-id 5220 df-xp 5318 df-rel 5319 df-cnv 5320 df-co 5321 df-dm 5322 df-rn 5323 df-res 5324 df-ima 5325 df-iota 6064 df-fun 6103 df-fn 6104 df-f 6105 df-f1 6106 df-fo 6107 df-f1o 6108 df-fv 6109 df-riota 6839 df-ov 6881 df-oprab 6882 df-mpt2 6883 df-map 8097 df-plt 17273 df-glb 17290 df-p0 17354 df-oposet 35197 df-ol 35199 df-oml 35200 df-covers 35287 df-ats 35288 df-hlat 35372 df-lhyp 36009 df-laut 36010 df-ldil 36125 df-ltrn 36126 |
This theorem is referenced by: ltrncoat 36165 trlcnv 36186 trljat2 36188 trlat 36190 trlval3 36208 trlval4 36209 cdlemc3 36214 cdlemc5 36216 cdlemg2kq 36623 cdlemg9a 36653 cdlemg9 36655 cdlemg10bALTN 36657 cdlemg10c 36660 cdlemg10a 36661 cdlemg10 36662 cdlemg12a 36664 cdlemg12c 36666 cdlemg13a 36672 cdlemg17a 36682 cdlemg17g 36688 cdlemg18a 36699 cdlemg18b 36700 cdlemg18c 36701 trlcoabs2N 36743 trlcolem 36747 cdlemg42 36750 cdlemi 36841 cdlemk3 36854 cdlemk4 36855 cdlemk6 36858 cdlemk9 36860 cdlemk9bN 36861 cdlemk10 36864 cdlemksat 36867 cdlemk7 36869 cdlemk12 36871 cdlemkole 36874 cdlemk14 36875 cdlemk15 36876 cdlemk17 36879 cdlemk5u 36882 cdlemk6u 36883 cdlemkuat 36887 cdlemk7u 36891 cdlemk12u 36893 cdlemk37 36935 cdlemk39 36937 cdlemkfid1N 36942 cdlemk47 36970 cdlemk48 36971 cdlemk50 36973 cdlemk51 36974 cdlemk52 36975 cdlemm10N 37139 |
Copyright terms: Public domain | W3C validator |