Metamath Proof Explorer

Theorem llnexchb2lem

Description: Lemma for llnexchb2 . (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 llnexchb2lem ( ( ( 𝐾 ∈ 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 simpl11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝐾 ∈ HL )
7 simpl21 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑃 ∈ 𝐴 )
8 simpl12 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑋 ∈ 𝑁 )
9 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
10 9 5 llnbase ⊢ ( 𝑋 ∈ 𝑁 → 𝑋 ∈ ( Base ‘ 𝐾 ) )
11 8 10 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
12 6 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝐾 ∈ Lat )
13 simpl13 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑌 ∈ 𝑁 )
14 9 5 llnbase ⊢ ( 𝑌 ∈ 𝑁 → 𝑌 ∈ ( Base ‘ 𝐾 ) )
15 13 14 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑌 ∈ ( Base ‘ 𝐾 ) )
16 9 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
17 12 11 15 16 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
18 9 1 3 latmle1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 )
19 12 11 15 18 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 )
20 9 1 2 3 4 atmod2i2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 ) → ( ( 𝑋 ∧ 𝑃 ) ∨ ( 𝑋 ∧ 𝑌 ) ) = ( 𝑋 ∧ ( 𝑃 ∨ ( 𝑋 ∧ 𝑌 ) ) ) )
21 6 7 11 17 19 20 syl131anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑋 ∧ 𝑃 ) ∨ ( 𝑋 ∧ 𝑌 ) ) = ( 𝑋 ∧ ( 𝑃 ∨ ( 𝑋 ∧ 𝑌 ) ) ) )
22 9 4 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
23 7 22 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
24 9 3 latmcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ∧ 𝑃 ) = ( 𝑃 ∧ 𝑋 ) )
25 12 11 23 24 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑋 ∧ 𝑃 ) = ( 𝑃 ∧ 𝑋 ) )
26 simpl23 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → ¬ 𝑃 ≤ 𝑋 )
27 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
28 6 27 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝐾 ∈ AtLat )
29 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
30 9 1 3 29 4 atnle ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ) → ( ¬ 𝑃 ≤ 𝑋 ↔ ( 𝑃 ∧ 𝑋 ) = ( 0. ‘ 𝐾 ) ) )
31 28 7 11 30 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ¬ 𝑃 ≤ 𝑋 ↔ ( 𝑃 ∧ 𝑋 ) = ( 0. ‘ 𝐾 ) ) )
32 26 31 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑃 ∧ 𝑋 ) = ( 0. ‘ 𝐾 ) )
33 25 32 eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑋 ∧ 𝑃 ) = ( 0. ‘ 𝐾 ) )
34 33 oveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑋 ∧ 𝑃 ) ∨ ( 𝑋 ∧ 𝑌 ) ) = ( ( 0. ‘ 𝐾 ) ∨ ( 𝑋 ∧ 𝑌 ) ) )
35 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) )
36 hlcvl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ CvLat )
37 6 36 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝐾 ∈ CvLat )
38 simpl3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 )
39 simpl22 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑄 ∈ 𝐴 )
40 breq1 ⊢ ( 𝑃 = ( 𝑋 ∧ 𝑌 ) → ( 𝑃 ≤ 𝑋 ↔ ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 ) )
41 19 40 syl5ibrcom ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑃 = ( 𝑋 ∧ 𝑌 ) → 𝑃 ≤ 𝑋 ) )
42 41 necon3bd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ¬ 𝑃 ≤ 𝑋 → 𝑃 ≠ ( 𝑋 ∧ 𝑌 ) ) )
43 26 42 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑃 ≠ ( 𝑋 ∧ 𝑌 ) )
44 43 necomd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑋 ∧ 𝑌 ) ≠ 𝑃 )
45 1 2 4 cvlatexchb1 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≠ 𝑃 ) → ( ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ↔ ( 𝑃 ∨ ( 𝑋 ∧ 𝑌 ) ) = ( 𝑃 ∨ 𝑄 ) ) )
46 37 38 39 7 44 45 syl131anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ↔ ( 𝑃 ∨ ( 𝑋 ∧ 𝑌 ) ) = ( 𝑃 ∨ 𝑄 ) ) )
47 35 46 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑃 ∨ ( 𝑋 ∧ 𝑌 ) ) = ( 𝑃 ∨ 𝑄 ) )
48 47 oveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑋 ∧ ( 𝑃 ∨ ( 𝑋 ∧ 𝑌 ) ) ) = ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) )
49 21 34 48 3eqtr3rd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) = ( ( 0. ‘ 𝐾 ) ∨ ( 𝑋 ∧ 𝑌 ) ) )
50 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
51 6 50 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝐾 ∈ OL )
52 9 2 29 olj02 ⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑋 ∧ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 0. ‘ 𝐾 ) ∨ ( 𝑋 ∧ 𝑌 ) ) = ( 𝑋 ∧ 𝑌 ) )
53 51 17 52 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 0. ‘ 𝐾 ) ∨ ( 𝑋 ∧ 𝑌 ) ) = ( 𝑋 ∧ 𝑌 ) )
54 49 53 eqtr2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) )
55 54 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → ( ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) → ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) ) )
56 simp11 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → 𝐾 ∈ HL )
57 56 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → 𝐾 ∈ Lat )
58 simp12 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → 𝑋 ∈ 𝑁 )
59 58 10 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
60 simp21 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → 𝑃 ∈ 𝐴 )
61 simp22 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → 𝑄 ∈ 𝐴 )
62 9 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
63 56 60 61 62 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
64 9 1 3 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) ≤ ( 𝑃 ∨ 𝑄 ) )
65 57 59 63 64 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) ≤ ( 𝑃 ∨ 𝑄 ) )
66 breq1 ⊢ ( ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ↔ ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ) )
67 65 66 syl5ibrcom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → ( ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ) )
68 55 67 impbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → ( ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑃 ∨ 𝑄 ) ↔ ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) ) )