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 39942
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 5151 . . . . 5 (𝑠 = 𝑢 → (𝑠 (𝑃 𝑄) ↔ 𝑢 (𝑃 𝑄)))
2 cdleme40.g . . . . . . . . . . . 12 𝐺 = ((𝑃 𝑄) (𝐸 ((𝑠 𝑡) 𝑊)))
3 oveq1 7427 . . . . . . . . . . . . . . 15 (𝑠 = 𝑢 → (𝑠 𝑡) = (𝑢 𝑡))
43oveq1d 7435 . . . . . . . . . . . . . 14 (𝑠 = 𝑢 → ((𝑠 𝑡) 𝑊) = ((𝑢 𝑡) 𝑊))
54oveq2d 7436 . . . . . . . . . . . . 13 (𝑠 = 𝑢 → (𝐸 ((𝑠 𝑡) 𝑊)) = (𝐸 ((𝑢 𝑡) 𝑊)))
65oveq2d 7436 . . . . . . . . . . . 12 (𝑠 = 𝑢 → ((𝑃 𝑄) (𝐸 ((𝑠 𝑡) 𝑊))) = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))))
72, 6eqtrid 2780 . . . . . . . . . . 11 (𝑠 = 𝑢𝐺 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))))
87eqeq2d 2739 . . . . . . . . . 10 (𝑠 = 𝑢 → (𝑦 = 𝐺𝑦 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊)))))
98imbi2d 340 . . . . . . . . 9 (𝑠 = 𝑢 → (((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = 𝐺) ↔ ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))))))
109ralbidv 3174 . . . . . . . 8 (𝑠 = 𝑢 → (∀𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = 𝐺) ↔ ∀𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))))))
1110riotabidv 7378 . . . . . . 7 (𝑠 = 𝑢 → (𝑦𝐵𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = 𝐺)) = (𝑦𝐵𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))))))
12 eqeq1 2732 . . . . . . . . . . 11 (𝑦 = 𝑧 → (𝑦 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))) ↔ 𝑧 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊)))))
1312imbi2d 340 . . . . . . . . . 10 (𝑦 = 𝑧 → (((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊)))) ↔ ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑧 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))))))
1413ralbidv 3174 . . . . . . . . 9 (𝑦 = 𝑧 → (∀𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊)))) ↔ ∀𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑧 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))))))
15 breq1 5151 . . . . . . . . . . . . 13 (𝑡 = 𝑣 → (𝑡 𝑊𝑣 𝑊))
1615notbid 318 . . . . . . . . . . . 12 (𝑡 = 𝑣 → (¬ 𝑡 𝑊 ↔ ¬ 𝑣 𝑊))
17 breq1 5151 . . . . . . . . . . . . 13 (𝑡 = 𝑣 → (𝑡 (𝑃 𝑄) ↔ 𝑣 (𝑃 𝑄)))
1817notbid 318 . . . . . . . . . . . 12 (𝑡 = 𝑣 → (¬ 𝑡 (𝑃 𝑄) ↔ ¬ 𝑣 (𝑃 𝑄)))
1916, 18anbi12d 631 . . . . . . . . . . 11 (𝑡 = 𝑣 → ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) ↔ (¬ 𝑣 𝑊 ∧ ¬ 𝑣 (𝑃 𝑄))))
20 oveq1 7427 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑣 → (𝑡 𝑈) = (𝑣 𝑈))
21 oveq2 7428 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑣 → (𝑃 𝑡) = (𝑃 𝑣))
2221oveq1d 7435 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑣 → ((𝑃 𝑡) 𝑊) = ((𝑃 𝑣) 𝑊))
2322oveq2d 7436 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑣 → (𝑄 ((𝑃 𝑡) 𝑊)) = (𝑄 ((𝑃 𝑣) 𝑊)))
2420, 23oveq12d 7438 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑣 → ((𝑡 𝑈) (𝑄 ((𝑃 𝑡) 𝑊))) = ((𝑣 𝑈) (𝑄 ((𝑃 𝑣) 𝑊))))
25 cdleme40.e . . . . . . . . . . . . . . . 16 𝐸 = ((𝑡 𝑈) (𝑄 ((𝑃 𝑡) 𝑊)))
26 cdleme40r.t . . . . . . . . . . . . . . . 16 𝑇 = ((𝑣 𝑈) (𝑄 ((𝑃 𝑣) 𝑊)))
2724, 25, 263eqtr4g 2793 . . . . . . . . . . . . . . 15 (𝑡 = 𝑣𝐸 = 𝑇)
28 oveq2 7428 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑣 → (𝑢 𝑡) = (𝑢 𝑣))
2928oveq1d 7435 . . . . . . . . . . . . . . 15 (𝑡 = 𝑣 → ((𝑢 𝑡) 𝑊) = ((𝑢 𝑣) 𝑊))
3027, 29oveq12d 7438 . . . . . . . . . . . . . 14 (𝑡 = 𝑣 → (𝐸 ((𝑢 𝑡) 𝑊)) = (𝑇 ((𝑢 𝑣) 𝑊)))
3130oveq2d 7436 . . . . . . . . . . . . 13 (𝑡 = 𝑣 → ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))) = ((𝑃 𝑄) (𝑇 ((𝑢 𝑣) 𝑊))))
32 cdleme40r.x . . . . . . . . . . . . 13 𝑋 = ((𝑃 𝑄) (𝑇 ((𝑢 𝑣) 𝑊)))
3331, 32eqtr4di 2786 . . . . . . . . . . . 12 (𝑡 = 𝑣 → ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))) = 𝑋)
3433eqeq2d 2739 . . . . . . . . . . 11 (𝑡 = 𝑣 → (𝑧 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))) ↔ 𝑧 = 𝑋))
3519, 34imbi12d 344 . . . . . . . . . 10 (𝑡 = 𝑣 → (((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑧 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊)))) ↔ ((¬ 𝑣 𝑊 ∧ ¬ 𝑣 (𝑃 𝑄)) → 𝑧 = 𝑋)))
3635cbvralvw 3231 . . . . . . . . 9 (∀𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑧 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊)))) ↔ ∀𝑣𝐴 ((¬ 𝑣 𝑊 ∧ ¬ 𝑣 (𝑃 𝑄)) → 𝑧 = 𝑋))
3714, 36bitrdi 287 . . . . . . . 8 (𝑦 = 𝑧 → (∀𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊)))) ↔ ∀𝑣𝐴 ((¬ 𝑣 𝑊 ∧ ¬ 𝑣 (𝑃 𝑄)) → 𝑧 = 𝑋)))
3837cbvriotavw 7386 . . . . . . 7 (𝑦𝐵𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = ((𝑃 𝑄) (𝐸 ((𝑢 𝑡) 𝑊))))) = (𝑧𝐵𝑣𝐴 ((¬ 𝑣 𝑊 ∧ ¬ 𝑣 (𝑃 𝑄)) → 𝑧 = 𝑋))
3911, 38eqtrdi 2784 . . . . . 6 (𝑠 = 𝑢 → (𝑦𝐵𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = 𝐺)) = (𝑧𝐵𝑣𝐴 ((¬ 𝑣 𝑊 ∧ ¬ 𝑣 (𝑃 𝑄)) → 𝑧 = 𝑋)))
40 cdleme40.i . . . . . 6 𝐼 = (𝑦𝐵𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑦 = 𝐺))
41 cdleme40r.o . . . . . 6 𝑂 = (𝑧𝐵𝑣𝐴 ((¬ 𝑣 𝑊 ∧ ¬ 𝑣 (𝑃 𝑄)) → 𝑧 = 𝑋))
4239, 40, 413eqtr4g 2793 . . . . 5 (𝑠 = 𝑢𝐼 = 𝑂)
43 oveq1 7427 . . . . . . 7 (𝑠 = 𝑢 → (𝑠 𝑈) = (𝑢 𝑈))
44 oveq2 7428 . . . . . . . . 9 (𝑠 = 𝑢 → (𝑃 𝑠) = (𝑃 𝑢))
4544oveq1d 7435 . . . . . . . 8 (𝑠 = 𝑢 → ((𝑃 𝑠) 𝑊) = ((𝑃 𝑢) 𝑊))
4645oveq2d 7436 . . . . . . 7 (𝑠 = 𝑢 → (𝑄 ((𝑃 𝑠) 𝑊)) = (𝑄 ((𝑃 𝑢) 𝑊)))
4743, 46oveq12d 7438 . . . . . 6 (𝑠 = 𝑢 → ((𝑠 𝑈) (𝑄 ((𝑃 𝑠) 𝑊))) = ((𝑢 𝑈) (𝑄 ((𝑃 𝑢) 𝑊))))
48 cdleme40.d . . . . . 6 𝐷 = ((𝑠 𝑈) (𝑄 ((𝑃 𝑠) 𝑊)))
49 cdleme40r.y . . . . . 6 𝑌 = ((𝑢 𝑈) (𝑄 ((𝑃 𝑢) 𝑊)))
5047, 48, 493eqtr4g 2793 . . . . 5 (𝑠 = 𝑢𝐷 = 𝑌)
511, 42, 50ifbieq12d 4557 . . . 4 (𝑠 = 𝑢 → if(𝑠 (𝑃 𝑄), 𝐼, 𝐷) = if(𝑢 (𝑃 𝑄), 𝑂, 𝑌))
52 cdleme40.n . . . 4 𝑁 = if(𝑠 (𝑃 𝑄), 𝐼, 𝐷)
53 cdleme40r.v . . . 4 𝑉 = if(𝑢 (𝑃 𝑄), 𝑂, 𝑌)
5451, 52, 533eqtr4g 2793 . . 3 (𝑠 = 𝑢𝑁 = 𝑉)
5554cbvcsbv 3904 . 2 𝑅 / 𝑠𝑁 = 𝑅 / 𝑢𝑉
5655a1i 11 1 (𝑅𝐴𝑅 / 𝑠𝑁 = 𝑅 / 𝑢𝑉)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395   = wceq 1534  wcel 2099  wral 3058  csb 3892  ifcif 4529   class class class wbr 5148  cfv 6548  crio 7375  (class class class)co 7420  Basecbs 17179  lecple 17239  joincjn 18302  meetcmee 18303  Atomscatm 38735  LHypclh 39457
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-11 2147  ax-12 2167  ax-ext 2699
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ral 3059  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-iota 6500  df-fv 6556  df-riota 7376  df-ov 7423
This theorem is referenced by:  cdleme40w  39943
  Copyright terms: Public domain W3C validator