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

Theorem cdleme22b 38355
Description: Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 5th line on p. 115. Show that t v =/= p q and s p q implies ¬ t p q. (Contributed by NM, 2-Dec-2012.)
Hypotheses
Ref Expression
cdleme22.l = (le‘𝐾)
cdleme22.j = (join‘𝐾)
cdleme22.m = (meet‘𝐾)
cdleme22.a 𝐴 = (Atoms‘𝐾)
cdleme22.h 𝐻 = (LHyp‘𝐾)
Assertion
Ref Expression
cdleme22b (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → ¬ 𝑇 (𝑃 𝑄))

Proof of Theorem cdleme22b
StepHypRef Expression
1 simp1l 1196 . . . . 5 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → 𝐾 ∈ HL)
2 simp1r1 1268 . . . . . 6 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → 𝑆𝐴)
3 simp1r2 1269 . . . . . 6 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → 𝑇𝐴)
4 simp1r3 1270 . . . . . 6 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → 𝑆𝑇)
5 cdleme22.j . . . . . . 7 = (join‘𝐾)
6 cdleme22.a . . . . . . 7 𝐴 = (Atoms‘𝐾)
7 eqid 2738 . . . . . . 7 (LLines‘𝐾) = (LLines‘𝐾)
85, 6, 7llni2 37526 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴) ∧ 𝑆𝑇) → (𝑆 𝑇) ∈ (LLines‘𝐾))
91, 2, 3, 4, 8syl31anc 1372 . . . . 5 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → (𝑆 𝑇) ∈ (LLines‘𝐾))
106, 7llnneat 37528 . . . . 5 ((𝐾 ∈ HL ∧ (𝑆 𝑇) ∈ (LLines‘𝐾)) → ¬ (𝑆 𝑇) ∈ 𝐴)
111, 9, 10syl2anc 584 . . . 4 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → ¬ (𝑆 𝑇) ∈ 𝐴)
12 eqid 2738 . . . . . 6 (0.‘𝐾) = (0.‘𝐾)
1312, 7llnn0 37530 . . . . 5 ((𝐾 ∈ HL ∧ (𝑆 𝑇) ∈ (LLines‘𝐾)) → (𝑆 𝑇) ≠ (0.‘𝐾))
141, 9, 13syl2anc 584 . . . 4 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → (𝑆 𝑇) ≠ (0.‘𝐾))
1511, 14jca 512 . . 3 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → (¬ (𝑆 𝑇) ∈ 𝐴 ∧ (𝑆 𝑇) ≠ (0.‘𝐾)))
16 df-ne 2944 . . . . 5 ((𝑆 𝑇) ≠ (0.‘𝐾) ↔ ¬ (𝑆 𝑇) = (0.‘𝐾))
1716anbi2i 623 . . . 4 ((¬ (𝑆 𝑇) ∈ 𝐴 ∧ (𝑆 𝑇) ≠ (0.‘𝐾)) ↔ (¬ (𝑆 𝑇) ∈ 𝐴 ∧ ¬ (𝑆 𝑇) = (0.‘𝐾)))
18 pm4.56 986 . . . 4 ((¬ (𝑆 𝑇) ∈ 𝐴 ∧ ¬ (𝑆 𝑇) = (0.‘𝐾)) ↔ ¬ ((𝑆 𝑇) ∈ 𝐴 ∨ (𝑆 𝑇) = (0.‘𝐾)))
1917, 18bitri 274 . . 3 ((¬ (𝑆 𝑇) ∈ 𝐴 ∧ (𝑆 𝑇) ≠ (0.‘𝐾)) ↔ ¬ ((𝑆 𝑇) ∈ 𝐴 ∨ (𝑆 𝑇) = (0.‘𝐾)))
2015, 19sylib 217 . 2 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → ¬ ((𝑆 𝑇) ∈ 𝐴 ∨ (𝑆 𝑇) = (0.‘𝐾)))
21 simp3r2 1281 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → 𝑆 (𝑇 𝑉))
22 simp3l 1200 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → 𝑉𝐴)
23 cdleme22.l . . . . . . . . 9 = (le‘𝐾)
2423, 5, 6hlatlej1 37389 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑉𝐴) → 𝑇 (𝑇 𝑉))
251, 3, 22, 24syl3anc 1370 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → 𝑇 (𝑇 𝑉))
261hllatd 37378 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → 𝐾 ∈ Lat)
27 eqid 2738 . . . . . . . . . 10 (Base‘𝐾) = (Base‘𝐾)
2827, 6atbase 37303 . . . . . . . . 9 (𝑆𝐴𝑆 ∈ (Base‘𝐾))
292, 28syl 17 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → 𝑆 ∈ (Base‘𝐾))
3027, 6atbase 37303 . . . . . . . . 9 (𝑇𝐴𝑇 ∈ (Base‘𝐾))
313, 30syl 17 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → 𝑇 ∈ (Base‘𝐾))
3227, 5, 6hlatjcl 37381 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑉𝐴) → (𝑇 𝑉) ∈ (Base‘𝐾))
331, 3, 22, 32syl3anc 1370 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → (𝑇 𝑉) ∈ (Base‘𝐾))
3427, 23, 5latjle12 18168 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾) ∧ (𝑇 𝑉) ∈ (Base‘𝐾))) → ((𝑆 (𝑇 𝑉) ∧ 𝑇 (𝑇 𝑉)) ↔ (𝑆 𝑇) (𝑇 𝑉)))
3526, 29, 31, 33, 34syl13anc 1371 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → ((𝑆 (𝑇 𝑉) ∧ 𝑇 (𝑇 𝑉)) ↔ (𝑆 𝑇) (𝑇 𝑉)))
3621, 25, 35mpbi2and 709 . . . . . 6 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → (𝑆 𝑇) (𝑇 𝑉))
3736adantr 481 . . . . 5 ((((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) ∧ 𝑇 (𝑃 𝑄)) → (𝑆 𝑇) (𝑇 𝑉))
38 simp3r3 1282 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → 𝑆 (𝑃 𝑄))
3938adantr 481 . . . . . 6 ((((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) ∧ 𝑇 (𝑃 𝑄)) → 𝑆 (𝑃 𝑄))
40 simpr 485 . . . . . 6 ((((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) ∧ 𝑇 (𝑃 𝑄)) → 𝑇 (𝑃 𝑄))
41 simp21 1205 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → 𝑃𝐴)
42 simp22 1206 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → 𝑄𝐴)
4327, 5, 6hlatjcl 37381 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) ∈ (Base‘𝐾))
441, 41, 42, 43syl3anc 1370 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → (𝑃 𝑄) ∈ (Base‘𝐾))
4527, 23, 5latjle12 18168 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾) ∧ (𝑃 𝑄) ∈ (Base‘𝐾))) → ((𝑆 (𝑃 𝑄) ∧ 𝑇 (𝑃 𝑄)) ↔ (𝑆 𝑇) (𝑃 𝑄)))
4626, 29, 31, 44, 45syl13anc 1371 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → ((𝑆 (𝑃 𝑄) ∧ 𝑇 (𝑃 𝑄)) ↔ (𝑆 𝑇) (𝑃 𝑄)))
4746adantr 481 . . . . . 6 ((((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) ∧ 𝑇 (𝑃 𝑄)) → ((𝑆 (𝑃 𝑄) ∧ 𝑇 (𝑃 𝑄)) ↔ (𝑆 𝑇) (𝑃 𝑄)))
4839, 40, 47mpbi2and 709 . . . . 5 ((((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) ∧ 𝑇 (𝑃 𝑄)) → (𝑆 𝑇) (𝑃 𝑄))
4927, 5, 6hlatjcl 37381 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴) → (𝑆 𝑇) ∈ (Base‘𝐾))
501, 2, 3, 49syl3anc 1370 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → (𝑆 𝑇) ∈ (Base‘𝐾))
51 cdleme22.m . . . . . . . 8 = (meet‘𝐾)
5227, 23, 51latlem12 18184 . . . . . . 7 ((𝐾 ∈ Lat ∧ ((𝑆 𝑇) ∈ (Base‘𝐾) ∧ (𝑇 𝑉) ∈ (Base‘𝐾) ∧ (𝑃 𝑄) ∈ (Base‘𝐾))) → (((𝑆 𝑇) (𝑇 𝑉) ∧ (𝑆 𝑇) (𝑃 𝑄)) ↔ (𝑆 𝑇) ((𝑇 𝑉) (𝑃 𝑄))))
5326, 50, 33, 44, 52syl13anc 1371 . . . . . 6 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → (((𝑆 𝑇) (𝑇 𝑉) ∧ (𝑆 𝑇) (𝑃 𝑄)) ↔ (𝑆 𝑇) ((𝑇 𝑉) (𝑃 𝑄))))
5453adantr 481 . . . . 5 ((((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) ∧ 𝑇 (𝑃 𝑄)) → (((𝑆 𝑇) (𝑇 𝑉) ∧ (𝑆 𝑇) (𝑃 𝑄)) ↔ (𝑆 𝑇) ((𝑇 𝑉) (𝑃 𝑄))))
5537, 48, 54mpbi2and 709 . . . 4 ((((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) ∧ 𝑇 (𝑃 𝑄)) → (𝑆 𝑇) ((𝑇 𝑉) (𝑃 𝑄)))
5655ex 413 . . 3 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → (𝑇 (𝑃 𝑄) → (𝑆 𝑇) ((𝑇 𝑉) (𝑃 𝑄))))
57 hlop 37376 . . . . . . . 8 (𝐾 ∈ HL → 𝐾 ∈ OP)
581, 57syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → 𝐾 ∈ OP)
5958adantr 481 . . . . . 6 ((((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) ∧ (((𝑇 𝑉) (𝑃 𝑄)) ∈ 𝐴 ∧ (𝑆 𝑇) ((𝑇 𝑉) (𝑃 𝑄)))) → 𝐾 ∈ OP)
6050adantr 481 . . . . . 6 ((((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) ∧ (((𝑇 𝑉) (𝑃 𝑄)) ∈ 𝐴 ∧ (𝑆 𝑇) ((𝑇 𝑉) (𝑃 𝑄)))) → (𝑆 𝑇) ∈ (Base‘𝐾))
61 simprl 768 . . . . . 6 ((((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) ∧ (((𝑇 𝑉) (𝑃 𝑄)) ∈ 𝐴 ∧ (𝑆 𝑇) ((𝑇 𝑉) (𝑃 𝑄)))) → ((𝑇 𝑉) (𝑃 𝑄)) ∈ 𝐴)
62 simprr 770 . . . . . 6 ((((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) ∧ (((𝑇 𝑉) (𝑃 𝑄)) ∈ 𝐴 ∧ (𝑆 𝑇) ((𝑇 𝑉) (𝑃 𝑄)))) → (𝑆 𝑇) ((𝑇 𝑉) (𝑃 𝑄)))
6327, 23, 12, 6leat3 37309 . . . . . 6 (((𝐾 ∈ OP ∧ (𝑆 𝑇) ∈ (Base‘𝐾) ∧ ((𝑇 𝑉) (𝑃 𝑄)) ∈ 𝐴) ∧ (𝑆 𝑇) ((𝑇 𝑉) (𝑃 𝑄))) → ((𝑆 𝑇) ∈ 𝐴 ∨ (𝑆 𝑇) = (0.‘𝐾)))
6459, 60, 61, 62, 63syl31anc 1372 . . . . 5 ((((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) ∧ (((𝑇 𝑉) (𝑃 𝑄)) ∈ 𝐴 ∧ (𝑆 𝑇) ((𝑇 𝑉) (𝑃 𝑄)))) → ((𝑆 𝑇) ∈ 𝐴 ∨ (𝑆 𝑇) = (0.‘𝐾)))
6564exp32 421 . . . 4 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → (((𝑇 𝑉) (𝑃 𝑄)) ∈ 𝐴 → ((𝑆 𝑇) ((𝑇 𝑉) (𝑃 𝑄)) → ((𝑆 𝑇) ∈ 𝐴 ∨ (𝑆 𝑇) = (0.‘𝐾)))))
66 breq2 5078 . . . . . . . . 9 (((𝑇 𝑉) (𝑃 𝑄)) = (0.‘𝐾) → ((𝑆 𝑇) ((𝑇 𝑉) (𝑃 𝑄)) ↔ (𝑆 𝑇) (0.‘𝐾)))
6766biimpa 477 . . . . . . . 8 ((((𝑇 𝑉) (𝑃 𝑄)) = (0.‘𝐾) ∧ (𝑆 𝑇) ((𝑇 𝑉) (𝑃 𝑄))) → (𝑆 𝑇) (0.‘𝐾))
6827, 23, 12ople0 37201 . . . . . . . . 9 ((𝐾 ∈ OP ∧ (𝑆 𝑇) ∈ (Base‘𝐾)) → ((𝑆 𝑇) (0.‘𝐾) ↔ (𝑆 𝑇) = (0.‘𝐾)))
6958, 50, 68syl2anc 584 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → ((𝑆 𝑇) (0.‘𝐾) ↔ (𝑆 𝑇) = (0.‘𝐾)))
7067, 69syl5ib 243 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → ((((𝑇 𝑉) (𝑃 𝑄)) = (0.‘𝐾) ∧ (𝑆 𝑇) ((𝑇 𝑉) (𝑃 𝑄))) → (𝑆 𝑇) = (0.‘𝐾)))
7170imp 407 . . . . . 6 ((((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) ∧ (((𝑇 𝑉) (𝑃 𝑄)) = (0.‘𝐾) ∧ (𝑆 𝑇) ((𝑇 𝑉) (𝑃 𝑄)))) → (𝑆 𝑇) = (0.‘𝐾))
7271olcd 871 . . . . 5 ((((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) ∧ (((𝑇 𝑉) (𝑃 𝑄)) = (0.‘𝐾) ∧ (𝑆 𝑇) ((𝑇 𝑉) (𝑃 𝑄)))) → ((𝑆 𝑇) ∈ 𝐴 ∨ (𝑆 𝑇) = (0.‘𝐾)))
7372exp32 421 . . . 4 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → (((𝑇 𝑉) (𝑃 𝑄)) = (0.‘𝐾) → ((𝑆 𝑇) ((𝑇 𝑉) (𝑃 𝑄)) → ((𝑆 𝑇) ∈ 𝐴 ∨ (𝑆 𝑇) = (0.‘𝐾)))))
74 simp3r1 1280 . . . . 5 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → (𝑇 𝑉) ≠ (𝑃 𝑄))
755, 51, 12, 62atmat0 37540 . . . . 5 (((𝐾 ∈ HL ∧ 𝑇𝐴𝑉𝐴) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑇 𝑉) ≠ (𝑃 𝑄))) → (((𝑇 𝑉) (𝑃 𝑄)) ∈ 𝐴 ∨ ((𝑇 𝑉) (𝑃 𝑄)) = (0.‘𝐾)))
761, 3, 22, 41, 42, 74, 75syl33anc 1384 . . . 4 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → (((𝑇 𝑉) (𝑃 𝑄)) ∈ 𝐴 ∨ ((𝑇 𝑉) (𝑃 𝑄)) = (0.‘𝐾)))
7765, 73, 76mpjaod 857 . . 3 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → ((𝑆 𝑇) ((𝑇 𝑉) (𝑃 𝑄)) → ((𝑆 𝑇) ∈ 𝐴 ∨ (𝑆 𝑇) = (0.‘𝐾))))
7856, 77syld 47 . 2 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → (𝑇 (𝑃 𝑄) → ((𝑆 𝑇) ∈ 𝐴 ∨ (𝑆 𝑇) = (0.‘𝐾))))
7920, 78mtod 197 1 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑇 𝑉) ≠ (𝑃 𝑄) ∧ 𝑆 (𝑇 𝑉) ∧ 𝑆 (𝑃 𝑄)))) → ¬ 𝑇 (𝑃 𝑄))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 844  w3a 1086   = wceq 1539  wcel 2106  wne 2943   class class class wbr 5074  cfv 6433  (class class class)co 7275  Basecbs 16912  lecple 16969  joincjn 18029  meetcmee 18030  0.cp0 18141  Latclat 18149  OPcops 37186  Atomscatm 37277  HLchlt 37364  LLinesclln 37505  LHypclh 37998
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-oprab 7279  df-proset 18013  df-poset 18031  df-plt 18048  df-lub 18064  df-glb 18065  df-join 18066  df-meet 18067  df-p0 18143  df-p1 18144  df-lat 18150  df-clat 18217  df-oposet 37190  df-ol 37192  df-oml 37193  df-covers 37280  df-ats 37281  df-atl 37312  df-cvlat 37336  df-hlat 37365  df-llines 37512
This theorem is referenced by:  cdleme22cN  38356  cdleme27a  38381
  Copyright terms: Public domain W3C validator