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

Theorem dalem25 35861
Description: Lemma for dath 35899. Show that the dummy center of perspectivity 𝑐 is different from auxiliary atom 𝐺. (Contributed by NM, 3-Aug-2012.)
Hypotheses
Ref Expression
dalem.ph (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (𝑌𝑂𝑍𝑂) ∧ ((¬ 𝐶 (𝑃 𝑄) ∧ ¬ 𝐶 (𝑄 𝑅) ∧ ¬ 𝐶 (𝑅 𝑃)) ∧ (¬ 𝐶 (𝑆 𝑇) ∧ ¬ 𝐶 (𝑇 𝑈) ∧ ¬ 𝐶 (𝑈 𝑆)) ∧ (𝐶 (𝑃 𝑆) ∧ 𝐶 (𝑄 𝑇) ∧ 𝐶 (𝑅 𝑈)))))
dalem.l = (le‘𝐾)
dalem.j = (join‘𝐾)
dalem.a 𝐴 = (Atoms‘𝐾)
dalem.ps (𝜓 ↔ ((𝑐𝐴𝑑𝐴) ∧ ¬ 𝑐 𝑌 ∧ (𝑑𝑐 ∧ ¬ 𝑑 𝑌𝐶 (𝑐 𝑑))))
dalem23.m = (meet‘𝐾)
dalem23.o 𝑂 = (LPlanes‘𝐾)
dalem23.y 𝑌 = ((𝑃 𝑄) 𝑅)
dalem23.z 𝑍 = ((𝑆 𝑇) 𝑈)
dalem23.g 𝐺 = ((𝑐 𝑃) (𝑑 𝑆))
Assertion
Ref Expression
dalem25 ((𝜑𝑌 = 𝑍𝜓) → 𝑐𝐺)

Proof of Theorem dalem25
StepHypRef Expression
1 dalem.ph . . . 4 (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (𝑌𝑂𝑍𝑂) ∧ ((¬ 𝐶 (𝑃 𝑄) ∧ ¬ 𝐶 (𝑄 𝑅) ∧ ¬ 𝐶 (𝑅 𝑃)) ∧ (¬ 𝐶 (𝑆 𝑇) ∧ ¬ 𝐶 (𝑇 𝑈) ∧ ¬ 𝐶 (𝑈 𝑆)) ∧ (𝐶 (𝑃 𝑆) ∧ 𝐶 (𝑄 𝑇) ∧ 𝐶 (𝑅 𝑈)))))
2 dalem.l . . . 4 = (le‘𝐾)
3 dalem.j . . . 4 = (join‘𝐾)
4 dalem.a . . . 4 𝐴 = (Atoms‘𝐾)
51, 2, 3, 4dalemcnes 35813 . . 3 (𝜑𝐶𝑆)
653ad2ant1 1124 . 2 ((𝜑𝑌 = 𝑍𝜓) → 𝐶𝑆)
7 dalem.ps . . . . . . . . . . 11 (𝜓 ↔ ((𝑐𝐴𝑑𝐴) ∧ ¬ 𝑐 𝑌 ∧ (𝑑𝑐 ∧ ¬ 𝑑 𝑌𝐶 (𝑐 𝑑))))
87dalemclccjdd 35851 . . . . . . . . . 10 (𝜓𝐶 (𝑐 𝑑))
983ad2ant3 1126 . . . . . . . . 9 ((𝜑𝑌 = 𝑍𝜓) → 𝐶 (𝑐 𝑑))
109adantr 474 . . . . . . . 8 (((𝜑𝑌 = 𝑍𝜓) ∧ 𝑐 = 𝐺) → 𝐶 (𝑐 𝑑))
11 simpr 479 . . . . . . . . . 10 (((𝜑𝑌 = 𝑍𝜓) ∧ 𝑐 = 𝐺) → 𝑐 = 𝐺)
12 dalem23.g . . . . . . . . . . . . 13 𝐺 = ((𝑐 𝑃) (𝑑 𝑆))
131dalemkelat 35787 . . . . . . . . . . . . . . 15 (𝜑𝐾 ∈ Lat)
14133ad2ant1 1124 . . . . . . . . . . . . . 14 ((𝜑𝑌 = 𝑍𝜓) → 𝐾 ∈ Lat)
151dalemkehl 35786 . . . . . . . . . . . . . . . 16 (𝜑𝐾 ∈ HL)
16153ad2ant1 1124 . . . . . . . . . . . . . . 15 ((𝜑𝑌 = 𝑍𝜓) → 𝐾 ∈ HL)
177dalemccea 35846 . . . . . . . . . . . . . . . 16 (𝜓𝑐𝐴)
18173ad2ant3 1126 . . . . . . . . . . . . . . 15 ((𝜑𝑌 = 𝑍𝜓) → 𝑐𝐴)
191dalempea 35789 . . . . . . . . . . . . . . . 16 (𝜑𝑃𝐴)
20193ad2ant1 1124 . . . . . . . . . . . . . . 15 ((𝜑𝑌 = 𝑍𝜓) → 𝑃𝐴)
21 eqid 2778 . . . . . . . . . . . . . . . 16 (Base‘𝐾) = (Base‘𝐾)
2221, 3, 4hlatjcl 35530 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ 𝑐𝐴𝑃𝐴) → (𝑐 𝑃) ∈ (Base‘𝐾))
2316, 18, 20, 22syl3anc 1439 . . . . . . . . . . . . . 14 ((𝜑𝑌 = 𝑍𝜓) → (𝑐 𝑃) ∈ (Base‘𝐾))
247dalemddea 35847 . . . . . . . . . . . . . . . 16 (𝜓𝑑𝐴)
25243ad2ant3 1126 . . . . . . . . . . . . . . 15 ((𝜑𝑌 = 𝑍𝜓) → 𝑑𝐴)
261dalemsea 35792 . . . . . . . . . . . . . . . 16 (𝜑𝑆𝐴)
27263ad2ant1 1124 . . . . . . . . . . . . . . 15 ((𝜑𝑌 = 𝑍𝜓) → 𝑆𝐴)
2821, 3, 4hlatjcl 35530 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ 𝑑𝐴𝑆𝐴) → (𝑑 𝑆) ∈ (Base‘𝐾))
2916, 25, 27, 28syl3anc 1439 . . . . . . . . . . . . . 14 ((𝜑𝑌 = 𝑍𝜓) → (𝑑 𝑆) ∈ (Base‘𝐾))
30 dalem23.m . . . . . . . . . . . . . . 15 = (meet‘𝐾)
3121, 2, 30latmle2 17474 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ (𝑐 𝑃) ∈ (Base‘𝐾) ∧ (𝑑 𝑆) ∈ (Base‘𝐾)) → ((𝑐 𝑃) (𝑑 𝑆)) (𝑑 𝑆))
3214, 23, 29, 31syl3anc 1439 . . . . . . . . . . . . 13 ((𝜑𝑌 = 𝑍𝜓) → ((𝑐 𝑃) (𝑑 𝑆)) (𝑑 𝑆))
3312, 32syl5eqbr 4923 . . . . . . . . . . . 12 ((𝜑𝑌 = 𝑍𝜓) → 𝐺 (𝑑 𝑆))
343, 4hlatjcom 35531 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑑𝐴𝑆𝐴) → (𝑑 𝑆) = (𝑆 𝑑))
3516, 25, 27, 34syl3anc 1439 . . . . . . . . . . . 12 ((𝜑𝑌 = 𝑍𝜓) → (𝑑 𝑆) = (𝑆 𝑑))
3633, 35breqtrd 4914 . . . . . . . . . . 11 ((𝜑𝑌 = 𝑍𝜓) → 𝐺 (𝑆 𝑑))
3736adantr 474 . . . . . . . . . 10 (((𝜑𝑌 = 𝑍𝜓) ∧ 𝑐 = 𝐺) → 𝐺 (𝑆 𝑑))
3811, 37eqbrtrd 4910 . . . . . . . . 9 (((𝜑𝑌 = 𝑍𝜓) ∧ 𝑐 = 𝐺) → 𝑐 (𝑆 𝑑))
392, 3, 4hlatlej2 35539 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ 𝑆𝐴𝑑𝐴) → 𝑑 (𝑆 𝑑))
4016, 27, 25, 39syl3anc 1439 . . . . . . . . . 10 ((𝜑𝑌 = 𝑍𝜓) → 𝑑 (𝑆 𝑑))
4140adantr 474 . . . . . . . . 9 (((𝜑𝑌 = 𝑍𝜓) ∧ 𝑐 = 𝐺) → 𝑑 (𝑆 𝑑))
427, 4dalemcceb 35852 . . . . . . . . . . . 12 (𝜓𝑐 ∈ (Base‘𝐾))
43423ad2ant3 1126 . . . . . . . . . . 11 ((𝜑𝑌 = 𝑍𝜓) → 𝑐 ∈ (Base‘𝐾))
4421, 4atbase 35452 . . . . . . . . . . . . 13 (𝑑𝐴𝑑 ∈ (Base‘𝐾))
4524, 44syl 17 . . . . . . . . . . . 12 (𝜓𝑑 ∈ (Base‘𝐾))
46453ad2ant3 1126 . . . . . . . . . . 11 ((𝜑𝑌 = 𝑍𝜓) → 𝑑 ∈ (Base‘𝐾))
4721, 3, 4hlatjcl 35530 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑆𝐴𝑑𝐴) → (𝑆 𝑑) ∈ (Base‘𝐾))
4816, 27, 25, 47syl3anc 1439 . . . . . . . . . . 11 ((𝜑𝑌 = 𝑍𝜓) → (𝑆 𝑑) ∈ (Base‘𝐾))
4921, 2, 3latjle12 17459 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑐 ∈ (Base‘𝐾) ∧ 𝑑 ∈ (Base‘𝐾) ∧ (𝑆 𝑑) ∈ (Base‘𝐾))) → ((𝑐 (𝑆 𝑑) ∧ 𝑑 (𝑆 𝑑)) ↔ (𝑐 𝑑) (𝑆 𝑑)))
5014, 43, 46, 48, 49syl13anc 1440 . . . . . . . . . 10 ((𝜑𝑌 = 𝑍𝜓) → ((𝑐 (𝑆 𝑑) ∧ 𝑑 (𝑆 𝑑)) ↔ (𝑐 𝑑) (𝑆 𝑑)))
5150adantr 474 . . . . . . . . 9 (((𝜑𝑌 = 𝑍𝜓) ∧ 𝑐 = 𝐺) → ((𝑐 (𝑆 𝑑) ∧ 𝑑 (𝑆 𝑑)) ↔ (𝑐 𝑑) (𝑆 𝑑)))
5238, 41, 51mpbi2and 702 . . . . . . . 8 (((𝜑𝑌 = 𝑍𝜓) ∧ 𝑐 = 𝐺) → (𝑐 𝑑) (𝑆 𝑑))
531, 4dalemceb 35801 . . . . . . . . . . 11 (𝜑𝐶 ∈ (Base‘𝐾))
54533ad2ant1 1124 . . . . . . . . . 10 ((𝜑𝑌 = 𝑍𝜓) → 𝐶 ∈ (Base‘𝐾))
5521, 3, 4hlatjcl 35530 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ 𝑐𝐴𝑑𝐴) → (𝑐 𝑑) ∈ (Base‘𝐾))
5616, 18, 25, 55syl3anc 1439 . . . . . . . . . 10 ((𝜑𝑌 = 𝑍𝜓) → (𝑐 𝑑) ∈ (Base‘𝐾))
5721, 2lattr 17453 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝐶 ∈ (Base‘𝐾) ∧ (𝑐 𝑑) ∈ (Base‘𝐾) ∧ (𝑆 𝑑) ∈ (Base‘𝐾))) → ((𝐶 (𝑐 𝑑) ∧ (𝑐 𝑑) (𝑆 𝑑)) → 𝐶 (𝑆 𝑑)))
5814, 54, 56, 48, 57syl13anc 1440 . . . . . . . . 9 ((𝜑𝑌 = 𝑍𝜓) → ((𝐶 (𝑐 𝑑) ∧ (𝑐 𝑑) (𝑆 𝑑)) → 𝐶 (𝑆 𝑑)))
5958adantr 474 . . . . . . . 8 (((𝜑𝑌 = 𝑍𝜓) ∧ 𝑐 = 𝐺) → ((𝐶 (𝑐 𝑑) ∧ (𝑐 𝑑) (𝑆 𝑑)) → 𝐶 (𝑆 𝑑)))
6010, 52, 59mp2and 689 . . . . . . 7 (((𝜑𝑌 = 𝑍𝜓) ∧ 𝑐 = 𝐺) → 𝐶 (𝑆 𝑑))
61 dalem23.o . . . . . . . . . . 11 𝑂 = (LPlanes‘𝐾)
621, 61dalemyeb 35812 . . . . . . . . . 10 (𝜑𝑌 ∈ (Base‘𝐾))
63623ad2ant1 1124 . . . . . . . . 9 ((𝜑𝑌 = 𝑍𝜓) → 𝑌 ∈ (Base‘𝐾))
6421, 2, 30latmlem1 17478 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (𝐶 ∈ (Base‘𝐾) ∧ (𝑆 𝑑) ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾))) → (𝐶 (𝑆 𝑑) → (𝐶 𝑌) ((𝑆 𝑑) 𝑌)))
6514, 54, 48, 63, 64syl13anc 1440 . . . . . . . 8 ((𝜑𝑌 = 𝑍𝜓) → (𝐶 (𝑆 𝑑) → (𝐶 𝑌) ((𝑆 𝑑) 𝑌)))
6665adantr 474 . . . . . . 7 (((𝜑𝑌 = 𝑍𝜓) ∧ 𝑐 = 𝐺) → (𝐶 (𝑆 𝑑) → (𝐶 𝑌) ((𝑆 𝑑) 𝑌)))
6760, 66mpd 15 . . . . . 6 (((𝜑𝑌 = 𝑍𝜓) ∧ 𝑐 = 𝐺) → (𝐶 𝑌) ((𝑆 𝑑) 𝑌))
68 dalem23.y . . . . . . . . . 10 𝑌 = ((𝑃 𝑄) 𝑅)
69 dalem23.z . . . . . . . . . 10 𝑍 = ((𝑆 𝑇) 𝑈)
701, 2, 3, 4, 61, 68, 69dalem17 35843 . . . . . . . . 9 ((𝜑𝑌 = 𝑍) → 𝐶 𝑌)
71703adant3 1123 . . . . . . . 8 ((𝜑𝑌 = 𝑍𝜓) → 𝐶 𝑌)
7221, 2, 30latleeqm1 17476 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ 𝐶 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → (𝐶 𝑌 ↔ (𝐶 𝑌) = 𝐶))
7314, 54, 63, 72syl3anc 1439 . . . . . . . 8 ((𝜑𝑌 = 𝑍𝜓) → (𝐶 𝑌 ↔ (𝐶 𝑌) = 𝐶))
7471, 73mpbid 224 . . . . . . 7 ((𝜑𝑌 = 𝑍𝜓) → (𝐶 𝑌) = 𝐶)
7574adantr 474 . . . . . 6 (((𝜑𝑌 = 𝑍𝜓) ∧ 𝑐 = 𝐺) → (𝐶 𝑌) = 𝐶)
761, 2, 3, 4, 69dalemsly 35818 . . . . . . . . 9 ((𝜑𝑌 = 𝑍) → 𝑆 𝑌)
77763adant3 1123 . . . . . . . 8 ((𝜑𝑌 = 𝑍𝜓) → 𝑆 𝑌)
787dalem-ddly 35849 . . . . . . . . 9 (𝜓 → ¬ 𝑑 𝑌)
79783ad2ant3 1126 . . . . . . . 8 ((𝜑𝑌 = 𝑍𝜓) → ¬ 𝑑 𝑌)
8021, 2, 3, 30, 42atjm 35608 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑆𝐴𝑑𝐴𝑌 ∈ (Base‘𝐾)) ∧ (𝑆 𝑌 ∧ ¬ 𝑑 𝑌)) → ((𝑆 𝑑) 𝑌) = 𝑆)
8116, 27, 25, 63, 77, 79, 80syl132anc 1456 . . . . . . 7 ((𝜑𝑌 = 𝑍𝜓) → ((𝑆 𝑑) 𝑌) = 𝑆)
8281adantr 474 . . . . . 6 (((𝜑𝑌 = 𝑍𝜓) ∧ 𝑐 = 𝐺) → ((𝑆 𝑑) 𝑌) = 𝑆)
8367, 75, 823brtr3d 4919 . . . . 5 (((𝜑𝑌 = 𝑍𝜓) ∧ 𝑐 = 𝐺) → 𝐶 𝑆)
84 hlatl 35523 . . . . . . . . 9 (𝐾 ∈ HL → 𝐾 ∈ AtLat)
8515, 84syl 17 . . . . . . . 8 (𝜑𝐾 ∈ AtLat)
861, 2, 3, 4, 61, 68dalemcea 35823 . . . . . . . 8 (𝜑𝐶𝐴)
872, 4atcmp 35474 . . . . . . . 8 ((𝐾 ∈ AtLat ∧ 𝐶𝐴𝑆𝐴) → (𝐶 𝑆𝐶 = 𝑆))
8885, 86, 26, 87syl3anc 1439 . . . . . . 7 (𝜑 → (𝐶 𝑆𝐶 = 𝑆))
89883ad2ant1 1124 . . . . . 6 ((𝜑𝑌 = 𝑍𝜓) → (𝐶 𝑆𝐶 = 𝑆))
9089adantr 474 . . . . 5 (((𝜑𝑌 = 𝑍𝜓) ∧ 𝑐 = 𝐺) → (𝐶 𝑆𝐶 = 𝑆))
9183, 90mpbid 224 . . . 4 (((𝜑𝑌 = 𝑍𝜓) ∧ 𝑐 = 𝐺) → 𝐶 = 𝑆)
9291ex 403 . . 3 ((𝜑𝑌 = 𝑍𝜓) → (𝑐 = 𝐺𝐶 = 𝑆))
9392necon3d 2990 . 2 ((𝜑𝑌 = 𝑍𝜓) → (𝐶𝑆𝑐𝐺))
946, 93mpd 15 1 ((𝜑𝑌 = 𝑍𝜓) → 𝑐𝐺)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  w3a 1071   = wceq 1601  wcel 2107  wne 2969   class class class wbr 4888  cfv 6137  (class class class)co 6924  Basecbs 16266  lecple 16356  joincjn 17341  meetcmee 17342  Latclat 17442  Atomscatm 35426  AtLatcal 35427  HLchlt 35513  LPlanesclpl 35655
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5008  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-iun 4757  df-br 4889  df-opab 4951  df-mpt 4968  df-id 5263  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-riota 6885  df-ov 6927  df-oprab 6928  df-proset 17325  df-poset 17343  df-plt 17355  df-lub 17371  df-glb 17372  df-join 17373  df-meet 17374  df-p0 17436  df-lat 17443  df-clat 17505  df-oposet 35339  df-ol 35341  df-oml 35342  df-covers 35429  df-ats 35430  df-atl 35461  df-cvlat 35485  df-hlat 35514  df-llines 35661  df-lplanes 35662
This theorem is referenced by:  dalem28  35863  dalem31N  35866
  Copyright terms: Public domain W3C validator