lautj

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

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

Proof

Step	Hyp	Ref	Expression
1		lautj.b	$⊢ B = {Base}_{K}$
2		lautj.j	$⊢ \underset{˙}{\lor} = join (K)$
3		lautj.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	latjcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\lor} Y \in B$
9	8	3adant3r1	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to X \underset{˙}{\lor} Y \in B$
10	1 3	lautcl	$⊢ ((K \in Lat \land F \in I) \land X \underset{˙}{\lor} Y \in B) \to F (X \underset{˙}{\lor} 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{˙}{\lor} 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	latjcl	$⊢ (K \in Lat \land F (X) \in B \land F (Y) \in B) \to F (X) \underset{˙}{\lor} 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{˙}{\lor} F (Y) \in B$
20	1 3	laut1o	$⊢ (K \in Lat \land F \in I) \to F : B \underset{1-1 onto}{⟶} B$
21	20	3ad2antr1	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F : B \underset{1-1 onto}{⟶} B$
22		f1ocnvfv1	$⊢ (F : B \underset{1-1 onto}{⟶} B \land X \underset{˙}{\lor} Y \in B) \to F^{-1} (F (X \underset{˙}{\lor} Y)) = X \underset{˙}{\lor} Y$
23	21 9 22	syl2anc	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F^{-1} (F (X \underset{˙}{\lor} Y)) = X \underset{˙}{\lor} Y$
24	1 4 2	latlej1	$⊢ (K \in Lat \land F (X) \in B \land F (Y) \in B) \to F (X) \leq_{K} (F (X) \underset{˙}{\lor} F (Y))$
25	5 14 17 24	syl3anc	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F (X) \leq_{K} (F (X) \underset{˙}{\lor} F (Y))$
26		f1ocnvfv2	$⊢ (F : B \underset{1-1 onto}{⟶} B \land F (X) \underset{˙}{\lor} F (Y) \in B) \to F (F^{-1} (F (X) \underset{˙}{\lor} F (Y))) = F (X) \underset{˙}{\lor} F (Y)$
27	21 19 26	syl2anc	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F (F^{-1} (F (X) \underset{˙}{\lor} F (Y))) = F (X) \underset{˙}{\lor} F (Y)$
28	25 27	breqtrrd	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F (X) \leq_{K} F (F^{-1} (F (X) \underset{˙}{\lor} F (Y)))$
29		f1ocnvdm	$⊢ (F : B \underset{1-1 onto}{⟶} B \land F (X) \underset{˙}{\lor} F (Y) \in B) \to F^{-1} (F (X) \underset{˙}{\lor} F (Y)) \in B$
30	21 19 29	syl2anc	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F^{-1} (F (X) \underset{˙}{\lor} F (Y)) \in B$
31	1 4 3	lautle	$⊢ ((K \in Lat \land F \in I) \land (X \in B \land F^{-1} (F (X) \underset{˙}{\lor} F (Y)) \in B)) \to (X \leq_{K} F^{-1} (F (X) \underset{˙}{\lor} F (Y)) \leftrightarrow F (X) \leq_{K} F (F^{-1} (F (X) \underset{˙}{\lor} F (Y))))$
32	7 12 30 31	syl12anc	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to (X \leq_{K} F^{-1} (F (X) \underset{˙}{\lor} F (Y)) \leftrightarrow F (X) \leq_{K} F (F^{-1} (F (X) \underset{˙}{\lor} F (Y))))$
33	28 32	mpbird	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to X \leq_{K} F^{-1} (F (X) \underset{˙}{\lor} F (Y))$
34	1 4 2	latlej2	$⊢ (K \in Lat \land F (X) \in B \land F (Y) \in B) \to F (Y) \leq_{K} (F (X) \underset{˙}{\lor} F (Y))$
35	5 14 17 34	syl3anc	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F (Y) \leq_{K} (F (X) \underset{˙}{\lor} F (Y))$
36	35 27	breqtrrd	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F (Y) \leq_{K} F (F^{-1} (F (X) \underset{˙}{\lor} F (Y)))$
37	1 4 3	lautle	$⊢ ((K \in Lat \land F \in I) \land (Y \in B \land F^{-1} (F (X) \underset{˙}{\lor} F (Y)) \in B)) \to (Y \leq_{K} F^{-1} (F (X) \underset{˙}{\lor} F (Y)) \leftrightarrow F (Y) \leq_{K} F (F^{-1} (F (X) \underset{˙}{\lor} F (Y))))$
38	7 15 30 37	syl12anc	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to (Y \leq_{K} F^{-1} (F (X) \underset{˙}{\lor} F (Y)) \leftrightarrow F (Y) \leq_{K} F (F^{-1} (F (X) \underset{˙}{\lor} F (Y))))$
39	36 38	mpbird	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to Y \leq_{K} F^{-1} (F (X) \underset{˙}{\lor} F (Y))$
40	1 4 2	latjle12	$⊢ (K \in Lat \land (X \in B \land Y \in B \land F^{-1} (F (X) \underset{˙}{\lor} F (Y)) \in B)) \to ((X \leq_{K} F^{-1} (F (X) \underset{˙}{\lor} F (Y)) \land Y \leq_{K} F^{-1} (F (X) \underset{˙}{\lor} F (Y))) \leftrightarrow (X \underset{˙}{\lor} Y) \leq_{K} F^{-1} (F (X) \underset{˙}{\lor} F (Y)))$
41	5 12 15 30 40	syl13anc	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to ((X \leq_{K} F^{-1} (F (X) \underset{˙}{\lor} F (Y)) \land Y \leq_{K} F^{-1} (F (X) \underset{˙}{\lor} F (Y))) \leftrightarrow (X \underset{˙}{\lor} Y) \leq_{K} F^{-1} (F (X) \underset{˙}{\lor} F (Y)))$
42	33 39 41	mpbi2and	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to (X \underset{˙}{\lor} Y) \leq_{K} F^{-1} (F (X) \underset{˙}{\lor} F (Y))$
43	23 42	eqbrtrd	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F^{-1} (F (X \underset{˙}{\lor} Y)) \leq_{K} F^{-1} (F (X) \underset{˙}{\lor} F (Y))$
44	1 4 3	lautcnvle	$⊢ ((K \in Lat \land F \in I) \land (F (X \underset{˙}{\lor} Y) \in B \land F (X) \underset{˙}{\lor} F (Y) \in B)) \to (F (X \underset{˙}{\lor} Y) \leq_{K} (F (X) \underset{˙}{\lor} F (Y)) \leftrightarrow F^{-1} (F (X \underset{˙}{\lor} Y)) \leq_{K} F^{-1} (F (X) \underset{˙}{\lor} F (Y)))$
45	7 11 19 44	syl12anc	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to (F (X \underset{˙}{\lor} Y) \leq_{K} (F (X) \underset{˙}{\lor} F (Y)) \leftrightarrow F^{-1} (F (X \underset{˙}{\lor} Y)) \leq_{K} F^{-1} (F (X) \underset{˙}{\lor} F (Y)))$
46	43 45	mpbird	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F (X \underset{˙}{\lor} Y) \leq_{K} (F (X) \underset{˙}{\lor} F (Y))$
47	1 4 2	latlej1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \leq_{K} (X \underset{˙}{\lor} Y)$
48	47	3adant3r1	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to X \leq_{K} (X \underset{˙}{\lor} Y)$
49	1 4 3	lautle	$⊢ ((K \in Lat \land F \in I) \land (X \in B \land X \underset{˙}{\lor} Y \in B)) \to (X \leq_{K} (X \underset{˙}{\lor} Y) \leftrightarrow F (X) \leq_{K} F (X \underset{˙}{\lor} Y))$
50	7 12 9 49	syl12anc	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to (X \leq_{K} (X \underset{˙}{\lor} Y) \leftrightarrow F (X) \leq_{K} F (X \underset{˙}{\lor} Y))$
51	48 50	mpbid	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F (X) \leq_{K} F (X \underset{˙}{\lor} Y)$
52	1 4 2	latlej2	$⊢ (K \in Lat \land X \in B \land Y \in B) \to Y \leq_{K} (X \underset{˙}{\lor} Y)$
53	52	3adant3r1	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to Y \leq_{K} (X \underset{˙}{\lor} Y)$
54	1 4 3	lautle	$⊢ ((K \in Lat \land F \in I) \land (Y \in B \land X \underset{˙}{\lor} Y \in B)) \to (Y \leq_{K} (X \underset{˙}{\lor} Y) \leftrightarrow F (Y) \leq_{K} F (X \underset{˙}{\lor} Y))$
55	7 15 9 54	syl12anc	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to (Y \leq_{K} (X \underset{˙}{\lor} Y) \leftrightarrow F (Y) \leq_{K} F (X \underset{˙}{\lor} Y))$
56	53 55	mpbid	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F (Y) \leq_{K} F (X \underset{˙}{\lor} Y)$
57	1 4 2	latjle12	$⊢ (K \in Lat \land (F (X) \in B \land F (Y) \in B \land F (X \underset{˙}{\lor} Y) \in B)) \to ((F (X) \leq_{K} F (X \underset{˙}{\lor} Y) \land F (Y) \leq_{K} F (X \underset{˙}{\lor} Y)) \leftrightarrow (F (X) \underset{˙}{\lor} F (Y)) \leq_{K} F (X \underset{˙}{\lor} Y))$
58	5 14 17 11 57	syl13anc	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to ((F (X) \leq_{K} F (X \underset{˙}{\lor} Y) \land F (Y) \leq_{K} F (X \underset{˙}{\lor} Y)) \leftrightarrow (F (X) \underset{˙}{\lor} F (Y)) \leq_{K} F (X \underset{˙}{\lor} Y))$
59	51 56 58	mpbi2and	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to (F (X) \underset{˙}{\lor} F (Y)) \leq_{K} F (X \underset{˙}{\lor} Y)$
60	1 4 5 11 19 46 59	latasymd	$⊢ (K \in Lat \land (F \in I \land X \in B \land Y \in B)) \to F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{\lor} F (Y)$

Metamath Proof Explorer

Theorem lautj

Proof