ltrncnvleN

Description: Less-than or equal property of lattice translation converse. (Contributed by NM, 10-May-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ltrnle.b	$⊢ B = {Base}_{K}$
	ltrnle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	ltrnle.h	$⊢ H = LHyp (K)$
	ltrnle.t	$⊢ T = LTrn (K) (W)$
Assertion	ltrncnvleN	$⊢ ((K \in V \land W \in H) \land F \in T \land (X \in B \land Y \in B)) \to (X \underset{˙}{\leq} Y \leftrightarrow F^{-1} (X) \underset{˙}{\leq} F^{-1} (Y))$

Step	Hyp	Ref	Expression
1		ltrnle.b	$⊢ B = {Base}_{K}$
2		ltrnle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		ltrnle.h	$⊢ H = LHyp (K)$
4		ltrnle.t	$⊢ T = LTrn (K) (W)$
5		simp1l	$⊢ ((K \in V \land W \in H) \land F \in T \land (X \in B \land Y \in B)) \to K \in V$
6		eqid	$⊢ LAut (K) = LAut (K)$
7	3 6 4	ltrnlaut	$⊢ ((K \in V \land W \in H) \land F \in T) \to F \in LAut (K)$
8	7	3adant3	$⊢ ((K \in V \land W \in H) \land F \in T \land (X \in B \land Y \in B)) \to F \in LAut (K)$
9		simp3	$⊢ ((K \in V \land W \in H) \land F \in T \land (X \in B \land Y \in B)) \to (X \in B \land Y \in B)$
10	1 2 6	lautcnvle	$⊢ ((K \in V \land F \in LAut (K)) \land (X \in B \land Y \in B)) \to (X \underset{˙}{\leq} Y \leftrightarrow F^{-1} (X) \underset{˙}{\leq} F^{-1} (Y))$
11	5 8 9 10	syl21anc	$⊢ ((K \in V \land W \in H) \land F \in T \land (X \in B \land Y \in B)) \to (X \underset{˙}{\leq} Y \leftrightarrow F^{-1} (X) \underset{˙}{\leq} F^{-1} (Y))$

Metamath Proof Explorer