lautcvr

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

	Ref	Expression
Hypotheses	lautcvr.b	$⊢ B = {Base}_{K}$
	lautcvr.c	$⊢ C = ⋖_{K}$
	lautcvr.i	$⊢ I = LAut (K)$
Assertion	lautcvr	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to (X C Y \leftrightarrow F (X) C F (Y))$

Proof

Step	Hyp	Ref	Expression
1		lautcvr.b	$⊢ B = {Base}_{K}$
2		lautcvr.c	$⊢ C = ⋖_{K}$
3		lautcvr.i	$⊢ I = LAut (K)$
4		eqid	$⊢ <_{K} = <_{K}$
5	1 4 3	lautlt	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to (X <_{K} Y \leftrightarrow F (X) <_{K} F (Y))$
6		simpll	$⊢ ((K \in A \land (F \in I \land X \in B \land Y \in B)) \land w \in B) \to K \in A$
7		simplr1	$⊢ ((K \in A \land (F \in I \land X \in B \land Y \in B)) \land w \in B) \to F \in I$
8		simplr2	$⊢ ((K \in A \land (F \in I \land X \in B \land Y \in B)) \land w \in B) \to X \in B$
9		simpr	$⊢ ((K \in A \land (F \in I \land X \in B \land Y \in B)) \land w \in B) \to w \in B$
10	1 4 3	lautlt	$⊢ (K \in A \land (F \in I \land X \in B \land w \in B)) \to (X <_{K} w \leftrightarrow F (X) <_{K} F (w))$
11	6 7 8 9 10	syl13anc	$⊢ ((K \in A \land (F \in I \land X \in B \land Y \in B)) \land w \in B) \to (X <_{K} w \leftrightarrow F (X) <_{K} F (w))$
12		simplr3	$⊢ ((K \in A \land (F \in I \land X \in B \land Y \in B)) \land w \in B) \to Y \in B$
13	1 4 3	lautlt	$⊢ (K \in A \land (F \in I \land w \in B \land Y \in B)) \to (w <_{K} Y \leftrightarrow F (w) <_{K} F (Y))$
14	6 7 9 12 13	syl13anc	$⊢ ((K \in A \land (F \in I \land X \in B \land Y \in B)) \land w \in B) \to (w <_{K} Y \leftrightarrow F (w) <_{K} F (Y))$
15	11 14	anbi12d	$⊢ ((K \in A \land (F \in I \land X \in B \land Y \in B)) \land w \in B) \to ((X <_{K} w \land w <_{K} Y) \leftrightarrow (F (X) <_{K} F (w) \land F (w) <_{K} F (Y)))$
16	1 3	lautcl	$⊢ ((K \in A \land F \in I) \land w \in B) \to F (w) \in B$
17	6 7 9 16	syl21anc	$⊢ ((K \in A \land (F \in I \land X \in B \land Y \in B)) \land w \in B) \to F (w) \in B$
18		breq2	$⊢ z = F (w) \to (F (X) <_{K} z \leftrightarrow F (X) <_{K} F (w))$
19		breq1	$⊢ z = F (w) \to (z <_{K} F (Y) \leftrightarrow F (w) <_{K} F (Y))$
20	18 19	anbi12d	$⊢ z = F (w) \to ((F (X) <_{K} z \land z <_{K} F (Y)) \leftrightarrow (F (X) <_{K} F (w) \land F (w) <_{K} F (Y)))$
21	20	rspcev	$⊢ (F (w) \in B \land (F (X) <_{K} F (w) \land F (w) <_{K} F (Y))) \to \exists z \in B (F (X) <_{K} z \land z <_{K} F (Y))$
22	21	ex	$⊢ F (w) \in B \to ((F (X) <_{K} F (w) \land F (w) <_{K} F (Y)) \to \exists z \in B (F (X) <_{K} z \land z <_{K} F (Y)))$
23	17 22	syl	$⊢ ((K \in A \land (F \in I \land X \in B \land Y \in B)) \land w \in B) \to ((F (X) <_{K} F (w) \land F (w) <_{K} F (Y)) \to \exists z \in B (F (X) <_{K} z \land z <_{K} F (Y)))$
24	15 23	sylbid	$⊢ ((K \in A \land (F \in I \land X \in B \land Y \in B)) \land w \in B) \to ((X <_{K} w \land w <_{K} Y) \to \exists z \in B (F (X) <_{K} z \land z <_{K} F (Y)))$
25	24	rexlimdva	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to (\exists w \in B (X <_{K} w \land w <_{K} Y) \to \exists z \in B (F (X) <_{K} z \land z <_{K} F (Y)))$
26		simpll	$⊢ ((K \in A \land (F \in I \land X \in B \land Y \in B)) \land z \in B) \to K \in A$
27		simplr1	$⊢ ((K \in A \land (F \in I \land X \in B \land Y \in B)) \land z \in B) \to F \in I$
28		simplr2	$⊢ ((K \in A \land (F \in I \land X \in B \land Y \in B)) \land z \in B) \to X \in B$
29	1 3	laut1o	$⊢ (K \in A \land F \in I) \to F : B \underset{1-1 onto}{⟶} B$
30	26 27 29	syl2anc	$⊢ ((K \in A \land (F \in I \land X \in B \land Y \in B)) \land z \in B) \to F : B \underset{1-1 onto}{⟶} B$
31		f1ocnvdm	$⊢ (F : B \underset{1-1 onto}{⟶} B \land z \in B) \to F^{-1} (z) \in B$
32	30 31	sylancom	$⊢ ((K \in A \land (F \in I \land X \in B \land Y \in B)) \land z \in B) \to F^{-1} (z) \in B$
33	1 4 3	lautlt	$⊢ (K \in A \land (F \in I \land X \in B \land F^{-1} (z) \in B)) \to (X <_{K} F^{-1} (z) \leftrightarrow F (X) <_{K} F (F^{-1} (z)))$
34	26 27 28 32 33	syl13anc	$⊢ ((K \in A \land (F \in I \land X \in B \land Y \in B)) \land z \in B) \to (X <_{K} F^{-1} (z) \leftrightarrow F (X) <_{K} F (F^{-1} (z)))$
35		f1ocnvfv2	$⊢ (F : B \underset{1-1 onto}{⟶} B \land z \in B) \to F (F^{-1} (z)) = z$
36	30 35	sylancom	$⊢ ((K \in A \land (F \in I \land X \in B \land Y \in B)) \land z \in B) \to F (F^{-1} (z)) = z$
37	36	breq2d	$⊢ ((K \in A \land (F \in I \land X \in B \land Y \in B)) \land z \in B) \to (F (X) <_{K} F (F^{-1} (z)) \leftrightarrow F (X) <_{K} z)$
38	34 37	bitr2d	$⊢ ((K \in A \land (F \in I \land X \in B \land Y \in B)) \land z \in B) \to (F (X) <_{K} z \leftrightarrow X <_{K} F^{-1} (z))$
39		simplr3	$⊢ ((K \in A \land (F \in I \land X \in B \land Y \in B)) \land z \in B) \to Y \in B$
40	1 4 3	lautlt	$⊢ (K \in A \land (F \in I \land F^{-1} (z) \in B \land Y \in B)) \to (F^{-1} (z) <_{K} Y \leftrightarrow F (F^{-1} (z)) <_{K} F (Y))$
41	26 27 32 39 40	syl13anc	$⊢ ((K \in A \land (F \in I \land X \in B \land Y \in B)) \land z \in B) \to (F^{-1} (z) <_{K} Y \leftrightarrow F (F^{-1} (z)) <_{K} F (Y))$
42	36	breq1d	$⊢ ((K \in A \land (F \in I \land X \in B \land Y \in B)) \land z \in B) \to (F (F^{-1} (z)) <_{K} F (Y) \leftrightarrow z <_{K} F (Y))$
43	41 42	bitr2d	$⊢ ((K \in A \land (F \in I \land X \in B \land Y \in B)) \land z \in B) \to (z <_{K} F (Y) \leftrightarrow F^{-1} (z) <_{K} Y)$
44	38 43	anbi12d	$⊢ ((K \in A \land (F \in I \land X \in B \land Y \in B)) \land z \in B) \to ((F (X) <_{K} z \land z <_{K} F (Y)) \leftrightarrow (X <_{K} F^{-1} (z) \land F^{-1} (z) <_{K} Y))$
45		breq2	$⊢ w = F^{-1} (z) \to (X <_{K} w \leftrightarrow X <_{K} F^{-1} (z))$
46		breq1	$⊢ w = F^{-1} (z) \to (w <_{K} Y \leftrightarrow F^{-1} (z) <_{K} Y)$
47	45 46	anbi12d	$⊢ w = F^{-1} (z) \to ((X <_{K} w \land w <_{K} Y) \leftrightarrow (X <_{K} F^{-1} (z) \land F^{-1} (z) <_{K} Y))$
48	47	rspcev	$⊢ (F^{-1} (z) \in B \land (X <_{K} F^{-1} (z) \land F^{-1} (z) <_{K} Y)) \to \exists w \in B (X <_{K} w \land w <_{K} Y)$
49	48	ex	$⊢ F^{-1} (z) \in B \to ((X <_{K} F^{-1} (z) \land F^{-1} (z) <_{K} Y) \to \exists w \in B (X <_{K} w \land w <_{K} Y))$
50	32 49	syl	$⊢ ((K \in A \land (F \in I \land X \in B \land Y \in B)) \land z \in B) \to ((X <_{K} F^{-1} (z) \land F^{-1} (z) <_{K} Y) \to \exists w \in B (X <_{K} w \land w <_{K} Y))$
51	44 50	sylbid	$⊢ ((K \in A \land (F \in I \land X \in B \land Y \in B)) \land z \in B) \to ((F (X) <_{K} z \land z <_{K} F (Y)) \to \exists w \in B (X <_{K} w \land w <_{K} Y))$
52	51	rexlimdva	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to (\exists z \in B (F (X) <_{K} z \land z <_{K} F (Y)) \to \exists w \in B (X <_{K} w \land w <_{K} Y))$
53	25 52	impbid	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to (\exists w \in B (X <_{K} w \land w <_{K} Y) \leftrightarrow \exists z \in B (F (X) <_{K} z \land z <_{K} F (Y)))$
54	53	notbid	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to (\neg \exists w \in B (X <_{K} w \land w <_{K} Y) \leftrightarrow \neg \exists z \in B (F (X) <_{K} z \land z <_{K} F (Y)))$
55	5 54	anbi12d	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to ((X <_{K} Y \land \neg \exists w \in B (X <_{K} w \land w <_{K} Y)) \leftrightarrow (F (X) <_{K} F (Y) \land \neg \exists z \in B (F (X) <_{K} z \land z <_{K} F (Y))))$
56	1 4 2	cvrval	$⊢ (K \in A \land X \in B \land Y \in B) \to (X C Y \leftrightarrow (X <_{K} Y \land \neg \exists w \in B (X <_{K} w \land w <_{K} Y)))$
57	56	3adant3r1	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to (X C Y \leftrightarrow (X <_{K} Y \land \neg \exists w \in B (X <_{K} w \land w <_{K} Y)))$
58		simpl	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to K \in A$
59		simpr1	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to F \in I$
60		simpr2	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to X \in B$
61	1 3	lautcl	$⊢ ((K \in A \land F \in I) \land X \in B) \to F (X) \in B$
62	58 59 60 61	syl21anc	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to F (X) \in B$
63		simpr3	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to Y \in B$
64	1 3	lautcl	$⊢ ((K \in A \land F \in I) \land Y \in B) \to F (Y) \in B$
65	58 59 63 64	syl21anc	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to F (Y) \in B$
66	1 4 2	cvrval	$⊢ (K \in A \land F (X) \in B \land F (Y) \in B) \to (F (X) C F (Y) \leftrightarrow (F (X) <_{K} F (Y) \land \neg \exists z \in B (F (X) <_{K} z \land z <_{K} F (Y))))$
67	58 62 65 66	syl3anc	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to (F (X) C F (Y) \leftrightarrow (F (X) <_{K} F (Y) \land \neg \exists z \in B (F (X) <_{K} z \land z <_{K} F (Y))))$
68	55 57 67	3bitr4d	$⊢ (K \in A \land (F \in I \land X \in B \land Y \in B)) \to (X C Y \leftrightarrow F (X) C F (Y))$

Metamath Proof Explorer

Theorem lautcvr

Proof