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 Base K = Base K
11 10 2 atbase F -1 P A F -1 P Base K
12 6 11 syl K HL W H F T P A ¬ P ˙ W F -1 P Base K
13 simp1r K HL W H F T P A ¬ P ˙ W W H
14 10 3 lhpbase W H W Base K
15 13 14 syl K HL W H F T P A ¬ P ˙ W W Base K
16 10 1 3 4 ltrnle K HL W H F T F -1 P Base K W Base K 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 : Base K 1-1 onto Base K
19 18 3adant3 K HL W H F T P A ¬ P ˙ W F : Base K 1-1 onto Base K
20 simp3l K HL W H F T P A ¬ P ˙ W P A
21 10 2 atbase P A P Base K
22 20 21 syl K HL W H F T P A ¬ P ˙ W P Base K
23 f1ocnvfv2 F : Base K 1-1 onto Base K P Base K 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 Base K 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 Base K 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