Metamath Proof Explorer

Theorem dia2dimlem1

Description: Lemma for dia2dim . Show properties of the auxiliary atom Q . Part of proof of Lemma M in Crawley p. 121 line 3. (Contributed by NM, 8-Sep-2014)

Ref Expression
Hypotheses dia2dimlem1.l ⊢ ≤ = ( le ‘ 𝐾 )
dia2dimlem1.j ⊢ ∨ = ( join ‘ 𝐾 )
dia2dimlem1.m ⊢ ∧ = ( meet ‘ 𝐾 )
dia2dimlem1.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
dia2dimlem1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dia2dimlem1.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dia2dimlem1.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
dia2dimlem1.q ⊢ 𝑄 = ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) )
dia2dimlem1.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dia2dimlem1.u ⊢ ( 𝜑 → ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) )
dia2dimlem1.v ⊢ ( 𝜑 → ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) )
dia2dimlem1.p ⊢ ( 𝜑 → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
dia2dimlem1.f ⊢ ( 𝜑 → ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) )
dia2dimlem1.rf ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑈 ∨ 𝑉 ) )
dia2dimlem1.uv ⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
dia2dimlem1.ru ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≠ 𝑈 )
Assertion dia2dimlem1 ( 𝜑 → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )

Proof

Step Hyp Ref Expression
1 dia2dimlem1.l ⊢ ≤ = ( le ‘ 𝐾 )
2 dia2dimlem1.j ⊢ ∨ = ( join ‘ 𝐾 )
3 dia2dimlem1.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 dia2dimlem1.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 dia2dimlem1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 dia2dimlem1.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
7 dia2dimlem1.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
8 dia2dimlem1.q ⊢ 𝑄 = ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) )
9 dia2dimlem1.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10 dia2dimlem1.u ⊢ ( 𝜑 → ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) )
11 dia2dimlem1.v ⊢ ( 𝜑 → ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) )
12 dia2dimlem1.p ⊢ ( 𝜑 → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
13 dia2dimlem1.f ⊢ ( 𝜑 → ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) )
14 dia2dimlem1.rf ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑈 ∨ 𝑉 ) )
15 dia2dimlem1.uv ⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
16 dia2dimlem1.ru ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≠ 𝑈 )
17 9 simpld ⊢ ( 𝜑 → 𝐾 ∈ HL )
18 12 simpld ⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
19 1 4 5 6 7 trlat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) ) → ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 )
20 9 12 13 19 syl3anc ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 )
21 10 simpld ⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
22 13 simpld ⊢ ( 𝜑 → 𝐹 ∈ 𝑇 )
23 1 4 5 6 ltrnel ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑃 ) ≤ 𝑊 ) )
24 9 22 12 23 syl3anc ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑃 ) ≤ 𝑊 ) )
25 24 simpld ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 )
26 11 simpld ⊢ ( 𝜑 → 𝑉 ∈ 𝐴 )
27 12 simprd ⊢ ( 𝜑 → ¬ 𝑃 ≤ 𝑊 )
28 1 5 6 7 trlle ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) ≤ 𝑊 )
29 9 22 28 syl2anc ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≤ 𝑊 )
30 10 simprd ⊢ ( 𝜑 → 𝑈 ≤ 𝑊 )
31 17 hllatd ⊢ ( 𝜑 → 𝐾 ∈ Lat )
32 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
33 32 4 atbase ⊢ ( ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 → ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) )
34 20 33 syl ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) )
35 32 4 atbase ⊢ ( 𝑈 ∈ 𝐴 → 𝑈 ∈ ( Base ‘ 𝐾 ) )
36 21 35 syl ⊢ ( 𝜑 → 𝑈 ∈ ( Base ‘ 𝐾 ) )
37 9 simprd ⊢ ( 𝜑 → 𝑊 ∈ 𝐻 )
38 32 5 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
39 37 38 syl ⊢ ( 𝜑 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
40 32 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑅 ‘ 𝐹 ) ≤ 𝑊 ∧ 𝑈 ≤ 𝑊 ) ↔ ( ( 𝑅 ‘ 𝐹 ) ∨ 𝑈 ) ≤ 𝑊 ) )
41 31 34 36 39 40 syl13anc ⊢ ( 𝜑 → ( ( ( 𝑅 ‘ 𝐹 ) ≤ 𝑊 ∧ 𝑈 ≤ 𝑊 ) ↔ ( ( 𝑅 ‘ 𝐹 ) ∨ 𝑈 ) ≤ 𝑊 ) )
42 29 30 41 mpbi2and ⊢ ( 𝜑 → ( ( 𝑅 ‘ 𝐹 ) ∨ 𝑈 ) ≤ 𝑊 )
43 32 4 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
44 18 43 syl ⊢ ( 𝜑 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
45 32 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) → ( ( 𝑅 ‘ 𝐹 ) ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
46 17 20 21 45 syl3anc ⊢ ( 𝜑 → ( ( 𝑅 ‘ 𝐹 ) ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
47 32 1 lattr ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ 𝑈 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ∨ 𝑈 ) ≤ 𝑊 ) → 𝑃 ≤ 𝑊 ) )
48 31 44 46 39 47 syl13anc ⊢ ( 𝜑 → ( ( 𝑃 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ 𝑈 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ∨ 𝑈 ) ≤ 𝑊 ) → 𝑃 ≤ 𝑊 ) )
49 42 48 mpan2d ⊢ ( 𝜑 → ( 𝑃 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ 𝑈 ) → 𝑃 ≤ 𝑊 ) )
50 27 49 mtod ⊢ ( 𝜑 → ¬ 𝑃 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ 𝑈 ) )
51 11 simprd ⊢ ( 𝜑 → 𝑉 ≤ 𝑊 )
52 24 simprd ⊢ ( 𝜑 → ¬ ( 𝐹 ‘ 𝑃 ) ≤ 𝑊 )
53 nbrne2 ⊢ ( ( 𝑉 ≤ 𝑊 ∧ ¬ ( 𝐹 ‘ 𝑃 ) ≤ 𝑊 ) → 𝑉 ≠ ( 𝐹 ‘ 𝑃 ) )
54 51 52 53 syl2anc ⊢ ( 𝜑 → 𝑉 ≠ ( 𝐹 ‘ 𝑃 ) )
55 54 necomd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) ≠ 𝑉 )
56 50 55 jca ⊢ ( 𝜑 → ( ¬ 𝑃 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ 𝑈 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑉 ) )
57 31 adantr ⊢ ( ( 𝜑 ∧ ( 𝑃 ∨ 𝑈 ) = ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) → 𝐾 ∈ Lat )
58 44 adantr ⊢ ( ( 𝜑 ∧ ( 𝑃 ∨ 𝑈 ) = ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
59 32 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑉 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) → ( 𝑉 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
60 17 26 21 59 syl3anc ⊢ ( 𝜑 → ( 𝑉 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
61 60 adantr ⊢ ( ( 𝜑 ∧ ( 𝑃 ∨ 𝑈 ) = ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) → ( 𝑉 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
62 39 adantr ⊢ ( ( 𝜑 ∧ ( 𝑃 ∨ 𝑈 ) = ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
63 1 2 4 hlatlej2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) → 𝑉 ≤ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) )
64 17 25 26 63 syl3anc ⊢ ( 𝜑 → 𝑉 ≤ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) )
65 64 adantr ⊢ ( ( 𝜑 ∧ ( 𝑃 ∨ 𝑈 ) = ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) → 𝑉 ≤ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) )
66 simpr ⊢ ( ( 𝜑 ∧ ( 𝑃 ∨ 𝑈 ) = ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) → ( 𝑃 ∨ 𝑈 ) = ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) )
67 65 66 breqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑃 ∨ 𝑈 ) = ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) → 𝑉 ≤ ( 𝑃 ∨ 𝑈 ) )
68 15 necomd ⊢ ( 𝜑 → 𝑉 ≠ 𝑈 )
69 1 2 4 hlatexch2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ 𝑉 ≠ 𝑈 ) → ( 𝑉 ≤ ( 𝑃 ∨ 𝑈 ) → 𝑃 ≤ ( 𝑉 ∨ 𝑈 ) ) )
70 17 26 18 21 68 69 syl131anc ⊢ ( 𝜑 → ( 𝑉 ≤ ( 𝑃 ∨ 𝑈 ) → 𝑃 ≤ ( 𝑉 ∨ 𝑈 ) ) )
71 70 adantr ⊢ ( ( 𝜑 ∧ ( 𝑃 ∨ 𝑈 ) = ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) → ( 𝑉 ≤ ( 𝑃 ∨ 𝑈 ) → 𝑃 ≤ ( 𝑉 ∨ 𝑈 ) ) )
72 67 71 mpd ⊢ ( ( 𝜑 ∧ ( 𝑃 ∨ 𝑈 ) = ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) → 𝑃 ≤ ( 𝑉 ∨ 𝑈 ) )
73 32 4 atbase ⊢ ( 𝑉 ∈ 𝐴 → 𝑉 ∈ ( Base ‘ 𝐾 ) )
74 26 73 syl ⊢ ( 𝜑 → 𝑉 ∈ ( Base ‘ 𝐾 ) )
75 32 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑉 ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑉 ≤ 𝑊 ∧ 𝑈 ≤ 𝑊 ) ↔ ( 𝑉 ∨ 𝑈 ) ≤ 𝑊 ) )
76 31 74 36 39 75 syl13anc ⊢ ( 𝜑 → ( ( 𝑉 ≤ 𝑊 ∧ 𝑈 ≤ 𝑊 ) ↔ ( 𝑉 ∨ 𝑈 ) ≤ 𝑊 ) )
77 51 30 76 mpbi2and ⊢ ( 𝜑 → ( 𝑉 ∨ 𝑈 ) ≤ 𝑊 )
78 77 adantr ⊢ ( ( 𝜑 ∧ ( 𝑃 ∨ 𝑈 ) = ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) → ( 𝑉 ∨ 𝑈 ) ≤ 𝑊 )
79 32 1 57 58 61 62 72 78 lattrd ⊢ ( ( 𝜑 ∧ ( 𝑃 ∨ 𝑈 ) = ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) → 𝑃 ≤ 𝑊 )
80 79 ex ⊢ ( 𝜑 → ( ( 𝑃 ∨ 𝑈 ) = ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) → 𝑃 ≤ 𝑊 ) )
81 80 necon3bd ⊢ ( 𝜑 → ( ¬ 𝑃 ≤ 𝑊 → ( 𝑃 ∨ 𝑈 ) ≠ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) )
82 27 81 mpd ⊢ ( 𝜑 → ( 𝑃 ∨ 𝑈 ) ≠ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) )
83 1 2 4 hlatlej2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ) → ( 𝐹 ‘ 𝑃 ) ≤ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) )
84 17 18 25 83 syl3anc ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) ≤ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) )
85 1 2 3 4 5 6 7 trlval2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑅 ‘ 𝐹 ) = ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) )
86 9 22 12 85 syl3anc ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) = ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) )
87 86 oveq2d ⊢ ( 𝜑 → ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) = ( 𝑃 ∨ ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) ) )
88 32 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ) → ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) )
89 17 18 25 88 syl3anc ⊢ ( 𝜑 → ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) )
90 1 2 4 hlatlej1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ) → 𝑃 ≤ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) )
91 17 18 25 90 syl3anc ⊢ ( 𝜑 → 𝑃 ≤ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) )
92 32 1 2 3 4 atmod3i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑃 ≤ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ) → ( 𝑃 ∨ ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) ) = ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ ( 𝑃 ∨ 𝑊 ) ) )
93 17 18 89 39 91 92 syl131anc ⊢ ( 𝜑 → ( 𝑃 ∨ ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) ) = ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ ( 𝑃 ∨ 𝑊 ) ) )
94 eqid ⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
95 1 2 94 4 5 lhpjat2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
96 9 12 95 syl2anc ⊢ ( 𝜑 → ( 𝑃 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
97 96 oveq2d ⊢ ( 𝜑 → ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ ( 𝑃 ∨ 𝑊 ) ) = ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ ( 1. ‘ 𝐾 ) ) )
98 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
99 17 98 syl ⊢ ( 𝜑 → 𝐾 ∈ OL )
100 32 3 94 olm11 ⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) )
101 99 89 100 syl2anc ⊢ ( 𝜑 → ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) )
102 97 101 eqtrd ⊢ ( 𝜑 → ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ ( 𝑃 ∨ 𝑊 ) ) = ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) )
103 93 102 eqtrd ⊢ ( 𝜑 → ( 𝑃 ∨ ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) ) = ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) )
104 87 103 eqtrd ⊢ ( 𝜑 → ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) = ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) )
105 84 104 breqtrrd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) )
106 2 4 hlatjcom ⊢ ( ( 𝐾 ∈ HL ∧ 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) → ( 𝑈 ∨ 𝑉 ) = ( 𝑉 ∨ 𝑈 ) )
107 17 21 26 106 syl3anc ⊢ ( 𝜑 → ( 𝑈 ∨ 𝑉 ) = ( 𝑉 ∨ 𝑈 ) )
108 14 107 breqtrd ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑉 ∨ 𝑈 ) )
109 1 2 4 hlatexch2 ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 𝑈 ) → ( ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑉 ∨ 𝑈 ) → 𝑉 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ 𝑈 ) ) )
110 17 20 26 21 16 109 syl131anc ⊢ ( 𝜑 → ( ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑉 ∨ 𝑈 ) → 𝑉 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ 𝑈 ) ) )
111 108 110 mpd ⊢ ( 𝜑 → 𝑉 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ 𝑈 ) )
112 105 111 jca ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑃 ) ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ 𝑉 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ 𝑈 ) ) )
113 1 2 3 4 ps-2c ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( ( ¬ 𝑃 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ 𝑈 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑉 ) ∧ ( 𝑃 ∨ 𝑈 ) ≠ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ 𝑉 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ 𝑈 ) ) ) ) → ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ∈ 𝐴 )
114 17 18 20 21 25 26 56 82 112 113 syl333anc ⊢ ( 𝜑 → ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ∈ 𝐴 )
115 8 114 eqeltrid ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
116 32 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
117 17 18 21 116 syl3anc ⊢ ( 𝜑 → ( 𝑃 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
118 32 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) )
119 17 25 26 118 syl3anc ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) )
120 32 1 3 latmle1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ≤ ( 𝑃 ∨ 𝑈 ) )
121 31 117 119 120 syl3anc ⊢ ( 𝜑 → ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ≤ ( 𝑃 ∨ 𝑈 ) )
122 8 121 eqbrtrid ⊢ ( 𝜑 → 𝑄 ≤ ( 𝑃 ∨ 𝑈 ) )
123 32 4 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
124 115 123 syl ⊢ ( 𝜑 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
125 32 1 3 latlem12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑄 ≤ ( 𝑃 ∨ 𝑈 ) ∧ 𝑄 ≤ 𝑊 ) ↔ 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∧ 𝑊 ) ) )
126 31 124 117 39 125 syl13anc ⊢ ( 𝜑 → ( ( 𝑄 ≤ ( 𝑃 ∨ 𝑈 ) ∧ 𝑄 ≤ 𝑊 ) ↔ 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∧ 𝑊 ) ) )
127 126 biimpd ⊢ ( 𝜑 → ( ( 𝑄 ≤ ( 𝑃 ∨ 𝑈 ) ∧ 𝑄 ≤ 𝑊 ) → 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∧ 𝑊 ) ) )
128 122 127 mpand ⊢ ( 𝜑 → ( 𝑄 ≤ 𝑊 → 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∧ 𝑊 ) ) )
129 128 imp ⊢ ( ( 𝜑 ∧ 𝑄 ≤ 𝑊 ) → 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∧ 𝑊 ) )
130 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
131 1 3 130 4 5 lhpmat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∧ 𝑊 ) = ( 0. ‘ 𝐾 ) )
132 9 12 131 syl2anc ⊢ ( 𝜑 → ( 𝑃 ∧ 𝑊 ) = ( 0. ‘ 𝐾 ) )
133 132 oveq1d ⊢ ( 𝜑 → ( ( 𝑃 ∧ 𝑊 ) ∨ 𝑈 ) = ( ( 0. ‘ 𝐾 ) ∨ 𝑈 ) )
134 32 1 2 3 4 atmod4i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑈 ≤ 𝑊 ) → ( ( 𝑃 ∧ 𝑊 ) ∨ 𝑈 ) = ( ( 𝑃 ∨ 𝑈 ) ∧ 𝑊 ) )
135 17 21 44 39 30 134 syl131anc ⊢ ( 𝜑 → ( ( 𝑃 ∧ 𝑊 ) ∨ 𝑈 ) = ( ( 𝑃 ∨ 𝑈 ) ∧ 𝑊 ) )
136 32 2 130 olj02 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ) → ( ( 0. ‘ 𝐾 ) ∨ 𝑈 ) = 𝑈 )
137 99 36 136 syl2anc ⊢ ( 𝜑 → ( ( 0. ‘ 𝐾 ) ∨ 𝑈 ) = 𝑈 )
138 133 135 137 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑃 ∨ 𝑈 ) ∧ 𝑊 ) = 𝑈 )
139 138 adantr ⊢ ( ( 𝜑 ∧ 𝑄 ≤ 𝑊 ) → ( ( 𝑃 ∨ 𝑈 ) ∧ 𝑊 ) = 𝑈 )
140 129 139 breqtrd ⊢ ( ( 𝜑 ∧ 𝑄 ≤ 𝑊 ) → 𝑄 ≤ 𝑈 )
141 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
142 17 141 syl ⊢ ( 𝜑 → 𝐾 ∈ AtLat )
143 142 adantr ⊢ ( ( 𝜑 ∧ 𝑄 ≤ 𝑊 ) → 𝐾 ∈ AtLat )
144 115 adantr ⊢ ( ( 𝜑 ∧ 𝑄 ≤ 𝑊 ) → 𝑄 ∈ 𝐴 )
145 21 adantr ⊢ ( ( 𝜑 ∧ 𝑄 ≤ 𝑊 ) → 𝑈 ∈ 𝐴 )
146 1 4 atcmp ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑄 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) → ( 𝑄 ≤ 𝑈 ↔ 𝑄 = 𝑈 ) )
147 143 144 145 146 syl3anc ⊢ ( ( 𝜑 ∧ 𝑄 ≤ 𝑊 ) → ( 𝑄 ≤ 𝑈 ↔ 𝑄 = 𝑈 ) )
148 140 147 mpbid ⊢ ( ( 𝜑 ∧ 𝑄 ≤ 𝑊 ) → 𝑄 = 𝑈 )
149 32 1 3 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ≤ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) )
150 31 117 119 149 syl3anc ⊢ ( 𝜑 → ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ≤ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) )
151 8 150 eqbrtrid ⊢ ( 𝜑 → 𝑄 ≤ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) )
152 32 1 3 latlem12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑄 ≤ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ∧ 𝑄 ≤ 𝑊 ) ↔ 𝑄 ≤ ( ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ∧ 𝑊 ) ) )
153 31 124 119 39 152 syl13anc ⊢ ( 𝜑 → ( ( 𝑄 ≤ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ∧ 𝑄 ≤ 𝑊 ) ↔ 𝑄 ≤ ( ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ∧ 𝑊 ) ) )
154 153 biimpd ⊢ ( 𝜑 → ( ( 𝑄 ≤ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ∧ 𝑄 ≤ 𝑊 ) → 𝑄 ≤ ( ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ∧ 𝑊 ) ) )
155 151 154 mpand ⊢ ( 𝜑 → ( 𝑄 ≤ 𝑊 → 𝑄 ≤ ( ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ∧ 𝑊 ) ) )
156 155 imp ⊢ ( ( 𝜑 ∧ 𝑄 ≤ 𝑊 ) → 𝑄 ≤ ( ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ∧ 𝑊 ) )
157 1 3 130 4 5 lhpmat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑃 ) ≤ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∧ 𝑊 ) = ( 0. ‘ 𝐾 ) )
158 9 24 157 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑃 ) ∧ 𝑊 ) = ( 0. ‘ 𝐾 ) )
159 158 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑃 ) ∧ 𝑊 ) ∨ 𝑉 ) = ( ( 0. ‘ 𝐾 ) ∨ 𝑉 ) )
160 32 4 atbase ⊢ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 → ( 𝐹 ‘ 𝑃 ) ∈ ( Base ‘ 𝐾 ) )
161 25 160 syl ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) ∈ ( Base ‘ 𝐾 ) )
162 32 1 2 3 4 atmod4i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑉 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑃 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑉 ≤ 𝑊 ) → ( ( ( 𝐹 ‘ 𝑃 ) ∧ 𝑊 ) ∨ 𝑉 ) = ( ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ∧ 𝑊 ) )
163 17 26 161 39 51 162 syl131anc ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑃 ) ∧ 𝑊 ) ∨ 𝑉 ) = ( ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ∧ 𝑊 ) )
164 32 2 130 olj02 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑉 ∈ ( Base ‘ 𝐾 ) ) → ( ( 0. ‘ 𝐾 ) ∨ 𝑉 ) = 𝑉 )
165 99 74 164 syl2anc ⊢ ( 𝜑 → ( ( 0. ‘ 𝐾 ) ∨ 𝑉 ) = 𝑉 )
166 159 163 165 3eqtr3d ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ∧ 𝑊 ) = 𝑉 )
167 166 adantr ⊢ ( ( 𝜑 ∧ 𝑄 ≤ 𝑊 ) → ( ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ∧ 𝑊 ) = 𝑉 )
168 156 167 breqtrd ⊢ ( ( 𝜑 ∧ 𝑄 ≤ 𝑊 ) → 𝑄 ≤ 𝑉 )
169 26 adantr ⊢ ( ( 𝜑 ∧ 𝑄 ≤ 𝑊 ) → 𝑉 ∈ 𝐴 )
170 1 4 atcmp ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑄 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) → ( 𝑄 ≤ 𝑉 ↔ 𝑄 = 𝑉 ) )
171 143 144 169 170 syl3anc ⊢ ( ( 𝜑 ∧ 𝑄 ≤ 𝑊 ) → ( 𝑄 ≤ 𝑉 ↔ 𝑄 = 𝑉 ) )
172 168 171 mpbid ⊢ ( ( 𝜑 ∧ 𝑄 ≤ 𝑊 ) → 𝑄 = 𝑉 )
173 148 172 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑄 ≤ 𝑊 ) → 𝑈 = 𝑉 )
174 173 ex ⊢ ( 𝜑 → ( 𝑄 ≤ 𝑊 → 𝑈 = 𝑉 ) )
175 174 necon3ad ⊢ ( 𝜑 → ( 𝑈 ≠ 𝑉 → ¬ 𝑄 ≤ 𝑊 ) )
176 15 175 mpd ⊢ ( 𝜑 → ¬ 𝑄 ≤ 𝑊 )
177 115 176 jca ⊢ ( 𝜑 → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )