Metamath Proof Explorer

Theorem ltrncnvel

Description: The converse of the lattice translation of an atom not under the fiducial co-atom. (Contributed by NM, 10-May-2013)

Ref Expression
Hypotheses ltrnel.l ⊢≤˙=≤K
ltrnel.a ⊢A=Atoms⁡K
ltrnel.h ⊢H=LHyp⁡K
ltrnel.t ⊢T=LTrn⁡K⁡W
Assertion ltrncnvel ⊢K∈HL∧W∈H∧F∈T∧P∈A∧¬P≤˙W→F-1⁡P∈A∧¬F-1⁡P≤˙W

Proof

Step Hyp Ref Expression
1 ltrnel.l ⊢≤˙=≤K
2 ltrnel.a ⊢A=Atoms⁡K
3 ltrnel.h ⊢H=LHyp⁡K
4 ltrnel.t ⊢T=LTrn⁡K⁡W
5 1 2 3 4 ltrncnvat ⊢K∈HL∧W∈H∧F∈T∧P∈A→F-1⁡P∈A
6 5 3adant3r ⊢K∈HL∧W∈H∧F∈T∧P∈A∧¬P≤˙W→F-1⁡P∈A
7 simp3r ⊢K∈HL∧W∈H∧F∈T∧P∈A∧¬P≤˙W→¬P≤˙W
8 simp1 ⊢K∈HL∧W∈H∧F∈T∧P∈A∧¬P≤˙W→K∈HL∧W∈H
9 simp2 ⊢K∈HL∧W∈H∧F∈T∧P∈A∧¬P≤˙W→F∈T
10 eqid ⊢BaseK=BaseK
11 10 2 atbase ⊢F-1⁡P∈A→F-1⁡P∈BaseK
12 6 11 syl ⊢K∈HL∧W∈H∧F∈T∧P∈A∧¬P≤˙W→F-1⁡P∈BaseK
13 simp1r ⊢K∈HL∧W∈H∧F∈T∧P∈A∧¬P≤˙W→W∈H
14 10 3 lhpbase ⊢W∈H→W∈BaseK
15 13 14 syl ⊢K∈HL∧W∈H∧F∈T∧P∈A∧¬P≤˙W→W∈BaseK
16 10 1 3 4 ltrnle ⊢K∈HL∧W∈H∧F∈T∧F-1⁡P∈BaseK∧W∈BaseK→F-1⁡P≤˙W↔F⁡F-1⁡P≤˙F⁡W
17 8 9 12 15 16 syl112anc ⊢K∈HL∧W∈H∧F∈T∧P∈A∧¬P≤˙W→F-1⁡P≤˙W↔F⁡F-1⁡P≤˙F⁡W
18 10 3 4 ltrn1o ⊢K∈HL∧W∈H∧F∈T→F:BaseK⟶1-1 ontoBaseK
19 18 3adant3 ⊢K∈HL∧W∈H∧F∈T∧P∈A∧¬P≤˙W→F:BaseK⟶1-1 ontoBaseK
20 simp3l ⊢K∈HL∧W∈H∧F∈T∧P∈A∧¬P≤˙W→P∈A
21 10 2 atbase ⊢P∈A→P∈BaseK
22 20 21 syl ⊢K∈HL∧W∈H∧F∈T∧P∈A∧¬P≤˙W→P∈BaseK
23 f1ocnvfv2 ⊢F:BaseK⟶1-1 ontoBaseK∧P∈BaseK→F⁡F-1⁡P=P
24 19 22 23 syl2anc ⊢K∈HL∧W∈H∧F∈T∧P∈A∧¬P≤˙W→F⁡F-1⁡P=P
25 simp1l ⊢K∈HL∧W∈H∧F∈T∧P∈A∧¬P≤˙W→K∈HL
26 25 hllatd ⊢K∈HL∧W∈H∧F∈T∧P∈A∧¬P≤˙W→K∈Lat
27 10 1 latref ⊢K∈Lat∧W∈BaseK→W≤˙W
28 26 15 27 syl2anc ⊢K∈HL∧W∈H∧F∈T∧P∈A∧¬P≤˙W→W≤˙W
29 10 1 3 4 ltrnval1 ⊢K∈HL∧W∈H∧F∈T∧W∈BaseK∧W≤˙W→F⁡W=W
30 8 9 15 28 29 syl112anc ⊢K∈HL∧W∈H∧F∈T∧P∈A∧¬P≤˙W→F⁡W=W
31 24 30 breq12d ⊢K∈HL∧W∈H∧F∈T∧P∈A∧¬P≤˙W→F⁡F-1⁡P≤˙F⁡W↔P≤˙W
32 17 31 bitrd ⊢K∈HL∧W∈H∧F∈T∧P∈A∧¬P≤˙W→F-1⁡P≤˙W↔P≤˙W
33 7 32 mtbird ⊢K∈HL∧W∈H∧F∈T∧P∈A∧¬P≤˙W→¬F-1⁡P≤˙W
34 6 33 jca ⊢K∈HL∧W∈H∧F∈T∧P∈A∧¬P≤˙W→F-1⁡P∈A∧¬F-1⁡P≤˙W