lautm

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

	Ref	Expression
Hypotheses	lautm.b	$⊢ B = {Base}_{K}$
	lautm.m	$⊢ \underset{˙}{\land} = meet (K)$
	lautm.i	$⊢ I = LAut (K)$
Assertion	lautm	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F (X \underset{˙}{\land} Y) = F (X) \underset{˙}{\land} F (Y)$

Proof

Step	Hyp	Ref	Expression
1		lautm.b	$⊢ B = {Base}_{K}$
2		lautm.m	$⊢ \underset{˙}{\land} = meet (K)$
3		lautm.i	$⊢ I = LAut (K)$
4		eqid	$⊢ \leq_{K} = \leq_{K}$
5		simpl	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to K \in Lat$
6		simpr1	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F \in I$
7	5 6	jca	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to (K \in Lat \land F \in I)$
8	1 2	latmcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y \in B$
9	8	3adant3r1	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to X \underset{˙}{\land} Y \in B$
10	1 3	lautcl	$⊢ ((K \in Lat \land F \in I) \land X \underset{˙}{\land} Y \in B) \to F (X \underset{˙}{\land} Y) \in B$
11	7 9 10	syl2anc	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F (X \underset{˙}{\land} Y) \in B$
12		simpr2	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to X \in B$
13	1 3	lautcl	$⊢ ((K \in Lat \land F \in I) \land X \in B) \to F (X) \in B$
14	7 12 13	syl2anc	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F (X) \in B$
15		simpr3	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to Y \in B$
16	1 3	lautcl	$⊢ ((K \in Lat \land F \in I) \land Y \in B) \to F (Y) \in B$
17	7 15 16	syl2anc	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F (Y) \in B$
18	1 2	latmcl	$⊢ (K \in Lat \land F (X) \in B \land F (Y) \in B) \to F (X) \underset{˙}{\land} F (Y) \in B$
19	5 14 17 18	syl3anc	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F (X) \underset{˙}{\land} F (Y) \in B$
20	1 4 2	latmle1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\land} Y) \leq_{K} X$
21	20	3adant3r1	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to (X \underset{˙}{\land} Y) \leq_{K} X$
22	1 4 3	lautle	$⊢ ((K \in Lat \land F \in I) \land (X \underset{˙}{\land} Y \in B \land X \in B)) \to ((X \underset{˙}{\land} Y) \leq_{K} X \leftrightarrow F (X \underset{˙}{\land} Y) \leq_{K} F (X))$
23	7 9 12 22	syl12anc	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to ((X \underset{˙}{\land} Y) \leq_{K} X \leftrightarrow F (X \underset{˙}{\land} Y) \leq_{K} F (X))$
24	21 23	mpbid	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F (X \underset{˙}{\land} Y) \leq_{K} F (X)$
25	1 4 2	latmle2	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\land} Y) \leq_{K} Y$
26	25	3adant3r1	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to (X \underset{˙}{\land} Y) \leq_{K} Y$
27	1 4 3	lautle	$⊢ ((K \in Lat \land F \in I) \land (X \underset{˙}{\land} Y \in B \land Y \in B)) \to ((X \underset{˙}{\land} Y) \leq_{K} Y \leftrightarrow F (X \underset{˙}{\land} Y) \leq_{K} F (Y))$
28	7 9 15 27	syl12anc	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to ((X \underset{˙}{\land} Y) \leq_{K} Y \leftrightarrow F (X \underset{˙}{\land} Y) \leq_{K} F (Y))$
29	26 28	mpbid	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F (X \underset{˙}{\land} Y) \leq_{K} F (Y)$
30	1 4 2	latlem12	$⊢ (K \in Lat \land (F (X \underset{˙}{\land} Y) \in B \land F (X) \in B \land F (Y) \in B)) \to ((F (X \underset{˙}{\land} Y) \leq_{K} F (X) \land F (X \underset{˙}{\land} Y) \leq_{K} F (Y)) \leftrightarrow F (X \underset{˙}{\land} Y) \leq_{K} (F (X) \underset{˙}{\land} F (Y)))$
31	5 11 14 17 30	syl13anc	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to ((F (X \underset{˙}{\land} Y) \leq_{K} F (X) \land F (X \underset{˙}{\land} Y) \leq_{K} F (Y)) \leftrightarrow F (X \underset{˙}{\land} Y) \leq_{K} (F (X) \underset{˙}{\land} F (Y)))$
32	24 29 31	mpbi2and	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F (X \underset{˙}{\land} Y) \leq_{K} (F (X) \underset{˙}{\land} F (Y))$
33	1 3	laut1o	$⊢ (K \in Lat \land F \in I) \to F : B \underset{1-1 onto}{⟶} B$
34	33	3ad2antr1	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F : B \underset{1-1 onto}{⟶} B$
35		f1ocnvfv2	$⊢ (F : B \underset{1-1 onto}{⟶} B \land F (X) \underset{˙}{\land} F (Y) \in B) \to F (F^{-1} (F (X) \underset{˙}{\land} F (Y))) = F (X) \underset{˙}{\land} F (Y)$
36	34 19 35	syl2anc	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F (F^{-1} (F (X) \underset{˙}{\land} F (Y))) = F (X) \underset{˙}{\land} F (Y)$
37	1 4 2	latmle1	$⊢ (K \in Lat \land F (X) \in B \land F (Y) \in B) \to (F (X) \underset{˙}{\land} F (Y)) \leq_{K} F (X)$
38	5 14 17 37	syl3anc	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to (F (X) \underset{˙}{\land} F (Y)) \leq_{K} F (X)$
39	1 4 3	lautcnvle	$⊢ ((K \in Lat \land F \in I) \land (F (X) \underset{˙}{\land} F (Y) \in B \land F (X) \in B)) \to ((F (X) \underset{˙}{\land} F (Y)) \leq_{K} F (X) \leftrightarrow F^{-1} (F (X) \underset{˙}{\land} F (Y)) \leq_{K} F^{-1} (F (X)))$
40	7 19 14 39	syl12anc	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to ((F (X) \underset{˙}{\land} F (Y)) \leq_{K} F (X) \leftrightarrow F^{-1} (F (X) \underset{˙}{\land} F (Y)) \leq_{K} F^{-1} (F (X)))$
41	38 40	mpbid	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F^{-1} (F (X) \underset{˙}{\land} F (Y)) \leq_{K} F^{-1} (F (X))$
42		f1ocnvfv1	$⊢ (F : B \underset{1-1 onto}{⟶} B \land X \in B) \to F^{-1} (F (X)) = X$
43	34 12 42	syl2anc	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F^{-1} (F (X)) = X$
44	41 43	breqtrd	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F^{-1} (F (X) \underset{˙}{\land} F (Y)) \leq_{K} X$
45	1 4 2	latmle2	$⊢ (K \in Lat \land F (X) \in B \land F (Y) \in B) \to (F (X) \underset{˙}{\land} F (Y)) \leq_{K} F (Y)$
46	5 14 17 45	syl3anc	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to (F (X) \underset{˙}{\land} F (Y)) \leq_{K} F (Y)$
47	1 4 3	lautcnvle	$⊢ ((K \in Lat \land F \in I) \land (F (X) \underset{˙}{\land} F (Y) \in B \land F (Y) \in B)) \to ((F (X) \underset{˙}{\land} F (Y)) \leq_{K} F (Y) \leftrightarrow F^{-1} (F (X) \underset{˙}{\land} F (Y)) \leq_{K} F^{-1} (F (Y)))$
48	7 19 17 47	syl12anc	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to ((F (X) \underset{˙}{\land} F (Y)) \leq_{K} F (Y) \leftrightarrow F^{-1} (F (X) \underset{˙}{\land} F (Y)) \leq_{K} F^{-1} (F (Y)))$
49	46 48	mpbid	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F^{-1} (F (X) \underset{˙}{\land} F (Y)) \leq_{K} F^{-1} (F (Y))$
50		f1ocnvfv1	$⊢ (F : B \underset{1-1 onto}{⟶} B \land Y \in B) \to F^{-1} (F (Y)) = Y$
51	34 15 50	syl2anc	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F^{-1} (F (Y)) = Y$
52	49 51	breqtrd	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F^{-1} (F (X) \underset{˙}{\land} F (Y)) \leq_{K} Y$
53		f1ocnvdm	$⊢ (F : B \underset{1-1 onto}{⟶} B \land F (X) \underset{˙}{\land} F (Y) \in B) \to F^{-1} (F (X) \underset{˙}{\land} F (Y)) \in B$
54	34 19 53	syl2anc	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F^{-1} (F (X) \underset{˙}{\land} F (Y)) \in B$
55	1 4 2	latlem12	$⊢ (K \in Lat \land (F^{-1} (F (X) \underset{˙}{\land} F (Y)) \in B \land X \in B \land Y \in B)) \to ((F^{-1} (F (X) \underset{˙}{\land} F (Y)) \leq_{K} X \land F^{-1} (F (X) \underset{˙}{\land} F (Y)) \leq_{K} Y) \leftrightarrow F^{-1} (F (X) \underset{˙}{\land} F (Y)) \leq_{K} (X \underset{˙}{\land} Y))$
56	5 54 12 15 55	syl13anc	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to ((F^{-1} (F (X) \underset{˙}{\land} F (Y)) \leq_{K} X \land F^{-1} (F (X) \underset{˙}{\land} F (Y)) \leq_{K} Y) \leftrightarrow F^{-1} (F (X) \underset{˙}{\land} F (Y)) \leq_{K} (X \underset{˙}{\land} Y))$
57	44 52 56	mpbi2and	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F^{-1} (F (X) \underset{˙}{\land} F (Y)) \leq_{K} (X \underset{˙}{\land} Y)$
58	1 4 3	lautle	$⊢ ((K \in Lat \land F \in I) \land (F^{-1} (F (X) \underset{˙}{\land} F (Y)) \in B \land X \underset{˙}{\land} Y \in B)) \to (F^{-1} (F (X) \underset{˙}{\land} F (Y)) \leq_{K} (X \underset{˙}{\land} Y) \leftrightarrow F (F^{-1} (F (X) \underset{˙}{\land} F (Y))) \leq_{K} F (X \underset{˙}{\land} Y))$
59	7 54 9 58	syl12anc	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to (F^{-1} (F (X) \underset{˙}{\land} F (Y)) \leq_{K} (X \underset{˙}{\land} Y) \leftrightarrow F (F^{-1} (F (X) \underset{˙}{\land} F (Y))) \leq_{K} F (X \underset{˙}{\land} Y))$
60	57 59	mpbid	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F (F^{-1} (F (X) \underset{˙}{\land} F (Y))) \leq_{K} F (X \underset{˙}{\land} Y)$
61	36 60	eqbrtrrd	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to (F (X) \underset{˙}{\land} F (Y)) \leq_{K} F (X \underset{˙}{\land} Y)$
62	1 4 5 11 19 32 61	latasymd	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F (X \underset{˙}{\land} Y) = F (X) \underset{˙}{\land} F (Y)$

Metamath Proof Explorer

Theorem lautm

Proof