![]() |
Metamath
Proof Explorer Theorem List (p. 400 of 484) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30748) |
![]() (30749-32271) |
![]() (32272-48316) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cdlemefrs29bpre0 39901* | TODO fix comment. (Contributed by NM, 29-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ (𝑠 = 𝑅 → (𝜑 ↔ 𝜓)) & ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑))) → 𝑁 ∈ 𝐵) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) → (∀𝑠 ∈ 𝐴 (((¬ 𝑠 ≤ 𝑊 ∧ 𝜑) ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅) → 𝑧 = (𝑁 ∨ (𝑅 ∧ 𝑊))) ↔ 𝑧 = ⦋𝑅 / 𝑠⦌𝑁)) | ||
Theorem | cdlemefrs29bpre1 39902* | TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ (𝑠 = 𝑅 → (𝜑 ↔ 𝜓)) & ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑))) → 𝑁 ∈ 𝐵) & ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) → ⦋𝑅 / 𝑠⦌𝑁 ∈ 𝐵) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) → ∃𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 (((¬ 𝑠 ≤ 𝑊 ∧ 𝜑) ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅) → 𝑧 = (𝑁 ∨ (𝑅 ∧ 𝑊)))) | ||
Theorem | cdlemefrs29cpre1 39903* | TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ (𝑠 = 𝑅 → (𝜑 ↔ 𝜓)) & ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑))) → 𝑁 ∈ 𝐵) & ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) → ⦋𝑅 / 𝑠⦌𝑁 ∈ 𝐵) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) → ∃!𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 (((¬ 𝑠 ≤ 𝑊 ∧ 𝜑) ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅) → 𝑧 = (𝑁 ∨ (𝑅 ∧ 𝑊)))) | ||
Theorem | cdlemefrs29clN 39904* | TODO: NOT USED? Show closure of the unique element in cdlemefrs29cpre1 39903. (Contributed by NM, 29-Mar-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ (𝑠 = 𝑅 → (𝜑 ↔ 𝜓)) & ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑))) → 𝑁 ∈ 𝐵) & ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) → ⦋𝑅 / 𝑠⦌𝑁 ∈ 𝐵) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅) → 𝑧 = (𝑁 ∨ (𝑅 ∧ 𝑊)))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) → 𝑂 ∈ 𝐵) | ||
Theorem | cdlemefrs32fva 39905* | Part of proof of Lemma E in [Crawley] p. 113. Value of 𝐹 at an atom not under 𝑊. TODO: FIX COMMENT. TODO: consolidate uses of lhpmat 39535 here and elsewhere, and presence/absence of 𝑠 ≤ (𝑃 ∨ 𝑄) term. Also, why can proof be shortened with cdleme29cl 39882? What is difference from cdlemefs27cl 39918? (Contributed by NM, 29-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ (𝑠 = 𝑅 → (𝜑 ↔ 𝜓)) & ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑))) → 𝑁 ∈ 𝐵) & ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) → ⦋𝑅 / 𝑠⦌𝑁 ∈ 𝐵) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) → ⦋𝑅 / 𝑥⦌𝑂 = ⦋𝑅 / 𝑠⦌𝑁) | ||
Theorem | cdlemefrs32fva1 39906* | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ (𝑠 = 𝑅 → (𝜑 ↔ 𝜓)) & ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑))) → 𝑁 ∈ 𝐵) & ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) → ⦋𝑅 / 𝑠⦌𝑁 ∈ 𝐵) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) → (𝐹‘𝑅) = ⦋𝑅 / 𝑠⦌𝑁) | ||
Theorem | cdlemefr29exN 39907* | Lemma for cdlemefs29bpre1N 39922. (Compare cdleme25a 39858.) TODO: FIX COMMENT. TODO: IS THIS NEEDED? (Contributed by NM, 28-Mar-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ ∀𝑠 ∈ 𝐴 𝐶 ∈ 𝐵) → ∃𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝐶 ∨ (𝑋 ∧ 𝑊)) ∈ 𝐵)) | ||
Theorem | cdlemefr27cl 39908 | Part of proof of Lemma E in [Crawley] p. 113. Closure of 𝑁. (Contributed by NM, 23-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐶 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑃 ≠ 𝑄)) → 𝑁 ∈ 𝐵) | ||
Theorem | cdlemefr32sn2aw 39909* | Show that ⦋𝑅 / 𝑠⦌𝑁 is an atom not under 𝑊 when ¬ 𝑅 ≤ (𝑃 ∨ 𝑄). (Contributed by NM, 28-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐶 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (⦋𝑅 / 𝑠⦌𝑁 ∈ 𝐴 ∧ ¬ ⦋𝑅 / 𝑠⦌𝑁 ≤ 𝑊)) | ||
Theorem | cdlemefr32snb 39910* | Show closure of ⦋𝑅 / 𝑠⦌𝑁. (Contributed by NM, 28-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐶 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ⦋𝑅 / 𝑠⦌𝑁 ∈ 𝐵) | ||
Theorem | cdlemefr29bpre0N 39911* | TODO fix comment. (Contributed by NM, 28-Mar-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐶 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (∀𝑠 ∈ 𝐴 (((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅) → 𝑧 = (𝑁 ∨ (𝑅 ∧ 𝑊))) ↔ 𝑧 = ⦋𝑅 / 𝑠⦌𝑁)) | ||
Theorem | cdlemefr29clN 39912* | Show closure of the unique element in cdleme29c 39881. TODO fix comment. TODO Not needed? (Contributed by NM, 29-Mar-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐶 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅) → 𝑧 = (𝑁 ∨ (𝑅 ∧ 𝑊)))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑂 ∈ 𝐵) | ||
Theorem | cdleme43frv1snN 39913* | Value of ⦋𝑅 / 𝑠⦌𝑁 when ¬ 𝑅 ≤ (𝑃 ∨ 𝑄). (Contributed by NM, 30-Mar-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐶 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) & ⊢ 𝑋 = ((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊))) ⇒ ⊢ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ⦋𝑅 / 𝑠⦌𝑁 = 𝑋) | ||
Theorem | cdlemefr32fvaN 39914* | Part of proof of Lemma E in [Crawley] p. 113. Value of 𝐹 at an atom not under 𝑊. TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐶 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ⦋𝑅 / 𝑥⦌𝑂 = ⦋𝑅 / 𝑠⦌𝑁) | ||
Theorem | cdlemefr32fva1 39915* | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐶 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝐹‘𝑅) = ⦋𝑅 / 𝑠⦌𝑁) | ||
Theorem | cdlemefr31fv1 39916* | Value of (𝐹‘𝑅) when ¬ 𝑅 ≤ (𝑃 ∨ 𝑄). TODO This may be useful for shortening others that now use riotasv 38463 3d . TODO: FIX COMMENT. (Contributed by NM, 30-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐶 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) & ⊢ 𝑋 = ((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝐹‘𝑅) = 𝑋) | ||
Theorem | cdlemefs29pre00N 39917 | FIX COMMENT. TODO: see if this is the optimal utility theorem using lhpmat 39535. (Contributed by NM, 27-Mar-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ 𝑠 ∈ 𝐴) → (((¬ 𝑠 ≤ 𝑊 ∧ 𝑠 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅) ↔ (¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅))) | ||
Theorem | cdlemefs27cl 39918* | Part of proof of Lemma E in [Crawley] p. 113. Closure of 𝑁. TODO FIX COMMENT This is the start of a re-proof of cdleme27cl 39871 etc. with the 𝑠 ≤ (𝑃 ∨ 𝑄) condition (so as to not have the 𝐶 hypothesis). (Contributed by NM, 24-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑢 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝐸)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊) ∧ 𝑠 ≤ (𝑃 ∨ 𝑄) ∧ 𝑃 ≠ 𝑄)) → 𝑁 ∈ 𝐵) | ||
Theorem | cdlemefs32sn1aw 39919* | Show that ⦋𝑅 / 𝑠⦌𝑁 is an atom not under 𝑊 when 𝑅 ≤ (𝑃 ∨ 𝑄). (Contributed by NM, 24-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑅 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝑍 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝑌)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (⦋𝑅 / 𝑠⦌𝑁 ∈ 𝐴 ∧ ¬ ⦋𝑅 / 𝑠⦌𝑁 ≤ 𝑊)) | ||
Theorem | cdlemefs32snb 39920* | Show closure of ⦋𝑅 / 𝑠⦌𝑁. (Contributed by NM, 24-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ⦋𝑅 / 𝑠⦌𝑁 ∈ 𝐵) | ||
Theorem | cdlemefs29bpre0N 39921* | TODO: FIX COMMENT. (Contributed by NM, 26-Mar-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (∀𝑠 ∈ 𝐴 (((¬ 𝑠 ≤ 𝑊 ∧ 𝑠 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅) → 𝑧 = (𝑁 ∨ (𝑅 ∧ 𝑊))) ↔ 𝑧 = ⦋𝑅 / 𝑠⦌𝑁)) | ||
Theorem | cdlemefs29bpre1N 39922* | TODO: FIX COMMENT. (Contributed by NM, 27-Mar-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ∃𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 (((¬ 𝑠 ≤ 𝑊 ∧ 𝑠 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅) → 𝑧 = (𝑁 ∨ (𝑅 ∧ 𝑊)))) | ||
Theorem | cdlemefs29cpre1N 39923* | TODO: FIX COMMENT. (Contributed by NM, 26-Mar-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ∃!𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 (((¬ 𝑠 ≤ 𝑊 ∧ 𝑠 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅) → 𝑧 = (𝑁 ∨ (𝑅 ∧ 𝑊)))) | ||
Theorem | cdlemefs29clN 39924* | Show closure of the unique element in cdleme29c 39881. (Contributed by NM, 27-Mar-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅) → 𝑧 = (𝑁 ∨ (𝑅 ∧ 𝑊)))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑂 ∈ 𝐵) | ||
Theorem | cdleme43fsv1snlem 39925* | Value of ⦋𝑅 / 𝑠⦌𝑁 when 𝑅 ≤ (𝑃 ∨ 𝑄). (Contributed by NM, 30-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) & ⊢ 𝑌 = ((𝑆 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊))) & ⊢ 𝑍 = ((𝑃 ∨ 𝑄) ∧ (𝑌 ∨ ((𝑅 ∨ 𝑆) ∧ 𝑊))) & ⊢ 𝑉 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑅 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝑋 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝑉)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → ⦋𝑅 / 𝑠⦌𝑁 = 𝑍) | ||
Theorem | cdleme43fsv1sn 39926* | Value of ⦋𝑅 / 𝑠⦌𝑁 when 𝑅 ≤ (𝑃 ∨ 𝑄). (Contributed by NM, 30-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) & ⊢ 𝑌 = ((𝑆 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊))) & ⊢ 𝑍 = ((𝑃 ∨ 𝑄) ∧ (𝑌 ∨ ((𝑅 ∨ 𝑆) ∧ 𝑊))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → ⦋𝑅 / 𝑠⦌𝑁 = 𝑍) | ||
Theorem | cdlemefs32fvaN 39927* | Part of proof of Lemma E in [Crawley] p. 113. Value of 𝐹 at an atom not under 𝑊. TODO: FIX COMMENT. TODO: consolidate uses of lhpmat 39535 here and elsewhere, and presence/absence of 𝑠 ≤ (𝑃 ∨ 𝑄) term. Also, why can proof be shortened with cdleme27cl 39871? What is difference from cdlemefs27cl 39918? (Contributed by NM, 29-Mar-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ⦋𝑅 / 𝑥⦌𝑂 = ⦋𝑅 / 𝑠⦌𝑁) | ||
Theorem | cdlemefs32fva1 39928* | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝐹‘𝑅) = ⦋𝑅 / 𝑠⦌𝑁) | ||
Theorem | cdlemefs31fv1 39929* |
Value of (𝐹‘𝑅) when 𝑅 ≤ (𝑃 ∨ 𝑄).
TODO This may be useful for shortening others that now use riotasv 38463
3d . TODO: FIX COMMENT.
***END OF VALUE AT ATOM STUFF TO REPLACE
ONES BELOW***
"cdleme3xsn1aw" decreased using "cdlemefs32sn1aw" "cdleme32sn1aw" decreased from 3302 to 36 using "cdlemefs32sn1aw". "cdleme32sn2aw" decreased from 1687 to 26 using "cdlemefr32sn2aw". "cdleme32snaw" decreased from 376 to 375 using "cdlemefs32sn1aw". "cdleme32snaw" decreased from 375 to 368 using "cdlemefr32sn2aw". "cdleme35sn3a" decreased from 547 to 523 using "cdleme43frv1sn".(Contributed by NM, 27-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) & ⊢ 𝑌 = ((𝑆 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊))) & ⊢ 𝑍 = ((𝑃 ∨ 𝑄) ∧ (𝑌 ∨ ((𝑅 ∨ 𝑆) ∧ 𝑊))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → (𝐹‘𝑅) = 𝑍) | ||
Theorem | cdlemefr44 39930* | Value of f(r) when r is an atom not under pq, using more compact hypotheses. TODO: eliminate and use cdlemefr45 instead? TODO: FIX COMMENT. (Contributed by NM, 31-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝐹‘𝑅) = ⦋𝑅 / 𝑡⦌𝐷) | ||
Theorem | cdlemefs44 39931* | Value of fs(r) when r is an atom under pq and s is any atom not under pq, using more compact hypotheses. TODO: eliminate and use cdlemefs45 39934 instead TODO: FIX COMMENT. (Contributed by NM, 31-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → (𝐹‘𝑅) = ⦋𝑅 / 𝑠⦌⦋𝑆 / 𝑡⦌𝐸) | ||
Theorem | cdlemefr45 39932* | Value of f(r) when r is an atom not under pq, using very compact hypotheses. TODO: FIX COMMENT. (Contributed by NM, 1-Apr-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝐹‘𝑅) = ⦋𝑅 / 𝑡⦌𝐷) | ||
Theorem | cdlemefr45e 39933* | Explicit expansion of cdlemefr45 39932. TODO: use to shorten cdlemefr45 39932 uses? TODO: FIX COMMENT. (Contributed by NM, 10-Apr-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝐹‘𝑅) = ((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊)))) | ||
Theorem | cdlemefs45 39934* | Value of fs(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.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥)) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → (𝐹‘𝑅) = ⦋𝑅 / 𝑠⦌⦋𝑆 / 𝑡⦌𝐸) | ||
Theorem | cdlemefs45ee 39935* | Explicit expansion of cdlemefs45 39934. TODO: use to shorten cdlemefs45 39934 uses? Should ((𝑆 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊))) be assigned to a hypothesis letter? TODO: FIX COMMENT. (Contributed by NM, 10-Apr-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥)) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → (𝐹‘𝑅) = ((𝑃 ∨ 𝑄) ∧ (((𝑆 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑆) ∧ 𝑊)))) | ||
Theorem | cdlemefs45eN 39936* | Explicit expansion of cdlemefs45 39934. TODO: use to shorten cdlemefs45 39934 uses? TODO: FIX COMMENT. (Contributed by NM, 10-Apr-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥)) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → (𝐹‘𝑅) = ((𝑃 ∨ 𝑄) ∧ ((𝐹‘𝑆) ∨ ((𝑅 ∨ 𝑆) ∧ 𝑊)))) | ||
Theorem | cdleme32sn1awN 39937* | Show that ⦋𝑅 / 𝑠⦌𝑁 is an atom not under 𝑊 when 𝑅 ≤ (𝑃 ∨ 𝑄). (Contributed by NM, 6-Mar-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐶 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑅 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝑍 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝑌)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (⦋𝑅 / 𝑠⦌𝑁 ∈ 𝐴 ∧ ¬ ⦋𝑅 / 𝑠⦌𝑁 ≤ 𝑊)) | ||
Theorem | cdleme41sn3a 39938* | Show that ⦋𝑅 / 𝑠⦌𝑁 is under 𝑃 ∨ 𝑄 when 𝑅 ≤ (𝑃 ∨ 𝑄). (Contributed by NM, 19-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐶 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑅 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝑍 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝑌)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ⦋𝑅 / 𝑠⦌𝑁 ≤ (𝑃 ∨ 𝑄)) | ||
Theorem | cdleme32sn2awN 39939* | Show that ⦋𝑅 / 𝑠⦌𝑁 is an atom not under 𝑊 when ¬ 𝑅 ≤ (𝑃 ∨ 𝑄). (Contributed by NM, 6-Mar-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐶 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (⦋𝑅 / 𝑠⦌𝑁 ∈ 𝐴 ∧ ¬ ⦋𝑅 / 𝑠⦌𝑁 ≤ 𝑊)) | ||
Theorem | cdleme32snaw 39940* | Show that ⦋𝑅 / 𝑠⦌𝑁 is an atom not under 𝑊. (Contributed by NM, 6-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐶 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → (⦋𝑅 / 𝑠⦌𝑁 ∈ 𝐴 ∧ ¬ ⦋𝑅 / 𝑠⦌𝑁 ≤ 𝑊)) | ||
Theorem | cdleme32snb 39941* | Show closure of ⦋𝑅 / 𝑠⦌𝑁. (Contributed by NM, 1-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐶 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → ⦋𝑅 / 𝑠⦌𝑁 ∈ 𝐵) | ||
Theorem | cdleme32fva 39942* | Part of proof of Lemma D in [Crawley] p. 113. Value of 𝐹 at an atom not under 𝑊. (Contributed by NM, 2-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐶 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ 𝑃 ≠ 𝑄) → ⦋𝑅 / 𝑥⦌𝑂 = ⦋𝑅 / 𝑠⦌𝑁) | ||
Theorem | cdleme32fva1 39943* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 2-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐶 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ 𝑃 ≠ 𝑄) → (𝐹‘𝑅) = ⦋𝑅 / 𝑠⦌𝑁) | ||
Theorem | cdleme32fvaw 39944* | Show that (𝐹‘𝑅) is an atom not under 𝑊 when 𝑅 is an atom not under 𝑊. (Contributed by NM, 18-Apr-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐶 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → ((𝐹‘𝑅) ∈ 𝐴 ∧ ¬ (𝐹‘𝑅) ≤ 𝑊)) | ||
Theorem | cdleme32fvcl 39945* | Part of proof of Lemma D in [Crawley] p. 113. Closure of the function 𝐹. (Contributed by NM, 10-Feb-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐶 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ 𝐵) | ||
Theorem | cdleme32a 39946* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 19-Feb-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐶 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ ((𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊) ∧ (𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝐹‘𝑋) = (𝑁 ∨ (𝑋 ∧ 𝑊))) | ||
Theorem | cdleme32b 39947* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 19-Feb-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐶 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ ((𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊) ∧ (𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → (𝐹‘𝑌) = (𝑁 ∨ (𝑌 ∧ 𝑊))) | ||
Theorem | cdleme32c 39948* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 19-Feb-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐶 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ ((𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊) ∧ (𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → (𝐹‘𝑋) ≤ (𝐹‘𝑌)) | ||
Theorem | cdleme32d 39949* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐶 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ 𝑋 ≤ 𝑌) → (𝐹‘𝑋) ≤ (𝐹‘𝑌)) | ||
Theorem | cdleme32e 39950* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐶 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ (𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ ((𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊) ∧ (𝑠 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → (𝐹‘𝑋) ≤ (𝐹‘𝑌)) | ||
Theorem | cdleme32f 39951* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐶 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ (𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ 𝑋 ≤ 𝑌) → (𝐹‘𝑋) ≤ (𝐹‘𝑌)) | ||
Theorem | cdleme32le 39952* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐶 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝐹‘𝑋) ≤ (𝐹‘𝑌)) | ||
Theorem | cdleme35a 39953 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 10-Mar-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐹 = ((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝐹 ∨ 𝑈) = (𝑅 ∨ 𝑈)) | ||
Theorem | cdleme35fnpq 39954 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 19-Mar-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐹 = ((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ¬ 𝐹 ≤ (𝑃 ∨ 𝑄)) | ||
Theorem | cdleme35b 39955 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 10-Mar-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐹 = ((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊)) ≤ (𝑄 ∨ (𝑅 ∨ 𝑈))) | ||
Theorem | cdleme35c 39956 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 10-Mar-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐹 = ((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝑄 ∨ 𝐹) = (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊))) | ||
Theorem | cdleme35d 39957 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 10-Mar-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐹 = ((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ((𝑄 ∨ 𝐹) ∧ 𝑊) = ((𝑃 ∨ 𝑅) ∧ 𝑊)) | ||
Theorem | cdleme35e 39958 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 10-Mar-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐹 = ((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝑃 ∨ ((𝑄 ∨ 𝐹) ∧ 𝑊)) = (𝑃 ∨ 𝑅)) | ||
Theorem | cdleme35f 39959 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 10-Mar-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐹 = ((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ((𝑅 ∨ 𝑈) ∧ (𝑃 ∨ 𝑅)) = 𝑅) | ||
Theorem | cdleme35g 39960 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 10-Mar-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐹 = ((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ((𝐹 ∨ 𝑈) ∧ (𝑃 ∨ ((𝑄 ∨ 𝐹) ∧ 𝑊))) = 𝑅) | ||
Theorem | cdleme35h 39961 | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one outside of 𝑃 ∨ 𝑄 line. TODO: FIX COMMENT. (Contributed by NM, 11-Mar-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐹 = ((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑆 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝐹 = 𝐺)) → 𝑅 = 𝑆) | ||
Theorem | cdleme35h2 39962 | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one outside of 𝑃 ∨ 𝑄 line. TODO: FIX COMMENT. (Contributed by NM, 18-Mar-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐹 = ((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑆 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≠ 𝑆)) → 𝐹 ≠ 𝐺) | ||
Theorem | cdleme35sn2aw 39963* | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one outside of 𝑃 ∨ 𝑄 line case; compare cdleme32sn2awN 39939. TODO: FIX COMMENT. (Contributed by NM, 18-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≠ 𝑆)) → ⦋𝑅 / 𝑠⦌𝑁 ≠ ⦋𝑆 / 𝑠⦌𝑁) | ||
Theorem | cdleme35sn3a 39964* | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 19-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ¬ ⦋𝑅 / 𝑠⦌𝑁 ≤ (𝑃 ∨ 𝑄)) | ||
Theorem | cdleme36a 39965 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 11-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ ((𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄))) → ¬ 𝑅 ≤ (𝑡 ∨ 𝐸)) | ||
Theorem | cdleme36m 39966 | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on 𝑃 ∨ 𝑄 line. TODO: FIX COMMENT. (Contributed by NM, 11-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝑉 = ((𝑡 ∨ 𝐸) ∧ 𝑊) & ⊢ 𝐹 = ((𝑅 ∨ 𝑉) ∧ (𝐸 ∨ ((𝑡 ∨ 𝑅) ∧ 𝑊))) & ⊢ 𝐶 = ((𝑆 ∨ 𝑉) ∧ (𝐸 ∨ ((𝑡 ∨ 𝑆) ∧ 𝑊))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ ((𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝐹 = 𝐶) ∧ ((𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)))) → 𝑅 = 𝑆) | ||
Theorem | cdleme37m 39967 | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on 𝑃 ∨ 𝑄 line. TODO: FIX COMMENT. (Contributed by NM, 13-Mar-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐷 = ((𝑢 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑢) ∧ 𝑊))) & ⊢ 𝑉 = ((𝑡 ∨ 𝐸) ∧ 𝑊) & ⊢ 𝑋 = ((𝑢 ∨ 𝐷) ∧ 𝑊) & ⊢ 𝐶 = ((𝑆 ∨ 𝑉) ∧ (𝐸 ∨ ((𝑡 ∨ 𝑆) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑆 ∨ 𝑋) ∧ (𝐷 ∨ ((𝑢 ∨ 𝑆) ∧ 𝑊))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ ((𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑆 ≤ (𝑃 ∨ 𝑄)) ∧ ((𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ ((𝑢 ∈ 𝐴 ∧ ¬ 𝑢 ≤ 𝑊) ∧ ¬ 𝑢 ≤ (𝑃 ∨ 𝑄)))) → 𝐶 = 𝐺) | ||
Theorem | cdleme38m 39968 | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on 𝑃 ∨ 𝑄 line. TODO: FIX COMMENT. (Contributed by NM, 13-Mar-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐷 = ((𝑢 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑢) ∧ 𝑊))) & ⊢ 𝑉 = ((𝑡 ∨ 𝐸) ∧ 𝑊) & ⊢ 𝑋 = ((𝑢 ∨ 𝐷) ∧ 𝑊) & ⊢ 𝐹 = ((𝑅 ∨ 𝑉) ∧ (𝐸 ∨ ((𝑡 ∨ 𝑅) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑆 ∨ 𝑋) ∧ (𝐷 ∨ ((𝑢 ∨ 𝑆) ∧ 𝑊))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ ((𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝐹 = 𝐺) ∧ ((𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ ((𝑢 ∈ 𝐴 ∧ ¬ 𝑢 ≤ 𝑊) ∧ ¬ 𝑢 ≤ (𝑃 ∨ 𝑄)))) → 𝑅 = 𝑆) | ||
Theorem | cdleme38n 39969 | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on 𝑃 ∨ 𝑄 line. TODO: FIX COMMENT. TODO shorter if proved directly from cdleme36m 39966 and cdleme37m 39967? (Contributed by NM, 14-Mar-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐷 = ((𝑢 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑢) ∧ 𝑊))) & ⊢ 𝑉 = ((𝑡 ∨ 𝐸) ∧ 𝑊) & ⊢ 𝑋 = ((𝑢 ∨ 𝐷) ∧ 𝑊) & ⊢ 𝐹 = ((𝑅 ∨ 𝑉) ∧ (𝐸 ∨ ((𝑡 ∨ 𝑅) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑆 ∨ 𝑋) ∧ (𝐷 ∨ ((𝑢 ∨ 𝑆) ∧ 𝑊))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ ((𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≠ 𝑆) ∧ ((𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ ((𝑢 ∈ 𝐴 ∧ ¬ 𝑢 ≤ 𝑊) ∧ ¬ 𝑢 ≤ (𝑃 ∨ 𝑄)))) → 𝐹 ≠ 𝐺) | ||
Theorem | cdleme39a 39970 | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on 𝑃 ∨ 𝑄 line. TODO: FIX COMMENT. 𝐸, 𝑌, 𝐺, 𝑍 serve as f(t), f(u), ft(𝑅), ft(𝑆). Put hypotheses of cdleme38n 39969 in convention of cdleme32sn1awN 39937. TODO see if this hypothesis conversion would be better if done earlier. (Contributed by NM, 15-Mar-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑅 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝑉 = ((𝑡 ∨ 𝐸) ∧ 𝑊) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊))) → 𝐺 = ((𝑅 ∨ 𝑉) ∧ (𝐸 ∨ ((𝑡 ∨ 𝑅) ∧ 𝑊)))) | ||
Theorem | cdleme39n 39971 | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on 𝑃 ∨ 𝑄 line. TODO: FIX COMMENT. 𝐸, 𝑌, 𝐺, 𝑍 serve as f(t), f(u), ft(𝑅), ft(𝑆). Put hypotheses of cdleme38n 39969 in convention of cdleme32sn1awN 39937. TODO see if this hypothesis conversion would be better if done earlier. (Contributed by NM, 15-Mar-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑅 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝑌 = ((𝑢 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑢) ∧ 𝑊))) & ⊢ 𝑍 = ((𝑃 ∨ 𝑄) ∧ (𝑌 ∨ ((𝑆 ∨ 𝑢) ∧ 𝑊))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ ((𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≠ 𝑆) ∧ ((𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ∧ ((𝑢 ∈ 𝐴 ∧ ¬ 𝑢 ≤ 𝑊) ∧ ¬ 𝑢 ≤ (𝑃 ∨ 𝑄)))) → 𝐺 ≠ 𝑍) | ||
Theorem | cdleme40m 39972* | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on 𝑃 ∨ 𝑄 line. TODO: FIX COMMENT Use proof idea from cdleme32sn1awN 39937. (Contributed by NM, 18-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑅 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐶 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝑌)) & ⊢ 𝑇 = ((𝑣 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑣) ∧ 𝑊))) & ⊢ 𝐹 = ((𝑃 ∨ 𝑄) ∧ (𝑇 ∨ ((𝑆 ∨ 𝑣) ∧ 𝑊))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ ((𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≠ 𝑆) ∧ (𝑣 ∈ 𝐴 ∧ ¬ 𝑣 ≤ 𝑊 ∧ ¬ 𝑣 ≤ (𝑃 ∨ 𝑄)))) → ⦋𝑅 / 𝑠⦌𝑁 ≠ 𝐹) | ||
Theorem | cdleme40n 39973* | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on 𝑃 ∨ 𝑄 line. TODO: FIX COMMENT. TODO get rid of '.<' class? (Contributed by NM, 18-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑅 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐶 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝑌)) & ⊢ 𝑇 = ((𝑣 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑣) ∧ 𝑊))) & ⊢ 𝐹 = ((𝑃 ∨ 𝑄) ∧ (𝑇 ∨ ((𝑆 ∨ 𝑣) ∧ 𝑊))) & ⊢ 𝑋 = ((𝑃 ∨ 𝑄) ∧ (𝑇 ∨ ((𝑢 ∨ 𝑣) ∧ 𝑊))) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑣 ∈ 𝐴 ((¬ 𝑣 ≤ 𝑊 ∧ ¬ 𝑣 ≤ (𝑃 ∨ 𝑄)) → 𝑧 = 𝑋)) & ⊢ 𝑉 = if(𝑢 ≤ (𝑃 ∨ 𝑄), 𝑂, < ) & ⊢ 𝑍 = (℩𝑧 ∈ 𝐵 ∀𝑣 ∈ 𝐴 ((¬ 𝑣 ≤ 𝑊 ∧ ¬ 𝑣 ≤ (𝑃 ∨ 𝑄)) → 𝑧 = 𝐹)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≠ 𝑆)) → ⦋𝑅 / 𝑠⦌𝑁 ≠ ⦋𝑆 / 𝑢⦌𝑉) | ||
Theorem | cdleme40v 39974* | 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.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) & ⊢ 𝐷 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝑌 = ((𝑢 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑢) ∧ 𝑊))) & ⊢ 𝑇 = ((𝑣 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑣) ∧ 𝑊))) & ⊢ 𝑋 = ((𝑃 ∨ 𝑄) ∧ (𝑇 ∨ ((𝑢 ∨ 𝑣) ∧ 𝑊))) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑣 ∈ 𝐴 ((¬ 𝑣 ≤ 𝑊 ∧ ¬ 𝑣 ≤ (𝑃 ∨ 𝑄)) → 𝑧 = 𝑋)) & ⊢ 𝑉 = if(𝑢 ≤ (𝑃 ∨ 𝑄), 𝑂, 𝑌) ⇒ ⊢ (𝑅 ∈ 𝐴 → ⦋𝑅 / 𝑠⦌𝑁 = ⦋𝑅 / 𝑢⦌𝑉) | ||
Theorem | cdleme40w 39975* | Part of proof of Lemma E in [Crawley] p. 113. Apply cdleme40v 39974 bound variable change to ⦋𝑆 / 𝑢⦌𝑉. TODO: FIX COMMENT. (Contributed by NM, 19-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) & ⊢ 𝐷 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝑌 = ((𝑢 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑢) ∧ 𝑊))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≠ 𝑆)) → ⦋𝑅 / 𝑠⦌𝑁 ≠ ⦋𝑆 / 𝑠⦌𝑁) | ||
Theorem | cdleme42a 39976 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 3-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑉 = ((𝑅 ∨ 𝑆) ∧ 𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → (𝑅 ∨ 𝑆) = (𝑅 ∨ 𝑉)) | ||
Theorem | cdleme42c 39977 | Part of proof of Lemma E in [Crawley] p. 113. Match ¬ 𝑥 ≤ 𝑊. (Contributed by NM, 6-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑉 = ((𝑅 ∨ 𝑆) ∧ 𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → ¬ (𝑅 ∨ 𝑉) ≤ 𝑊) | ||
Theorem | cdleme42d 39978 | Part of proof of Lemma E in [Crawley] p. 113. Match (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥. (Contributed by NM, 6-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑉 = ((𝑅 ∨ 𝑆) ∧ 𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → (𝑅 ∨ ((𝑅 ∨ 𝑉) ∧ 𝑊)) = (𝑅 ∨ 𝑉)) | ||
Theorem | cdleme41sn3aw 39979* | Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is different on and off the 𝑃 ∨ 𝑄 line. TODO: FIX COMMENT. (Contributed by NM, 18-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≠ 𝑆)) → ⦋𝑅 / 𝑠⦌𝑁 ≠ ⦋𝑆 / 𝑠⦌𝑁) | ||
Theorem | cdleme41sn4aw 39980* | Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is for on and off 𝑃 ∨ 𝑄 line. TODO: FIX COMMENT. (Contributed by NM, 19-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≠ 𝑆)) → ⦋𝑅 / 𝑠⦌𝑁 ≠ ⦋𝑆 / 𝑠⦌𝑁) | ||
Theorem | cdleme41snaw 39981* | Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is for combined cases; compare cdleme32snaw 39940. TODO: FIX COMMENT. (Contributed by NM, 18-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑅 ≠ 𝑆) → ⦋𝑅 / 𝑠⦌𝑁 ≠ ⦋𝑆 / 𝑠⦌𝑁) | ||
Theorem | cdleme41fva11 39982* | Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is one-to-one for r in W (r an atom not under w). TODO: FIX COMMENT. (Contributed by NM, 19-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑅 ≠ 𝑆) → (𝐹‘𝑅) ≠ (𝐹‘𝑆)) | ||
Theorem | cdleme42b 39983* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 6-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑅 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝐹‘𝑋) = (⦋𝑅 / 𝑠⦌𝑁 ∨ (𝑋 ∧ 𝑊))) | ||
Theorem | cdleme42e 39984* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) & ⊢ 𝑉 = ((𝑅 ∨ 𝑆) ∧ 𝑊) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → (𝐹‘(𝑅 ∨ 𝑉)) = (⦋𝑅 / 𝑠⦌𝑁 ∨ ((𝑅 ∨ 𝑉) ∧ 𝑊))) | ||
Theorem | cdleme42f 39985* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) & ⊢ 𝑉 = ((𝑅 ∨ 𝑆) ∧ 𝑊) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → (𝐹‘(𝑅 ∨ 𝑉)) = ((𝐹‘𝑅) ∨ 𝑉)) | ||
Theorem | cdleme42g 39986* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) & ⊢ 𝑉 = ((𝑅 ∨ 𝑆) ∧ 𝑊) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → (𝐹‘(𝑅 ∨ 𝑆)) = ((𝐹‘𝑅) ∨ 𝑉)) | ||
Theorem | cdleme42h 39987* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) & ⊢ 𝑉 = ((𝑅 ∨ 𝑆) ∧ 𝑊) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → (𝐹‘𝑆) ≤ ((𝐹‘𝑅) ∨ 𝑉)) | ||
Theorem | cdleme42i 39988* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) & ⊢ 𝑉 = ((𝑅 ∨ 𝑆) ∧ 𝑊) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → ((𝐹‘𝑅) ∨ (𝐹‘𝑆)) ≤ ((𝐹‘𝑅) ∨ 𝑉)) | ||
Theorem | cdleme42k 39989* | Part of proof of Lemma E in [Crawley] p. 113. Since F ' S =/= F'R when S =/= R (i.e. 1-1); then ( ( F ' R ) .\/ ( F ' S ) ) is 2-dim therefore = ( ( F ' R ) .\/ V ) by cdleme42i 39988 and ps-1 38982 TODO: FIX COMMENT. (Contributed by NM, 20-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) & ⊢ 𝑉 = ((𝑅 ∨ 𝑆) ∧ 𝑊) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑅 ≠ 𝑆) → ((𝐹‘𝑅) ∨ (𝐹‘𝑆)) = ((𝐹‘𝑅) ∨ 𝑉)) | ||
Theorem | cdleme42ke 39990* | Part of proof of Lemma E in [Crawley] p. 113. Remove 𝑅 ≠ 𝑆 condition. TODO: FIX COMMENT. (Contributed by NM, 2-Apr-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) & ⊢ 𝑉 = ((𝑅 ∨ 𝑆) ∧ 𝑊) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊))) → ((𝐹‘𝑅) ∨ (𝐹‘𝑆)) = ((𝐹‘𝑅) ∨ 𝑉)) | ||
Theorem | cdleme42keg 39991* | Part of proof of Lemma E in [Crawley] p. 113. Remove 𝑃 ≠ 𝑄 condition. TODO: FIX COMMENT. TODO: Use instead of cdleme42ke 39990 and even combine with it? (Contributed by NM, 22-Apr-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) & ⊢ 𝑉 = ((𝑅 ∨ 𝑆) ∧ 𝑊) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊))) → ((𝐹‘𝑅) ∨ (𝐹‘𝑆)) = ((𝐹‘𝑅) ∨ 𝑉)) | ||
Theorem | cdleme42mN 39992* | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT . f preserves join: f(r ∨ s) = f(r) ∨ s, p. 115 10th line from bottom. (Contributed by NM, 20-Mar-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊))) → (𝐹‘(𝑅 ∨ 𝑆)) = ((𝐹‘𝑅) ∨ (𝐹‘𝑆))) | ||
Theorem | cdleme42mgN 39993* | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT . f preserves join: f(r ∨ s) = f(r) ∨ s, p. 115 10th line from bottom. TODO: Use instead of cdleme42mN 39992? Combine with cdleme42mN 39992? (Contributed by NM, 20-Mar-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺)) & ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) & ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊))) → (𝐹‘(𝑅 ∨ 𝑆)) = ((𝐹‘𝑅) ∨ (𝐹‘𝑆))) | ||
Theorem | cdleme43aN 39994 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT p. 115 penultimate line: g(f(r)) = (p v q) ^ (g(s) v v1). (Contributed by NM, 20-Mar-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝑋 = ((𝑄 ∨ 𝑃) ∧ 𝑊) & ⊢ 𝐶 = ((𝑆 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊))) & ⊢ 𝑍 = ((𝑃 ∨ 𝑄) ∧ (𝐶 ∨ ((𝑅 ∨ 𝑆) ∧ 𝑊))) & ⊢ 𝐷 = ((𝑆 ∨ 𝑋) ∧ (𝑃 ∨ ((𝑄 ∨ 𝑆) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑄 ∨ 𝑃) ∧ (𝐷 ∨ ((𝑍 ∨ 𝑆) ∧ 𝑊))) & ⊢ 𝐸 = ((𝐷 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝐷) ∧ 𝑊))) & ⊢ 𝑉 = ((𝑍 ∨ 𝑆) ∧ 𝑊) & ⊢ 𝑌 = ((𝑅 ∨ 𝐷) ∧ 𝑊) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝐺 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ 𝑉))) | ||
Theorem | cdleme43bN 39995 | Lemma for Lemma E in [Crawley] p. 113. g(s) is an atom not under w. (Contributed by NM, 20-Mar-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝑋 = ((𝑄 ∨ 𝑃) ∧ 𝑊) & ⊢ 𝐶 = ((𝑆 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊))) & ⊢ 𝑍 = ((𝑃 ∨ 𝑄) ∧ (𝐶 ∨ ((𝑅 ∨ 𝑆) ∧ 𝑊))) & ⊢ 𝐷 = ((𝑆 ∨ 𝑋) ∧ (𝑃 ∨ ((𝑄 ∨ 𝑆) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑄 ∨ 𝑃) ∧ (𝐷 ∨ ((𝑍 ∨ 𝑆) ∧ 𝑊))) & ⊢ 𝐸 = ((𝐷 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝐷) ∧ 𝑊))) & ⊢ 𝑉 = ((𝑍 ∨ 𝑆) ∧ 𝑊) & ⊢ 𝑌 = ((𝑅 ∨ 𝐷) ∧ 𝑊) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)) → (𝐷 ∈ 𝐴 ∧ ¬ 𝐷 ≤ 𝑊)) | ||
Theorem | cdleme43cN 39996 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT p. 115 last line: r v g(s) = r v v2. (Contributed by NM, 20-Mar-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝑋 = ((𝑄 ∨ 𝑃) ∧ 𝑊) & ⊢ 𝐶 = ((𝑆 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊))) & ⊢ 𝑍 = ((𝑃 ∨ 𝑄) ∧ (𝐶 ∨ ((𝑅 ∨ 𝑆) ∧ 𝑊))) & ⊢ 𝐷 = ((𝑆 ∨ 𝑋) ∧ (𝑃 ∨ ((𝑄 ∨ 𝑆) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑄 ∨ 𝑃) ∧ (𝐷 ∨ ((𝑍 ∨ 𝑆) ∧ 𝑊))) & ⊢ 𝐸 = ((𝐷 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝐷) ∧ 𝑊))) & ⊢ 𝑉 = ((𝑍 ∨ 𝑆) ∧ 𝑊) & ⊢ 𝑌 = ((𝑅 ∨ 𝐷) ∧ 𝑊) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)) → (𝑅 ∨ 𝐷) = (𝑅 ∨ 𝑌)) | ||
Theorem | cdleme43dN 39997 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT p. 116 2nd line: f(r) v s = f(r) v f(g(s)). (Contributed by NM, 20-Mar-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝑋 = ((𝑄 ∨ 𝑃) ∧ 𝑊) & ⊢ 𝐶 = ((𝑆 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊))) & ⊢ 𝑍 = ((𝑃 ∨ 𝑄) ∧ (𝐶 ∨ ((𝑅 ∨ 𝑆) ∧ 𝑊))) & ⊢ 𝐷 = ((𝑆 ∨ 𝑋) ∧ (𝑃 ∨ ((𝑄 ∨ 𝑆) ∧ 𝑊))) & ⊢ 𝐺 = ((𝑄 ∨ 𝑃) ∧ (𝐷 ∨ ((𝑍 ∨ 𝑆) ∧ 𝑊))) & ⊢ 𝐸 = ((𝐷 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝐷) ∧ 𝑊))) & ⊢ 𝑉 = ((𝑍 ∨ 𝑆) ∧ 𝑊) & ⊢ 𝑌 = ((𝑅 ∨ 𝐷) ∧ 𝑊) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → (𝑍 ∨ 𝑆) = (𝑍 ∨ 𝐸)) | ||
Theorem | cdleme46f2g2 39998 | Conversion for 𝐺 to reuse 𝐹 theorems. TODO FIX COMMENT. TODO What other conversion theorems would be reused? e.g. cdlemeg46nlpq 40022? Find other hlatjcom 38872 uses giving 𝑄 ∨ 𝑃. (Contributed by NM, 1-Apr-2013.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)) → (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝑄 ≠ 𝑃 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑃))) | ||
Theorem | cdleme46f2g1 39999 | Conversion for 𝐺 to reuse 𝐹 theorems. TODO FIX COMMENT. (Contributed by NM, 1-Apr-2013.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝑄 ≠ 𝑃 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑄 ∨ 𝑃) ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑃)))) | ||
Theorem | cdleme17d2 40000* | Part of proof of Lemma E in [Crawley] p. 114, first part of 4th paragraph. 𝐹, 𝐺 represent f(s), fs(p) respectively. We show, in their notation, fs(p)=q. TODO: FIX COMMENT. (Contributed by NM, 5-Apr-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)) → (𝐹‘𝑃) = 𝑄) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |