Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lhp2lt Structured version   Visualization version   GIF version

Theorem lhp2lt 35889
Description: The join of two atoms under a co-atom is strictly less than it. (Contributed by NM, 8-Jul-2013.)
Hypotheses
Ref Expression
lhp2lt.l = (le‘𝐾)
lhp2lt.s < = (lt‘𝐾)
lhp2lt.j = (join‘𝐾)
lhp2lt.a 𝐴 = (Atoms‘𝐾)
lhp2lt.h 𝐻 = (LHyp‘𝐾)
Assertion
Ref Expression
lhp2lt (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) → (𝑃 𝑄) < 𝑊)

Proof of Theorem lhp2lt
Dummy variables 𝑠 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp2r 1257 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) → 𝑃 𝑊)
2 simp3r 1259 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) → 𝑄 𝑊)
3 simp1l 1254 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) → 𝐾 ∈ HL)
43hllatd 35252 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) → 𝐾 ∈ Lat)
5 simp2l 1256 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) → 𝑃𝐴)
6 eqid 2764 . . . . . 6 (Base‘𝐾) = (Base‘𝐾)
7 lhp2lt.a . . . . . 6 𝐴 = (Atoms‘𝐾)
86, 7atbase 35177 . . . . 5 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
95, 8syl 17 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) → 𝑃 ∈ (Base‘𝐾))
10 simp3l 1258 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) → 𝑄𝐴)
116, 7atbase 35177 . . . . 5 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
1210, 11syl 17 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) → 𝑄 ∈ (Base‘𝐾))
13 simp1r 1255 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) → 𝑊𝐻)
14 lhp2lt.h . . . . . 6 𝐻 = (LHyp‘𝐾)
156, 14lhpbase 35886 . . . . 5 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
1613, 15syl 17 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) → 𝑊 ∈ (Base‘𝐾))
17 lhp2lt.l . . . . 5 = (le‘𝐾)
18 lhp2lt.j . . . . 5 = (join‘𝐾)
196, 17, 18latjle12 17329 . . . 4 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑃 𝑊𝑄 𝑊) ↔ (𝑃 𝑄) 𝑊))
204, 9, 12, 16, 19syl13anc 1491 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) → ((𝑃 𝑊𝑄 𝑊) ↔ (𝑃 𝑄) 𝑊))
211, 2, 20mpbi2and 703 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) → (𝑃 𝑄) 𝑊)
2218, 17, 73dim2 35356 . . . 4 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → ∃𝑟𝐴𝑠𝐴𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)))
233, 5, 10, 22syl3anc 1490 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) → ∃𝑟𝐴𝑠𝐴𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)))
24 simp11l 1383 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ (𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟))) → 𝐾 ∈ HL)
25 hlop 35250 . . . . . . . 8 (𝐾 ∈ HL → 𝐾 ∈ OP)
2624, 25syl 17 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ (𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟))) → 𝐾 ∈ OP)
2724hllatd 35252 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ (𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟))) → 𝐾 ∈ Lat)
28 simp12l 1385 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ (𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟))) → 𝑃𝐴)
29 simp13l 1387 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ (𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟))) → 𝑄𝐴)
306, 18, 7hlatjcl 35255 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) ∈ (Base‘𝐾))
3124, 28, 29, 30syl3anc 1490 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ (𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟))) → (𝑃 𝑄) ∈ (Base‘𝐾))
32 simp2l 1256 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ (𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟))) → 𝑟𝐴)
336, 7atbase 35177 . . . . . . . . . 10 (𝑟𝐴𝑟 ∈ (Base‘𝐾))
3432, 33syl 17 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ (𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟))) → 𝑟 ∈ (Base‘𝐾))
356, 18latjcl 17318 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑟 ∈ (Base‘𝐾)) → ((𝑃 𝑄) 𝑟) ∈ (Base‘𝐾))
3627, 31, 34, 35syl3anc 1490 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ (𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟))) → ((𝑃 𝑄) 𝑟) ∈ (Base‘𝐾))
37 simp2r 1257 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ (𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟))) → 𝑠𝐴)
386, 7atbase 35177 . . . . . . . . 9 (𝑠𝐴𝑠 ∈ (Base‘𝐾))
3937, 38syl 17 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ (𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟))) → 𝑠 ∈ (Base‘𝐾))
406, 18latjcl 17318 . . . . . . . 8 ((𝐾 ∈ Lat ∧ ((𝑃 𝑄) 𝑟) ∈ (Base‘𝐾) ∧ 𝑠 ∈ (Base‘𝐾)) → (((𝑃 𝑄) 𝑟) 𝑠) ∈ (Base‘𝐾))
4127, 36, 39, 40syl3anc 1490 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ (𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟))) → (((𝑃 𝑄) 𝑟) 𝑠) ∈ (Base‘𝐾))
42 eqid 2764 . . . . . . . 8 (1.‘𝐾) = (1.‘𝐾)
43 eqid 2764 . . . . . . . 8 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
446, 42, 43ncvr1 35160 . . . . . . 7 ((𝐾 ∈ OP ∧ (((𝑃 𝑄) 𝑟) 𝑠) ∈ (Base‘𝐾)) → ¬ (1.‘𝐾)( ⋖ ‘𝐾)(((𝑃 𝑄) 𝑟) 𝑠))
4526, 41, 44syl2anc 579 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ (𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟))) → ¬ (1.‘𝐾)( ⋖ ‘𝐾)(((𝑃 𝑄) 𝑟) 𝑠))
46 eqid 2764 . . . . . . . . . . . 12 (lub‘𝐾) = (lub‘𝐾)
47 simpl1l 1293 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ ((𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) ∧ (𝑃 𝑄) = 𝑊)) → 𝐾 ∈ HL)
4847hllatd 35252 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ ((𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) ∧ (𝑃 𝑄) = 𝑊)) → 𝐾 ∈ Lat)
49 simpl2l 1297 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ ((𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) ∧ (𝑃 𝑄) = 𝑊)) → 𝑃𝐴)
50 simpl3l 1301 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ ((𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) ∧ (𝑃 𝑄) = 𝑊)) → 𝑄𝐴)
5147, 49, 50, 30syl3anc 1490 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ ((𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) ∧ (𝑃 𝑄) = 𝑊)) → (𝑃 𝑄) ∈ (Base‘𝐾))
52 simpr1l 1305 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ ((𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) ∧ (𝑃 𝑄) = 𝑊)) → 𝑟𝐴)
5352, 33syl 17 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ ((𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) ∧ (𝑃 𝑄) = 𝑊)) → 𝑟 ∈ (Base‘𝐾))
5448, 51, 53, 35syl3anc 1490 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ ((𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) ∧ (𝑃 𝑄) = 𝑊)) → ((𝑃 𝑄) 𝑟) ∈ (Base‘𝐾))
5547, 25syl 17 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ ((𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) ∧ (𝑃 𝑄) = 𝑊)) → 𝐾 ∈ OP)
56 eqid 2764 . . . . . . . . . . . . . . 15 (glb‘𝐾) = (glb‘𝐾)
576, 46, 56op01dm 35071 . . . . . . . . . . . . . 14 (𝐾 ∈ OP → ((Base‘𝐾) ∈ dom (lub‘𝐾) ∧ (Base‘𝐾) ∈ dom (glb‘𝐾)))
5857simpld 488 . . . . . . . . . . . . 13 (𝐾 ∈ OP → (Base‘𝐾) ∈ dom (lub‘𝐾))
5955, 58syl 17 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ ((𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) ∧ (𝑃 𝑄) = 𝑊)) → (Base‘𝐾) ∈ dom (lub‘𝐾))
606, 46, 17, 42, 47, 54, 59ple1 17311 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ ((𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) ∧ (𝑃 𝑄) = 𝑊)) → ((𝑃 𝑄) 𝑟) (1.‘𝐾))
61 hlpos 35254 . . . . . . . . . . . . 13 (𝐾 ∈ HL → 𝐾 ∈ Poset)
6247, 61syl 17 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ ((𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) ∧ (𝑃 𝑄) = 𝑊)) → 𝐾 ∈ Poset)
636, 42op1cl 35073 . . . . . . . . . . . . 13 (𝐾 ∈ OP → (1.‘𝐾) ∈ (Base‘𝐾))
6455, 63syl 17 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ ((𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) ∧ (𝑃 𝑄) = 𝑊)) → (1.‘𝐾) ∈ (Base‘𝐾))
65 simpr2l 1309 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ ((𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) ∧ (𝑃 𝑄) = 𝑊)) → ¬ 𝑟 (𝑃 𝑄))
666, 17, 18, 43, 7cvr1 35298 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑟𝐴) → (¬ 𝑟 (𝑃 𝑄) ↔ (𝑃 𝑄)( ⋖ ‘𝐾)((𝑃 𝑄) 𝑟)))
6747, 51, 52, 66syl3anc 1490 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ ((𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) ∧ (𝑃 𝑄) = 𝑊)) → (¬ 𝑟 (𝑃 𝑄) ↔ (𝑃 𝑄)( ⋖ ‘𝐾)((𝑃 𝑄) 𝑟)))
6865, 67mpbid 223 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ ((𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) ∧ (𝑃 𝑄) = 𝑊)) → (𝑃 𝑄)( ⋖ ‘𝐾)((𝑃 𝑄) 𝑟))
69 simpr3 1252 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ ((𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) ∧ (𝑃 𝑄) = 𝑊)) → (𝑃 𝑄) = 𝑊)
70 simpl1r 1295 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ ((𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) ∧ (𝑃 𝑄) = 𝑊)) → 𝑊𝐻)
7142, 43, 14lhp1cvr 35887 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝑊( ⋖ ‘𝐾)(1.‘𝐾))
7247, 70, 71syl2anc 579 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ ((𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) ∧ (𝑃 𝑄) = 𝑊)) → 𝑊( ⋖ ‘𝐾)(1.‘𝐾))
7369, 72eqbrtrd 4830 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ ((𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) ∧ (𝑃 𝑄) = 𝑊)) → (𝑃 𝑄)( ⋖ ‘𝐾)(1.‘𝐾))
746, 17, 43cvrcmp 35171 . . . . . . . . . . . 12 ((𝐾 ∈ Poset ∧ (((𝑃 𝑄) 𝑟) ∈ (Base‘𝐾) ∧ (1.‘𝐾) ∈ (Base‘𝐾) ∧ (𝑃 𝑄) ∈ (Base‘𝐾)) ∧ ((𝑃 𝑄)( ⋖ ‘𝐾)((𝑃 𝑄) 𝑟) ∧ (𝑃 𝑄)( ⋖ ‘𝐾)(1.‘𝐾))) → (((𝑃 𝑄) 𝑟) (1.‘𝐾) ↔ ((𝑃 𝑄) 𝑟) = (1.‘𝐾)))
7562, 54, 64, 51, 68, 73, 74syl132anc 1507 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ ((𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) ∧ (𝑃 𝑄) = 𝑊)) → (((𝑃 𝑄) 𝑟) (1.‘𝐾) ↔ ((𝑃 𝑄) 𝑟) = (1.‘𝐾)))
7660, 75mpbid 223 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ ((𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) ∧ (𝑃 𝑄) = 𝑊)) → ((𝑃 𝑄) 𝑟) = (1.‘𝐾))
77 simpr2r 1311 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ ((𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) ∧ (𝑃 𝑄) = 𝑊)) → ¬ 𝑠 ((𝑃 𝑄) 𝑟))
78 simpr1r 1307 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ ((𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) ∧ (𝑃 𝑄) = 𝑊)) → 𝑠𝐴)
796, 17, 18, 43, 7cvr1 35298 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ ((𝑃 𝑄) 𝑟) ∈ (Base‘𝐾) ∧ 𝑠𝐴) → (¬ 𝑠 ((𝑃 𝑄) 𝑟) ↔ ((𝑃 𝑄) 𝑟)( ⋖ ‘𝐾)(((𝑃 𝑄) 𝑟) 𝑠)))
8047, 54, 78, 79syl3anc 1490 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ ((𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) ∧ (𝑃 𝑄) = 𝑊)) → (¬ 𝑠 ((𝑃 𝑄) 𝑟) ↔ ((𝑃 𝑄) 𝑟)( ⋖ ‘𝐾)(((𝑃 𝑄) 𝑟) 𝑠)))
8177, 80mpbid 223 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ ((𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) ∧ (𝑃 𝑄) = 𝑊)) → ((𝑃 𝑄) 𝑟)( ⋖ ‘𝐾)(((𝑃 𝑄) 𝑟) 𝑠))
8276, 81eqbrtrrd 4832 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ ((𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) ∧ (𝑃 𝑄) = 𝑊)) → (1.‘𝐾)( ⋖ ‘𝐾)(((𝑃 𝑄) 𝑟) 𝑠))
83823exp2 1463 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) → ((𝑟𝐴𝑠𝐴) → ((¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) → ((𝑃 𝑄) = 𝑊 → (1.‘𝐾)( ⋖ ‘𝐾)(((𝑃 𝑄) 𝑟) 𝑠)))))
84833imp 1137 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ (𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟))) → ((𝑃 𝑄) = 𝑊 → (1.‘𝐾)( ⋖ ‘𝐾)(((𝑃 𝑄) 𝑟) 𝑠)))
8584necon3bd 2950 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ (𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟))) → (¬ (1.‘𝐾)( ⋖ ‘𝐾)(((𝑃 𝑄) 𝑟) 𝑠) → (𝑃 𝑄) ≠ 𝑊))
8645, 85mpd 15 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) ∧ (𝑟𝐴𝑠𝐴) ∧ (¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟))) → (𝑃 𝑄) ≠ 𝑊)
87863exp 1148 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) → ((𝑟𝐴𝑠𝐴) → ((¬ 𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) → (𝑃 𝑄) ≠ 𝑊)))
8887rexlimdvv 3183 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) → (∃𝑟𝐴𝑠𝐴𝑟 (𝑃 𝑄) ∧ ¬ 𝑠 ((𝑃 𝑄) 𝑟)) → (𝑃 𝑄) ≠ 𝑊))
8923, 88mpd 15 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) → (𝑃 𝑄) ≠ 𝑊)
903, 5, 10, 30syl3anc 1490 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) → (𝑃 𝑄) ∈ (Base‘𝐾))
91 lhp2lt.s . . . 4 < = (lt‘𝐾)
9217, 91pltval 17227 . . 3 ((𝐾 ∈ HL ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑊𝐻) → ((𝑃 𝑄) < 𝑊 ↔ ((𝑃 𝑄) 𝑊 ∧ (𝑃 𝑄) ≠ 𝑊)))
933, 90, 13, 92syl3anc 1490 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) → ((𝑃 𝑄) < 𝑊 ↔ ((𝑃 𝑄) 𝑊 ∧ (𝑃 𝑄) ≠ 𝑊)))
9421, 89, 93mpbir2and 704 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑃 𝑊) ∧ (𝑄𝐴𝑄 𝑊)) → (𝑃 𝑄) < 𝑊)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wne 2936  wrex 3055   class class class wbr 4808  dom cdm 5276  cfv 6067  (class class class)co 6841  Basecbs 16131  lecple 16222  Posetcpo 17207  ltcplt 17208  lubclub 17209  glbcglb 17210  joincjn 17211  1.cp1 17305  Latclat 17312  OPcops 35060  ccvr 35150  Atomscatm 35151  HLchlt 35238  LHypclh 35872
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-ral 3059  df-rex 3060  df-reu 3061  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-op 4340  df-uni 4594  df-iun 4677  df-br 4809  df-opab 4871  df-mpt 4888  df-id 5184  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-riota 6802  df-ov 6844  df-oprab 6845  df-proset 17195  df-poset 17213  df-plt 17225  df-lub 17241  df-glb 17242  df-join 17243  df-meet 17244  df-p0 17306  df-p1 17307  df-lat 17313  df-clat 17375  df-oposet 35064  df-ol 35066  df-oml 35067  df-covers 35154  df-ats 35155  df-atl 35186  df-cvlat 35210  df-hlat 35239  df-lhyp 35876
This theorem is referenced by:  lhpexle3lem  35899
  Copyright terms: Public domain W3C validator