Theorem ltrncnvatb

Description: The converse of the lattice translation of an atom is an atom. (Contributed by NM, 2-Jun-2012)

	Ref	Expression
Hypotheses	ltrnatb.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	ltrnatb.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	ltrnatb.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	ltrnatb.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion	ltrncnvatb	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐵 ) → ( 𝑃 ∈ 𝐴 ↔ ( ◡ 𝐹 ‘ 𝑃 ) ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ltrnatb.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		ltrnatb.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		ltrnatb.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		ltrnatb.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5	1 3 4	ltrn1o	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐹 : 𝐵 –1-1-onto→ 𝐵 )
6		f1ocnvdm	⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 ∧ 𝑃 ∈ 𝐵 ) → ( ◡ 𝐹 ‘ 𝑃 ) ∈ 𝐵 )
7	5 6	stoic3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐵 ) → ( ◡ 𝐹 ‘ 𝑃 ) ∈ 𝐵 )
8	1 2 3 4	ltrnatb	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ◡ 𝐹 ‘ 𝑃 ) ∈ 𝐵 ) → ( ( ◡ 𝐹 ‘ 𝑃 ) ∈ 𝐴 ↔ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑃 ) ) ∈ 𝐴 ) )
9	7 8	syld3an3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐵 ) → ( ( ◡ 𝐹 ‘ 𝑃 ) ∈ 𝐴 ↔ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑃 ) ) ∈ 𝐴 ) )
10		f1ocnvfv2	⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 ∧ 𝑃 ∈ 𝐵 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑃 ) ) = 𝑃 )
11	5 10	stoic3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐵 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑃 ) ) = 𝑃 )
12	11	eleq1d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐵 ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑃 ) ) ∈ 𝐴 ↔ 𝑃 ∈ 𝐴 ) )
13	9 12	bitr2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐵 ) → ( 𝑃 ∈ 𝐴 ↔ ( ◡ 𝐹 ‘ 𝑃 ) ∈ 𝐴 ) )