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

Theorem cdlemk10 38044
Description: Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 29-Jun-2013.)
Hypotheses
Ref Expression
cdlemk.b 𝐵 = (Base‘𝐾)
cdlemk.l = (le‘𝐾)
cdlemk.j = (join‘𝐾)
cdlemk.a 𝐴 = (Atoms‘𝐾)
cdlemk.h 𝐻 = (LHyp‘𝐾)
cdlemk.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
cdlemk.r 𝑅 = ((trL‘𝐾)‘𝑊)
cdlemk.m = (meet‘𝐾)
cdlemk.v1 𝑉 = (((𝐺𝑃) (𝑋𝑃)) ((𝑅‘(𝐺𝐹)) (𝑅‘(𝑋𝐹))))
Assertion
Ref Expression
cdlemk10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑉 (𝑅‘(𝑋𝐺)))

Proof of Theorem cdlemk10
StepHypRef Expression
1 cdlemk.v1 . 2 𝑉 = (((𝐺𝑃) (𝑋𝑃)) ((𝑅‘(𝐺𝐹)) (𝑅‘(𝑋𝐹))))
2 simp1 1133 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
3 simp22 1204 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝐺𝑇)
4 simp21 1203 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝐹𝑇)
5 cdlemk.h . . . . . . . . 9 𝐻 = (LHyp‘𝐾)
6 cdlemk.t . . . . . . . . 9 𝑇 = ((LTrn‘𝐾)‘𝑊)
75, 6ltrncnv 37347 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) → 𝐹𝑇)
82, 4, 7syl2anc 587 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝐹𝑇)
95, 6ltrnco 37920 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐺𝑇𝐹𝑇) → (𝐺𝐹) ∈ 𝑇)
102, 3, 8, 9syl3anc 1368 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝐺𝐹) ∈ 𝑇)
11 cdlemk.l . . . . . . 7 = (le‘𝐾)
12 cdlemk.r . . . . . . 7 𝑅 = ((trL‘𝐾)‘𝑊)
1311, 5, 6, 12trlle 37385 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐺𝐹) ∈ 𝑇) → (𝑅‘(𝐺𝐹)) 𝑊)
142, 10, 13syl2anc 587 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅‘(𝐺𝐹)) 𝑊)
15 simp23 1205 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑋𝑇)
165, 6ltrnco 37920 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋𝑇𝐹𝑇) → (𝑋𝐹) ∈ 𝑇)
172, 15, 8, 16syl3anc 1368 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑋𝐹) ∈ 𝑇)
1811, 5, 6, 12trlle 37385 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐹) ∈ 𝑇) → (𝑅‘(𝑋𝐹)) 𝑊)
192, 17, 18syl2anc 587 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅‘(𝑋𝐹)) 𝑊)
20 simp1l 1194 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝐾 ∈ HL)
2120hllatd 36565 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝐾 ∈ Lat)
22 cdlemk.b . . . . . . . 8 𝐵 = (Base‘𝐾)
2322, 5, 6, 12trlcl 37365 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐺𝐹) ∈ 𝑇) → (𝑅‘(𝐺𝐹)) ∈ 𝐵)
242, 10, 23syl2anc 587 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅‘(𝐺𝐹)) ∈ 𝐵)
2522, 5, 6, 12trlcl 37365 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐹) ∈ 𝑇) → (𝑅‘(𝑋𝐹)) ∈ 𝐵)
262, 17, 25syl2anc 587 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅‘(𝑋𝐹)) ∈ 𝐵)
27 simp1r 1195 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑊𝐻)
2822, 5lhpbase 37199 . . . . . . 7 (𝑊𝐻𝑊𝐵)
2927, 28syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑊𝐵)
30 cdlemk.j . . . . . . 7 = (join‘𝐾)
3122, 11, 30latjle12 17663 . . . . . 6 ((𝐾 ∈ Lat ∧ ((𝑅‘(𝐺𝐹)) ∈ 𝐵 ∧ (𝑅‘(𝑋𝐹)) ∈ 𝐵𝑊𝐵)) → (((𝑅‘(𝐺𝐹)) 𝑊 ∧ (𝑅‘(𝑋𝐹)) 𝑊) ↔ ((𝑅‘(𝐺𝐹)) (𝑅‘(𝑋𝐹))) 𝑊))
3221, 24, 26, 29, 31syl13anc 1369 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (((𝑅‘(𝐺𝐹)) 𝑊 ∧ (𝑅‘(𝑋𝐹)) 𝑊) ↔ ((𝑅‘(𝐺𝐹)) (𝑅‘(𝑋𝐹))) 𝑊))
3314, 19, 32mpbi2and 711 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑅‘(𝐺𝐹)) (𝑅‘(𝑋𝐹))) 𝑊)
3422, 30latjcl 17652 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑅‘(𝐺𝐹)) ∈ 𝐵 ∧ (𝑅‘(𝑋𝐹)) ∈ 𝐵) → ((𝑅‘(𝐺𝐹)) (𝑅‘(𝑋𝐹))) ∈ 𝐵)
3521, 24, 26, 34syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑅‘(𝐺𝐹)) (𝑅‘(𝑋𝐹))) ∈ 𝐵)
36 simp3l 1198 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑃𝐴)
37 cdlemk.a . . . . . . . 8 𝐴 = (Atoms‘𝐾)
3811, 37, 5, 6ltrnat 37341 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐺𝑇𝑃𝐴) → (𝐺𝑃) ∈ 𝐴)
392, 3, 36, 38syl3anc 1368 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝐺𝑃) ∈ 𝐴)
4011, 37, 5, 6ltrnat 37341 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋𝑇𝑃𝐴) → (𝑋𝑃) ∈ 𝐴)
412, 15, 36, 40syl3anc 1368 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑋𝑃) ∈ 𝐴)
4222, 30, 37hlatjcl 36568 . . . . . 6 ((𝐾 ∈ HL ∧ (𝐺𝑃) ∈ 𝐴 ∧ (𝑋𝑃) ∈ 𝐴) → ((𝐺𝑃) (𝑋𝑃)) ∈ 𝐵)
4320, 39, 41, 42syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝐺𝑃) (𝑋𝑃)) ∈ 𝐵)
44 cdlemk.m . . . . . 6 = (meet‘𝐾)
4522, 11, 44latmlem2 17683 . . . . 5 ((𝐾 ∈ Lat ∧ (((𝑅‘(𝐺𝐹)) (𝑅‘(𝑋𝐹))) ∈ 𝐵𝑊𝐵 ∧ ((𝐺𝑃) (𝑋𝑃)) ∈ 𝐵)) → (((𝑅‘(𝐺𝐹)) (𝑅‘(𝑋𝐹))) 𝑊 → (((𝐺𝑃) (𝑋𝑃)) ((𝑅‘(𝐺𝐹)) (𝑅‘(𝑋𝐹)))) (((𝐺𝑃) (𝑋𝑃)) 𝑊)))
4621, 35, 29, 43, 45syl13anc 1369 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (((𝑅‘(𝐺𝐹)) (𝑅‘(𝑋𝐹))) 𝑊 → (((𝐺𝑃) (𝑋𝑃)) ((𝑅‘(𝐺𝐹)) (𝑅‘(𝑋𝐹)))) (((𝐺𝑃) (𝑋𝑃)) 𝑊)))
4733, 46mpd 15 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (((𝐺𝑃) (𝑋𝑃)) ((𝑅‘(𝐺𝐹)) (𝑅‘(𝑋𝐹)))) (((𝐺𝑃) (𝑋𝑃)) 𝑊))
48 simp3 1135 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
4922, 11, 30, 37, 5, 6, 12, 44cdlemk9 38040 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (((𝐺𝑃) (𝑋𝑃)) 𝑊) = (𝑅‘(𝑋𝐺)))
5020, 27, 3, 15, 48, 49syl221anc 1378 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (((𝐺𝑃) (𝑋𝑃)) 𝑊) = (𝑅‘(𝑋𝐺)))
5147, 50breqtrd 5075 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (((𝐺𝑃) (𝑋𝑃)) ((𝑅‘(𝐺𝐹)) (𝑅‘(𝑋𝐹)))) (𝑅‘(𝑋𝐺)))
521, 51eqbrtrid 5084 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇𝑋𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑉 (𝑅‘(𝑋𝐺)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2115   class class class wbr 5049  ccnv 5537  ccom 5542  cfv 6338  (class class class)co 7140  Basecbs 16474  lecple 16563  joincjn 17545  meetcmee 17546  Latclat 17646  Atomscatm 36464  HLchlt 36551  LHypclh 37185  LTrncltrn 37302  trLctrl 37359
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5173  ax-sep 5186  ax-nul 5193  ax-pow 5249  ax-pr 5313  ax-un 7446  ax-riotaBAD 36154
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3014  df-ral 3137  df-rex 3138  df-reu 3139  df-rmo 3140  df-rab 3141  df-v 3481  df-sbc 3758  df-csb 3866  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-nul 4275  df-if 4449  df-pw 4522  df-sn 4549  df-pr 4551  df-op 4555  df-uni 4822  df-iun 4904  df-iin 4905  df-br 5050  df-opab 5112  df-mpt 5130  df-id 5443  df-xp 5544  df-rel 5545  df-cnv 5546  df-co 5547  df-dm 5548  df-rn 5549  df-res 5550  df-ima 5551  df-iota 6297  df-fun 6340  df-fn 6341  df-f 6342  df-f1 6343  df-fo 6344  df-f1o 6345  df-fv 6346  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-1st 7674  df-2nd 7675  df-undef 7924  df-map 8393  df-proset 17529  df-poset 17547  df-plt 17559  df-lub 17575  df-glb 17576  df-join 17577  df-meet 17578  df-p0 17640  df-p1 17641  df-lat 17647  df-clat 17709  df-oposet 36377  df-ol 36379  df-oml 36380  df-covers 36467  df-ats 36468  df-atl 36499  df-cvlat 36523  df-hlat 36552  df-llines 36699  df-lplanes 36700  df-lvols 36701  df-lines 36702  df-psubsp 36704  df-pmap 36705  df-padd 36997  df-lhyp 37189  df-laut 37190  df-ldil 37305  df-ltrn 37306  df-trl 37360
This theorem is referenced by:  cdlemk11  38050  cdlemk11u  38072
  Copyright terms: Public domain W3C validator