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

Theorem cdlemeg47rv2 40490
Description: Value of gs(r) when r is an atom under pq and s is any atom not under pq, using very compact hypotheses. TODO: FIX COMMENT. (Contributed by NM, 1-Apr-2013.)
Hypotheses
Ref Expression
cdlemef47.b 𝐵 = (Base‘𝐾)
cdlemef47.l = (le‘𝐾)
cdlemef47.j = (join‘𝐾)
cdlemef47.m = (meet‘𝐾)
cdlemef47.a 𝐴 = (Atoms‘𝐾)
cdlemef47.h 𝐻 = (LHyp‘𝐾)
cdlemef47.v 𝑉 = ((𝑄 𝑃) 𝑊)
cdlemef47.n 𝑁 = ((𝑣 𝑉) (𝑃 ((𝑄 𝑣) 𝑊)))
cdlemefs47.o 𝑂 = ((𝑄 𝑃) (𝑁 ((𝑢 𝑣) 𝑊)))
cdlemef47.g 𝐺 = (𝑎𝐵 ↦ if((𝑄𝑃 ∧ ¬ 𝑎 𝑊), (𝑐𝐵𝑢𝐴 ((¬ 𝑢 𝑊 ∧ (𝑢 (𝑎 𝑊)) = 𝑎) → 𝑐 = (if(𝑢 (𝑄 𝑃), (𝑏𝐵𝑣𝐴 ((¬ 𝑣 𝑊 ∧ ¬ 𝑣 (𝑄 𝑃)) → 𝑏 = 𝑂)), 𝑢 / 𝑣𝑁) (𝑎 𝑊)))), 𝑎))
Assertion
Ref Expression
cdlemeg47rv2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → (𝐺𝑅) = ((𝑄 𝑃) ((𝐺𝑆) ((𝑅 𝑆) 𝑊))))
Distinct variable groups:   𝑎,𝑏,𝑐,𝑢,𝑣,𝐴   𝐵,𝑎,𝑏,𝑐,𝑢,𝑣   𝐻,𝑎,𝑏,𝑐,𝑢,𝑣   ,𝑎,𝑏,𝑐,𝑢,𝑣   𝐾,𝑎,𝑏,𝑐,𝑢,𝑣   ,𝑎,𝑏,𝑐,𝑢,𝑣   ,𝑎,𝑏,𝑐,𝑢,𝑣   𝑁,𝑎,𝑏,𝑐,𝑢   𝑂,𝑎,𝑏,𝑐   𝑃,𝑎,𝑏,𝑐,𝑢,𝑣   𝑄,𝑎,𝑏,𝑐,𝑢,𝑣   𝑅,𝑎,𝑏,𝑐,𝑢,𝑣   𝑆,𝑎,𝑏,𝑐,𝑢,𝑣   𝑉,𝑎,𝑏,𝑐,𝑢,𝑣   𝑊,𝑎,𝑏,𝑐,𝑢,𝑣
Allowed substitution hints:   𝐺(𝑣,𝑢,𝑎,𝑏,𝑐)   𝑁(𝑣)   𝑂(𝑣,𝑢)

Proof of Theorem cdlemeg47rv2
StepHypRef Expression
1 cdlemef47.b . . 3 𝐵 = (Base‘𝐾)
2 cdlemef47.l . . 3 = (le‘𝐾)
3 cdlemef47.j . . 3 = (join‘𝐾)
4 cdlemef47.m . . 3 = (meet‘𝐾)
5 cdlemef47.a . . 3 𝐴 = (Atoms‘𝐾)
6 cdlemef47.h . . 3 𝐻 = (LHyp‘𝐾)
7 cdlemef47.v . . 3 𝑉 = ((𝑄 𝑃) 𝑊)
8 cdlemef47.n . . 3 𝑁 = ((𝑣 𝑉) (𝑃 ((𝑄 𝑣) 𝑊)))
9 cdlemefs47.o . . 3 𝑂 = ((𝑄 𝑃) (𝑁 ((𝑢 𝑣) 𝑊)))
10 cdlemef47.g . . 3 𝐺 = (𝑎𝐵 ↦ if((𝑄𝑃 ∧ ¬ 𝑎 𝑊), (𝑐𝐵𝑢𝐴 ((¬ 𝑢 𝑊 ∧ (𝑢 (𝑎 𝑊)) = 𝑎) → 𝑐 = (if(𝑢 (𝑄 𝑃), (𝑏𝐵𝑣𝐴 ((¬ 𝑣 𝑊 ∧ ¬ 𝑣 (𝑄 𝑃)) → 𝑏 = 𝑂)), 𝑢 / 𝑣𝑁) (𝑎 𝑊)))), 𝑎))
111, 2, 3, 4, 5, 6, 7, 8, 9, 10cdlemeg47rv 40489 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → (𝐺𝑅) = 𝑅 / 𝑢𝑆 / 𝑣𝑂)
12 simp22l 1293 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑅𝐴)
13 nfcvd 2905 . . . . 5 (𝑅𝐴𝑢((𝑄 𝑃) (𝑆 / 𝑣𝑁 ((𝑅 𝑆) 𝑊))))
14 oveq1 7436 . . . . . . . 8 (𝑢 = 𝑅 → (𝑢 𝑆) = (𝑅 𝑆))
1514oveq1d 7444 . . . . . . 7 (𝑢 = 𝑅 → ((𝑢 𝑆) 𝑊) = ((𝑅 𝑆) 𝑊))
1615oveq2d 7445 . . . . . 6 (𝑢 = 𝑅 → (𝑆 / 𝑣𝑁 ((𝑢 𝑆) 𝑊)) = (𝑆 / 𝑣𝑁 ((𝑅 𝑆) 𝑊)))
1716oveq2d 7445 . . . . 5 (𝑢 = 𝑅 → ((𝑄 𝑃) (𝑆 / 𝑣𝑁 ((𝑢 𝑆) 𝑊))) = ((𝑄 𝑃) (𝑆 / 𝑣𝑁 ((𝑅 𝑆) 𝑊))))
1813, 17csbiegf 3931 . . . 4 (𝑅𝐴𝑅 / 𝑢((𝑄 𝑃) (𝑆 / 𝑣𝑁 ((𝑢 𝑆) 𝑊))) = ((𝑄 𝑃) (𝑆 / 𝑣𝑁 ((𝑅 𝑆) 𝑊))))
1912, 18syl 17 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑅 / 𝑢((𝑄 𝑃) (𝑆 / 𝑣𝑁 ((𝑢 𝑆) 𝑊))) = ((𝑄 𝑃) (𝑆 / 𝑣𝑁 ((𝑅 𝑆) 𝑊))))
20 simp23l 1295 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑆𝐴)
21 eqid 2736 . . . . . 6 ((𝑄 𝑃) (𝑆 / 𝑣𝑁 ((𝑢 𝑆) 𝑊))) = ((𝑄 𝑃) (𝑆 / 𝑣𝑁 ((𝑢 𝑆) 𝑊)))
229, 21cdleme31se2 40363 . . . . 5 (𝑆𝐴𝑆 / 𝑣𝑂 = ((𝑄 𝑃) (𝑆 / 𝑣𝑁 ((𝑢 𝑆) 𝑊))))
2320, 22syl 17 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑆 / 𝑣𝑂 = ((𝑄 𝑃) (𝑆 / 𝑣𝑁 ((𝑢 𝑆) 𝑊))))
2423csbeq2dv 3905 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑅 / 𝑢𝑆 / 𝑣𝑂 = 𝑅 / 𝑢((𝑄 𝑃) (𝑆 / 𝑣𝑁 ((𝑢 𝑆) 𝑊))))
25 simp1 1137 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → ((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)))
26 simp21 1207 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑃𝑄)
27 simp23 1209 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → (𝑆𝐴 ∧ ¬ 𝑆 𝑊))
28 simp3r 1203 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → ¬ 𝑆 (𝑃 𝑄))
291, 2, 3, 4, 5, 6, 7, 8, 9, 10cdlemeg47b 40488 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ ¬ 𝑆 (𝑃 𝑄)) → (𝐺𝑆) = 𝑆 / 𝑣𝑁)
3025, 26, 27, 28, 29syl121anc 1377 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → (𝐺𝑆) = 𝑆 / 𝑣𝑁)
3130oveq1d 7444 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → ((𝐺𝑆) ((𝑅 𝑆) 𝑊)) = (𝑆 / 𝑣𝑁 ((𝑅 𝑆) 𝑊)))
3231oveq2d 7445 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → ((𝑄 𝑃) ((𝐺𝑆) ((𝑅 𝑆) 𝑊))) = ((𝑄 𝑃) (𝑆 / 𝑣𝑁 ((𝑅 𝑆) 𝑊))))
3319, 24, 323eqtr4d 2786 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑅 / 𝑢𝑆 / 𝑣𝑂 = ((𝑄 𝑃) ((𝐺𝑆) ((𝑅 𝑆) 𝑊))))
3411, 33eqtrd 2776 1 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → (𝐺𝑅) = ((𝑄 𝑃) ((𝐺𝑆) ((𝑅 𝑆) 𝑊))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  w3a 1087   = wceq 1540  wcel 2108  wne 2939  wral 3060  csb 3898  ifcif 4524   class class class wbr 5141  cmpt 5223  cfv 6559  crio 7385  (class class class)co 7429  Basecbs 17243  lecple 17300  joincjn 18353  meetcmee 18354  Atomscatm 39242  HLchlt 39329  LHypclh 39964
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5277  ax-sep 5294  ax-nul 5304  ax-pow 5363  ax-pr 5430  ax-un 7751  ax-riotaBAD 38932
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4906  df-iun 4991  df-iin 4992  df-br 5142  df-opab 5204  df-mpt 5224  df-id 5576  df-xp 5689  df-rel 5690  df-cnv 5691  df-co 5692  df-dm 5693  df-rn 5694  df-res 5695  df-ima 5696  df-iota 6512  df-fun 6561  df-fn 6562  df-f 6563  df-f1 6564  df-fo 6565  df-f1o 6566  df-fv 6567  df-riota 7386  df-ov 7432  df-oprab 7433  df-mpo 7434  df-1st 8010  df-2nd 8011  df-undef 8294  df-proset 18336  df-poset 18355  df-plt 18371  df-lub 18387  df-glb 18388  df-join 18389  df-meet 18390  df-p0 18466  df-p1 18467  df-lat 18473  df-clat 18540  df-oposet 39155  df-ol 39157  df-oml 39158  df-covers 39245  df-ats 39246  df-atl 39277  df-cvlat 39301  df-hlat 39330  df-llines 39478  df-lplanes 39479  df-lvols 39480  df-lines 39481  df-psubsp 39483  df-pmap 39484  df-padd 39776  df-lhyp 39968
This theorem is referenced by:  cdlemeg46rv2OLDN  40495  cdlemeg46gfv  40510
  Copyright terms: Public domain W3C validator