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

Theorem cdlema1N 33985
Description: A condition for required for proof of Lemma A in [Crawley] p. 112. (Contributed by NM, 29-Apr-2012.) (New usage is discouraged.)
Hypotheses
Ref Expression
cdlema1.b 𝐵 = (Base‘𝐾)
cdlema1.l = (le‘𝐾)
cdlema1.j = (join‘𝐾)
cdlema1.m = (meet‘𝐾)
cdlema1.a 𝐴 = (Atoms‘𝐾)
cdlema1.n 𝑁 = (Lines‘𝐾)
cdlema1.f 𝐹 = (pmap‘𝐾)
Assertion
Ref Expression
cdlema1N (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → (𝑋 𝑅) = (𝑋 𝑌))

Proof of Theorem cdlema1N
StepHypRef Expression
1 cdlema1.b . 2 𝐵 = (Base‘𝐾)
2 cdlema1.l . 2 = (le‘𝐾)
3 simp11 1083 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → 𝐾 ∈ HL)
4 hllat 33558 . . 3 (𝐾 ∈ HL → 𝐾 ∈ Lat)
53, 4syl 17 . 2 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → 𝐾 ∈ Lat)
6 simp12 1084 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → 𝑋𝐵)
7 simp23 1088 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → 𝑅𝐴)
8 cdlema1.a . . . . 5 𝐴 = (Atoms‘𝐾)
91, 8atbase 33484 . . . 4 (𝑅𝐴𝑅𝐵)
107, 9syl 17 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → 𝑅𝐵)
11 cdlema1.j . . . 4 = (join‘𝐾)
121, 11latjcl 16766 . . 3 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑅𝐵) → (𝑋 𝑅) ∈ 𝐵)
135, 6, 10, 12syl3anc 1317 . 2 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → (𝑋 𝑅) ∈ 𝐵)
14 simp13 1085 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → 𝑌𝐵)
151, 11latjcl 16766 . . 3 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)
165, 6, 14, 15syl3anc 1317 . 2 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → (𝑋 𝑌) ∈ 𝐵)
171, 2, 11latlej1 16775 . . . 4 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝑋 (𝑋 𝑌))
185, 6, 14, 17syl3anc 1317 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → 𝑋 (𝑋 𝑌))
19 simp21 1086 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → 𝑃𝐴)
201, 8atbase 33484 . . . . . 6 (𝑃𝐴𝑃𝐵)
2119, 20syl 17 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → 𝑃𝐵)
22 simp22 1087 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → 𝑄𝐴)
231, 8atbase 33484 . . . . . 6 (𝑄𝐴𝑄𝐵)
2422, 23syl 17 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → 𝑄𝐵)
251, 11latjcl 16766 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑃𝐵𝑄𝐵) → (𝑃 𝑄) ∈ 𝐵)
265, 21, 24, 25syl3anc 1317 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → (𝑃 𝑄) ∈ 𝐵)
27 simp31r 1177 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → 𝑅 (𝑃 𝑄))
28 simp32l 1178 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → 𝑃 𝑋)
29 simp32r 1179 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → 𝑄 𝑌)
301, 2, 11latjlej12 16782 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑃𝐵𝑋𝐵) ∧ (𝑄𝐵𝑌𝐵)) → ((𝑃 𝑋𝑄 𝑌) → (𝑃 𝑄) (𝑋 𝑌)))
315, 21, 6, 24, 14, 30syl122anc 1326 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → ((𝑃 𝑋𝑄 𝑌) → (𝑃 𝑄) (𝑋 𝑌)))
3228, 29, 31mp2and 710 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → (𝑃 𝑄) (𝑋 𝑌))
331, 2, 5, 10, 26, 16, 27, 32lattrd 16773 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → 𝑅 (𝑋 𝑌))
341, 2, 11latjle12 16777 . . . 4 ((𝐾 ∈ Lat ∧ (𝑋𝐵𝑅𝐵 ∧ (𝑋 𝑌) ∈ 𝐵)) → ((𝑋 (𝑋 𝑌) ∧ 𝑅 (𝑋 𝑌)) ↔ (𝑋 𝑅) (𝑋 𝑌)))
355, 6, 10, 16, 34syl13anc 1319 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → ((𝑋 (𝑋 𝑌) ∧ 𝑅 (𝑋 𝑌)) ↔ (𝑋 𝑅) (𝑋 𝑌)))
3618, 33, 35mpbi2and 957 . 2 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → (𝑋 𝑅) (𝑋 𝑌))
371, 2, 11latlej1 16775 . . . 4 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑅𝐵) → 𝑋 (𝑋 𝑅))
385, 6, 10, 37syl3anc 1317 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → 𝑋 (𝑋 𝑅))
39 simp331 1206 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → (𝐹𝑌) ∈ 𝑁)
40 simp332 1207 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → (𝑋 𝑌) ∈ 𝐴)
41 simp333 1208 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → ¬ 𝑄 𝑋)
42 cdlema1.m . . . . . . . . . 10 = (meet‘𝐾)
431, 2, 42latmle1 16791 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) 𝑋)
445, 6, 14, 43syl3anc 1317 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → (𝑋 𝑌) 𝑋)
45 breq1 4484 . . . . . . . 8 (𝑄 = (𝑋 𝑌) → (𝑄 𝑋 ↔ (𝑋 𝑌) 𝑋))
4644, 45syl5ibrcom 235 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → (𝑄 = (𝑋 𝑌) → 𝑄 𝑋))
4746necon3bd 2700 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → (¬ 𝑄 𝑋𝑄 ≠ (𝑋 𝑌)))
4841, 47mpd 15 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → 𝑄 ≠ (𝑋 𝑌))
491, 2, 42latmle2 16792 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) 𝑌)
505, 6, 14, 49syl3anc 1317 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → (𝑋 𝑌) 𝑌)
51 cdlema1.n . . . . . 6 𝑁 = (Lines‘𝐾)
52 cdlema1.f . . . . . 6 𝐹 = (pmap‘𝐾)
531, 2, 11, 8, 51, 52lneq2at 33972 . . . . 5 (((𝐾 ∈ HL ∧ 𝑌𝐵 ∧ (𝐹𝑌) ∈ 𝑁) ∧ (𝑄𝐴 ∧ (𝑋 𝑌) ∈ 𝐴𝑄 ≠ (𝑋 𝑌)) ∧ (𝑄 𝑌 ∧ (𝑋 𝑌) 𝑌)) → 𝑌 = (𝑄 (𝑋 𝑌)))
543, 14, 39, 22, 40, 48, 29, 50, 53syl332anc 1348 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → 𝑌 = (𝑄 (𝑋 𝑌)))
551, 11latjcl 16766 . . . . . . 7 ((𝐾 ∈ Lat ∧ 𝑃𝐵𝑅𝐵) → (𝑃 𝑅) ∈ 𝐵)
565, 21, 10, 55syl3anc 1317 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → (𝑃 𝑅) ∈ 𝐵)
577, 22, 193jca 1234 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → (𝑅𝐴𝑄𝐴𝑃𝐴))
58 simp31l 1176 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → 𝑅𝑃)
593, 57, 583jca 1234 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → (𝐾 ∈ HL ∧ (𝑅𝐴𝑄𝐴𝑃𝐴) ∧ 𝑅𝑃))
602, 11, 8hlatexch1 33589 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑅𝐴𝑄𝐴𝑃𝐴) ∧ 𝑅𝑃) → (𝑅 (𝑃 𝑄) → 𝑄 (𝑃 𝑅)))
6159, 27, 60sylc 62 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → 𝑄 (𝑃 𝑅))
6221, 6, 103jca 1234 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → (𝑃𝐵𝑋𝐵𝑅𝐵))
635, 62jca 552 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → (𝐾 ∈ Lat ∧ (𝑃𝐵𝑋𝐵𝑅𝐵)))
641, 2, 11latjlej1 16780 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑃𝐵𝑋𝐵𝑅𝐵)) → (𝑃 𝑋 → (𝑃 𝑅) (𝑋 𝑅)))
6563, 28, 64sylc 62 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → (𝑃 𝑅) (𝑋 𝑅))
661, 2, 5, 24, 56, 13, 61, 65lattrd 16773 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → 𝑄 (𝑋 𝑅))
671, 2, 11, 42latmlej11 16805 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑋𝐵𝑌𝐵𝑅𝐵)) → (𝑋 𝑌) (𝑋 𝑅))
685, 6, 14, 10, 67syl13anc 1319 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → (𝑋 𝑌) (𝑋 𝑅))
691, 42latmcl 16767 . . . . . . 7 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)
705, 6, 14, 69syl3anc 1317 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → (𝑋 𝑌) ∈ 𝐵)
711, 2, 11latjle12 16777 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑄𝐵 ∧ (𝑋 𝑌) ∈ 𝐵 ∧ (𝑋 𝑅) ∈ 𝐵)) → ((𝑄 (𝑋 𝑅) ∧ (𝑋 𝑌) (𝑋 𝑅)) ↔ (𝑄 (𝑋 𝑌)) (𝑋 𝑅)))
725, 24, 70, 13, 71syl13anc 1319 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → ((𝑄 (𝑋 𝑅) ∧ (𝑋 𝑌) (𝑋 𝑅)) ↔ (𝑄 (𝑋 𝑌)) (𝑋 𝑅)))
7366, 68, 72mpbi2and 957 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → (𝑄 (𝑋 𝑌)) (𝑋 𝑅))
7454, 73eqbrtrd 4503 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → 𝑌 (𝑋 𝑅))
751, 2, 11latjle12 16777 . . . 4 ((𝐾 ∈ Lat ∧ (𝑋𝐵𝑌𝐵 ∧ (𝑋 𝑅) ∈ 𝐵)) → ((𝑋 (𝑋 𝑅) ∧ 𝑌 (𝑋 𝑅)) ↔ (𝑋 𝑌) (𝑋 𝑅)))
765, 6, 14, 13, 75syl13anc 1319 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → ((𝑋 (𝑋 𝑅) ∧ 𝑌 (𝑋 𝑅)) ↔ (𝑋 𝑌) (𝑋 𝑅)))
7738, 74, 76mpbi2and 957 . 2 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → (𝑋 𝑌) (𝑋 𝑅))
781, 2, 5, 13, 16, 36, 77latasymd 16772 1 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ((𝑅𝑃𝑅 (𝑃 𝑄)) ∧ (𝑃 𝑋𝑄 𝑌) ∧ ((𝐹𝑌) ∈ 𝑁 ∧ (𝑋 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 𝑋))) → (𝑋 𝑅) = (𝑋 𝑌))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1938  wne 2684   class class class wbr 4481  cfv 5689  (class class class)co 6426  Basecbs 15579  lecple 15659  joincjn 16659  meetcmee 16660  Latclat 16760  Atomscatm 33458  HLchlt 33545  Linesclines 33688  pmapcpmap 33691
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-rep 4597  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732  ax-un 6723
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-ral 2805  df-rex 2806  df-reu 2807  df-rab 2809  df-v 3079  df-sbc 3307  df-csb 3404  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-op 4035  df-uni 4271  df-iun 4355  df-br 4482  df-opab 4542  df-mpt 4543  df-id 4847  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-iota 5653  df-fun 5691  df-fn 5692  df-f 5693  df-f1 5694  df-fo 5695  df-f1o 5696  df-fv 5697  df-riota 6388  df-ov 6429  df-oprab 6430  df-preset 16643  df-poset 16661  df-plt 16673  df-lub 16689  df-glb 16690  df-join 16691  df-meet 16692  df-p0 16754  df-lat 16761  df-clat 16823  df-oposet 33371  df-ol 33373  df-oml 33374  df-covers 33461  df-ats 33462  df-atl 33493  df-cvlat 33517  df-hlat 33546  df-lines 33695  df-pmap 33698
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator