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

Theorem cvrat4 36573
Description: A condition implying existence of an atom with the properties shown. Lemma 3.2.20 in [PtakPulmannova] p. 68. Also Lemma 9.2(delta) in [MaedaMaeda] p. 41. (atcvat4i 30168 analog.) (Contributed by NM, 30-Nov-2011.)
Hypotheses
Ref Expression
cvrat4.b 𝐵 = (Base‘𝐾)
cvrat4.l = (le‘𝐾)
cvrat4.j = (join‘𝐾)
cvrat4.z 0 = (0.‘𝐾)
cvrat4.a 𝐴 = (Atoms‘𝐾)
Assertion
Ref Expression
cvrat4 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → ((𝑋0𝑃 (𝑋 𝑄)) → ∃𝑟𝐴 (𝑟 𝑋𝑃 (𝑄 𝑟))))
Distinct variable groups:   𝐴,𝑟   𝐵,𝑟   ,𝑟   𝐾,𝑟   ,𝑟   𝑃,𝑟   𝑄,𝑟   𝑋,𝑟
Allowed substitution hint:   0 (𝑟)

Proof of Theorem cvrat4
StepHypRef Expression
1 hlatl 36490 . . . . . . . . . 10 (𝐾 ∈ HL → 𝐾 ∈ AtLat)
21adantr 483 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → 𝐾 ∈ AtLat)
3 simpr1 1190 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → 𝑋𝐵)
4 cvrat4.b . . . . . . . . . . 11 𝐵 = (Base‘𝐾)
5 cvrat4.l . . . . . . . . . . 11 = (le‘𝐾)
6 cvrat4.z . . . . . . . . . . 11 0 = (0.‘𝐾)
7 cvrat4.a . . . . . . . . . . 11 𝐴 = (Atoms‘𝐾)
84, 5, 6, 7atlex 36446 . . . . . . . . . 10 ((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑋0 ) → ∃𝑟𝐴 𝑟 𝑋)
983exp 1115 . . . . . . . . 9 (𝐾 ∈ AtLat → (𝑋𝐵 → (𝑋0 → ∃𝑟𝐴 𝑟 𝑋)))
102, 3, 9sylc 65 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (𝑋0 → ∃𝑟𝐴 𝑟 𝑋))
1110adantr 483 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ 𝑃 = 𝑄) → (𝑋0 → ∃𝑟𝐴 𝑟 𝑋))
12 simpll 765 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ 𝑟𝐴) → 𝐾 ∈ HL)
13 simplr3 1213 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ 𝑟𝐴) → 𝑄𝐴)
14 simpr 487 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ 𝑟𝐴) → 𝑟𝐴)
15 cvrat4.j . . . . . . . . . . . . . . 15 = (join‘𝐾)
165, 15, 7hlatlej1 36505 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑟𝐴) → 𝑄 (𝑄 𝑟))
1712, 13, 14, 16syl3anc 1367 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ 𝑟𝐴) → 𝑄 (𝑄 𝑟))
18 breq1 5061 . . . . . . . . . . . . 13 (𝑃 = 𝑄 → (𝑃 (𝑄 𝑟) ↔ 𝑄 (𝑄 𝑟)))
1917, 18syl5ibr 248 . . . . . . . . . . . 12 (𝑃 = 𝑄 → (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ 𝑟𝐴) → 𝑃 (𝑄 𝑟)))
2019expd 418 . . . . . . . . . . 11 (𝑃 = 𝑄 → ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (𝑟𝐴𝑃 (𝑄 𝑟))))
2120impcom 410 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ 𝑃 = 𝑄) → (𝑟𝐴𝑃 (𝑄 𝑟)))
2221anim2d 613 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ 𝑃 = 𝑄) → ((𝑟 𝑋𝑟𝐴) → (𝑟 𝑋𝑃 (𝑄 𝑟))))
2322expcomd 419 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ 𝑃 = 𝑄) → (𝑟𝐴 → (𝑟 𝑋 → (𝑟 𝑋𝑃 (𝑄 𝑟)))))
2423reximdvai 3272 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ 𝑃 = 𝑄) → (∃𝑟𝐴 𝑟 𝑋 → ∃𝑟𝐴 (𝑟 𝑋𝑃 (𝑄 𝑟))))
2511, 24syld 47 . . . . . 6 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ 𝑃 = 𝑄) → (𝑋0 → ∃𝑟𝐴 (𝑟 𝑋𝑃 (𝑄 𝑟))))
2625ex 415 . . . . 5 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (𝑃 = 𝑄 → (𝑋0 → ∃𝑟𝐴 (𝑟 𝑋𝑃 (𝑄 𝑟)))))
2726a1i 11 . . . 4 (𝑃 (𝑋 𝑄) → ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (𝑃 = 𝑄 → (𝑋0 → ∃𝑟𝐴 (𝑟 𝑋𝑃 (𝑄 𝑟))))))
2827com4l 92 . . 3 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (𝑃 = 𝑄 → (𝑋0 → (𝑃 (𝑋 𝑄) → ∃𝑟𝐴 (𝑟 𝑋𝑃 (𝑄 𝑟))))))
2928imp4a 425 . 2 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (𝑃 = 𝑄 → ((𝑋0𝑃 (𝑋 𝑄)) → ∃𝑟𝐴 (𝑟 𝑋𝑃 (𝑄 𝑟)))))
30 hllat 36493 . . . . . . . . . . . . . 14 (𝐾 ∈ HL → 𝐾 ∈ Lat)
3130adantr 483 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → 𝐾 ∈ Lat)
32 simpr3 1192 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → 𝑄𝐴)
334, 7atbase 36419 . . . . . . . . . . . . . 14 (𝑄𝐴𝑄𝐵)
3432, 33syl 17 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → 𝑄𝐵)
354, 5, 15latleeqj2 17668 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ 𝑄𝐵𝑋𝐵) → (𝑄 𝑋 ↔ (𝑋 𝑄) = 𝑋))
3631, 34, 3, 35syl3anc 1367 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (𝑄 𝑋 ↔ (𝑋 𝑄) = 𝑋))
3736biimpa 479 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ 𝑄 𝑋) → (𝑋 𝑄) = 𝑋)
3837breq2d 5070 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ 𝑄 𝑋) → (𝑃 (𝑋 𝑄) ↔ 𝑃 𝑋))
3938biimpa 479 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ 𝑄 𝑋) ∧ 𝑃 (𝑋 𝑄)) → 𝑃 𝑋)
4039expl 460 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → ((𝑄 𝑋𝑃 (𝑋 𝑄)) → 𝑃 𝑋))
41 simpl 485 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → 𝐾 ∈ HL)
42 simpr2 1191 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → 𝑃𝐴)
435, 15, 7hlatlej2 36506 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑃𝐴) → 𝑃 (𝑄 𝑃))
4441, 32, 42, 43syl3anc 1367 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → 𝑃 (𝑄 𝑃))
4540, 44jctird 529 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → ((𝑄 𝑋𝑃 (𝑋 𝑄)) → (𝑃 𝑋𝑃 (𝑄 𝑃))))
4645, 42jctild 528 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → ((𝑄 𝑋𝑃 (𝑋 𝑄)) → (𝑃𝐴 ∧ (𝑃 𝑋𝑃 (𝑄 𝑃)))))
4746impl 458 . . . . 5 ((((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ 𝑄 𝑋) ∧ 𝑃 (𝑋 𝑄)) → (𝑃𝐴 ∧ (𝑃 𝑋𝑃 (𝑄 𝑃))))
48 breq1 5061 . . . . . . 7 (𝑟 = 𝑃 → (𝑟 𝑋𝑃 𝑋))
49 oveq2 7158 . . . . . . . 8 (𝑟 = 𝑃 → (𝑄 𝑟) = (𝑄 𝑃))
5049breq2d 5070 . . . . . . 7 (𝑟 = 𝑃 → (𝑃 (𝑄 𝑟) ↔ 𝑃 (𝑄 𝑃)))
5148, 50anbi12d 632 . . . . . 6 (𝑟 = 𝑃 → ((𝑟 𝑋𝑃 (𝑄 𝑟)) ↔ (𝑃 𝑋𝑃 (𝑄 𝑃))))
5251rspcev 3622 . . . . 5 ((𝑃𝐴 ∧ (𝑃 𝑋𝑃 (𝑄 𝑃))) → ∃𝑟𝐴 (𝑟 𝑋𝑃 (𝑄 𝑟)))
5347, 52syl 17 . . . 4 ((((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ 𝑄 𝑋) ∧ 𝑃 (𝑋 𝑄)) → ∃𝑟𝐴 (𝑟 𝑋𝑃 (𝑄 𝑟)))
5453adantrl 714 . . 3 ((((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ 𝑄 𝑋) ∧ (𝑋0𝑃 (𝑋 𝑄))) → ∃𝑟𝐴 (𝑟 𝑋𝑃 (𝑄 𝑟)))
5554exp31 422 . 2 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (𝑄 𝑋 → ((𝑋0𝑃 (𝑋 𝑄)) → ∃𝑟𝐴 (𝑟 𝑋𝑃 (𝑄 𝑟)))))
56 simpr 487 . . 3 ((𝑋0𝑃 (𝑋 𝑄)) → 𝑃 (𝑋 𝑄))
57 ioran 980 . . . . 5 (¬ (𝑃 = 𝑄𝑄 𝑋) ↔ (¬ 𝑃 = 𝑄 ∧ ¬ 𝑄 𝑋))
58 df-ne 3017 . . . . . 6 (𝑃𝑄 ↔ ¬ 𝑃 = 𝑄)
5958anbi1i 625 . . . . 5 ((𝑃𝑄 ∧ ¬ 𝑄 𝑋) ↔ (¬ 𝑃 = 𝑄 ∧ ¬ 𝑄 𝑋))
6057, 59bitr4i 280 . . . 4 (¬ (𝑃 = 𝑄𝑄 𝑋) ↔ (𝑃𝑄 ∧ ¬ 𝑄 𝑋))
61 eqid 2821 . . . . . . . . . 10 (meet‘𝐾) = (meet‘𝐾)
624, 5, 15, 61, 7cvrat3 36572 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → ((𝑃𝑄 ∧ ¬ 𝑄 𝑋𝑃 (𝑋 𝑄)) → (𝑋(meet‘𝐾)(𝑃 𝑄)) ∈ 𝐴))
63623expd 1349 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (𝑃𝑄 → (¬ 𝑄 𝑋 → (𝑃 (𝑋 𝑄) → (𝑋(meet‘𝐾)(𝑃 𝑄)) ∈ 𝐴))))
6463imp4c 426 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (((𝑃𝑄 ∧ ¬ 𝑄 𝑋) ∧ 𝑃 (𝑋 𝑄)) → (𝑋(meet‘𝐾)(𝑃 𝑄)) ∈ 𝐴))
654, 7atbase 36419 . . . . . . . . . . . . 13 (𝑃𝐴𝑃𝐵)
6642, 65syl 17 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → 𝑃𝐵)
674, 15latjcl 17655 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ 𝑃𝐵𝑄𝐵) → (𝑃 𝑄) ∈ 𝐵)
6831, 66, 34, 67syl3anc 1367 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (𝑃 𝑄) ∈ 𝐵)
694, 5, 61latmle1 17680 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ 𝑋𝐵 ∧ (𝑃 𝑄) ∈ 𝐵) → (𝑋(meet‘𝐾)(𝑃 𝑄)) 𝑋)
7031, 3, 68, 69syl3anc 1367 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (𝑋(meet‘𝐾)(𝑃 𝑄)) 𝑋)
7170adantr 483 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ ((𝑃𝑄 ∧ ¬ 𝑄 𝑋) ∧ 𝑃 (𝑋 𝑄))) → (𝑋(meet‘𝐾)(𝑃 𝑄)) 𝑋)
72 simpll 765 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ ((𝑃𝑄 ∧ ¬ 𝑄 𝑋) ∧ 𝑃 (𝑋 𝑄))) → 𝐾 ∈ HL)
7363imp44 431 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ ((𝑃𝑄 ∧ ¬ 𝑄 𝑋) ∧ 𝑃 (𝑋 𝑄))) → (𝑋(meet‘𝐾)(𝑃 𝑄)) ∈ 𝐴)
74 simplr2 1212 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ ((𝑃𝑄 ∧ ¬ 𝑄 𝑋) ∧ 𝑃 (𝑋 𝑄))) → 𝑃𝐴)
7534adantr 483 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ ((𝑃𝑄 ∧ ¬ 𝑄 𝑋) ∧ 𝑃 (𝑋 𝑄))) → 𝑄𝐵)
7673, 74, 753jca 1124 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ ((𝑃𝑄 ∧ ¬ 𝑄 𝑋) ∧ 𝑃 (𝑋 𝑄))) → ((𝑋(meet‘𝐾)(𝑃 𝑄)) ∈ 𝐴𝑃𝐴𝑄𝐵))
7772, 76jca 514 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ ((𝑃𝑄 ∧ ¬ 𝑄 𝑋) ∧ 𝑃 (𝑋 𝑄))) → (𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 𝑄)) ∈ 𝐴𝑃𝐴𝑄𝐵)))
784, 5, 61, 6, 7atnle 36447 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ AtLat ∧ 𝑄𝐴𝑋𝐵) → (¬ 𝑄 𝑋 ↔ (𝑄(meet‘𝐾)𝑋) = 0 ))
792, 32, 3, 78syl3anc 1367 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (¬ 𝑄 𝑋 ↔ (𝑄(meet‘𝐾)𝑋) = 0 ))
804, 61latmcom 17679 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ Lat ∧ 𝑄𝐵𝑋𝐵) → (𝑄(meet‘𝐾)𝑋) = (𝑋(meet‘𝐾)𝑄))
8131, 34, 3, 80syl3anc 1367 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (𝑄(meet‘𝐾)𝑋) = (𝑋(meet‘𝐾)𝑄))
8281eqeq1d 2823 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → ((𝑄(meet‘𝐾)𝑋) = 0 ↔ (𝑋(meet‘𝐾)𝑄) = 0 ))
8379, 82bitrd 281 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (¬ 𝑄 𝑋 ↔ (𝑋(meet‘𝐾)𝑄) = 0 ))
844, 61latmcl 17656 . . . . . . . . . . . . . . . . . . . . 21 ((𝐾 ∈ Lat ∧ 𝑋𝐵 ∧ (𝑃 𝑄) ∈ 𝐵) → (𝑋(meet‘𝐾)(𝑃 𝑄)) ∈ 𝐵)
8531, 3, 68, 84syl3anc 1367 . . . . . . . . . . . . . . . . . . . 20 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (𝑋(meet‘𝐾)(𝑃 𝑄)) ∈ 𝐵)
8685, 3, 343jca 1124 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → ((𝑋(meet‘𝐾)(𝑃 𝑄)) ∈ 𝐵𝑋𝐵𝑄𝐵))
8731, 86jca 514 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (𝐾 ∈ Lat ∧ ((𝑋(meet‘𝐾)(𝑃 𝑄)) ∈ 𝐵𝑋𝐵𝑄𝐵)))
884, 5, 61latmlem2 17686 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Lat ∧ ((𝑋(meet‘𝐾)(𝑃 𝑄)) ∈ 𝐵𝑋𝐵𝑄𝐵)) → ((𝑋(meet‘𝐾)(𝑃 𝑄)) 𝑋 → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 𝑄))) (𝑄(meet‘𝐾)𝑋)))
8987, 70, 88sylc 65 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 𝑄))) (𝑄(meet‘𝐾)𝑋))
9089, 81breqtrd 5084 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 𝑄))) (𝑋(meet‘𝐾)𝑄))
91 breq2 5062 . . . . . . . . . . . . . . . 16 ((𝑋(meet‘𝐾)𝑄) = 0 → ((𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 𝑄))) (𝑋(meet‘𝐾)𝑄) ↔ (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 𝑄))) 0 ))
9290, 91syl5ibcom 247 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → ((𝑋(meet‘𝐾)𝑄) = 0 → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 𝑄))) 0 ))
93 hlop 36492 . . . . . . . . . . . . . . . . 17 (𝐾 ∈ HL → 𝐾 ∈ OP)
9493adantr 483 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → 𝐾 ∈ OP)
954, 61latmcl 17656 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ Lat ∧ 𝑄𝐵 ∧ (𝑋(meet‘𝐾)(𝑃 𝑄)) ∈ 𝐵) → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 𝑄))) ∈ 𝐵)
9631, 34, 85, 95syl3anc 1367 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 𝑄))) ∈ 𝐵)
974, 5, 6ople0 36317 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ OP ∧ (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 𝑄))) ∈ 𝐵) → ((𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 𝑄))) 0 ↔ (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 𝑄))) = 0 ))
9894, 96, 97syl2anc 586 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → ((𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 𝑄))) 0 ↔ (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 𝑄))) = 0 ))
9992, 98sylibd 241 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → ((𝑋(meet‘𝐾)𝑄) = 0 → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 𝑄))) = 0 ))
10083, 99sylbid 242 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (¬ 𝑄 𝑋 → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 𝑄))) = 0 ))
101100imp 409 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ ¬ 𝑄 𝑋) → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 𝑄))) = 0 )
102101adantrl 714 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑄 𝑋)) → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 𝑄))) = 0 )
103102adantrr 715 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ ((𝑃𝑄 ∧ ¬ 𝑄 𝑋) ∧ 𝑃 (𝑋 𝑄))) → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 𝑄))) = 0 )
1044, 5, 61latmle2 17681 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ 𝑋𝐵 ∧ (𝑃 𝑄) ∈ 𝐵) → (𝑋(meet‘𝐾)(𝑃 𝑄)) (𝑃 𝑄))
10531, 3, 68, 104syl3anc 1367 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (𝑋(meet‘𝐾)(𝑃 𝑄)) (𝑃 𝑄))
1064, 15latjcom 17663 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ 𝑃𝐵𝑄𝐵) → (𝑃 𝑄) = (𝑄 𝑃))
10731, 66, 34, 106syl3anc 1367 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (𝑃 𝑄) = (𝑄 𝑃))
108105, 107breqtrd 5084 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (𝑋(meet‘𝐾)(𝑃 𝑄)) (𝑄 𝑃))
109108adantr 483 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ ((𝑃𝑄 ∧ ¬ 𝑄 𝑋) ∧ 𝑃 (𝑋 𝑄))) → (𝑋(meet‘𝐾)(𝑃 𝑄)) (𝑄 𝑃))
11030adantr 483 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 𝑄)) ∈ 𝐴𝑃𝐴𝑄𝐵)) → 𝐾 ∈ Lat)
111 simpr3 1192 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 𝑄)) ∈ 𝐴𝑃𝐴𝑄𝐵)) → 𝑄𝐵)
112 simpr1 1190 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 𝑄)) ∈ 𝐴𝑃𝐴𝑄𝐵)) → (𝑋(meet‘𝐾)(𝑃 𝑄)) ∈ 𝐴)
1134, 7atbase 36419 . . . . . . . . . . . . . 14 ((𝑋(meet‘𝐾)(𝑃 𝑄)) ∈ 𝐴 → (𝑋(meet‘𝐾)(𝑃 𝑄)) ∈ 𝐵)
114112, 113syl 17 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 𝑄)) ∈ 𝐴𝑃𝐴𝑄𝐵)) → (𝑋(meet‘𝐾)(𝑃 𝑄)) ∈ 𝐵)
1154, 61latmcom 17679 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ 𝑄𝐵 ∧ (𝑋(meet‘𝐾)(𝑃 𝑄)) ∈ 𝐵) → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 𝑄))) = ((𝑋(meet‘𝐾)(𝑃 𝑄))(meet‘𝐾)𝑄))
116110, 111, 114, 115syl3anc 1367 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 𝑄)) ∈ 𝐴𝑃𝐴𝑄𝐵)) → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 𝑄))) = ((𝑋(meet‘𝐾)(𝑃 𝑄))(meet‘𝐾)𝑄))
117116eqeq1d 2823 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 𝑄)) ∈ 𝐴𝑃𝐴𝑄𝐵)) → ((𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 𝑄))) = 0 ↔ ((𝑋(meet‘𝐾)(𝑃 𝑄))(meet‘𝐾)𝑄) = 0 ))
1184, 5, 15, 61, 6, 7hlexch3 36521 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 𝑄)) ∈ 𝐴𝑃𝐴𝑄𝐵) ∧ ((𝑋(meet‘𝐾)(𝑃 𝑄))(meet‘𝐾)𝑄) = 0 ) → ((𝑋(meet‘𝐾)(𝑃 𝑄)) (𝑄 𝑃) → 𝑃 (𝑄 (𝑋(meet‘𝐾)(𝑃 𝑄)))))
1191183expia 1117 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 𝑄)) ∈ 𝐴𝑃𝐴𝑄𝐵)) → (((𝑋(meet‘𝐾)(𝑃 𝑄))(meet‘𝐾)𝑄) = 0 → ((𝑋(meet‘𝐾)(𝑃 𝑄)) (𝑄 𝑃) → 𝑃 (𝑄 (𝑋(meet‘𝐾)(𝑃 𝑄))))))
120117, 119sylbid 242 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 𝑄)) ∈ 𝐴𝑃𝐴𝑄𝐵)) → ((𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 𝑄))) = 0 → ((𝑋(meet‘𝐾)(𝑃 𝑄)) (𝑄 𝑃) → 𝑃 (𝑄 (𝑋(meet‘𝐾)(𝑃 𝑄))))))
12177, 103, 109, 120syl3c 66 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ ((𝑃𝑄 ∧ ¬ 𝑄 𝑋) ∧ 𝑃 (𝑋 𝑄))) → 𝑃 (𝑄 (𝑋(meet‘𝐾)(𝑃 𝑄))))
12271, 121jca 514 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ ((𝑃𝑄 ∧ ¬ 𝑄 𝑋) ∧ 𝑃 (𝑋 𝑄))) → ((𝑋(meet‘𝐾)(𝑃 𝑄)) 𝑋𝑃 (𝑄 (𝑋(meet‘𝐾)(𝑃 𝑄)))))
123122ex 415 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (((𝑃𝑄 ∧ ¬ 𝑄 𝑋) ∧ 𝑃 (𝑋 𝑄)) → ((𝑋(meet‘𝐾)(𝑃 𝑄)) 𝑋𝑃 (𝑄 (𝑋(meet‘𝐾)(𝑃 𝑄))))))
12464, 123jcad 515 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (((𝑃𝑄 ∧ ¬ 𝑄 𝑋) ∧ 𝑃 (𝑋 𝑄)) → ((𝑋(meet‘𝐾)(𝑃 𝑄)) ∈ 𝐴 ∧ ((𝑋(meet‘𝐾)(𝑃 𝑄)) 𝑋𝑃 (𝑄 (𝑋(meet‘𝐾)(𝑃 𝑄)))))))
125 breq1 5061 . . . . . . . 8 (𝑟 = (𝑋(meet‘𝐾)(𝑃 𝑄)) → (𝑟 𝑋 ↔ (𝑋(meet‘𝐾)(𝑃 𝑄)) 𝑋))
126 oveq2 7158 . . . . . . . . 9 (𝑟 = (𝑋(meet‘𝐾)(𝑃 𝑄)) → (𝑄 𝑟) = (𝑄 (𝑋(meet‘𝐾)(𝑃 𝑄))))
127126breq2d 5070 . . . . . . . 8 (𝑟 = (𝑋(meet‘𝐾)(𝑃 𝑄)) → (𝑃 (𝑄 𝑟) ↔ 𝑃 (𝑄 (𝑋(meet‘𝐾)(𝑃 𝑄)))))
128125, 127anbi12d 632 . . . . . . 7 (𝑟 = (𝑋(meet‘𝐾)(𝑃 𝑄)) → ((𝑟 𝑋𝑃 (𝑄 𝑟)) ↔ ((𝑋(meet‘𝐾)(𝑃 𝑄)) 𝑋𝑃 (𝑄 (𝑋(meet‘𝐾)(𝑃 𝑄))))))
129128rspcev 3622 . . . . . 6 (((𝑋(meet‘𝐾)(𝑃 𝑄)) ∈ 𝐴 ∧ ((𝑋(meet‘𝐾)(𝑃 𝑄)) 𝑋𝑃 (𝑄 (𝑋(meet‘𝐾)(𝑃 𝑄))))) → ∃𝑟𝐴 (𝑟 𝑋𝑃 (𝑄 𝑟)))
130124, 129syl6 35 . . . . 5 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (((𝑃𝑄 ∧ ¬ 𝑄 𝑋) ∧ 𝑃 (𝑋 𝑄)) → ∃𝑟𝐴 (𝑟 𝑋𝑃 (𝑄 𝑟))))
131130expd 418 . . . 4 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → ((𝑃𝑄 ∧ ¬ 𝑄 𝑋) → (𝑃 (𝑋 𝑄) → ∃𝑟𝐴 (𝑟 𝑋𝑃 (𝑄 𝑟)))))
13260, 131syl5bi 244 . . 3 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (¬ (𝑃 = 𝑄𝑄 𝑋) → (𝑃 (𝑋 𝑄) → ∃𝑟𝐴 (𝑟 𝑋𝑃 (𝑄 𝑟)))))
13356, 132syl7 74 . 2 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (¬ (𝑃 = 𝑄𝑄 𝑋) → ((𝑋0𝑃 (𝑋 𝑄)) → ∃𝑟𝐴 (𝑟 𝑋𝑃 (𝑄 𝑟)))))
13429, 55, 133ecase3d 1029 1 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → ((𝑋0𝑃 (𝑋 𝑄)) → ∃𝑟𝐴 (𝑟 𝑋𝑃 (𝑄 𝑟))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398  wo 843  w3a 1083   = wceq 1533  wcel 2110  wne 3016  wrex 3139   class class class wbr 5058  cfv 6349  (class class class)co 7150  Basecbs 16477  lecple 16566  joincjn 17548  meetcmee 17549  0.cp0 17641  Latclat 17649  OPcops 36302  Atomscatm 36393  AtLatcal 36394  HLchlt 36480
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-iun 4913  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7108  df-ov 7153  df-oprab 7154  df-proset 17532  df-poset 17550  df-plt 17562  df-lub 17578  df-glb 17579  df-join 17580  df-meet 17581  df-p0 17643  df-lat 17650  df-clat 17712  df-oposet 36306  df-ol 36308  df-oml 36309  df-covers 36396  df-ats 36397  df-atl 36428  df-cvlat 36452  df-hlat 36481
This theorem is referenced by:  cvrat42  36574  ps-2  36608
  Copyright terms: Public domain W3C validator