lautlt

Description: Less-than property of a lattice automorphism. (Contributed by NM, 20-May-2012)

	Ref	Expression
Hypotheses	lautlt.b	$⊢ B = {Base}_{K}$
	lautlt.s	$⊢ \underset{˙}{<} = <_{K}$
	lautlt.i	$⊢ I = LAut (K)$
Assertion	lautlt	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to (X \underset{˙}{<} Y \leftrightarrow F (X) \underset{˙}{<} F (Y))$

Proof

Step	Hyp	Ref	Expression
1		lautlt.b	$⊢ B = {Base}_{K}$
2		lautlt.s	$⊢ \underset{˙}{<} = <_{K}$
3		lautlt.i	$⊢ I = LAut (K)$
4		simpl	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to K \in A$
5		simpr1	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to F \in I$
6		simpr2	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to X \in B$
7		simpr3	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to Y \in B$
8		eqid	$⊢ \leq_{K} = \leq_{K}$
9	1 8 3	lautle	$⊢ ((K \in A \land F \in I) \land (X \in B \land Y \in B)) \to (X \leq_{K} Y \leftrightarrow F (X) \leq_{K} F (Y))$
10	4 5 6 7 9	syl22anc	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to (X \leq_{K} Y \leftrightarrow F (X) \leq_{K} F (Y))$
11	1 3	laut11	$⊢ ((K \in A \land F \in I) \land (X \in B \land Y \in B)) \to (F (X) = F (Y) \leftrightarrow X = Y)$
12	4 5 6 7 11	syl22anc	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to (F (X) = F (Y) \leftrightarrow X = Y)$
13	12	bicomd	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to (X = Y \leftrightarrow F (X) = F (Y))$
14	13	necon3bid	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to (X \neq Y \leftrightarrow F (X) \neq F (Y))$
15	10 14	anbi12d	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to ((X \leq_{K} Y \land X \neq Y) \leftrightarrow (F (X) \leq_{K} F (Y) \land F (X) \neq F (Y)))$
16	8 2	pltval	$⊢ (K \in A \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \leftrightarrow (X \leq_{K} Y \land X \neq Y))$
17	16	3adant3r1	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to (X \underset{˙}{<} Y \leftrightarrow (X \leq_{K} Y \land X \neq Y))$
18	1 3	lautcl	$⊢ ((K \in A \land F \in I) \land X \in B) \to F (X) \in B$
19	4 5 6 18	syl21anc	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to F (X) \in B$
20	1 3	lautcl	$⊢ ((K \in A \land F \in I) \land Y \in B) \to F (Y) \in B$
21	4 5 7 20	syl21anc	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to F (Y) \in B$
22	8 2	pltval	$⊢ (K \in A \land F (X) \in B \land F (Y) \in B) \to (F (X) \underset{˙}{<} F (Y) \leftrightarrow (F (X) \leq_{K} F (Y) \land F (X) \neq F (Y)))$
23	4 19 21 22	syl3anc	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to (F (X) \underset{˙}{<} F (Y) \leftrightarrow (F (X) \leq_{K} F (Y) \land F (X) \neq F (Y)))$
24	15 17 23	3bitr4d	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to (X \underset{˙}{<} Y \leftrightarrow F (X) \underset{˙}{<} F (Y))$

Metamath Proof Explorer

Theorem lautlt

Proof