Theorem ltrnat

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

	Ref	Expression
Hypotheses	ltrnel.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	ltrnel.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	ltrnel.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	ltrnel.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
Assertion	ltrnat	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\wedge P\in A\right)\to F\left(P\right)\in A$$

Proof

Step	Hyp	Ref	Expression
1		ltrnel.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		ltrnel.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
3		ltrnel.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
4		ltrnel.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
5		simp3	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\wedge P\in A\right)\to P\in A$$
6		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
7	6 2	atbase	$$⊢P\in A\to P\in {\mathrm{Base}}_K$$
8	6 2 3 4	ltrnatb	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\wedge P\in {\mathrm{Base}}_K\right)\to \left(P\in A\leftrightarrow F\left(P\right)\in A\right)$$
9	7 8	syl3an3	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\wedge P\in A\right)\to \left(P\in A\leftrightarrow F\left(P\right)\in A\right)$$
10	5 9	mpbid	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\wedge P\in A\right)\to F\left(P\right)\in A$$