Metamath Proof Explorer

Theorem llnexchb2

Description: Line exchange property (compare cvlatexchb2 for atoms). (Contributed by NM, 17-Nov-2012)

Ref Expression
Hypotheses llnexch.l ⊢ ≤ = ( le ‘ 𝐾 )
llnexch.j ⊢ ∨ = ( join ‘ 𝐾 )
llnexch.m ⊢ ∧ = ( meet ‘ 𝐾 )
llnexch.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
llnexch.n ⊢ 𝑁 = ( LLines ‘ 𝐾 )
Assertion llnexchb2 ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) → ( ( 𝑋 ∧ 𝑌 ) ≤ 𝑍 ↔ ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 llnexch.l ⊢ ≤ = ( le ‘ 𝐾 )
2 llnexch.j ⊢ ∨ = ( join ‘ 𝐾 )
3 llnexch.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 llnexch.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 llnexch.n ⊢ 𝑁 = ( LLines ‘ 𝐾 )
6 simp23 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) → 𝑍 ∈ 𝑁 )
7 simp1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) → 𝐾 ∈ HL )
8 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
9 8 5 llnbase ⊢ ( 𝑍 ∈ 𝑁 → 𝑍 ∈ ( Base ‘ 𝐾 ) )
10 6 9 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) → 𝑍 ∈ ( Base ‘ 𝐾 ) )
11 8 2 4 5 islln3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑍 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑍 ∈ 𝑁 ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ 𝑍 = ( 𝑝 ∨ 𝑞 ) ) ) )
12 7 10 11 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) → ( 𝑍 ∈ 𝑁 ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ 𝑍 = ( 𝑝 ∨ 𝑞 ) ) ) )
13 6 12 mpbid ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ 𝑍 = ( 𝑝 ∨ 𝑞 ) ) )
14 simp3r ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) → 𝑋 ≠ 𝑍 )
15 14 necomd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) → 𝑍 ≠ 𝑋 )
16 simp11 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) → 𝐾 ∈ HL )
17 16 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) → 𝐾 ∈ Lat )
18 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) → 𝑝 ∈ 𝐴 )
19 8 4 atbase ⊢ ( 𝑝 ∈ 𝐴 → 𝑝 ∈ ( Base ‘ 𝐾 ) )
20 18 19 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) → 𝑝 ∈ ( Base ‘ 𝐾 ) )
21 simp2r ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) → 𝑞 ∈ 𝐴 )
22 8 4 atbase ⊢ ( 𝑞 ∈ 𝐴 → 𝑞 ∈ ( Base ‘ 𝐾 ) )
23 21 22 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) → 𝑞 ∈ ( Base ‘ 𝐾 ) )
24 simp121 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) → 𝑋 ∈ 𝑁 )
25 8 5 llnbase ⊢ ( 𝑋 ∈ 𝑁 → 𝑋 ∈ ( Base ‘ 𝐾 ) )
26 24 25 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
27 8 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑝 ≤ 𝑋 ∧ 𝑞 ≤ 𝑋 ) ↔ ( 𝑝 ∨ 𝑞 ) ≤ 𝑋 ) )
28 17 20 23 26 27 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) → ( ( 𝑝 ≤ 𝑋 ∧ 𝑞 ≤ 𝑋 ) ↔ ( 𝑝 ∨ 𝑞 ) ≤ 𝑋 ) )
29 simp3 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) → 𝑝 ≠ 𝑞 )
30 2 4 5 llni2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) → ( 𝑝 ∨ 𝑞 ) ∈ 𝑁 )
31 16 18 21 29 30 syl31anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) → ( 𝑝 ∨ 𝑞 ) ∈ 𝑁 )
32 1 5 llncmp ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∨ 𝑞 ) ∈ 𝑁 ∧ 𝑋 ∈ 𝑁 ) → ( ( 𝑝 ∨ 𝑞 ) ≤ 𝑋 ↔ ( 𝑝 ∨ 𝑞 ) = 𝑋 ) )
33 16 31 24 32 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) → ( ( 𝑝 ∨ 𝑞 ) ≤ 𝑋 ↔ ( 𝑝 ∨ 𝑞 ) = 𝑋 ) )
34 28 33 bitr2d ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) → ( ( 𝑝 ∨ 𝑞 ) = 𝑋 ↔ ( 𝑝 ≤ 𝑋 ∧ 𝑞 ≤ 𝑋 ) ) )
35 34 necon3abid ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) → ( ( 𝑝 ∨ 𝑞 ) ≠ 𝑋 ↔ ¬ ( 𝑝 ≤ 𝑋 ∧ 𝑞 ≤ 𝑋 ) ) )
36 ianor ⊢ ( ¬ ( 𝑝 ≤ 𝑋 ∧ 𝑞 ≤ 𝑋 ) ↔ ( ¬ 𝑝 ≤ 𝑋 ∨ ¬ 𝑞 ≤ 𝑋 ) )
37 35 36 bitrdi ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) → ( ( 𝑝 ∨ 𝑞 ) ≠ 𝑋 ↔ ( ¬ 𝑝 ≤ 𝑋 ∨ ¬ 𝑞 ≤ 𝑋 ) ) )
38 simpl11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) ∧ ¬ 𝑝 ≤ 𝑋 ) → 𝐾 ∈ HL )
39 24 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) ∧ ¬ 𝑝 ≤ 𝑋 ) → 𝑋 ∈ 𝑁 )
40 simp122 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) → 𝑌 ∈ 𝑁 )
41 40 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) ∧ ¬ 𝑝 ≤ 𝑋 ) → 𝑌 ∈ 𝑁 )
42 simpl2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) ∧ ¬ 𝑝 ≤ 𝑋 ) → 𝑝 ∈ 𝐴 )
43 simpl2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) ∧ ¬ 𝑝 ≤ 𝑋 ) → 𝑞 ∈ 𝐴 )
44 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) ∧ ¬ 𝑝 ≤ 𝑋 ) → ¬ 𝑝 ≤ 𝑋 )
45 simp13l ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 )
46 45 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) ∧ ¬ 𝑝 ≤ 𝑋 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 )
47 1 2 3 4 5 llnexchb2lem ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → ( ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑝 ∨ 𝑞 ) ↔ ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ ( 𝑝 ∨ 𝑞 ) ) ) )
48 38 39 41 42 43 44 46 47 syl331anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) ∧ ¬ 𝑝 ≤ 𝑋 ) → ( ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑝 ∨ 𝑞 ) ↔ ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ ( 𝑝 ∨ 𝑞 ) ) ) )
49 48 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) → ( ¬ 𝑝 ≤ 𝑋 → ( ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑝 ∨ 𝑞 ) ↔ ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ ( 𝑝 ∨ 𝑞 ) ) ) ) )
50 simpl11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) ∧ ¬ 𝑞 ≤ 𝑋 ) → 𝐾 ∈ HL )
51 24 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) ∧ ¬ 𝑞 ≤ 𝑋 ) → 𝑋 ∈ 𝑁 )
52 40 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) ∧ ¬ 𝑞 ≤ 𝑋 ) → 𝑌 ∈ 𝑁 )
53 simpl2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) ∧ ¬ 𝑞 ≤ 𝑋 ) → 𝑞 ∈ 𝐴 )
54 simpl2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) ∧ ¬ 𝑞 ≤ 𝑋 ) → 𝑝 ∈ 𝐴 )
55 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) ∧ ¬ 𝑞 ≤ 𝑋 ) → ¬ 𝑞 ≤ 𝑋 )
56 45 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) ∧ ¬ 𝑞 ≤ 𝑋 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 )
57 1 2 3 4 5 llnexchb2lem ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → ( ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑞 ∨ 𝑝 ) ↔ ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ ( 𝑞 ∨ 𝑝 ) ) ) )
58 50 51 52 53 54 55 56 57 syl331anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) ∧ ¬ 𝑞 ≤ 𝑋 ) → ( ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑞 ∨ 𝑝 ) ↔ ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ ( 𝑞 ∨ 𝑝 ) ) ) )
59 2 4 hlatjcom ⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑝 ∨ 𝑞 ) = ( 𝑞 ∨ 𝑝 ) )
60 50 54 53 59 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) ∧ ¬ 𝑞 ≤ 𝑋 ) → ( 𝑝 ∨ 𝑞 ) = ( 𝑞 ∨ 𝑝 ) )
61 60 breq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) ∧ ¬ 𝑞 ≤ 𝑋 ) → ( ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑝 ∨ 𝑞 ) ↔ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑞 ∨ 𝑝 ) ) )
62 60 oveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) ∧ ¬ 𝑞 ≤ 𝑋 ) → ( 𝑋 ∧ ( 𝑝 ∨ 𝑞 ) ) = ( 𝑋 ∧ ( 𝑞 ∨ 𝑝 ) ) )
63 62 eqeq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) ∧ ¬ 𝑞 ≤ 𝑋 ) → ( ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ ( 𝑝 ∨ 𝑞 ) ) ↔ ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ ( 𝑞 ∨ 𝑝 ) ) ) )
64 58 61 63 3bitr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) ∧ ¬ 𝑞 ≤ 𝑋 ) → ( ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑝 ∨ 𝑞 ) ↔ ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ ( 𝑝 ∨ 𝑞 ) ) ) )
65 64 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) → ( ¬ 𝑞 ≤ 𝑋 → ( ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑝 ∨ 𝑞 ) ↔ ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ ( 𝑝 ∨ 𝑞 ) ) ) ) )
66 49 65 jaod ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) → ( ( ¬ 𝑝 ≤ 𝑋 ∨ ¬ 𝑞 ≤ 𝑋 ) → ( ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑝 ∨ 𝑞 ) ↔ ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ ( 𝑝 ∨ 𝑞 ) ) ) ) )
67 37 66 sylbid ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) → ( ( 𝑝 ∨ 𝑞 ) ≠ 𝑋 → ( ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑝 ∨ 𝑞 ) ↔ ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ ( 𝑝 ∨ 𝑞 ) ) ) ) )
68 neeq1 ⊢ ( 𝑍 = ( 𝑝 ∨ 𝑞 ) → ( 𝑍 ≠ 𝑋 ↔ ( 𝑝 ∨ 𝑞 ) ≠ 𝑋 ) )
69 breq2 ⊢ ( 𝑍 = ( 𝑝 ∨ 𝑞 ) → ( ( 𝑋 ∧ 𝑌 ) ≤ 𝑍 ↔ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑝 ∨ 𝑞 ) ) )
70 oveq2 ⊢ ( 𝑍 = ( 𝑝 ∨ 𝑞 ) → ( 𝑋 ∧ 𝑍 ) = ( 𝑋 ∧ ( 𝑝 ∨ 𝑞 ) ) )
71 70 eqeq2d ⊢ ( 𝑍 = ( 𝑝 ∨ 𝑞 ) → ( ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ 𝑍 ) ↔ ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ ( 𝑝 ∨ 𝑞 ) ) ) )
72 69 71 bibi12d ⊢ ( 𝑍 = ( 𝑝 ∨ 𝑞 ) → ( ( ( 𝑋 ∧ 𝑌 ) ≤ 𝑍 ↔ ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ 𝑍 ) ) ↔ ( ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑝 ∨ 𝑞 ) ↔ ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ ( 𝑝 ∨ 𝑞 ) ) ) ) )
73 68 72 imbi12d ⊢ ( 𝑍 = ( 𝑝 ∨ 𝑞 ) → ( ( 𝑍 ≠ 𝑋 → ( ( 𝑋 ∧ 𝑌 ) ≤ 𝑍 ↔ ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ 𝑍 ) ) ) ↔ ( ( 𝑝 ∨ 𝑞 ) ≠ 𝑋 → ( ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑝 ∨ 𝑞 ) ↔ ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ ( 𝑝 ∨ 𝑞 ) ) ) ) ) )
74 67 73 syl5ibrcom ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) → ( 𝑍 = ( 𝑝 ∨ 𝑞 ) → ( 𝑍 ≠ 𝑋 → ( ( 𝑋 ∧ 𝑌 ) ≤ 𝑍 ↔ ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ 𝑍 ) ) ) ) )
75 74 3exp ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) → ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑝 ≠ 𝑞 → ( 𝑍 = ( 𝑝 ∨ 𝑞 ) → ( 𝑍 ≠ 𝑋 → ( ( 𝑋 ∧ 𝑌 ) ≤ 𝑍 ↔ ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ 𝑍 ) ) ) ) ) ) )
76 75 imp4a ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) → ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) → ( ( 𝑝 ≠ 𝑞 ∧ 𝑍 = ( 𝑝 ∨ 𝑞 ) ) → ( 𝑍 ≠ 𝑋 → ( ( 𝑋 ∧ 𝑌 ) ≤ 𝑍 ↔ ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ 𝑍 ) ) ) ) ) )
77 76 rexlimdvv ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) → ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ 𝑍 = ( 𝑝 ∨ 𝑞 ) ) → ( 𝑍 ≠ 𝑋 → ( ( 𝑋 ∧ 𝑌 ) ≤ 𝑍 ↔ ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ 𝑍 ) ) ) ) )
78 13 15 77 mp2d ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) → ( ( 𝑋 ∧ 𝑌 ) ≤ 𝑍 ↔ ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ 𝑍 ) ) )