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	$⊢ B = {Base}_{K}$
	ltrnatb.a	$⊢ A = Atoms (K)$
	ltrnatb.h	$⊢ H = LHyp (K)$
	ltrnatb.t	$⊢ T = LTrn (K) (W)$
Assertion	ltrncnvatb	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in B) \to (P \in A \leftrightarrow F^{-1} (P) \in A)$

Step	Hyp	Ref	Expression
1		ltrnatb.b	$⊢ B = {Base}_{K}$
2		ltrnatb.a	$⊢ A = Atoms (K)$
3		ltrnatb.h	$⊢ H = LHyp (K)$
4		ltrnatb.t	$⊢ T = LTrn (K) (W)$
5	1 3 4	ltrn1o	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F : B \underset{1-1 onto}{⟶} B$
6		f1ocnvdm	$⊢ (F : B \underset{1-1 onto}{⟶} B \land P \in B) \to F^{-1} (P) \in B$
7	5 6	stoic3	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in B) \to F^{-1} (P) \in B$
8	1 2 3 4	ltrnatb	$⊢ ((K \in HL \land W \in H) \land F \in T \land F^{-1} (P) \in B) \to (F^{-1} (P) \in A \leftrightarrow F (F^{-1} (P)) \in A)$
9	7 8	syld3an3	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in B) \to (F^{-1} (P) \in A \leftrightarrow F (F^{-1} (P)) \in A)$
10		f1ocnvfv2	$⊢ (F : B \underset{1-1 onto}{⟶} B \land P \in B) \to F (F^{-1} (P)) = P$
11	5 10	stoic3	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in B) \to F (F^{-1} (P)) = P$
12	11	eleq1d	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in B) \to (F (F^{-1} (P)) \in A \leftrightarrow P \in A)$
13	9 12	bitr2d	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in B) \to (P \in A \leftrightarrow F^{-1} (P) \in A)$

Metamath Proof Explorer