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

Theorem cdlemg16 37972
 Description: Part of proof of Lemma G of [Crawley] p. 116; 2nd line p. 117, which says that (our) cdlemg10 37956 "implies (2)" (of p. 116). No details are provided by the authors, so there may be a shorter proof; but ours requires the 14 lemmas, one using Desargues's law dalaw 37201, in order to make this inference. This final step eliminates the (𝑅‘𝐹) ≠ (𝑅‘𝐺) condition from cdlemg12 37965. TODO: FIX COMMENT. TODO: should we also eliminate 𝑃 ≠ 𝑄 here (or earlier)? Do it if we don't need to add it in for something else later. (Contributed by NM, 6-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‘𝐾)‘𝑊)
Assertion
Ref Expression
cdlemg16 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝐹𝑇𝐺𝑇𝑃𝑄) ∧ (¬ (𝑅𝐹) (𝑃 𝑄) ∧ ¬ (𝑅𝐺) (𝑃 𝑄) ∧ ((𝐹‘(𝐺𝑃)) (𝐹‘(𝐺𝑄))) ≠ (𝑃 𝑄))) → ((𝑃 (𝐹‘(𝐺𝑃))) 𝑊) = ((𝑄 (𝐹‘(𝐺𝑄))) 𝑊))

Proof of Theorem cdlemg16
StepHypRef Expression
1 simpl1 1188 . . 3 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝐹𝑇𝐺𝑇𝑃𝑄) ∧ (¬ (𝑅𝐹) (𝑃 𝑄) ∧ ¬ (𝑅𝐺) (𝑃 𝑄) ∧ ((𝐹‘(𝐺𝑃)) (𝐹‘(𝐺𝑄))) ≠ (𝑃 𝑄))) ∧ (𝑅𝐹) = (𝑅𝐺)) → ((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)))
2 simpl21 1248 . . 3 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝐹𝑇𝐺𝑇𝑃𝑄) ∧ (¬ (𝑅𝐹) (𝑃 𝑄) ∧ ¬ (𝑅𝐺) (𝑃 𝑄) ∧ ((𝐹‘(𝐺𝑃)) (𝐹‘(𝐺𝑄))) ≠ (𝑃 𝑄))) ∧ (𝑅𝐹) = (𝑅𝐺)) → 𝐹𝑇)
3 simpl22 1249 . . 3 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝐹𝑇𝐺𝑇𝑃𝑄) ∧ (¬ (𝑅𝐹) (𝑃 𝑄) ∧ ¬ (𝑅𝐺) (𝑃 𝑄) ∧ ((𝐹‘(𝐺𝑃)) (𝐹‘(𝐺𝑄))) ≠ (𝑃 𝑄))) ∧ (𝑅𝐹) = (𝑅𝐺)) → 𝐺𝑇)
4 simpr 488 . . 3 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝐹𝑇𝐺𝑇𝑃𝑄) ∧ (¬ (𝑅𝐹) (𝑃 𝑄) ∧ ¬ (𝑅𝐺) (𝑃 𝑄) ∧ ((𝐹‘(𝐺𝑃)) (𝐹‘(𝐺𝑄))) ≠ (𝑃 𝑄))) ∧ (𝑅𝐹) = (𝑅𝐺)) → (𝑅𝐹) = (𝑅𝐺))
5 cdlemg12.l . . . 4 = (le‘𝐾)
6 cdlemg12.j . . . 4 = (join‘𝐾)
7 cdlemg12.m . . . 4 = (meet‘𝐾)
8 cdlemg12.a . . . 4 𝐴 = (Atoms‘𝐾)
9 cdlemg12.h . . . 4 𝐻 = (LHyp‘𝐾)
10 cdlemg12.t . . . 4 𝑇 = ((LTrn‘𝐾)‘𝑊)
11 cdlemg12b.r . . . 4 𝑅 = ((trL‘𝐾)‘𝑊)
125, 6, 7, 8, 9, 10, 11cdlemg15 37971 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑅𝐹) = (𝑅𝐺)) → ((𝑃 (𝐹‘(𝐺𝑃))) 𝑊) = ((𝑄 (𝐹‘(𝐺𝑄))) 𝑊))
131, 2, 3, 4, 12syl121anc 1372 . 2 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝐹𝑇𝐺𝑇𝑃𝑄) ∧ (¬ (𝑅𝐹) (𝑃 𝑄) ∧ ¬ (𝑅𝐺) (𝑃 𝑄) ∧ ((𝐹‘(𝐺𝑃)) (𝐹‘(𝐺𝑄))) ≠ (𝑃 𝑄))) ∧ (𝑅𝐹) = (𝑅𝐺)) → ((𝑃 (𝐹‘(𝐺𝑃))) 𝑊) = ((𝑄 (𝐹‘(𝐺𝑄))) 𝑊))
14 simpl1 1188 . . 3 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝐹𝑇𝐺𝑇𝑃𝑄) ∧ (¬ (𝑅𝐹) (𝑃 𝑄) ∧ ¬ (𝑅𝐺) (𝑃 𝑄) ∧ ((𝐹‘(𝐺𝑃)) (𝐹‘(𝐺𝑄))) ≠ (𝑃 𝑄))) ∧ (𝑅𝐹) ≠ (𝑅𝐺)) → ((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)))
15 simpl2 1189 . . 3 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝐹𝑇𝐺𝑇𝑃𝑄) ∧ (¬ (𝑅𝐹) (𝑃 𝑄) ∧ ¬ (𝑅𝐺) (𝑃 𝑄) ∧ ((𝐹‘(𝐺𝑃)) (𝐹‘(𝐺𝑄))) ≠ (𝑃 𝑄))) ∧ (𝑅𝐹) ≠ (𝑅𝐺)) → (𝐹𝑇𝐺𝑇𝑃𝑄))
16 simpl31 1251 . . . 4 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝐹𝑇𝐺𝑇𝑃𝑄) ∧ (¬ (𝑅𝐹) (𝑃 𝑄) ∧ ¬ (𝑅𝐺) (𝑃 𝑄) ∧ ((𝐹‘(𝐺𝑃)) (𝐹‘(𝐺𝑄))) ≠ (𝑃 𝑄))) ∧ (𝑅𝐹) ≠ (𝑅𝐺)) → ¬ (𝑅𝐹) (𝑃 𝑄))
17 simpl32 1252 . . . 4 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝐹𝑇𝐺𝑇𝑃𝑄) ∧ (¬ (𝑅𝐹) (𝑃 𝑄) ∧ ¬ (𝑅𝐺) (𝑃 𝑄) ∧ ((𝐹‘(𝐺𝑃)) (𝐹‘(𝐺𝑄))) ≠ (𝑃 𝑄))) ∧ (𝑅𝐹) ≠ (𝑅𝐺)) → ¬ (𝑅𝐺) (𝑃 𝑄))
1816, 17jca 515 . . 3 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝐹𝑇𝐺𝑇𝑃𝑄) ∧ (¬ (𝑅𝐹) (𝑃 𝑄) ∧ ¬ (𝑅𝐺) (𝑃 𝑄) ∧ ((𝐹‘(𝐺𝑃)) (𝐹‘(𝐺𝑄))) ≠ (𝑃 𝑄))) ∧ (𝑅𝐹) ≠ (𝑅𝐺)) → (¬ (𝑅𝐹) (𝑃 𝑄) ∧ ¬ (𝑅𝐺) (𝑃 𝑄)))
19 simpr 488 . . 3 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝐹𝑇𝐺𝑇𝑃𝑄) ∧ (¬ (𝑅𝐹) (𝑃 𝑄) ∧ ¬ (𝑅𝐺) (𝑃 𝑄) ∧ ((𝐹‘(𝐺𝑃)) (𝐹‘(𝐺𝑄))) ≠ (𝑃 𝑄))) ∧ (𝑅𝐹) ≠ (𝑅𝐺)) → (𝑅𝐹) ≠ (𝑅𝐺))
20 simpl33 1253 . . 3 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝐹𝑇𝐺𝑇𝑃𝑄) ∧ (¬ (𝑅𝐹) (𝑃 𝑄) ∧ ¬ (𝑅𝐺) (𝑃 𝑄) ∧ ((𝐹‘(𝐺𝑃)) (𝐹‘(𝐺𝑄))) ≠ (𝑃 𝑄))) ∧ (𝑅𝐹) ≠ (𝑅𝐺)) → ((𝐹‘(𝐺𝑃)) (𝐹‘(𝐺𝑄))) ≠ (𝑃 𝑄))
215, 6, 7, 8, 9, 10, 11cdlemg12 37965 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝐹𝑇𝐺𝑇𝑃𝑄) ∧ ((¬ (𝑅𝐹) (𝑃 𝑄) ∧ ¬ (𝑅𝐺) (𝑃 𝑄)) ∧ (𝑅𝐹) ≠ (𝑅𝐺) ∧ ((𝐹‘(𝐺𝑃)) (𝐹‘(𝐺𝑄))) ≠ (𝑃 𝑄))) → ((𝑃 (𝐹‘(𝐺𝑃))) 𝑊) = ((𝑄 (𝐹‘(𝐺𝑄))) 𝑊))
2214, 15, 18, 19, 20, 21syl113anc 1379 . 2 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝐹𝑇𝐺𝑇𝑃𝑄) ∧ (¬ (𝑅𝐹) (𝑃 𝑄) ∧ ¬ (𝑅𝐺) (𝑃 𝑄) ∧ ((𝐹‘(𝐺𝑃)) (𝐹‘(𝐺𝑄))) ≠ (𝑃 𝑄))) ∧ (𝑅𝐹) ≠ (𝑅𝐺)) → ((𝑃 (𝐹‘(𝐺𝑃))) 𝑊) = ((𝑄 (𝐹‘(𝐺𝑄))) 𝑊))
2313, 22pm2.61dane 3074 1 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝐹𝑇𝐺𝑇𝑃𝑄) ∧ (¬ (𝑅𝐹) (𝑃 𝑄) ∧ ¬ (𝑅𝐺) (𝑃 𝑄) ∧ ((𝐹‘(𝐺𝑃)) (𝐹‘(𝐺𝑄))) ≠ (𝑃 𝑄))) → ((𝑃 (𝐹‘(𝐺𝑃))) 𝑊) = ((𝑄 (𝐹‘(𝐺𝑄))) 𝑊))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2987   class class class wbr 5031  ‘cfv 6325  (class class class)co 7136  lecple 16567  joincjn 17549  meetcmee 17550  Atomscatm 36578  HLchlt 36665  LHypclh 37299  LTrncltrn 37416  trLctrl 37473 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7444  ax-riotaBAD 36268 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 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-iun 4884  df-iin 4885  df-br 5032  df-opab 5094  df-mpt 5112  df-id 5426  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-iota 6284  df-fun 6327  df-fn 6328  df-f 6329  df-f1 6330  df-fo 6331  df-f1o 6332  df-fv 6333  df-riota 7094  df-ov 7139  df-oprab 7140  df-mpo 7141  df-1st 7674  df-2nd 7675  df-undef 7925  df-map 8394  df-proset 17533  df-poset 17551  df-plt 17563  df-lub 17579  df-glb 17580  df-join 17581  df-meet 17582  df-p0 17644  df-p1 17645  df-lat 17651  df-clat 17713  df-oposet 36491  df-ol 36493  df-oml 36494  df-covers 36581  df-ats 36582  df-atl 36613  df-cvlat 36637  df-hlat 36666  df-llines 36813  df-lplanes 36814  df-lvols 36815  df-lines 36816  df-psubsp 36818  df-pmap 36819  df-padd 37111  df-lhyp 37303  df-laut 37304  df-ldil 37419  df-ltrn 37420  df-trl 37474 This theorem is referenced by:  cdlemg16z  37974
 Copyright terms: Public domain W3C validator