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

Theorem ps-1 38664
Description: The join of two atoms 𝑅 ∨ 𝑆 (specifying a projective geometry line) is determined uniquely by any two atoms (specifying two points) less than or equal to that join. Part of Lemma 16.4 of [MaedaMaeda] p. 69, showing projective space postulate PS1 in [MaedaMaeda] p. 67. (Contributed by NM, 15-Nov-2011.)
Hypotheses
Ref Expression
ps1.l ≀ = (leβ€˜πΎ)
ps1.j ∨ = (joinβ€˜πΎ)
ps1.a 𝐴 = (Atomsβ€˜πΎ)
Assertion
Ref Expression
ps-1 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ≀ (𝑅 ∨ 𝑆) ↔ (𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑆)))

Proof of Theorem ps-1
StepHypRef Expression
1 oveq1 7419 . . . . . 6 (𝑅 = 𝑃 β†’ (𝑅 ∨ 𝑆) = (𝑃 ∨ 𝑆))
21breq2d 5160 . . . . 5 (𝑅 = 𝑃 β†’ ((𝑃 ∨ 𝑄) ≀ (𝑅 ∨ 𝑆) ↔ (𝑃 ∨ 𝑄) ≀ (𝑃 ∨ 𝑆)))
31eqeq2d 2742 . . . . 5 (𝑅 = 𝑃 β†’ ((𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑆) ↔ (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑆)))
42, 3imbi12d 344 . . . 4 (𝑅 = 𝑃 β†’ (((𝑃 ∨ 𝑄) ≀ (𝑅 ∨ 𝑆) β†’ (𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑆)) ↔ ((𝑃 ∨ 𝑄) ≀ (𝑃 ∨ 𝑆) β†’ (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑆))))
54eqcoms 2739 . . 3 (𝑃 = 𝑅 β†’ (((𝑃 ∨ 𝑄) ≀ (𝑅 ∨ 𝑆) β†’ (𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑆)) ↔ ((𝑃 ∨ 𝑄) ≀ (𝑃 ∨ 𝑆) β†’ (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑆))))
6 simp3 1137 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 β‰  𝑅 ∧ (𝑃 ∨ 𝑄) ≀ (𝑅 ∨ 𝑆)) β†’ (𝑃 ∨ 𝑄) ≀ (𝑅 ∨ 𝑆))
7 simp1 1135 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ 𝐾 ∈ HL)
8 simp21 1205 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ 𝑃 ∈ 𝐴)
9 simp3l 1200 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ 𝑅 ∈ 𝐴)
10 ps1.j . . . . . . . . . . . . 13 ∨ = (joinβ€˜πΎ)
11 ps1.a . . . . . . . . . . . . 13 𝐴 = (Atomsβ€˜πΎ)
1210, 11hlatjcom 38554 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) β†’ (𝑃 ∨ 𝑅) = (𝑅 ∨ 𝑃))
137, 8, 9, 12syl3anc 1370 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ (𝑃 ∨ 𝑅) = (𝑅 ∨ 𝑃))
14133ad2ant1 1132 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 β‰  𝑅 ∧ (𝑃 ∨ 𝑄) ≀ (𝑅 ∨ 𝑆)) β†’ (𝑃 ∨ 𝑅) = (𝑅 ∨ 𝑃))
15 hllat 38549 . . . . . . . . . . . . . . . 16 (𝐾 ∈ HL β†’ 𝐾 ∈ Lat)
16153ad2ant1 1132 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ 𝐾 ∈ Lat)
17 eqid 2731 . . . . . . . . . . . . . . . . 17 (Baseβ€˜πΎ) = (Baseβ€˜πΎ)
1817, 11atbase 38475 . . . . . . . . . . . . . . . 16 (𝑃 ∈ 𝐴 β†’ 𝑃 ∈ (Baseβ€˜πΎ))
198, 18syl 17 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ 𝑃 ∈ (Baseβ€˜πΎ))
20 simp22 1206 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ 𝑄 ∈ 𝐴)
2117, 11atbase 38475 . . . . . . . . . . . . . . . 16 (𝑄 ∈ 𝐴 β†’ 𝑄 ∈ (Baseβ€˜πΎ))
2220, 21syl 17 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ 𝑄 ∈ (Baseβ€˜πΎ))
23 simp3r 1201 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ 𝑆 ∈ 𝐴)
2417, 10, 11hlatjcl 38553 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) β†’ (𝑅 ∨ 𝑆) ∈ (Baseβ€˜πΎ))
257, 9, 23, 24syl3anc 1370 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ (𝑅 ∨ 𝑆) ∈ (Baseβ€˜πΎ))
26 ps1.l . . . . . . . . . . . . . . . 16 ≀ = (leβ€˜πΎ)
2717, 26, 10latjle12 18410 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Baseβ€˜πΎ) ∧ 𝑄 ∈ (Baseβ€˜πΎ) ∧ (𝑅 ∨ 𝑆) ∈ (Baseβ€˜πΎ))) β†’ ((𝑃 ≀ (𝑅 ∨ 𝑆) ∧ 𝑄 ≀ (𝑅 ∨ 𝑆)) ↔ (𝑃 ∨ 𝑄) ≀ (𝑅 ∨ 𝑆)))
2816, 19, 22, 25, 27syl13anc 1371 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ ((𝑃 ≀ (𝑅 ∨ 𝑆) ∧ 𝑄 ≀ (𝑅 ∨ 𝑆)) ↔ (𝑃 ∨ 𝑄) ≀ (𝑅 ∨ 𝑆)))
29 simpl 482 . . . . . . . . . . . . . 14 ((𝑃 ≀ (𝑅 ∨ 𝑆) ∧ 𝑄 ≀ (𝑅 ∨ 𝑆)) β†’ 𝑃 ≀ (𝑅 ∨ 𝑆))
3028, 29syl6bir 254 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ≀ (𝑅 ∨ 𝑆) β†’ 𝑃 ≀ (𝑅 ∨ 𝑆)))
3130adantr 480 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 β‰  𝑅) β†’ ((𝑃 ∨ 𝑄) ≀ (𝑅 ∨ 𝑆) β†’ 𝑃 ≀ (𝑅 ∨ 𝑆)))
32 simpl1 1190 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 β‰  𝑅) β†’ 𝐾 ∈ HL)
33 simpl21 1250 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 β‰  𝑅) β†’ 𝑃 ∈ 𝐴)
34 simpl3r 1228 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 β‰  𝑅) β†’ 𝑆 ∈ 𝐴)
35 simpl3l 1227 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 β‰  𝑅) β†’ 𝑅 ∈ 𝐴)
36 simpr 484 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 β‰  𝑅) β†’ 𝑃 β‰  𝑅)
3726, 10, 11hlatexchb1 38580 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 β‰  𝑅) β†’ (𝑃 ≀ (𝑅 ∨ 𝑆) ↔ (𝑅 ∨ 𝑃) = (𝑅 ∨ 𝑆)))
3832, 33, 34, 35, 36, 37syl131anc 1382 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 β‰  𝑅) β†’ (𝑃 ≀ (𝑅 ∨ 𝑆) ↔ (𝑅 ∨ 𝑃) = (𝑅 ∨ 𝑆)))
3931, 38sylibd 238 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 β‰  𝑅) β†’ ((𝑃 ∨ 𝑄) ≀ (𝑅 ∨ 𝑆) β†’ (𝑅 ∨ 𝑃) = (𝑅 ∨ 𝑆)))
40393impia 1116 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 β‰  𝑅 ∧ (𝑃 ∨ 𝑄) ≀ (𝑅 ∨ 𝑆)) β†’ (𝑅 ∨ 𝑃) = (𝑅 ∨ 𝑆))
4114, 40eqtrd 2771 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 β‰  𝑅 ∧ (𝑃 ∨ 𝑄) ≀ (𝑅 ∨ 𝑆)) β†’ (𝑃 ∨ 𝑅) = (𝑅 ∨ 𝑆))
426, 41breqtrrd 5176 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 β‰  𝑅 ∧ (𝑃 ∨ 𝑄) ≀ (𝑅 ∨ 𝑆)) β†’ (𝑃 ∨ 𝑄) ≀ (𝑃 ∨ 𝑅))
43423expia 1120 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 β‰  𝑅) β†’ ((𝑃 ∨ 𝑄) ≀ (𝑅 ∨ 𝑆) β†’ (𝑃 ∨ 𝑄) ≀ (𝑃 ∨ 𝑅)))
4417, 10, 11hlatjcl 38553 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) β†’ (𝑃 ∨ 𝑅) ∈ (Baseβ€˜πΎ))
457, 8, 9, 44syl3anc 1370 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ (𝑃 ∨ 𝑅) ∈ (Baseβ€˜πΎ))
4617, 26, 10latjle12 18410 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Baseβ€˜πΎ) ∧ 𝑄 ∈ (Baseβ€˜πΎ) ∧ (𝑃 ∨ 𝑅) ∈ (Baseβ€˜πΎ))) β†’ ((𝑃 ≀ (𝑃 ∨ 𝑅) ∧ 𝑄 ≀ (𝑃 ∨ 𝑅)) ↔ (𝑃 ∨ 𝑄) ≀ (𝑃 ∨ 𝑅)))
4716, 19, 22, 45, 46syl13anc 1371 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ ((𝑃 ≀ (𝑃 ∨ 𝑅) ∧ 𝑄 ≀ (𝑃 ∨ 𝑅)) ↔ (𝑃 ∨ 𝑄) ≀ (𝑃 ∨ 𝑅)))
48 simpr 484 . . . . . . . . . 10 ((𝑃 ≀ (𝑃 ∨ 𝑅) ∧ 𝑄 ≀ (𝑃 ∨ 𝑅)) β†’ 𝑄 ≀ (𝑃 ∨ 𝑅))
49 simp23 1207 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ 𝑃 β‰  𝑄)
5049necomd 2995 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ 𝑄 β‰  𝑃)
5126, 10, 11hlatexchb1 38580 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) ∧ 𝑄 β‰  𝑃) β†’ (𝑄 ≀ (𝑃 ∨ 𝑅) ↔ (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑅)))
527, 20, 9, 8, 50, 51syl131anc 1382 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ (𝑄 ≀ (𝑃 ∨ 𝑅) ↔ (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑅)))
5348, 52imbitrid 243 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ ((𝑃 ≀ (𝑃 ∨ 𝑅) ∧ 𝑄 ≀ (𝑃 ∨ 𝑅)) β†’ (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑅)))
5447, 53sylbird 260 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ≀ (𝑃 ∨ 𝑅) β†’ (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑅)))
5554adantr 480 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 β‰  𝑅) β†’ ((𝑃 ∨ 𝑄) ≀ (𝑃 ∨ 𝑅) β†’ (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑅)))
5643, 55syld 47 . . . . . 6 (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 β‰  𝑅) β†’ ((𝑃 ∨ 𝑄) ≀ (𝑅 ∨ 𝑆) β†’ (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑅)))
57563impia 1116 . . . . 5 (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 β‰  𝑅 ∧ (𝑃 ∨ 𝑄) ≀ (𝑅 ∨ 𝑆)) β†’ (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑅))
5857, 41eqtrd 2771 . . . 4 (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 β‰  𝑅 ∧ (𝑃 ∨ 𝑄) ≀ (𝑅 ∨ 𝑆)) β†’ (𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑆))
59583expia 1120 . . 3 (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 β‰  𝑅) β†’ ((𝑃 ∨ 𝑄) ≀ (𝑅 ∨ 𝑆) β†’ (𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑆)))
6017, 10, 11hlatjcl 38553 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) β†’ (𝑃 ∨ 𝑆) ∈ (Baseβ€˜πΎ))
617, 8, 23, 60syl3anc 1370 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ (𝑃 ∨ 𝑆) ∈ (Baseβ€˜πΎ))
6217, 26, 10latjle12 18410 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Baseβ€˜πΎ) ∧ 𝑄 ∈ (Baseβ€˜πΎ) ∧ (𝑃 ∨ 𝑆) ∈ (Baseβ€˜πΎ))) β†’ ((𝑃 ≀ (𝑃 ∨ 𝑆) ∧ 𝑄 ≀ (𝑃 ∨ 𝑆)) ↔ (𝑃 ∨ 𝑄) ≀ (𝑃 ∨ 𝑆)))
6316, 19, 22, 61, 62syl13anc 1371 . . . . 5 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ ((𝑃 ≀ (𝑃 ∨ 𝑆) ∧ 𝑄 ≀ (𝑃 ∨ 𝑆)) ↔ (𝑃 ∨ 𝑄) ≀ (𝑃 ∨ 𝑆)))
64 simpr 484 . . . . 5 ((𝑃 ≀ (𝑃 ∨ 𝑆) ∧ 𝑄 ≀ (𝑃 ∨ 𝑆)) β†’ 𝑄 ≀ (𝑃 ∨ 𝑆))
6563, 64syl6bir 254 . . . 4 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ≀ (𝑃 ∨ 𝑆) β†’ 𝑄 ≀ (𝑃 ∨ 𝑆)))
6626, 10, 11hlatexchb1 38580 . . . . 5 ((𝐾 ∈ HL ∧ (𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) ∧ 𝑄 β‰  𝑃) β†’ (𝑄 ≀ (𝑃 ∨ 𝑆) ↔ (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑆)))
677, 20, 23, 8, 50, 66syl131anc 1382 . . . 4 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ (𝑄 ≀ (𝑃 ∨ 𝑆) ↔ (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑆)))
6865, 67sylibd 238 . . 3 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ≀ (𝑃 ∨ 𝑆) β†’ (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑆)))
695, 59, 68pm2.61ne 3026 . 2 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ≀ (𝑅 ∨ 𝑆) β†’ (𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑆)))
7017, 10, 11hlatjcl 38553 . . . . 5 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) β†’ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ))
717, 8, 20, 70syl3anc 1370 . . . 4 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ))
7217, 26latref 18401 . . . 4 ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ)) β†’ (𝑃 ∨ 𝑄) ≀ (𝑃 ∨ 𝑄))
7316, 71, 72syl2anc 583 . . 3 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ (𝑃 ∨ 𝑄) ≀ (𝑃 ∨ 𝑄))
74 breq2 5152 . . 3 ((𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑆) β†’ ((𝑃 ∨ 𝑄) ≀ (𝑃 ∨ 𝑄) ↔ (𝑃 ∨ 𝑄) ≀ (𝑅 ∨ 𝑆)))
7573, 74syl5ibcom 244 . 2 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑆) β†’ (𝑃 ∨ 𝑄) ≀ (𝑅 ∨ 𝑆)))
7669, 75impbid 211 1 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ≀ (𝑅 ∨ 𝑆) ↔ (𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑆)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105   β‰  wne 2939   class class class wbr 5148  β€˜cfv 6543  (class class class)co 7412  Basecbs 17151  lecple 17211  joincjn 18271  Latclat 18391  Atomscatm 38449  HLchlt 38536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7368  df-ov 7415  df-oprab 7416  df-proset 18255  df-poset 18273  df-plt 18290  df-lub 18306  df-glb 18307  df-join 18308  df-meet 18309  df-p0 18385  df-lat 18392  df-covers 38452  df-ats 38453  df-atl 38484  df-cvlat 38508  df-hlat 38537
This theorem is referenced by:  2atjlej  38666  hlatexch3N  38667  hlatexch4  38668  2llnjaN  38753  dalem1  38846  lneq2at  38965  2llnma3r  38975  cdleme11c  39448  cdleme11  39457  cdleme35a  39635  cdleme42k  39671  cdlemg8b  39815  cdlemg13a  39838  cdlemg18b  39866  cdlemg42  39916  trljco  39927
  Copyright terms: Public domain W3C validator