ltrncvr

Description: Covering property of a lattice translation. (Contributed by NM, 20-May-2012)

	Ref	Expression
Hypotheses	ltrncvr.b	$⊢ B = {Base}_{K}$
	ltrncvr.c	$⊢ C = ⋖_{K}$
	ltrncvr.h	$⊢ H = LHyp (K)$
	ltrncvr.t	$⊢ T = LTrn (K) (W)$
Assertion	ltrncvr	$⊢ ((K \in V \land W \in H) \land F \in T \land (X \in B \land Y \in B)) \to (X C Y \leftrightarrow F (X) C F (Y))$

Step	Hyp	Ref	Expression
1		ltrncvr.b	$⊢ B = {Base}_{K}$
2		ltrncvr.c	$⊢ C = ⋖_{K}$
3		ltrncvr.h	$⊢ H = LHyp (K)$
4		ltrncvr.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		simp3l	$⊢ ((K \in V \land W \in H) \land F \in T \land (X \in B \land Y \in B)) \to X \in B$
10		simp3r	$⊢ ((K \in V \land W \in H) \land F \in T \land (X \in B \land Y \in B)) \to Y \in B$
11	1 2 6	lautcvr	$⊢ (K \in V \land (F \in LAut (K) \land X \in B \land Y \in B)) \to (X C Y \leftrightarrow F (X) C F (Y))$
12	5 8 9 10 11	syl13anc	$⊢ ((K \in V \land W \in H) \land F \in T \land (X \in B \land Y \in B)) \to (X C Y \leftrightarrow F (X) C F (Y))$

Metamath Proof Explorer