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 = ( le ‘ 𝐾 )
ltrnel.a 𝐴 = ( Atoms ‘ 𝐾 )
ltrnel.h 𝐻 = ( LHyp ‘ 𝐾 )
ltrnel.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion ltrncnvel ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( ( 𝐹𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐹𝑃 ) 𝑊 ) )

Proof

Step Hyp Ref Expression
1 ltrnel.l = ( le ‘ 𝐾 )
2 ltrnel.a 𝐴 = ( Atoms ‘ 𝐾 )
3 ltrnel.h 𝐻 = ( LHyp ‘ 𝐾 )
4 ltrnel.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5 1 2 3 4 ltrncnvat ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝑃𝐴 ) → ( 𝐹𝑃 ) ∈ 𝐴 )
6 5 3adant3r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝐹𝑃 ) ∈ 𝐴 )
7 simp3r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ¬ 𝑃 𝑊 )
8 simp1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
9 simp2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝐹𝑇 )
10 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
11 10 2 atbase ( ( 𝐹𝑃 ) ∈ 𝐴 → ( 𝐹𝑃 ) ∈ ( Base ‘ 𝐾 ) )
12 6 11 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝐹𝑃 ) ∈ ( Base ‘ 𝐾 ) )
13 simp1r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝑊𝐻 )
14 10 3 lhpbase ( 𝑊𝐻𝑊 ∈ ( Base ‘ 𝐾 ) )
15 13 14 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
16 10 1 3 4 ltrnle ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( ( 𝐹𝑃 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝐹𝑃 ) 𝑊 ↔ ( 𝐹 ‘ ( 𝐹𝑃 ) ) ( 𝐹𝑊 ) ) )
17 8 9 12 15 16 syl112anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( ( 𝐹𝑃 ) 𝑊 ↔ ( 𝐹 ‘ ( 𝐹𝑃 ) ) ( 𝐹𝑊 ) ) )
18 10 3 4 ltrn1o ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
19 18 3adant3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
20 simp3l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝑃𝐴 )
21 10 2 atbase ( 𝑃𝐴𝑃 ∈ ( Base ‘ 𝐾 ) )
22 20 21 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
23 f1ocnvfv2 ( ( 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ) → ( 𝐹 ‘ ( 𝐹𝑃 ) ) = 𝑃 )
24 19 22 23 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝐹 ‘ ( 𝐹𝑃 ) ) = 𝑃 )
25 simp1l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝐾 ∈ HL )
26 25 hllatd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝐾 ∈ Lat )
27 10 1 latref ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → 𝑊 𝑊 )
28 26 15 27 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝑊 𝑊 )
29 10 1 3 4 ltrnval1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑊 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 𝑊 ) ) → ( 𝐹𝑊 ) = 𝑊 )
30 8 9 15 28 29 syl112anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝐹𝑊 ) = 𝑊 )
31 24 30 breq12d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( ( 𝐹 ‘ ( 𝐹𝑃 ) ) ( 𝐹𝑊 ) ↔ 𝑃 𝑊 ) )
32 17 31 bitrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( ( 𝐹𝑃 ) 𝑊𝑃 𝑊 ) )
33 7 32 mtbird ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ¬ ( 𝐹𝑃 ) 𝑊 )
34 6 33 jca ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( ( 𝐹𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐹𝑃 ) 𝑊 ) )