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

Theorem cdleme27b 36176
Description: Lemma for cdleme27N 36177. (Contributed by NM, 3-Feb-2013.)
Hypotheses
Ref Expression
cdleme26.b 𝐵 = (Base‘𝐾)
cdleme26.l = (le‘𝐾)
cdleme26.j = (join‘𝐾)
cdleme26.m = (meet‘𝐾)
cdleme26.a 𝐴 = (Atoms‘𝐾)
cdleme26.h 𝐻 = (LHyp‘𝐾)
cdleme27.u 𝑈 = ((𝑃 𝑄) 𝑊)
cdleme27.f 𝐹 = ((𝑠 𝑈) (𝑄 ((𝑃 𝑠) 𝑊)))
cdleme27.z 𝑍 = ((𝑧 𝑈) (𝑄 ((𝑃 𝑧) 𝑊)))
cdleme27.n 𝑁 = ((𝑃 𝑄) (𝑍 ((𝑠 𝑧) 𝑊)))
cdleme27.d 𝐷 = (𝑢𝐵𝑧𝐴 ((¬ 𝑧 𝑊 ∧ ¬ 𝑧 (𝑃 𝑄)) → 𝑢 = 𝑁))
cdleme27.c 𝐶 = if(𝑠 (𝑃 𝑄), 𝐷, 𝐹)
cdleme27.g 𝐺 = ((𝑡 𝑈) (𝑄 ((𝑃 𝑡) 𝑊)))
cdleme27.o 𝑂 = ((𝑃 𝑄) (𝑍 ((𝑡 𝑧) 𝑊)))
cdleme27.e 𝐸 = (𝑢𝐵𝑧𝐴 ((¬ 𝑧 𝑊 ∧ ¬ 𝑧 (𝑃 𝑄)) → 𝑢 = 𝑂))
cdleme27.y 𝑌 = if(𝑡 (𝑃 𝑄), 𝐸, 𝐺)
Assertion
Ref Expression
cdleme27b (𝑠 = 𝑡𝐶 = 𝑌)
Distinct variable groups:   𝑡,𝑠,𝑢,𝑧,𝐴   𝐵,𝑠,𝑡,𝑢,𝑧   𝑢,𝐹   𝑢,𝐺   𝐻,𝑠,𝑡,𝑧   ,𝑠,𝑡,𝑢,𝑧   𝐾,𝑠,𝑡,𝑧   ,𝑠,𝑡,𝑢,𝑧   ,𝑠,𝑡,𝑢,𝑧   𝑡,𝑁,𝑢   𝑂,𝑠,𝑢   𝑃,𝑠,𝑡,𝑢,𝑧   𝑄,𝑠,𝑡,𝑢,𝑧   𝑈,𝑠,𝑡,𝑢,𝑧   𝑊,𝑠,𝑡,𝑢,𝑧
Allowed substitution hints:   𝐶(𝑧,𝑢,𝑡,𝑠)   𝐷(𝑧,𝑢,𝑡,𝑠)   𝐸(𝑧,𝑢,𝑡,𝑠)   𝐹(𝑧,𝑡,𝑠)   𝐺(𝑧,𝑡,𝑠)   𝐻(𝑢)   𝐾(𝑢)   𝑁(𝑧,𝑠)   𝑂(𝑧,𝑡)   𝑌(𝑧,𝑢,𝑡,𝑠)   𝑍(𝑧,𝑢,𝑡,𝑠)

Proof of Theorem cdleme27b
StepHypRef Expression
1 breq1 4807 . . 3 (𝑠 = 𝑡 → (𝑠 (𝑃 𝑄) ↔ 𝑡 (𝑃 𝑄)))
2 oveq1 6821 . . . . . . . . . . . 12 (𝑠 = 𝑡 → (𝑠 𝑧) = (𝑡 𝑧))
32oveq1d 6829 . . . . . . . . . . 11 (𝑠 = 𝑡 → ((𝑠 𝑧) 𝑊) = ((𝑡 𝑧) 𝑊))
43oveq2d 6830 . . . . . . . . . 10 (𝑠 = 𝑡 → (𝑍 ((𝑠 𝑧) 𝑊)) = (𝑍 ((𝑡 𝑧) 𝑊)))
54oveq2d 6830 . . . . . . . . 9 (𝑠 = 𝑡 → ((𝑃 𝑄) (𝑍 ((𝑠 𝑧) 𝑊))) = ((𝑃 𝑄) (𝑍 ((𝑡 𝑧) 𝑊))))
6 cdleme27.n . . . . . . . . 9 𝑁 = ((𝑃 𝑄) (𝑍 ((𝑠 𝑧) 𝑊)))
7 cdleme27.o . . . . . . . . 9 𝑂 = ((𝑃 𝑄) (𝑍 ((𝑡 𝑧) 𝑊)))
85, 6, 73eqtr4g 2819 . . . . . . . 8 (𝑠 = 𝑡𝑁 = 𝑂)
98eqeq2d 2770 . . . . . . 7 (𝑠 = 𝑡 → (𝑢 = 𝑁𝑢 = 𝑂))
109imbi2d 329 . . . . . 6 (𝑠 = 𝑡 → (((¬ 𝑧 𝑊 ∧ ¬ 𝑧 (𝑃 𝑄)) → 𝑢 = 𝑁) ↔ ((¬ 𝑧 𝑊 ∧ ¬ 𝑧 (𝑃 𝑄)) → 𝑢 = 𝑂)))
1110ralbidv 3124 . . . . 5 (𝑠 = 𝑡 → (∀𝑧𝐴 ((¬ 𝑧 𝑊 ∧ ¬ 𝑧 (𝑃 𝑄)) → 𝑢 = 𝑁) ↔ ∀𝑧𝐴 ((¬ 𝑧 𝑊 ∧ ¬ 𝑧 (𝑃 𝑄)) → 𝑢 = 𝑂)))
1211riotabidv 6777 . . . 4 (𝑠 = 𝑡 → (𝑢𝐵𝑧𝐴 ((¬ 𝑧 𝑊 ∧ ¬ 𝑧 (𝑃 𝑄)) → 𝑢 = 𝑁)) = (𝑢𝐵𝑧𝐴 ((¬ 𝑧 𝑊 ∧ ¬ 𝑧 (𝑃 𝑄)) → 𝑢 = 𝑂)))
13 cdleme27.d . . . 4 𝐷 = (𝑢𝐵𝑧𝐴 ((¬ 𝑧 𝑊 ∧ ¬ 𝑧 (𝑃 𝑄)) → 𝑢 = 𝑁))
14 cdleme27.e . . . 4 𝐸 = (𝑢𝐵𝑧𝐴 ((¬ 𝑧 𝑊 ∧ ¬ 𝑧 (𝑃 𝑄)) → 𝑢 = 𝑂))
1512, 13, 143eqtr4g 2819 . . 3 (𝑠 = 𝑡𝐷 = 𝐸)
16 oveq1 6821 . . . . 5 (𝑠 = 𝑡 → (𝑠 𝑈) = (𝑡 𝑈))
17 oveq2 6822 . . . . . . 7 (𝑠 = 𝑡 → (𝑃 𝑠) = (𝑃 𝑡))
1817oveq1d 6829 . . . . . 6 (𝑠 = 𝑡 → ((𝑃 𝑠) 𝑊) = ((𝑃 𝑡) 𝑊))
1918oveq2d 6830 . . . . 5 (𝑠 = 𝑡 → (𝑄 ((𝑃 𝑠) 𝑊)) = (𝑄 ((𝑃 𝑡) 𝑊)))
2016, 19oveq12d 6832 . . . 4 (𝑠 = 𝑡 → ((𝑠 𝑈) (𝑄 ((𝑃 𝑠) 𝑊))) = ((𝑡 𝑈) (𝑄 ((𝑃 𝑡) 𝑊))))
21 cdleme27.f . . . 4 𝐹 = ((𝑠 𝑈) (𝑄 ((𝑃 𝑠) 𝑊)))
22 cdleme27.g . . . 4 𝐺 = ((𝑡 𝑈) (𝑄 ((𝑃 𝑡) 𝑊)))
2320, 21, 223eqtr4g 2819 . . 3 (𝑠 = 𝑡𝐹 = 𝐺)
241, 15, 23ifbieq12d 4257 . 2 (𝑠 = 𝑡 → if(𝑠 (𝑃 𝑄), 𝐷, 𝐹) = if(𝑡 (𝑃 𝑄), 𝐸, 𝐺))
25 cdleme27.c . 2 𝐶 = if(𝑠 (𝑃 𝑄), 𝐷, 𝐹)
26 cdleme27.y . 2 𝑌 = if(𝑡 (𝑃 𝑄), 𝐸, 𝐺)
2724, 25, 263eqtr4g 2819 1 (𝑠 = 𝑡𝐶 = 𝑌)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383   = wceq 1632  wral 3050  ifcif 4230   class class class wbr 4804  cfv 6049  crio 6774  (class class class)co 6814  Basecbs 16079  lecple 16170  joincjn 17165  meetcmee 17166  Atomscatm 35071  LHypclh 35791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-riota 6775  df-ov 6817
This theorem is referenced by:  cdleme27N  36177  cdleme28c  36180
  Copyright terms: Public domain W3C validator