trlcnv

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

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

Proof

Step	Hyp	Ref	Expression
1		trlcnv.h	$⊢ H = LHyp (K)$
2		trlcnv.t	$⊢ T = LTrn (K) (W)$
3		trlcnv.r	$⊢ R = trL (K) (W)$
4		eqid	$⊢ \leq_{K} = \leq_{K}$
5		eqid	$⊢ Atoms (K) = Atoms (K)$
6	4 5 1	lhpexnle	$⊢ (K \in HL \land W \in H) \to \exists p \in Atoms (K) \neg p \leq_{K} W$
7	6	adantr	$⊢ ((K \in HL \land W \in H) \land F \in T) \to \exists p \in Atoms (K) \neg p \leq_{K} W$
8		eqid	$⊢ {Base}_{K} = {Base}_{K}$
9	8 1 2	ltrn1o	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
10	9	3adant3	$⊢ ((K \in HL \land W \in H) \land F \in T \land (p \in Atoms (K) \land \neg p \leq_{K} W)) \to F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
11		simp3l	$⊢ ((K \in HL \land W \in H) \land F \in T \land (p \in Atoms (K) \land \neg p \leq_{K} W)) \to p \in Atoms (K)$
12	8 5	atbase	$⊢ p \in Atoms (K) \to p \in {Base}_{K}$
13	11 12	syl	$⊢ ((K \in HL \land W \in H) \land F \in T \land (p \in Atoms (K) \land \neg p \leq_{K} W)) \to p \in {Base}_{K}$
14		f1ocnvfv1	$⊢ (F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \land p \in {Base}_{K}) \to F^{-1} (F (p)) = p$
15	10 13 14	syl2anc	$⊢ ((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} (F (p)) = p$
16	15	oveq2d	$⊢ ((K \in HL \land W \in H) \land F \in T \land (p \in Atoms (K) \land \neg p \leq_{K} W)) \to F (p) join (K) F^{-1} (F (p)) = F (p) join (K) p$
17		simp1l	$⊢ ((K \in HL \land W \in H) \land F \in T \land (p \in Atoms (K) \land \neg p \leq_{K} W)) \to K \in HL$
18	4 5 1 2	ltrnat	$⊢ ((K \in HL \land W \in H) \land F \in T \land p \in Atoms (K)) \to F (p) \in Atoms (K)$
19	18	3adant3r	$⊢ ((K \in HL \land W \in H) \land F \in T \land (p \in Atoms (K) \land \neg p \leq_{K} W)) \to F (p) \in Atoms (K)$
20		eqid	$⊢ join (K) = join (K)$
21	20 5	hlatjcom	$⊢ (K \in HL \land F (p) \in Atoms (K) \land p \in Atoms (K)) \to F (p) join (K) p = p join (K) F (p)$
22	17 19 11 21	syl3anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land (p \in Atoms (K) \land \neg p \leq_{K} W)) \to F (p) join (K) p = p join (K) F (p)$
23	16 22	eqtrd	$⊢ ((K \in HL \land W \in H) \land F \in T \land (p \in Atoms (K) \land \neg p \leq_{K} W)) \to F (p) join (K) F^{-1} (F (p)) = p join (K) F (p)$
24	23	oveq1d	$⊢ ((K \in HL \land W \in H) \land F \in T \land (p \in Atoms (K) \land \neg p \leq_{K} W)) \to (F (p) join (K) F^{-1} (F (p))) meet (K) W = (p join (K) F (p)) meet (K) W$
25		simp1	$⊢ ((K \in HL \land W \in H) \land F \in T \land (p \in Atoms (K) \land \neg p \leq_{K} W)) \to (K \in HL \land W \in H)$
26	1 2	ltrncnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F^{-1} \in T$
27	26	3adant3	$⊢ ((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} \in T$
28	4 5 1 2	ltrnel	$⊢ ((K \in HL \land W \in H) \land F \in T \land (p \in Atoms (K) \land \neg p \leq_{K} W)) \to (F (p) \in Atoms (K) \land \neg F (p) \leq_{K} W)$
29		eqid	$⊢ meet (K) = meet (K)$
30	4 20 29 5 1 2 3	trlval2	$⊢ ((K \in HL \land W \in H) \land F^{-1} \in T \land (F (p) \in Atoms (K) \land \neg F (p) \leq_{K} W)) \to R (F^{-1}) = (F (p) join (K) F^{-1} (F (p))) meet (K) W$
31	25 27 28 30	syl3anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land (p \in Atoms (K) \land \neg p \leq_{K} W)) \to R (F^{-1}) = (F (p) join (K) F^{-1} (F (p))) meet (K) W$
32	4 20 29 5 1 2 3	trlval2	$⊢ ((K \in HL \land W \in H) \land F \in T \land (p \in Atoms (K) \land \neg p \leq_{K} W)) \to R (F) = (p join (K) F (p)) meet (K) W$
33	24 31 32	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land F \in T \land (p \in Atoms (K) \land \neg p \leq_{K} W)) \to R (F^{-1}) = R (F)$
34	33	3expa	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in Atoms (K) \land \neg p \leq_{K} W)) \to R (F^{-1}) = R (F)$
35	7 34	rexlimddv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F^{-1}) = R (F)$

Metamath Proof Explorer

Theorem trlcnv

Proof