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