Metamath Proof Explorer

Theorem 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 ∈ HL ∧ W ∈ H ∧ F ∈ T → 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 ⊢ ≤ K = ≤ K
5 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
6 4 5 1 lhpexnle ⊢ K ∈ HL ∧ W ∈ H → ∃ p ∈ Atoms ⁡ K ¬ p ≤ K W
7 6 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T → ∃ p ∈ Atoms ⁡ K ¬ p ≤ K W
8 eqid ⊢ Base K = Base K
9 8 1 2 ltrn1o ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T → F : Base K ⟶ 1-1 onto Base K
10 9 3adant3 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ K W → F : Base K ⟶ 1-1 onto Base K
11 simp3l ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ K W → p ∈ Atoms ⁡ K
12 8 5 atbase ⊢ p ∈ Atoms ⁡ K → p ∈ Base K
13 11 12 syl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ K W → p ∈ Base K
14 f1ocnvfv1 ⊢ F : Base K ⟶ 1-1 onto Base K ∧ p ∈ Base K → F -1 ⁡ F ⁡ p = p
15 10 13 14 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ K W → F -1 ⁡ F ⁡ p = p
16 15 oveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ K W → F ⁡ p join ⁡ K F -1 ⁡ F ⁡ p = F ⁡ p join ⁡ K p
17 simp1l ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ K W → K ∈ HL
18 4 5 1 2 ltrnat ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ p ∈ Atoms ⁡ K → F ⁡ p ∈ Atoms ⁡ K
19 18 3adant3r ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ K W → F ⁡ p ∈ Atoms ⁡ K
20 eqid ⊢ join ⁡ K = join ⁡ K
21 20 5 hlatjcom ⊢ K ∈ HL ∧ F ⁡ p ∈ Atoms ⁡ K ∧ p ∈ Atoms ⁡ K → F ⁡ p join ⁡ K p = p join ⁡ K F ⁡ p
22 17 19 11 21 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ K W → F ⁡ p join ⁡ K p = p join ⁡ K F ⁡ p
23 16 22 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ K W → F ⁡ p join ⁡ K F -1 ⁡ F ⁡ p = p join ⁡ K F ⁡ p
24 23 oveq1d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ K W → F ⁡ p join ⁡ K F -1 ⁡ F ⁡ p meet ⁡ K W = p join ⁡ K F ⁡ p meet ⁡ K W
25 simp1 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ K W → K ∈ HL ∧ W ∈ H
26 1 2 ltrncnv ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T → F -1 ∈ T
27 26 3adant3 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ K W → F -1 ∈ T
28 4 5 1 2 ltrnel ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ K W → F ⁡ p ∈ Atoms ⁡ K ∧ ¬ F ⁡ p ≤ K W
29 eqid ⊢ meet ⁡ K = meet ⁡ K
30 4 20 29 5 1 2 3 trlval2 ⊢ K ∈ HL ∧ W ∈ H ∧ F -1 ∈ T ∧ F ⁡ p ∈ Atoms ⁡ K ∧ ¬ F ⁡ p ≤ K W → R ⁡ F -1 = F ⁡ p join ⁡ K F -1 ⁡ F ⁡ p meet ⁡ K W
31 25 27 28 30 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ K W → R ⁡ F -1 = F ⁡ p join ⁡ K F -1 ⁡ F ⁡ p meet ⁡ K W
32 4 20 29 5 1 2 3 trlval2 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ K W → R ⁡ F = p join ⁡ K F ⁡ p meet ⁡ K W
33 24 31 32 3eqtr4d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ K W → R ⁡ F -1 = R ⁡ F
34 33 3expa ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ K W → R ⁡ F -1 = R ⁡ F
35 7 34 rexlimddv ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T → R ⁡ F -1 = R ⁡ F