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

Theorem cdlemeg47rv2 35278
 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 35277 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → (𝐺𝑅) = 𝑅 / 𝑢𝑆 / 𝑣𝑂)
12 simp22l 1178 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑅𝐴)
13 nfcvd 2762 . . . . 5 (𝑅𝐴𝑢((𝑄 𝑃) (𝑆 / 𝑣𝑁 ((𝑅 𝑆) 𝑊))))
14 oveq1 6611 . . . . . . . 8 (𝑢 = 𝑅 → (𝑢 𝑆) = (𝑅 𝑆))
1514oveq1d 6619 . . . . . . 7 (𝑢 = 𝑅 → ((𝑢 𝑆) 𝑊) = ((𝑅 𝑆) 𝑊))
1615oveq2d 6620 . . . . . 6 (𝑢 = 𝑅 → (𝑆 / 𝑣𝑁 ((𝑢 𝑆) 𝑊)) = (𝑆 / 𝑣𝑁 ((𝑅 𝑆) 𝑊)))
1716oveq2d 6620 . . . . 5 (𝑢 = 𝑅 → ((𝑄 𝑃) (𝑆 / 𝑣𝑁 ((𝑢 𝑆) 𝑊))) = ((𝑄 𝑃) (𝑆 / 𝑣𝑁 ((𝑅 𝑆) 𝑊))))
1813, 17csbiegf 3538 . . . 4 (𝑅𝐴𝑅 / 𝑢((𝑄 𝑃) (𝑆 / 𝑣𝑁 ((𝑢 𝑆) 𝑊))) = ((𝑄 𝑃) (𝑆 / 𝑣𝑁 ((𝑅 𝑆) 𝑊))))
1912, 18syl 17 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑅 / 𝑢((𝑄 𝑃) (𝑆 / 𝑣𝑁 ((𝑢 𝑆) 𝑊))) = ((𝑄 𝑃) (𝑆 / 𝑣𝑁 ((𝑅 𝑆) 𝑊))))
20 simp23l 1180 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑆𝐴)
21 eqid 2621 . . . . . 6 ((𝑄 𝑃) (𝑆 / 𝑣𝑁 ((𝑢 𝑆) 𝑊))) = ((𝑄 𝑃) (𝑆 / 𝑣𝑁 ((𝑢 𝑆) 𝑊)))
229, 21cdleme31se2 35151 . . . . 5 (𝑆𝐴𝑆 / 𝑣𝑂 = ((𝑄 𝑃) (𝑆 / 𝑣𝑁 ((𝑢 𝑆) 𝑊))))
2320, 22syl 17 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑆 / 𝑣𝑂 = ((𝑄 𝑃) (𝑆 / 𝑣𝑁 ((𝑢 𝑆) 𝑊))))
2423csbeq2dv 3964 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑅 / 𝑢𝑆 / 𝑣𝑂 = 𝑅 / 𝑢((𝑄 𝑃) (𝑆 / 𝑣𝑁 ((𝑢 𝑆) 𝑊))))
25 simp1 1059 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → ((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)))
26 simp21 1092 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑃𝑄)
27 simp23 1094 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → (𝑆𝐴 ∧ ¬ 𝑆 𝑊))
28 simp3r 1088 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → ¬ 𝑆 (𝑃 𝑄))
291, 2, 3, 4, 5, 6, 7, 8, 9, 10cdlemeg47b 35276 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ ¬ 𝑆 (𝑃 𝑄)) → (𝐺𝑆) = 𝑆 / 𝑣𝑁)
3025, 26, 27, 28, 29syl121anc 1328 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → (𝐺𝑆) = 𝑆 / 𝑣𝑁)
3130oveq1d 6619 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → ((𝐺𝑆) ((𝑅 𝑆) 𝑊)) = (𝑆 / 𝑣𝑁 ((𝑅 𝑆) 𝑊)))
3231oveq2d 6620 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → ((𝑄 𝑃) ((𝐺𝑆) ((𝑅 𝑆) 𝑊))) = ((𝑄 𝑃) (𝑆 / 𝑣𝑁 ((𝑅 𝑆) 𝑊))))
3319, 24, 323eqtr4d 2665 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑅 / 𝑢𝑆 / 𝑣𝑂 = ((𝑄 𝑃) ((𝐺𝑆) ((𝑅 𝑆) 𝑊))))
3411, 33eqtrd 2655 1 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → (𝐺𝑅) = ((𝑄 𝑃) ((𝐺𝑆) ((𝑅 𝑆) 𝑊))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 384   ∧ w3a 1036   = wceq 1480   ∈ wcel 1987   ≠ wne 2790  ∀wral 2907  ⦋csb 3514  ifcif 4058   class class class wbr 4613   ↦ cmpt 4673  ‘cfv 5847  ℩crio 6564  (class class class)co 6604  Basecbs 15781  lecple 15869  joincjn 16865  meetcmee 16866  Atomscatm 34030  HLchlt 34117  LHypclh 34750 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-riotaBAD 33719 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-iun 4487  df-iin 4488  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-1st 7113  df-2nd 7114  df-undef 7344  df-preset 16849  df-poset 16867  df-plt 16879  df-lub 16895  df-glb 16896  df-join 16897  df-meet 16898  df-p0 16960  df-p1 16961  df-lat 16967  df-clat 17029  df-oposet 33943  df-ol 33945  df-oml 33946  df-covers 34033  df-ats 34034  df-atl 34065  df-cvlat 34089  df-hlat 34118  df-llines 34264  df-lplanes 34265  df-lvols 34266  df-lines 34267  df-psubsp 34269  df-pmap 34270  df-padd 34562  df-lhyp 34754 This theorem is referenced by:  cdlemeg46rv2OLDN  35283  cdlemeg46gfv  35298
 Copyright terms: Public domain W3C validator