Metamath Proof Explorer


Theorem ltrncnvat

Description: The converse of the lattice translation of an atom is an atom. (Contributed by NM, 9-May-2013)

Ref Expression
Hypotheses ltrnel.l = ( le ‘ 𝐾 )
ltrnel.a 𝐴 = ( Atoms ‘ 𝐾 )
ltrnel.h 𝐻 = ( LHyp ‘ 𝐾 )
ltrnel.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion ltrncnvat ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝑃𝐴 ) → ( 𝐹𝑃 ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 ltrnel.l = ( le ‘ 𝐾 )
2 ltrnel.a 𝐴 = ( Atoms ‘ 𝐾 )
3 ltrnel.h 𝐻 = ( LHyp ‘ 𝐾 )
4 ltrnel.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5 simp3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝑃𝐴 ) → 𝑃𝐴 )
6 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
7 6 2 atbase ( 𝑃𝐴𝑃 ∈ ( Base ‘ 𝐾 ) )
8 6 2 3 4 ltrncnvatb ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝑃 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃𝐴 ↔ ( 𝐹𝑃 ) ∈ 𝐴 ) )
9 7 8 syl3an3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝑃𝐴 ) → ( 𝑃𝐴 ↔ ( 𝐹𝑃 ) ∈ 𝐴 ) )
10 5 9 mpbid ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝑃𝐴 ) → ( 𝐹𝑃 ) ∈ 𝐴 )