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

Theorem cdleme40v 36545
Description: Part of proof of Lemma E in [Crawley] p. 113. Change bound variables in 𝑆 / 𝑢𝑉 (but we use 𝑅 / 𝑢𝑉 for convenience since we have its hypotheses available). (Contributed by NM, 18-Mar-2013.)
Hypotheses
Ref Expression
cdleme40.b 𝐵 = (Base‘𝐾)
cdleme40.l = (le‘𝐾)
cdleme40.j = (join‘𝐾)
cdleme40.m = (meet‘𝐾)
cdleme40.a 𝐴 = (Atoms‘𝐾)
cdleme40.h 𝐻 = (LHyp‘𝐾)
cdleme40.u 𝑈 = ((𝑃 𝑄) 𝑊)
cdleme40.e 𝐸 = ((𝑡 𝑈) (𝑄 ((𝑃 𝑡) 𝑊)))
cdleme40.g 𝐺 = ((𝑃 𝑄) (𝐸 ((𝑠 𝑡) 𝑊)))
cdleme40.i 𝐼 = (𝑦𝐵𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = 𝐺))
cdleme40.n 𝑁 = if(𝑠 (𝑃 𝑄), 𝐼, 𝐷)
cdleme40.d 𝐷 = ((𝑠 𝑈) (𝑄 ((𝑃 𝑠) 𝑊)))
cdleme40r.y 𝑌 = ((𝑢 𝑈) (𝑄 ((𝑃 𝑢) 𝑊)))
cdleme40r.t 𝑇 = ((𝑣 𝑈) (𝑄 ((𝑃 𝑣) 𝑊)))
cdleme40r.x 𝑋 = ((𝑃 𝑄) (𝑇 ((𝑢 𝑣) 𝑊)))
cdleme40r.o 𝑂 = (𝑧𝐵𝑣𝐴 ((¬ 𝑣 𝑊 ∧ ¬ 𝑣 (𝑃 𝑄)) → 𝑧 = 𝑋))
cdleme40r.v 𝑉 = if(𝑢 (𝑃 𝑄), 𝑂, 𝑌)
Assertion
Ref Expression
cdleme40v (𝑅𝐴𝑅 / 𝑠𝑁 = 𝑅 / 𝑢𝑉)
Distinct variable groups:   𝑣,𝑢,𝑧,𝐴   𝑢,𝐵,𝑣,𝑧   𝑣,𝐻,𝑧   𝑢, ,𝑣,𝑧   𝑣,𝐾,𝑧   𝑢, ,𝑣,𝑧   𝑢, ,𝑣,𝑧   𝑢,𝑃,𝑣,𝑧   𝑢,𝑄,𝑣,𝑧   𝑣,𝑅,𝑧   𝑢,𝑇   𝑣,𝑈,𝑧   𝑢,𝑊,𝑣,𝑧,𝑠,𝑡,𝑦   𝐴,𝑠   𝑦,𝑡,𝐴   𝐵,𝑠,𝑡,𝑦   𝐸,𝑠   𝑡,𝐻,𝑦   ,𝑠,𝑡,𝑦   𝑡,𝐾,𝑦   ,𝑠,𝑡,𝑦   ,𝑠,𝑡,𝑦   𝑃,𝑠,𝑡,𝑦   𝑄,𝑠,𝑡,𝑦   𝑅,𝑠,𝑡,𝑦   𝑡,𝑈,𝑦   𝑊,𝑠,𝑡,𝑦   𝑦,𝑌   𝑣,𝑡,𝑦   𝑇,𝑠,𝑡,𝑦   𝑣,𝐸,𝑧   𝑢,𝑁,𝑣   𝑢,𝑅   𝑉,𝑠   𝑡,𝑋,𝑦   𝑢,𝑠,𝑧,𝑡,𝑦
Allowed substitution hints:   𝐷(𝑦,𝑧,𝑣,𝑢,𝑡,𝑠)   𝑇(𝑧,𝑣)   𝑈(𝑢,𝑠)   𝐸(𝑦,𝑢,𝑡)   𝐺(𝑦,𝑧,𝑣,𝑢,𝑡,𝑠)   𝐻(𝑢,𝑠)   𝐼(𝑦,𝑧,𝑣,𝑢,𝑡,𝑠)   𝐾(𝑢,𝑠)   𝑁(𝑦,𝑧,𝑡,𝑠)   𝑂(𝑦,𝑧,𝑣,𝑢,𝑡,𝑠)   𝑉(𝑦,𝑧,𝑣,𝑢,𝑡)   𝑋(𝑧,𝑣,𝑢,𝑠)   𝑌(𝑧,𝑣,𝑢,𝑡,𝑠)

Proof of Theorem cdleme40v
StepHypRef Expression
1 breq1 4877 . . . . 5 (𝑠 = 𝑢 → (𝑠 (𝑃 𝑄) ↔ 𝑢 (𝑃 𝑄)))
2 cdleme40.g . . . . . . . . . . . 12 𝐺 = ((𝑃 𝑄) (𝐸 ((𝑠 𝑡) 𝑊)))
3 oveq1 6913 . . . . . . . . . . . . . . 15 (𝑠 = 𝑢 → (𝑠 𝑡) = (𝑢 𝑡))
43oveq1d 6921 . . . . . . . . . . . . . 14 (𝑠 = 𝑢 → ((𝑠 𝑡) 𝑊) = ((𝑢 𝑡) 𝑊))
54oveq2d 6922 . . . . . . . . . . . . 13 (𝑠 = 𝑢 → (𝐸 ((𝑠 𝑡) 𝑊)) = (𝐸 ((𝑢 𝑡) 𝑊)))
65oveq2d 6922 . . . . . . . . . . . 12 (𝑠 = 𝑢 → ((𝑃 𝑄) (𝐸 ((𝑠 𝑡) 𝑊))) = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))))
72, 6syl5eq 2874 . . . . . . . . . . 11 (𝑠 = 𝑢𝐺 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))))
87eqeq2d 2836 . . . . . . . . . 10 (𝑠 = 𝑢 → (𝑦 = 𝐺𝑦 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊)))))
98imbi2d 332 . . . . . . . . 9 (𝑠 = 𝑢 → (((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = 𝐺) ↔ ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))))))
109ralbidv 3196 . . . . . . . 8 (𝑠 = 𝑢 → (∀𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = 𝐺) ↔ ∀𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))))))
1110riotabidv 6869 . . . . . . 7 (𝑠 = 𝑢 → (𝑦𝐵𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = 𝐺)) = (𝑦𝐵𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))))))
12 eqeq1 2830 . . . . . . . . . . 11 (𝑦 = 𝑧 → (𝑦 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))) ↔ 𝑧 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊)))))
1312imbi2d 332 . . . . . . . . . 10 (𝑦 = 𝑧 → (((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊)))) ↔ ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑧 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))))))
1413ralbidv 3196 . . . . . . . . 9 (𝑦 = 𝑧 → (∀𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊)))) ↔ ∀𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑧 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))))))
15 breq1 4877 . . . . . . . . . . . . 13 (𝑡 = 𝑣 → (𝑡 𝑊𝑣 𝑊))
1615notbid 310 . . . . . . . . . . . 12 (𝑡 = 𝑣 → (¬ 𝑡 𝑊 ↔ ¬ 𝑣 𝑊))
17 breq1 4877 . . . . . . . . . . . . 13 (𝑡 = 𝑣 → (𝑡 (𝑃 𝑄) ↔ 𝑣 (𝑃 𝑄)))
1817notbid 310 . . . . . . . . . . . 12 (𝑡 = 𝑣 → (¬ 𝑡 (𝑃 𝑄) ↔ ¬ 𝑣 (𝑃 𝑄)))
1916, 18anbi12d 626 . . . . . . . . . . 11 (𝑡 = 𝑣 → ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) ↔ (¬ 𝑣 𝑊 ∧ ¬ 𝑣 (𝑃 𝑄))))
20 oveq1 6913 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑣 → (𝑡 𝑈) = (𝑣 𝑈))
21 oveq2 6914 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑣 → (𝑃 𝑡) = (𝑃 𝑣))
2221oveq1d 6921 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑣 → ((𝑃 𝑡) 𝑊) = ((𝑃 𝑣) 𝑊))
2322oveq2d 6922 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑣 → (𝑄 ((𝑃 𝑡) 𝑊)) = (𝑄 ((𝑃 𝑣) 𝑊)))
2420, 23oveq12d 6924 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑣 → ((𝑡 𝑈) (𝑄 ((𝑃 𝑡) 𝑊))) = ((𝑣 𝑈) (𝑄 ((𝑃 𝑣) 𝑊))))
25 cdleme40.e . . . . . . . . . . . . . . . 16 𝐸 = ((𝑡 𝑈) (𝑄 ((𝑃 𝑡) 𝑊)))
26 cdleme40r.t . . . . . . . . . . . . . . . 16 𝑇 = ((𝑣 𝑈) (𝑄 ((𝑃 𝑣) 𝑊)))
2724, 25, 263eqtr4g 2887 . . . . . . . . . . . . . . 15 (𝑡 = 𝑣𝐸 = 𝑇)
28 oveq2 6914 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑣 → (𝑢 𝑡) = (𝑢 𝑣))
2928oveq1d 6921 . . . . . . . . . . . . . . 15 (𝑡 = 𝑣 → ((𝑢 𝑡) 𝑊) = ((𝑢 𝑣) 𝑊))
3027, 29oveq12d 6924 . . . . . . . . . . . . . 14 (𝑡 = 𝑣 → (𝐸 ((𝑢 𝑡) 𝑊)) = (𝑇 ((𝑢 𝑣) 𝑊)))
3130oveq2d 6922 . . . . . . . . . . . . 13 (𝑡 = 𝑣 → ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))) = ((𝑃 𝑄) (𝑇 ((𝑢 𝑣) 𝑊))))
32 cdleme40r.x . . . . . . . . . . . . 13 𝑋 = ((𝑃 𝑄) (𝑇 ((𝑢 𝑣) 𝑊)))
3331, 32syl6eqr 2880 . . . . . . . . . . . 12 (𝑡 = 𝑣 → ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))) = 𝑋)
3433eqeq2d 2836 . . . . . . . . . . 11 (𝑡 = 𝑣 → (𝑧 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))) ↔ 𝑧 = 𝑋))
3519, 34imbi12d 336 . . . . . . . . . 10 (𝑡 = 𝑣 → (((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑧 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊)))) ↔ ((¬ 𝑣 𝑊 ∧ ¬ 𝑣 (𝑃 𝑄)) → 𝑧 = 𝑋)))
3635cbvralv 3384 . . . . . . . . 9 (∀𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑧 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊)))) ↔ ∀𝑣𝐴 ((¬ 𝑣 𝑊 ∧ ¬ 𝑣 (𝑃 𝑄)) → 𝑧 = 𝑋))
3714, 36syl6bb 279 . . . . . . . 8 (𝑦 = 𝑧 → (∀𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊)))) ↔ ∀𝑣𝐴 ((¬ 𝑣 𝑊 ∧ ¬ 𝑣 (𝑃 𝑄)) → 𝑧 = 𝑋)))
3837cbvriotav 6878 . . . . . . 7 (𝑦𝐵𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))))) = (𝑧𝐵𝑣𝐴 ((¬ 𝑣 𝑊 ∧ ¬ 𝑣 (𝑃 𝑄)) → 𝑧 = 𝑋))
3911, 38syl6eq 2878 . . . . . 6 (𝑠 = 𝑢 → (𝑦𝐵𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = 𝐺)) = (𝑧𝐵𝑣𝐴 ((¬ 𝑣 𝑊 ∧ ¬ 𝑣 (𝑃 𝑄)) → 𝑧 = 𝑋)))
40 cdleme40.i . . . . . 6 𝐼 = (𝑦𝐵𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = 𝐺))
41 cdleme40r.o . . . . . 6 𝑂 = (𝑧𝐵𝑣𝐴 ((¬ 𝑣 𝑊 ∧ ¬ 𝑣 (𝑃 𝑄)) → 𝑧 = 𝑋))
4239, 40, 413eqtr4g 2887 . . . . 5 (𝑠 = 𝑢𝐼 = 𝑂)
43 oveq1 6913 . . . . . . 7 (𝑠 = 𝑢 → (𝑠 𝑈) = (𝑢 𝑈))
44 oveq2 6914 . . . . . . . . 9 (𝑠 = 𝑢 → (𝑃 𝑠) = (𝑃 𝑢))
4544oveq1d 6921 . . . . . . . 8 (𝑠 = 𝑢 → ((𝑃 𝑠) 𝑊) = ((𝑃 𝑢) 𝑊))
4645oveq2d 6922 . . . . . . 7 (𝑠 = 𝑢 → (𝑄 ((𝑃 𝑠) 𝑊)) = (𝑄 ((𝑃 𝑢) 𝑊)))
4743, 46oveq12d 6924 . . . . . 6 (𝑠 = 𝑢 → ((𝑠 𝑈) (𝑄 ((𝑃 𝑠) 𝑊))) = ((𝑢 𝑈) (𝑄 ((𝑃 𝑢) 𝑊))))
48 cdleme40.d . . . . . 6 𝐷 = ((𝑠 𝑈) (𝑄 ((𝑃 𝑠) 𝑊)))
49 cdleme40r.y . . . . . 6 𝑌 = ((𝑢 𝑈) (𝑄 ((𝑃 𝑢) 𝑊)))
5047, 48, 493eqtr4g 2887 . . . . 5 (𝑠 = 𝑢𝐷 = 𝑌)
511, 42, 50ifbieq12d 4334 . . . 4 (𝑠 = 𝑢 → if(𝑠 (𝑃 𝑄), 𝐼, 𝐷) = if(𝑢 (𝑃 𝑄), 𝑂, 𝑌))
52 cdleme40.n . . . 4 𝑁 = if(𝑠 (𝑃 𝑄), 𝐼, 𝐷)
53 cdleme40r.v . . . 4 𝑉 = if(𝑢 (𝑃 𝑄), 𝑂, 𝑌)
5451, 52, 533eqtr4g 2887 . . 3 (𝑠 = 𝑢𝑁 = 𝑉)
5554cbvcsbv 3764 . 2 𝑅 / 𝑠𝑁 = 𝑅 / 𝑢𝑉
5655a1i 11 1 (𝑅𝐴𝑅 / 𝑠𝑁 = 𝑅 / 𝑢𝑉)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 386   = wceq 1658  wcel 2166  wral 3118  csb 3758  ifcif 4307   class class class wbr 4874  cfv 6124  crio 6866  (class class class)co 6906  Basecbs 16223  lecple 16313  joincjn 17298  meetcmee 17299  Atomscatm 35339  LHypclh 36060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ral 3123  df-rex 3124  df-rab 3127  df-v 3417  df-sbc 3664  df-csb 3759  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-nul 4146  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4660  df-br 4875  df-iota 6087  df-fv 6132  df-riota 6867  df-ov 6909
This theorem is referenced by:  cdleme40w  36546
  Copyright terms: Public domain W3C validator