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

Theorem cdlemg27b 36673
Description: TODO: Fix comment. (Contributed by NM, 28-May-2013.)
Hypotheses
Ref Expression
cdlemg12.l = (le‘𝐾)
cdlemg12.j = (join‘𝐾)
cdlemg12.m = (meet‘𝐾)
cdlemg12.a 𝐴 = (Atoms‘𝐾)
cdlemg12.h 𝐻 = (LHyp‘𝐾)
cdlemg12.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
cdlemg12b.r 𝑅 = ((trL‘𝐾)‘𝑊)
cdlemg31.n 𝑁 = ((𝑃 𝑣) (𝑄 (𝑅𝐹)))
Assertion
Ref Expression
cdlemg27b ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → ¬ (𝑅𝐹) (𝑄 𝑧))

Proof of Theorem cdlemg27b
StepHypRef Expression
1 simp11 1260 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
2 simp12 1261 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
3 simp13 1262 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → (𝑄𝐴 ∧ ¬ 𝑄 𝑊))
4 simp22 1264 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → (𝑣𝐴𝑣 𝑊))
5 simp23l 1393 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → 𝐹𝑇)
6 simp31 1266 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → 𝑣 ≠ (𝑅𝐹))
7 cdlemg12.l . . . . . 6 = (le‘𝐾)
8 cdlemg12.j . . . . . 6 = (join‘𝐾)
9 cdlemg12.m . . . . . 6 = (meet‘𝐾)
10 cdlemg12.a . . . . . 6 𝐴 = (Atoms‘𝐾)
11 cdlemg12.h . . . . . 6 𝐻 = (LHyp‘𝐾)
12 cdlemg12.t . . . . . 6 𝑇 = ((LTrn‘𝐾)‘𝑊)
13 cdlemg12b.r . . . . . 6 𝑅 = ((trL‘𝐾)‘𝑊)
14 cdlemg31.n . . . . . 6 𝑁 = ((𝑃 𝑣) (𝑄 (𝑅𝐹)))
157, 8, 9, 10, 11, 12, 13, 14cdlemg31b0a 36672 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑣𝐴𝑣 𝑊)) ∧ (𝐹𝑇𝑣 ≠ (𝑅𝐹))) → (𝑁𝐴𝑁 = (0.‘𝐾)))
161, 2, 3, 4, 5, 6, 15syl132anc 1507 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → (𝑁𝐴𝑁 = (0.‘𝐾)))
17 simp23r 1394 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → 𝑧𝑁)
1817adantr 472 . . . . 5 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) ∧ (𝑁𝐴𝑁 = (0.‘𝐾))) → 𝑧𝑁)
19 simp11l 1383 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → 𝐾 ∈ HL)
2019adantr 472 . . . . . . . . 9 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) ∧ 𝑁𝐴) → 𝐾 ∈ HL)
21 hlatl 35337 . . . . . . . . 9 (𝐾 ∈ HL → 𝐾 ∈ AtLat)
2220, 21syl 17 . . . . . . . 8 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) ∧ 𝑁𝐴) → 𝐾 ∈ AtLat)
23 simpl21 1335 . . . . . . . 8 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) ∧ 𝑁𝐴) → 𝑧𝐴)
24 simpr 477 . . . . . . . 8 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) ∧ 𝑁𝐴) → 𝑁𝐴)
257, 10atcmp 35288 . . . . . . . 8 ((𝐾 ∈ AtLat ∧ 𝑧𝐴𝑁𝐴) → (𝑧 𝑁𝑧 = 𝑁))
2622, 23, 24, 25syl3anc 1490 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) ∧ 𝑁𝐴) → (𝑧 𝑁𝑧 = 𝑁))
2726necon3bbid 2974 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) ∧ 𝑁𝐴) → (¬ 𝑧 𝑁𝑧𝑁))
2819adantr 472 . . . . . . . . . 10 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) ∧ 𝑁 = (0.‘𝐾)) → 𝐾 ∈ HL)
2928, 21syl 17 . . . . . . . . 9 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) ∧ 𝑁 = (0.‘𝐾)) → 𝐾 ∈ AtLat)
30 simpl21 1335 . . . . . . . . 9 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) ∧ 𝑁 = (0.‘𝐾)) → 𝑧𝐴)
31 eqid 2765 . . . . . . . . . 10 (0.‘𝐾) = (0.‘𝐾)
327, 31, 10atnle0 35286 . . . . . . . . 9 ((𝐾 ∈ AtLat ∧ 𝑧𝐴) → ¬ 𝑧 (0.‘𝐾))
3329, 30, 32syl2anc 579 . . . . . . . 8 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) ∧ 𝑁 = (0.‘𝐾)) → ¬ 𝑧 (0.‘𝐾))
34 simpr 477 . . . . . . . . 9 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) ∧ 𝑁 = (0.‘𝐾)) → 𝑁 = (0.‘𝐾))
3534breq2d 4823 . . . . . . . 8 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) ∧ 𝑁 = (0.‘𝐾)) → (𝑧 𝑁𝑧 (0.‘𝐾)))
3633, 35mtbird 316 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) ∧ 𝑁 = (0.‘𝐾)) → ¬ 𝑧 𝑁)
3717adantr 472 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) ∧ 𝑁 = (0.‘𝐾)) → 𝑧𝑁)
3836, 372thd 256 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) ∧ 𝑁 = (0.‘𝐾)) → (¬ 𝑧 𝑁𝑧𝑁))
3927, 38jaodan 980 . . . . 5 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) ∧ (𝑁𝐴𝑁 = (0.‘𝐾))) → (¬ 𝑧 𝑁𝑧𝑁))
4018, 39mpbird 248 . . . 4 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) ∧ (𝑁𝐴𝑁 = (0.‘𝐾))) → ¬ 𝑧 𝑁)
4116, 40mpdan 678 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → ¬ 𝑧 𝑁)
42 simp32 1267 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → 𝑧 (𝑃 𝑣))
4319hllatd 35341 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → 𝐾 ∈ Lat)
44 simp21 1263 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → 𝑧𝐴)
45 eqid 2765 . . . . . . . . 9 (Base‘𝐾) = (Base‘𝐾)
4645, 10atbase 35266 . . . . . . . 8 (𝑧𝐴𝑧 ∈ (Base‘𝐾))
4744, 46syl 17 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → 𝑧 ∈ (Base‘𝐾))
48 simp12l 1385 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → 𝑃𝐴)
49 simp22l 1391 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → 𝑣𝐴)
5045, 8, 10hlatjcl 35344 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑣𝐴) → (𝑃 𝑣) ∈ (Base‘𝐾))
5119, 48, 49, 50syl3anc 1490 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → (𝑃 𝑣) ∈ (Base‘𝐾))
52 simp13l 1387 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → 𝑄𝐴)
53 simp33 1268 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → (𝐹𝑃) ≠ 𝑃)
547, 10, 11, 12, 13trlat 36146 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝐹𝑇 ∧ (𝐹𝑃) ≠ 𝑃)) → (𝑅𝐹) ∈ 𝐴)
551, 2, 5, 53, 54syl112anc 1493 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → (𝑅𝐹) ∈ 𝐴)
5645, 8, 10hlatjcl 35344 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑄𝐴 ∧ (𝑅𝐹) ∈ 𝐴) → (𝑄 (𝑅𝐹)) ∈ (Base‘𝐾))
5719, 52, 55, 56syl3anc 1490 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → (𝑄 (𝑅𝐹)) ∈ (Base‘𝐾))
5845, 7, 9latlem12 17358 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑧 ∈ (Base‘𝐾) ∧ (𝑃 𝑣) ∈ (Base‘𝐾) ∧ (𝑄 (𝑅𝐹)) ∈ (Base‘𝐾))) → ((𝑧 (𝑃 𝑣) ∧ 𝑧 (𝑄 (𝑅𝐹))) ↔ 𝑧 ((𝑃 𝑣) (𝑄 (𝑅𝐹)))))
5943, 47, 51, 57, 58syl13anc 1491 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → ((𝑧 (𝑃 𝑣) ∧ 𝑧 (𝑄 (𝑅𝐹))) ↔ 𝑧 ((𝑃 𝑣) (𝑄 (𝑅𝐹)))))
6014breq2i 4819 . . . . . 6 (𝑧 𝑁𝑧 ((𝑃 𝑣) (𝑄 (𝑅𝐹))))
6159, 60syl6bbr 280 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → ((𝑧 (𝑃 𝑣) ∧ 𝑧 (𝑄 (𝑅𝐹))) ↔ 𝑧 𝑁))
6261biimpd 220 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → ((𝑧 (𝑃 𝑣) ∧ 𝑧 (𝑄 (𝑅𝐹))) → 𝑧 𝑁))
6342, 62mpand 686 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → (𝑧 (𝑄 (𝑅𝐹)) → 𝑧 𝑁))
6441, 63mtod 189 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → ¬ 𝑧 (𝑄 (𝑅𝐹)))
657, 11, 12, 13trlle 36161 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) → (𝑅𝐹) 𝑊)
661, 5, 65syl2anc 579 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → (𝑅𝐹) 𝑊)
67 simp13r 1388 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → ¬ 𝑄 𝑊)
68 nbrne2 4831 . . . 4 (((𝑅𝐹) 𝑊 ∧ ¬ 𝑄 𝑊) → (𝑅𝐹) ≠ 𝑄)
6966, 67, 68syl2anc 579 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → (𝑅𝐹) ≠ 𝑄)
707, 8, 10hlatexch1 35372 . . 3 ((𝐾 ∈ HL ∧ ((𝑅𝐹) ∈ 𝐴𝑧𝐴𝑄𝐴) ∧ (𝑅𝐹) ≠ 𝑄) → ((𝑅𝐹) (𝑄 𝑧) → 𝑧 (𝑄 (𝑅𝐹))))
7119, 55, 44, 52, 69, 70syl131anc 1502 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → ((𝑅𝐹) (𝑄 𝑧) → 𝑧 (𝑄 (𝑅𝐹))))
7264, 71mtod 189 1 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑧𝐴 ∧ (𝑣𝐴𝑣 𝑊) ∧ (𝐹𝑇𝑧𝑁)) ∧ (𝑣 ≠ (𝑅𝐹) ∧ 𝑧 (𝑃 𝑣) ∧ (𝐹𝑃) ≠ 𝑃)) → ¬ (𝑅𝐹) (𝑄 𝑧))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 873  w3a 1107   = wceq 1652  wcel 2155  wne 2937   class class class wbr 4811  cfv 6070  (class class class)co 6846  Basecbs 16144  lecple 16235  joincjn 17224  meetcmee 17225  0.cp0 17317  Latclat 17325  Atomscatm 35240  AtLatcal 35241  HLchlt 35327  LHypclh 35961  LTrncltrn 36078  trLctrl 36135
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 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151
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 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-op 4343  df-uni 4597  df-iun 4680  df-iin 4681  df-br 4812  df-opab 4874  df-mpt 4891  df-id 5187  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-riota 6807  df-ov 6849  df-oprab 6850  df-mpt2 6851  df-1st 7370  df-2nd 7371  df-map 8066  df-proset 17208  df-poset 17226  df-plt 17238  df-lub 17254  df-glb 17255  df-join 17256  df-meet 17257  df-p0 17319  df-p1 17320  df-lat 17326  df-clat 17388  df-oposet 35153  df-ol 35155  df-oml 35156  df-covers 35243  df-ats 35244  df-atl 35275  df-cvlat 35299  df-hlat 35328  df-llines 35475  df-psubsp 35480  df-pmap 35481  df-padd 35773  df-lhyp 35965  df-laut 35966  df-ldil 36081  df-ltrn 36082  df-trl 36136
This theorem is referenced by:  cdlemg28b  36680
  Copyright terms: Public domain W3C validator