Theorem ltrnat 40600

Description: The lattice translation of an atom is also an atom. TODO: See if this can shorten some ltrnel 40599 uses. (Contributed by NM, 25-May-2012.)

Hypotheses

Ref	Expression
ltrnel.l	⊢ ≤ = (le‘𝐾)
ltrnel.a	⊢ 𝐴 = (Atoms‘𝐾)
ltrnel.h	⊢ 𝐻 = (LHyp‘𝐾)
ltrnel.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)

Assertion

Ref	Expression
ltrnat	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝐹‘𝑃) ∈ 𝐴)

Proof of Theorem ltrnat

Step	Hyp	Ref	Expression
1		simp3 1139	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → 𝑃 ∈ 𝐴)
2		eqid 2737	. . . 4 ⊢ (Base‘𝐾) = (Base‘𝐾)
3		ltrnel.a	. . . 4 ⊢ 𝐴 = (Atoms‘𝐾)
4	2, 3	atbase 39749	. . 3 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾))
5		ltrnel.h	. . . 4 ⊢ 𝐻 = (LHyp‘𝐾)
6		ltrnel.t	. . . 4 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
7	2, 3, 5, 6	ltrnatb 40597	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ (Base‘𝐾)) → (𝑃 ∈ 𝐴 ↔ (𝐹‘𝑃) ∈ 𝐴))
8	4, 7	syl3an3 1166	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝑃 ∈ 𝐴 ↔ (𝐹‘𝑃) ∈ 𝐴))
9	1, 8	mpbid 232	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝐹‘𝑃) ∈ 𝐴)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ‘cfv 6492  Basecbs 17170  lecple 17218  Atomscatm 39723  HLchlt 39810  LHypclh 40444  LTrncltrn 40561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-map 8768  df-plt 18285  df-glb 18302  df-p0 18380  df-oposet 39636  df-ol 39638  df-oml 39639  df-covers 39726  df-ats 39727  df-hlat 39811  df-lhyp 40448  df-laut 40449  df-ldil 40564  df-ltrn 40565

This theorem is referenced by:  ltrncoat  40604  trlcnv  40625  trljat2  40627  trlat  40629  trlval3  40647  trlval4  40648  cdlemc3  40653  cdlemc5  40655  cdlemg2kq  41062  cdlemg9a  41092  cdlemg9  41094  cdlemg10bALTN  41096  cdlemg10c  41099  cdlemg10a  41100  cdlemg10  41101  cdlemg12a  41103  cdlemg12c  41105  cdlemg13a  41111  cdlemg17a  41121  cdlemg17g  41127  cdlemg18a  41138  cdlemg18b  41139  cdlemg18c  41140  trlcoabs2N  41182  trlcolem  41186  cdlemg42  41189  cdlemi  41280  cdlemk3  41293  cdlemk4  41294  cdlemk6  41297  cdlemk9  41299  cdlemk9bN  41300  cdlemk10  41303  cdlemksat  41306  cdlemk7  41308  cdlemk12  41310  cdlemkole  41313  cdlemk14  41314  cdlemk15  41315  cdlemk17  41318  cdlemk5u  41321  cdlemk6u  41322  cdlemkuat  41326  cdlemk7u  41330  cdlemk12u  41332  cdlemk37  41374  cdlemk39  41376  cdlemkfid1N  41381  cdlemk47  41409  cdlemk48  41410  cdlemk50  41412  cdlemk51  41413  cdlemk52  41414  cdlemm10N  41578