ltrncnv

Description: The converse of a lattice translation is a lattice translation. (Contributed by NM, 10-May-2013)

	Ref	Expression
Hypotheses	ltrncnv.h	$⊢ H = LHyp (K)$
	ltrncnv.t	$⊢ T = LTrn (K) (W)$
Assertion	ltrncnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F^{-1} \in T$

Proof

Step	Hyp	Ref	Expression
1		ltrncnv.h	$⊢ H = LHyp (K)$
2		ltrncnv.t	$⊢ T = LTrn (K) (W)$
3		eqid	$⊢ LDil (K) (W) = LDil (K) (W)$
4	1 3 2	ltrnldil	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F \in LDil (K) (W)$
5	1 3	ldilcnv	$⊢ ((K \in HL \land W \in H) \land F \in LDil (K) (W)) \to F^{-1} \in LDil (K) (W)$
6	4 5	syldan	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F^{-1} \in LDil (K) (W)$
7		simp1	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to ((K \in HL \land W \in H) \land F \in T)$
8		simp1l	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to (K \in HL \land W \in H)$
9		simp1r	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to F \in T$
10		simp2l	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to p \in Atoms (K)$
11		simp3l	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to \neg p \leq_{K} W$
12		eqid	$⊢ \leq_{K} = \leq_{K}$
13		eqid	$⊢ Atoms (K) = Atoms (K)$
14	12 13 1 2	ltrncnvel	$⊢ ((K \in HL \land W \in H) \land F \in T \land (p \in Atoms (K) \land \neg p \leq_{K} W)) \to (F^{-1} (p) \in Atoms (K) \land \neg F^{-1} (p) \leq_{K} W)$
15	8 9 10 11 14	syl112anc	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to (F^{-1} (p) \in Atoms (K) \land \neg F^{-1} (p) \leq_{K} W)$
16		simp2r	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to q \in Atoms (K)$
17		simp3r	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to \neg q \leq_{K} W$
18	12 13 1 2	ltrncnvel	$⊢ ((K \in HL \land W \in H) \land F \in T \land (q \in Atoms (K) \land \neg q \leq_{K} W)) \to (F^{-1} (q) \in Atoms (K) \land \neg F^{-1} (q) \leq_{K} W)$
19	8 9 16 17 18	syl112anc	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to (F^{-1} (q) \in Atoms (K) \land \neg F^{-1} (q) \leq_{K} W)$
20		eqid	$⊢ join (K) = join (K)$
21		eqid	$⊢ meet (K) = meet (K)$
22	12 20 21 13 1 2	ltrnu	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (F^{-1} (p) \in Atoms (K) \land \neg F^{-1} (p) \leq_{K} W) \land (F^{-1} (q) \in Atoms (K) \land \neg F^{-1} (q) \leq_{K} W)) \to (F^{-1} (p) join (K) F (F^{-1} (p))) meet (K) W = (F^{-1} (q) join (K) F (F^{-1} (q))) meet (K) W$
23	7 15 19 22	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to (F^{-1} (p) join (K) F (F^{-1} (p))) meet (K) W = (F^{-1} (q) join (K) F (F^{-1} (q))) meet (K) W$
24		eqid	$⊢ {Base}_{K} = {Base}_{K}$
25	24 1 2	ltrn1o	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
26	25	3ad2ant1	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
27	24 13	atbase	$⊢ p \in Atoms (K) \to p \in {Base}_{K}$
28	10 27	syl	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to p \in {Base}_{K}$
29		f1ocnvfv2	$⊢ (F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \land p \in {Base}_{K}) \to F (F^{-1} (p)) = p$
30	26 28 29	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to F (F^{-1} (p)) = p$
31	30	oveq2d	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to F^{-1} (p) join (K) F (F^{-1} (p)) = F^{-1} (p) join (K) p$
32		simp1ll	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to K \in HL$
33	12 13 1 2	ltrncnvat	$⊢ ((K \in HL \land W \in H) \land F \in T \land p \in Atoms (K)) \to F^{-1} (p) \in Atoms (K)$
34	8 9 10 33	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to F^{-1} (p) \in Atoms (K)$
35	20 13	hlatjcom	$⊢ (K \in HL \land F^{-1} (p) \in Atoms (K) \land p \in Atoms (K)) \to F^{-1} (p) join (K) p = p join (K) F^{-1} (p)$
36	32 34 10 35	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to F^{-1} (p) join (K) p = p join (K) F^{-1} (p)$
37	31 36	eqtrd	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to F^{-1} (p) join (K) F (F^{-1} (p)) = p join (K) F^{-1} (p)$
38	37	oveq1d	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to (F^{-1} (p) join (K) F (F^{-1} (p))) meet (K) W = (p join (K) F^{-1} (p)) meet (K) W$
39	24 13	atbase	$⊢ q \in Atoms (K) \to q \in {Base}_{K}$
40	16 39	syl	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to q \in {Base}_{K}$
41		f1ocnvfv2	$⊢ (F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \land q \in {Base}_{K}) \to F (F^{-1} (q)) = q$
42	26 40 41	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to F (F^{-1} (q)) = q$
43	42	oveq2d	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to F^{-1} (q) join (K) F (F^{-1} (q)) = F^{-1} (q) join (K) q$
44	12 13 1 2	ltrncnvat	$⊢ ((K \in HL \land W \in H) \land F \in T \land q \in Atoms (K)) \to F^{-1} (q) \in Atoms (K)$
45	8 9 16 44	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to F^{-1} (q) \in Atoms (K)$
46	20 13	hlatjcom	$⊢ (K \in HL \land F^{-1} (q) \in Atoms (K) \land q \in Atoms (K)) \to F^{-1} (q) join (K) q = q join (K) F^{-1} (q)$
47	32 45 16 46	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to F^{-1} (q) join (K) q = q join (K) F^{-1} (q)$
48	43 47	eqtrd	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to F^{-1} (q) join (K) F (F^{-1} (q)) = q join (K) F^{-1} (q)$
49	48	oveq1d	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to (F^{-1} (q) join (K) F (F^{-1} (q))) meet (K) W = (q join (K) F^{-1} (q)) meet (K) W$
50	23 38 49	3eqtr3d	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to (p join (K) F^{-1} (p)) meet (K) W = (q join (K) F^{-1} (q)) meet (K) W$
51	50	3exp	$⊢ ((K \in HL \land W \in H) \land F \in T) \to ((p \in Atoms (K) \land q \in Atoms (K)) \to ((\neg p \leq_{K} W \land \neg q \leq_{K} W) \to (p join (K) F^{-1} (p)) meet (K) W = (q join (K) F^{-1} (q)) meet (K) W))$
52	51	ralrimivv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to \forall p \in Atoms (K) \forall q \in Atoms (K) ((\neg p \leq_{K} W \land \neg q \leq_{K} W) \to (p join (K) F^{-1} (p)) meet (K) W = (q join (K) F^{-1} (q)) meet (K) W)$
53	12 20 21 13 1 3 2	isltrn	$⊢ (K \in HL \land W \in H) \to (F^{-1} \in T \leftrightarrow (F^{-1} \in LDil (K) (W) \land \forall p \in Atoms (K) \forall q \in Atoms (K) ((\neg p \leq_{K} W \land \neg q \leq_{K} W) \to (p join (K) F^{-1} (p)) meet (K) W = (q join (K) F^{-1} (q)) meet (K) W)))$
54	53	adantr	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (F^{-1} \in T \leftrightarrow (F^{-1} \in LDil (K) (W) \land \forall p \in Atoms (K) \forall q \in Atoms (K) ((\neg p \leq_{K} W \land \neg q \leq_{K} W) \to (p join (K) F^{-1} (p)) meet (K) W = (q join (K) F^{-1} (q)) meet (K) W)))$
55	6 52 54	mpbir2and	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F^{-1} \in T$

Metamath Proof Explorer

Theorem ltrncnv

Proof