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 37647
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 5042 . . . . 5 (𝑠 = 𝑢 → (𝑠 (𝑃 𝑄) ↔ 𝑢 (𝑃 𝑄)))
2 cdleme40.g . . . . . . . . . . . 12 𝐺 = ((𝑃 𝑄) (𝐸 ((𝑠 𝑡) 𝑊)))
3 oveq1 7137 . . . . . . . . . . . . . . 15 (𝑠 = 𝑢 → (𝑠 𝑡) = (𝑢 𝑡))
43oveq1d 7145 . . . . . . . . . . . . . 14 (𝑠 = 𝑢 → ((𝑠 𝑡) 𝑊) = ((𝑢 𝑡) 𝑊))
54oveq2d 7146 . . . . . . . . . . . . 13 (𝑠 = 𝑢 → (𝐸 ((𝑠 𝑡) 𝑊)) = (𝐸 ((𝑢 𝑡) 𝑊)))
65oveq2d 7146 . . . . . . . . . . . 12 (𝑠 = 𝑢 → ((𝑃 𝑄) (𝐸 ((𝑠 𝑡) 𝑊))) = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))))
72, 6syl5eq 2868 . . . . . . . . . . 11 (𝑠 = 𝑢𝐺 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))))
87eqeq2d 2832 . . . . . . . . . 10 (𝑠 = 𝑢 → (𝑦 = 𝐺𝑦 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊)))))
98imbi2d 344 . . . . . . . . 9 (𝑠 = 𝑢 → (((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = 𝐺) ↔ ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))))))
109ralbidv 3185 . . . . . . . 8 (𝑠 = 𝑢 → (∀𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = 𝐺) ↔ ∀𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))))))
1110riotabidv 7090 . . . . . . 7 (𝑠 = 𝑢 → (𝑦𝐵𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = 𝐺)) = (𝑦𝐵𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))))))
12 eqeq1 2825 . . . . . . . . . . 11 (𝑦 = 𝑧 → (𝑦 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))) ↔ 𝑧 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊)))))
1312imbi2d 344 . . . . . . . . . 10 (𝑦 = 𝑧 → (((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊)))) ↔ ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑧 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))))))
1413ralbidv 3185 . . . . . . . . 9 (𝑦 = 𝑧 → (∀𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊)))) ↔ ∀𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑧 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))))))
15 breq1 5042 . . . . . . . . . . . . 13 (𝑡 = 𝑣 → (𝑡 𝑊𝑣 𝑊))
1615notbid 321 . . . . . . . . . . . 12 (𝑡 = 𝑣 → (¬ 𝑡 𝑊 ↔ ¬ 𝑣 𝑊))
17 breq1 5042 . . . . . . . . . . . . 13 (𝑡 = 𝑣 → (𝑡 (𝑃 𝑄) ↔ 𝑣 (𝑃 𝑄)))
1817notbid 321 . . . . . . . . . . . 12 (𝑡 = 𝑣 → (¬ 𝑡 (𝑃 𝑄) ↔ ¬ 𝑣 (𝑃 𝑄)))
1916, 18anbi12d 633 . . . . . . . . . . 11 (𝑡 = 𝑣 → ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) ↔ (¬ 𝑣 𝑊 ∧ ¬ 𝑣 (𝑃 𝑄))))
20 oveq1 7137 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑣 → (𝑡 𝑈) = (𝑣 𝑈))
21 oveq2 7138 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑣 → (𝑃 𝑡) = (𝑃 𝑣))
2221oveq1d 7145 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑣 → ((𝑃 𝑡) 𝑊) = ((𝑃 𝑣) 𝑊))
2322oveq2d 7146 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑣 → (𝑄 ((𝑃 𝑡) 𝑊)) = (𝑄 ((𝑃 𝑣) 𝑊)))
2420, 23oveq12d 7148 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑣 → ((𝑡 𝑈) (𝑄 ((𝑃 𝑡) 𝑊))) = ((𝑣 𝑈) (𝑄 ((𝑃 𝑣) 𝑊))))
25 cdleme40.e . . . . . . . . . . . . . . . 16 𝐸 = ((𝑡 𝑈) (𝑄 ((𝑃 𝑡) 𝑊)))
26 cdleme40r.t . . . . . . . . . . . . . . . 16 𝑇 = ((𝑣 𝑈) (𝑄 ((𝑃 𝑣) 𝑊)))
2724, 25, 263eqtr4g 2881 . . . . . . . . . . . . . . 15 (𝑡 = 𝑣𝐸 = 𝑇)
28 oveq2 7138 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑣 → (𝑢 𝑡) = (𝑢 𝑣))
2928oveq1d 7145 . . . . . . . . . . . . . . 15 (𝑡 = 𝑣 → ((𝑢 𝑡) 𝑊) = ((𝑢 𝑣) 𝑊))
3027, 29oveq12d 7148 . . . . . . . . . . . . . 14 (𝑡 = 𝑣 → (𝐸 ((𝑢 𝑡) 𝑊)) = (𝑇 ((𝑢 𝑣) 𝑊)))
3130oveq2d 7146 . . . . . . . . . . . . 13 (𝑡 = 𝑣 → ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))) = ((𝑃 𝑄) (𝑇 ((𝑢 𝑣) 𝑊))))
32 cdleme40r.x . . . . . . . . . . . . 13 𝑋 = ((𝑃 𝑄) (𝑇 ((𝑢 𝑣) 𝑊)))
3331, 32syl6eqr 2874 . . . . . . . . . . . 12 (𝑡 = 𝑣 → ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))) = 𝑋)
3433eqeq2d 2832 . . . . . . . . . . 11 (𝑡 = 𝑣 → (𝑧 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))) ↔ 𝑧 = 𝑋))
3519, 34imbi12d 348 . . . . . . . . . 10 (𝑡 = 𝑣 → (((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑧 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊)))) ↔ ((¬ 𝑣 𝑊 ∧ ¬ 𝑣 (𝑃 𝑄)) → 𝑧 = 𝑋)))
3635cbvralvw 3426 . . . . . . . . 9 (∀𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑧 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊)))) ↔ ∀𝑣𝐴 ((¬ 𝑣 𝑊 ∧ ¬ 𝑣 (𝑃 𝑄)) → 𝑧 = 𝑋))
3714, 36syl6bb 290 . . . . . . . 8 (𝑦 = 𝑧 → (∀𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊)))) ↔ ∀𝑣𝐴 ((¬ 𝑣 𝑊 ∧ ¬ 𝑣 (𝑃 𝑄)) → 𝑧 = 𝑋)))
3837cbvriotavw 7098 . . . . . . 7 (𝑦𝐵𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))))) = (𝑧𝐵𝑣𝐴 ((¬ 𝑣 𝑊 ∧ ¬ 𝑣 (𝑃 𝑄)) → 𝑧 = 𝑋))
3911, 38syl6eq 2872 . . . . . 6 (𝑠 = 𝑢 → (𝑦𝐵𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = 𝐺)) = (𝑧𝐵𝑣𝐴 ((¬ 𝑣 𝑊 ∧ ¬ 𝑣 (𝑃 𝑄)) → 𝑧 = 𝑋)))
40 cdleme40.i . . . . . 6 𝐼 = (𝑦𝐵𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = 𝐺))
41 cdleme40r.o . . . . . 6 𝑂 = (𝑧𝐵𝑣𝐴 ((¬ 𝑣 𝑊 ∧ ¬ 𝑣 (𝑃 𝑄)) → 𝑧 = 𝑋))
4239, 40, 413eqtr4g 2881 . . . . 5 (𝑠 = 𝑢𝐼 = 𝑂)
43 oveq1 7137 . . . . . . 7 (𝑠 = 𝑢 → (𝑠 𝑈) = (𝑢 𝑈))
44 oveq2 7138 . . . . . . . . 9 (𝑠 = 𝑢 → (𝑃 𝑠) = (𝑃 𝑢))
4544oveq1d 7145 . . . . . . . 8 (𝑠 = 𝑢 → ((𝑃 𝑠) 𝑊) = ((𝑃 𝑢) 𝑊))
4645oveq2d 7146 . . . . . . 7 (𝑠 = 𝑢 → (𝑄 ((𝑃 𝑠) 𝑊)) = (𝑄 ((𝑃 𝑢) 𝑊)))
4743, 46oveq12d 7148 . . . . . 6 (𝑠 = 𝑢 → ((𝑠 𝑈) (𝑄 ((𝑃 𝑠) 𝑊))) = ((𝑢 𝑈) (𝑄 ((𝑃 𝑢) 𝑊))))
48 cdleme40.d . . . . . 6 𝐷 = ((𝑠 𝑈) (𝑄 ((𝑃 𝑠) 𝑊)))
49 cdleme40r.y . . . . . 6 𝑌 = ((𝑢 𝑈) (𝑄 ((𝑃 𝑢) 𝑊)))
5047, 48, 493eqtr4g 2881 . . . . 5 (𝑠 = 𝑢𝐷 = 𝑌)
511, 42, 50ifbieq12d 4467 . . . 4 (𝑠 = 𝑢 → if(𝑠 (𝑃 𝑄), 𝐼, 𝐷) = if(𝑢 (𝑃 𝑄), 𝑂, 𝑌))
52 cdleme40.n . . . 4 𝑁 = if(𝑠 (𝑃 𝑄), 𝐼, 𝐷)
53 cdleme40r.v . . . 4 𝑉 = if(𝑢 (𝑃 𝑄), 𝑂, 𝑌)
5451, 52, 533eqtr4g 2881 . . 3 (𝑠 = 𝑢𝑁 = 𝑉)
5554cbvcsbv 3869 . 2 𝑅 / 𝑠𝑁 = 𝑅 / 𝑢𝑉
5655a1i 11 1 (𝑅𝐴𝑅 / 𝑠𝑁 = 𝑅 / 𝑢𝑉)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399   = wceq 1538  wcel 2115  wral 3126  csb 3857  ifcif 4440   class class class wbr 5039  cfv 6328  crio 7087  (class class class)co 7130  Basecbs 16462  lecple 16551  joincjn 17533  meetcmee 17534  Atomscatm 36441  LHypclh 37162
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ral 3131  df-rab 3135  df-v 3473  df-sbc 3750  df-csb 3858  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-sn 4541  df-pr 4543  df-op 4547  df-uni 4812  df-br 5040  df-iota 6287  df-fv 6336  df-riota 7088  df-ov 7133
This theorem is referenced by:  cdleme40w  37648
  Copyright terms: Public domain W3C validator