P. 368 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36701-36800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cdleme50f 36701*	Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. TODO: can we use just 𝐹 Fn 𝐵 since range is computed in cdleme50rn 36704? (Contributed by NM, 9-Apr-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐹:𝐵⟶𝐵)
Theorem	cdleme50f1 36702*	Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐹:𝐵–1-1→𝐵)
Theorem	cdleme50rnlem 36703*	Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. TODO: can we get rid of 𝐺 stuff if we show 𝐺 = ◡𝐹 earlier? (Contributed by NM, 9-Apr-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    &   ⊢ 𝑉 = ((𝑄 ∨ 𝑃) ∧ 𝑊)    &   ⊢ 𝑁 = ((𝑣 ∨ 𝑉) ∧ (𝑃 ∨ ((𝑄 ∨ 𝑣) ∧ 𝑊)))    &   ⊢ 𝑂 = ((𝑄 ∨ 𝑃) ∧ (𝑁 ∨ ((𝑢 ∨ 𝑣) ∧ 𝑊)))    &   ⊢ 𝐺 = (𝑎 ∈ 𝐵 ↦ if((𝑄 ≠ 𝑃 ∧ ¬ 𝑎 ≤ 𝑊), (℩𝑐 ∈ 𝐵 ∀𝑢 ∈ 𝐴 ((¬ 𝑢 ≤ 𝑊 ∧ (𝑢 ∨ (𝑎 ∧ 𝑊)) = 𝑎) → 𝑐 = (if(𝑢 ≤ (𝑄 ∨ 𝑃), (℩𝑏 ∈ 𝐵 ∀𝑣 ∈ 𝐴 ((¬ 𝑣 ≤ 𝑊 ∧ ¬ 𝑣 ≤ (𝑄 ∨ 𝑃)) → 𝑏 = 𝑂)), ⦋𝑢 / 𝑣⦌𝑁) ∨ (𝑎 ∧ 𝑊)))), 𝑎))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ran 𝐹 = 𝐵)
Theorem	cdleme50rn 36704*	Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ran 𝐹 = 𝐵)
Theorem	cdleme50f1o 36705*	Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐹:𝐵–1-1-onto→𝐵)
Theorem	cdleme50laut 36706*	Part of proof of Lemma D in [Crawley] p. 113. 𝐹 is a lattice automorphism. TODO: fix comment. (Contributed by NM, 9-Apr-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    &   ⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐹 ∈ 𝐼)
Theorem	cdleme50ldil 36707*	Part of proof of Lemma D in [Crawley] p. 113. 𝐹 is a lattice dilation. TODO: fix comment. (Contributed by NM, 9-Apr-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    &   ⊢ 𝐶 = ((LDil‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐹 ∈ 𝐶)
Theorem	cdleme50trn1 36708*	Part of proof that 𝐹 is a translation. ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) case. TODO: fix comment. (Contributed by NM, 10-Apr-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ((𝑅 ∨ (𝐹‘𝑅)) ∧ 𝑊) = 𝑈)
Theorem	cdleme50trn2a 36709*	Part of proof that 𝐹 is a translation. 𝑅 ≤ (𝑃 ∨ 𝑄) case. TODO: fix comment. (Contributed by NM, 10-Apr-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → ((𝑅 ∨ (𝐹‘𝑅)) ∧ 𝑊) = 𝑈)
Theorem	cdleme50trn2 36710*	Part of proof that 𝐹 is a translation. Remove 𝑆 hypotheses no longer needed from cdleme50trn2a 36709. TODO: fix comment. (Contributed by NM, 10-Apr-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ((𝑅 ∨ (𝐹‘𝑅)) ∧ 𝑊) = 𝑈)
Theorem	cdleme50trn12 36711*	Part of proof that 𝐹 is a translation. Combine 𝑅 ≤ (𝑃 ∨ 𝑄) and ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) cases. TODO: fix comment. (Contributed by NM, 10-Apr-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → ((𝑅 ∨ (𝐹‘𝑅)) ∧ 𝑊) = 𝑈)
Theorem	cdleme50trn3 36712*	Part of proof that 𝐹 is a translation. 𝑃 = 𝑄 case. TODO: fix comment. (Contributed by NM, 10-Apr-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 = 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → ((𝑅 ∨ (𝐹‘𝑅)) ∧ 𝑊) = 𝑈)
Theorem	cdleme50trn123 36713*	Part of proof that 𝐹 is a translation. Combine all cases. TODO: fix comment. (Contributed by NM, 10-Apr-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → ((𝑅 ∨ (𝐹‘𝑅)) ∧ 𝑊) = 𝑈)
Theorem	cdleme51finvfvN 36714*	Part of proof of Lemma E in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 14-Apr-2013.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    &   ⊢ 𝑉 = ((𝑄 ∨ 𝑃) ∧ 𝑊)    &   ⊢ 𝑁 = ((𝑣 ∨ 𝑉) ∧ (𝑃 ∨ ((𝑄 ∨ 𝑣) ∧ 𝑊)))    &   ⊢ 𝑂 = ((𝑄 ∨ 𝑃) ∧ (𝑁 ∨ ((𝑢 ∨ 𝑣) ∧ 𝑊)))    &   ⊢ 𝐺 = (𝑎 ∈ 𝐵 ↦ if((𝑄 ≠ 𝑃 ∧ ¬ 𝑎 ≤ 𝑊), (℩𝑐 ∈ 𝐵 ∀𝑢 ∈ 𝐴 ((¬ 𝑢 ≤ 𝑊 ∧ (𝑢 ∨ (𝑎 ∧ 𝑊)) = 𝑎) → 𝑐 = (if(𝑢 ≤ (𝑄 ∨ 𝑃), (℩𝑏 ∈ 𝐵 ∀𝑣 ∈ 𝐴 ((¬ 𝑣 ≤ 𝑊 ∧ ¬ 𝑣 ≤ (𝑄 ∨ 𝑃)) → 𝑏 = 𝑂)), ⦋𝑢 / 𝑣⦌𝑁) ∨ (𝑎 ∧ 𝑊)))), 𝑎))    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑋 ∈ 𝐵) → (◡𝐹‘𝑋) = (𝐺‘𝑋))
Theorem	cdleme51finvN 36715*	Part of proof of Lemma E in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 14-Apr-2013.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    &   ⊢ 𝑉 = ((𝑄 ∨ 𝑃) ∧ 𝑊)    &   ⊢ 𝑁 = ((𝑣 ∨ 𝑉) ∧ (𝑃 ∨ ((𝑄 ∨ 𝑣) ∧ 𝑊)))    &   ⊢ 𝑂 = ((𝑄 ∨ 𝑃) ∧ (𝑁 ∨ ((𝑢 ∨ 𝑣) ∧ 𝑊)))    &   ⊢ 𝐺 = (𝑎 ∈ 𝐵 ↦ if((𝑄 ≠ 𝑃 ∧ ¬ 𝑎 ≤ 𝑊), (℩𝑐 ∈ 𝐵 ∀𝑢 ∈ 𝐴 ((¬ 𝑢 ≤ 𝑊 ∧ (𝑢 ∨ (𝑎 ∧ 𝑊)) = 𝑎) → 𝑐 = (if(𝑢 ≤ (𝑄 ∨ 𝑃), (℩𝑏 ∈ 𝐵 ∀𝑣 ∈ 𝐴 ((¬ 𝑣 ≤ 𝑊 ∧ ¬ 𝑣 ≤ (𝑄 ∨ 𝑃)) → 𝑏 = 𝑂)), ⦋𝑢 / 𝑣⦌𝑁) ∨ (𝑎 ∧ 𝑊)))), 𝑎))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ◡𝐹 = 𝐺)
Theorem	cdleme50ltrn 36716*	Part of proof of Lemma E in [Crawley] p. 113. 𝐹 is a lattice translation. TODO: fix comment. (Contributed by NM, 10-Apr-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐹 ∈ 𝑇)
Theorem	cdleme51finvtrN 36717*	Part of proof of Lemma E in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 14-Apr-2013.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ◡𝐹 ∈ 𝑇)
Theorem	cdleme50ex 36718*	Part of Lemma E in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 11-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ∃𝑓 ∈ 𝑇 (𝑓‘𝑃) = 𝑄)
Theorem	cdleme 36719*	Lemma E in [Crawley] p. 113. If p,q are atoms not under hyperplane w, then there is a unique translation f such that f(p) = q. (Contributed by NM, 11-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ∃!𝑓 ∈ 𝑇 (𝑓‘𝑃) = 𝑄)
Theorem	cdlemf1 36720*	Part of Lemma F in [Crawley] p. 116. TODO: should this or part of it become a stand-alone theorem? (Contributed by NM, 12-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ∃𝑞 ∈ 𝐴 (𝑃 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ (𝑃 ∨ 𝑞)))
Theorem	cdlemf2 36721*	Part of Lemma F in [Crawley] p. 116. (Contributed by NM, 12-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊)) → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ((¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊) ∧ 𝑈 = ((𝑝 ∨ 𝑞) ∧ 𝑊)))
Theorem	cdlemf 36722*	Lemma F in [Crawley] p. 116. If u is an atom under w, there exists a translation whose trace is u. (Contributed by NM, 12-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊)) → ∃𝑓 ∈ 𝑇 (𝑅‘𝑓) = 𝑈)
Theorem	cdlemfnid 36723*	cdlemf 36722 with additional constraint of non-identity. (Contributed by NM, 20-Jun-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊)) → ∃𝑓 ∈ 𝑇 ((𝑅‘𝑓) = 𝑈 ∧ 𝑓 ≠ ( I ↾ 𝐵)))
Theorem	cdlemftr3 36724*	Special case of cdlemf 36722 showing existence of non-identity translation with trace different from any 3 given lattice elements. (Contributed by NM, 24-Jul-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∃𝑓 ∈ 𝑇 (𝑓 ≠ ( I ↾ 𝐵) ∧ ((𝑅‘𝑓) ≠ 𝑋 ∧ (𝑅‘𝑓) ≠ 𝑌 ∧ (𝑅‘𝑓) ≠ 𝑍)))
Theorem	cdlemftr2 36725*	Special case of cdlemf 36722 showing existence of non-identity translation with trace different from any 2 given lattice elements. (Contributed by NM, 25-Jul-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∃𝑓 ∈ 𝑇 (𝑓 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑓) ≠ 𝑋 ∧ (𝑅‘𝑓) ≠ 𝑌))
Theorem	cdlemftr1 36726*	Part of proof of Lemma G of [Crawley] p. 116, sixth line of third paragraph on p. 117: there is "a translation h, different from the identity, such that tr h ≠ tr f." (Contributed by NM, 25-Jul-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∃𝑓 ∈ 𝑇 (𝑓 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑓) ≠ 𝑋))
Theorem	cdlemftr0 36727*	Special case of cdlemf 36722 showing existence of a non-identity translation. (Contributed by NM, 1-Aug-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∃𝑓 ∈ 𝑇 𝑓 ≠ ( I ↾ 𝐵))
Theorem	trlord 36728*	The ordering of two Hilbert lattice elements (under the fiducial hyperplane 𝑊) is determined by the translations whose traces are under them. (Contributed by NM, 3-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → (𝑋 ≤ 𝑌 ↔ ∀𝑓 ∈ 𝑇 ((𝑅‘𝑓) ≤ 𝑋 → (𝑅‘𝑓) ≤ 𝑌)))
Theorem	cdlemg1a 36729*	Shorter expression for 𝐺. TODO: fix comment. TODO: shorten using cdleme 36719 or vice-versa? Also, if not shortened with cdleme 36719, then it can be moved up to save repeating hypotheses. (Contributed by NM, 15-Apr-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐺 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐺 = (℩𝑓 ∈ 𝑇 (𝑓‘𝑃) = 𝑄))
Theorem	cdlemg1b2 36730*	This theorem can be used to shorten 𝐺 = hypothesis. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐺 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (℩𝑓 ∈ 𝑇 (𝑓‘𝑃) = 𝑄)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐹 = 𝐺)
Theorem	cdlemg1idlemN 36731*	Lemma for cdlemg1idN 36736. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐺 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (℩𝑓 ∈ 𝑇 (𝑓‘𝑃) = 𝑄)    ⇒   ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑋 ∈ 𝐵) ∧ 𝑃 = 𝑄) → (𝐹‘𝑋) = 𝑋)
Theorem	cdlemg1fvawlemN 36732*	Lemma for ltrniotafvawN 36737. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐺 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (℩𝑓 ∈ 𝑇 (𝑓‘𝑃) = 𝑄)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → ((𝐹‘𝑅) ∈ 𝐴 ∧ ¬ (𝐹‘𝑅) ≤ 𝑊))
Theorem	cdlemg1ltrnlem 36733*	Lemma for ltrniotacl 36738. (Contributed by NM, 18-Apr-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐺 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (℩𝑓 ∈ 𝑇 (𝑓‘𝑃) = 𝑄)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐹 ∈ 𝑇)
Theorem	cdlemg1finvtrlemN 36734*	Lemma for ltrniotacnvN 36739. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐺 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (℩𝑓 ∈ 𝑇 (𝑓‘𝑃) = 𝑄)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ◡𝐹 ∈ 𝑇)
Theorem	cdlemg1bOLDN 36735*	This theorem can be used to shorten 𝐹 = hypothesis that have the form of the conclusion. TODO: fix comment. (Contributed by NM, 16-Apr-2013.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐹 = (℩𝑓 ∈ 𝑇 (𝑓‘𝑃) = 𝑄)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥)))
Theorem	cdlemg1idN 36736*	Version of cdleme31id 36553 with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐹 = (℩𝑓 ∈ 𝑇 (𝑓‘𝑃) = 𝑄)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐾)    ⇒   ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑋 ∈ 𝐵) ∧ 𝑃 = 𝑄) → (𝐹‘𝑋) = 𝑋)
Theorem	ltrniotafvawN 36737*	Version of cdleme46fvaw 36660 with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (℩𝑓 ∈ 𝑇 (𝑓‘𝑃) = 𝑄)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → ((𝐹‘𝑅) ∈ 𝐴 ∧ ¬ (𝐹‘𝑅) ≤ 𝑊))
Theorem	ltrniotacl 36738*	Version of cdleme50ltrn 36716 with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 17-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (℩𝑓 ∈ 𝑇 (𝑓‘𝑃) = 𝑄)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐹 ∈ 𝑇)
Theorem	ltrniotacnvN 36739*	Version of cdleme51finvtrN 36717 with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (℩𝑓 ∈ 𝑇 (𝑓‘𝑃) = 𝑄)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ◡𝐹 ∈ 𝑇)
Theorem	ltrniotaval 36740*	Value of the unique translation specified by a value. (Contributed by NM, 21-Feb-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (℩𝑓 ∈ 𝑇 (𝑓‘𝑃) = 𝑄)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐹‘𝑃) = 𝑄)
Theorem	ltrniotacnvval 36741*	Converse value of the unique translation specified by a value. (Contributed by NM, 21-Feb-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (℩𝑓 ∈ 𝑇 (𝑓‘𝑃) = 𝑄)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (◡𝐹‘𝑄) = 𝑃)
Theorem	ltrniotaidvalN 36742*	Value of the unique translation specified by identity value. (Contributed by NM, 25-Aug-2014.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (℩𝑓 ∈ 𝑇 (𝑓‘𝑃) = 𝑃)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐹 = ( I ↾ 𝐵))
Theorem	ltrniotavalbN 36743*	Value of the unique translation specified by a value. (Contributed by NM, 10-Mar-2014.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝐹 ∈ 𝑇) → ((𝐹‘𝑃) = 𝑄 ↔ 𝐹 = (℩𝑓 ∈ 𝑇 (𝑓‘𝑃) = 𝑄)))
Theorem	cdlemeiota 36744*	A translation is uniquely determined by one of its values. (Contributed by NM, 18-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) → 𝐹 = (℩𝑓 ∈ 𝑇 (𝑓‘𝑃) = (𝐹‘𝑃)))
Theorem	cdlemg1ci2 36745*	Any function of the form of the function constructed for cdleme 36719 is a translation. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝐹 = (℩𝑓 ∈ 𝑇 (𝑓‘𝑃) = 𝑄)) → 𝐹 ∈ 𝑇)
Theorem	cdlemg1cN 36746*	Any translation belongs to the set of functions constructed for cdleme 36719. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑄) → (𝐹 ∈ 𝑇 ↔ 𝐹 = (℩𝑓 ∈ 𝑇 (𝑓‘𝑃) = 𝑄)))
Theorem	cdlemg1cex 36747*	Any translation is one of our 𝐹 s. TODO: fix comment, move to its own block maybe? Would this help for cdlemf 36722? (Contributed by NM, 17-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝐹 ∈ 𝑇 ↔ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝐹 = (℩𝑓 ∈ 𝑇 (𝑓‘𝑝) = 𝑞))))
Theorem	cdlemg2cN 36748*	Any translation belongs to the set of functions constructed for cdleme 36719. TODO: Fix comment. (Contributed by NM, 22-Apr-2013.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐺 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑄) → (𝐹 ∈ 𝑇 ↔ 𝐹 = 𝐺))
Theorem	cdlemg2dN 36749*	This theorem can be used to shorten 𝐺 = hypothesis. TODO: Fix comment. (Contributed by NM, 21-Apr-2013.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐺 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) = 𝑄)) → 𝐹 = 𝐺)
Theorem	cdlemg2cex 36750*	Any translation is one of our 𝐹 s. TODO: fix comment, move to its own block maybe? Would this help for cdlemf 36722? (Contributed by NM, 22-Apr-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((𝑝 ∨ 𝑞) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑞 ∨ ((𝑝 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑝 ∨ 𝑞) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐺 = (𝑥 ∈ 𝐵 ↦ if((𝑝 ≠ 𝑞 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑝 ∨ 𝑞), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑝 ∨ 𝑞)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝐹 ∈ 𝑇 ↔ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝐹 = 𝐺)))
Theorem	cdlemg2ce 36751*	Utility theorem to eliminate p,q when converting theorems with explicit f. TODO: fix comment. (Contributed by NM, 22-Apr-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((𝑝 ∨ 𝑞) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑞 ∨ ((𝑝 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑝 ∨ 𝑞) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐺 = (𝑥 ∈ 𝐵 ↦ if((𝑝 ≠ 𝑞 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑝 ∨ 𝑞), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑝 ∨ 𝑞)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    &   ⊢ (𝐹 = 𝐺 → (𝜓 ↔ 𝜒))    &   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊)) ∧ 𝜑) → 𝜒)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝜑) → 𝜓)
Theorem	cdlemg2jlemOLDN 36752*	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: Combine with cdlemg2jOLDN 36757? (Contributed by NM, 22-Apr-2013.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((𝑝 ∨ 𝑞) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑞 ∨ ((𝑝 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑝 ∨ 𝑞) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐺 = (𝑥 ∈ 𝐵 ↦ if((𝑝 ≠ 𝑞 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑝 ∨ 𝑞), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑝 ∨ 𝑞)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝐹 ∈ 𝑇) → (𝐹‘(𝑃 ∨ 𝑄)) = ((𝐹‘𝑃) ∨ (𝐹‘𝑄)))
Theorem	cdlemg2fvlem 36753*	Lemma for cdlemg2fv 36758. (Contributed by NM, 23-Apr-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((𝑝 ∨ 𝑞) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑞 ∨ ((𝑝 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑝 ∨ 𝑞) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐺 = (𝑥 ∈ 𝐵 ↦ if((𝑝 ≠ 𝑞 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑝 ∨ 𝑞), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑝 ∨ 𝑞)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝐹‘𝑋) = ((𝐹‘𝑃) ∨ (𝑋 ∧ 𝑊)))
Theorem	cdlemg2klem 36754*	cdleme42keg 36645 with simpler hypotheses. TODO: FIX COMMENT. (Contributed by NM, 22-Apr-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((𝑝 ∨ 𝑞) ∧ 𝑊)    &   ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑞 ∨ ((𝑝 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐸 = ((𝑝 ∨ 𝑞) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))    &   ⊢ 𝐺 = (𝑥 ∈ 𝐵 ↦ if((𝑝 ≠ 𝑞 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑝 ∨ 𝑞), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑝 ∨ 𝑞)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝐹 ∈ 𝑇) → ((𝐹‘𝑃) ∨ (𝐹‘𝑄)) = ((𝐹‘𝑃) ∨ 𝑉))
Theorem	cdlemg2idN 36755	Version of cdleme31id 36553 with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 21-Apr-2013.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐾)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐹 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹‘𝑃) = 𝑄 ∧ 𝑋 ∈ 𝐵) ∧ 𝑃 = 𝑄) → (𝐹‘𝑋) = 𝑋)
Theorem	cdlemg3a 36756	Part of proof of Lemma G in [Crawley] p. 116, line 19. Show p ∨ q = p ∨ u. TODO: reformat cdleme0cp 36373 to match this, then replace with cdleme0cp 36373. (Contributed by NM, 19-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑈))
Theorem	cdlemg2jOLDN 36757	TODO: Replace this with ltrnj 36291. (Contributed by NM, 22-Apr-2013.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝐹 ∈ 𝑇) → (𝐹‘(𝑃 ∨ 𝑄)) = ((𝐹‘𝑃) ∨ (𝐹‘𝑄)))
Theorem	cdlemg2fv 36758	Value of a translation in terms of an associated atom. cdleme48fvg 36659 with simpler hypotheses. TODO: Use ltrnj 36291 to vastly simplify. (Contributed by NM, 23-Apr-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐵 = (Base‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝐹‘𝑋) = ((𝐹‘𝑃) ∨ (𝑋 ∧ 𝑊)))
Theorem	cdlemg2fv2 36759	Value of a translation in terms of an associated atom. TODO: FIX COMMENT. TODO: Is this useful elsewhere e.g. around cdlemeg46fjv 36682 that use more complex proofs? TODO: Use ltrnj 36291 to vastly simplify. (Contributed by NM, 23-Apr-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝐹 ∈ 𝑇) → (𝐹‘(𝑅 ∨ 𝑈)) = ((𝐹‘𝑅) ∨ 𝑈))
Theorem	cdlemg2k 36760	cdleme42keg 36645 with simpler hypotheses. TODO: FIX COMMENT. TODO: derive from cdlemg3a 36756, cdlemg2fv2 36759, cdlemg2jOLDN 36757, ltrnel 36298? (Contributed by NM, 22-Apr-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝐹 ∈ 𝑇) → ((𝐹‘𝑃) ∨ (𝐹‘𝑄)) = ((𝐹‘𝑃) ∨ 𝑈))
Theorem	cdlemg2kq 36761	cdlemg2k 36760 with 𝑃 and 𝑄 swapped. TODO: FIX COMMENT. (Contributed by NM, 15-May-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝐹 ∈ 𝑇) → ((𝐹‘𝑃) ∨ (𝐹‘𝑄)) = ((𝐹‘𝑄) ∨ 𝑈))
Theorem	cdlemg2l 36762	TODO: FIX COMMENT. (Contributed by NM, 23-Apr-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) = ((𝐹‘(𝐺‘𝑃)) ∨ 𝑈))
Theorem	cdlemg2m 36763	TODO: FIX COMMENT. (Contributed by NM, 25-Apr-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝐹 ∈ 𝑇) → (((𝐹‘𝑃) ∨ (𝐹‘𝑄)) ∧ 𝑊) = 𝑈)
Theorem	cdlemg5 36764*	TODO: Is there a simpler more direct proof, that could be placed earlier e.g. near lhpexle 36164? TODO: The ∨ hypothesis is unused. FIX COMMENT. (Contributed by NM, 26-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ∃𝑞 ∈ 𝐴 (𝑃 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊))
Theorem	cdlemb3 36765*	Given two atoms not under the fiducial co-atom 𝑊, there is a third. Lemma B in [Crawley] p. 112. TODO: Is there a simpler more direct proof, that could be placed earlier e.g. near lhpexle 36164? Then replace cdlemb2 36200 with it. This is a more general version of cdlemb2 36200 without 𝑃 ≠ 𝑄 condition. (Contributed by NM, 27-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ (𝑃 ∨ 𝑄)))
Theorem	cdlemg7fvbwN 36766	Properties of a translation of an element not under 𝑊. TODO: Fix comment. Can this be simplified? Perhaps derived from cdleme48bw 36661? Done with a *ltrn* theorem? (Contributed by NM, 28-Apr-2013.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) → ((𝐹‘𝑋) ∈ 𝐵 ∧ ¬ (𝐹‘𝑋) ≤ 𝑊))
Theorem	cdlemg4a 36767	TODO: FIX COMMENT If fg(p) = p, then tr f = tr g. (Contributed by NM, 23-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹‘(𝐺‘𝑃)) = 𝑃) → (𝑅‘𝐹) = (𝑅‘𝐺))
Theorem	cdlemg4b1 36768	TODO: FIX COMMENT. (Contributed by NM, 24-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝑉 = (𝑅‘𝐺)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 ∈ 𝑇) → (𝑃 ∨ 𝑉) = (𝑃 ∨ (𝐺‘𝑃)))
Theorem	cdlemg4b2 36769	TODO: FIX COMMENT. (Contributed by NM, 24-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝑉 = (𝑅‘𝐺)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 ∈ 𝑇) → ((𝐺‘𝑃) ∨ 𝑉) = (𝑃 ∨ (𝐺‘𝑃)))
Theorem	cdlemg4b12 36770	TODO: FIX COMMENT. (Contributed by NM, 24-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝑉 = (𝑅‘𝐺)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 ∈ 𝑇) → ((𝐺‘𝑃) ∨ 𝑉) = (𝑃 ∨ 𝑉))
Theorem	cdlemg4c 36771	TODO: FIX COMMENT. (Contributed by NM, 24-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝑉 = (𝑅‘𝐺)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐺 ∈ 𝑇) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑉)) → ¬ (𝐺‘𝑄) ≤ (𝑃 ∨ 𝑉))
Theorem	cdlemg4d 36772	TODO: FIX COMMENT. (Contributed by NM, 25-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝑉 = (𝑅‘𝐺)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ (𝐺 ∈ 𝑇 ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑉) ∧ (𝐹‘(𝐺‘𝑃)) = 𝑃)) → ¬ (𝐺‘𝑄) ≤ ((𝐺‘𝑃) ∨ (𝐹‘(𝐺‘𝑃))))
Theorem	cdlemg4e 36773	TODO: FIX COMMENT. (Contributed by NM, 25-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝑉 = (𝑅‘𝐺)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ (𝐺 ∈ 𝑇 ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑉) ∧ (𝐹‘(𝐺‘𝑃)) = 𝑃)) → (𝐹‘(𝐺‘𝑄)) = (((𝐺‘𝑄) ∨ (𝑅‘𝐹)) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (((𝐺‘𝑃) ∨ (𝐺‘𝑄)) ∧ 𝑊))))
Theorem	cdlemg4f 36774	TODO: FIX COMMENT. (Contributed by NM, 25-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝑉 = (𝑅‘𝐺)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ (𝐺 ∈ 𝑇 ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑉) ∧ (𝐹‘(𝐺‘𝑃)) = 𝑃)) → (𝐹‘(𝐺‘𝑄)) = ((𝑄 ∨ 𝑉) ∧ (𝑃 ∨ ((𝑃 ∨ 𝑄) ∧ 𝑊))))
Theorem	cdlemg4g 36775	TODO: FIX COMMENT. (Contributed by NM, 25-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝑉 = (𝑅‘𝐺)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ (𝐺 ∈ 𝑇 ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑉) ∧ (𝐹‘(𝐺‘𝑃)) = 𝑃)) → (𝐹‘(𝐺‘𝑄)) = ((𝑄 ∨ 𝑉) ∧ (𝑃 ∨ 𝑄)))
Theorem	cdlemg4 36776	TODO: FIX COMMENT. (Contributed by NM, 25-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝑉 = (𝑅‘𝐺)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ (𝐺 ∈ 𝑇 ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑉) ∧ (𝐹‘(𝐺‘𝑃)) = 𝑃)) → (𝐹‘(𝐺‘𝑄)) = 𝑄)
Theorem	cdlemg6a 36777*	TODO: FIX COMMENT. TODO: replace with cdlemg4 36776. (Contributed by NM, 27-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝑉 = (𝑅‘𝐺)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ (𝐺 ∈ 𝑇 ∧ ¬ 𝑟 ≤ (𝑃 ∨ 𝑉) ∧ (𝐹‘(𝐺‘𝑃)) = 𝑃)) → (𝐹‘(𝐺‘𝑟)) = 𝑟)
Theorem	cdlemg6b 36778*	TODO: FIX COMMENT. TODO: replace with cdlemg4 36776. (Contributed by NM, 27-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝑉 = (𝑅‘𝐺)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ (𝐺 ∈ 𝑇 ∧ ¬ 𝑄 ≤ (𝑟 ∨ 𝑉) ∧ (𝐹‘(𝐺‘𝑟)) = 𝑟)) → (𝐹‘(𝐺‘𝑄)) = 𝑄)
Theorem	cdlemg6c 36779*	TODO: FIX COMMENT. (Contributed by NM, 27-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝑉 = (𝑅‘𝐺)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ (𝐺 ∈ 𝑇 ∧ 𝑄 ≤ (𝑃 ∨ 𝑉) ∧ (𝐹‘(𝐺‘𝑃)) = 𝑃)) → (((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ ¬ 𝑟 ≤ (𝑃 ∨ 𝑉)) → (𝐹‘(𝐺‘𝑄)) = 𝑄))
Theorem	cdlemg6d 36780*	TODO: FIX COMMENT. (Contributed by NM, 27-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝑉 = (𝑅‘𝐺)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ (𝐺 ∈ 𝑇 ∧ 𝑄 ≤ (𝑃 ∨ 𝑉) ∧ (𝐹‘(𝐺‘𝑃)) = 𝑃)) → (((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ ¬ 𝑟 ≤ (𝑃 ∨ (𝐺‘𝑃))) → (𝐹‘(𝐺‘𝑄)) = 𝑄))
Theorem	cdlemg6e 36781	TODO: FIX COMMENT. (Contributed by NM, 27-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝑉 = (𝑅‘𝐺)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ (𝐺 ∈ 𝑇 ∧ 𝑄 ≤ (𝑃 ∨ 𝑉) ∧ (𝐹‘(𝐺‘𝑃)) = 𝑃)) → (𝐹‘(𝐺‘𝑄)) = 𝑄)
Theorem	cdlemg6 36782	TODO: FIX COMMENT. (Contributed by NM, 27-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ (𝐹‘(𝐺‘𝑃)) = 𝑃)) → (𝐹‘(𝐺‘𝑄)) = 𝑄)
Theorem	cdlemg7fvN 36783	Value of a translation composition in terms of an associated atom. (Contributed by NM, 28-Apr-2013.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ (𝑃 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝐹‘(𝐺‘𝑋)) = ((𝐹‘(𝐺‘𝑃)) ∨ (𝑋 ∧ 𝑊)))
Theorem	cdlemg7aN 36784	TODO: FIX COMMENT. (Contributed by NM, 28-Apr-2013.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ (𝐹‘(𝐺‘𝑃)) = 𝑃)) → (𝐹‘(𝐺‘𝑋)) = 𝑋)
Theorem	cdlemg7N 36785	TODO: FIX COMMENT. (Contributed by NM, 28-Apr-2013.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑋 ∈ 𝐵) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ (𝐹‘(𝐺‘𝑃)) = 𝑃)) → (𝐹‘(𝐺‘𝑋)) = 𝑋)
Theorem	cdlemg8a 36786	TODO: FIX COMMENT. (Contributed by NM, 29-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ (𝐹‘(𝐺‘𝑃)) = 𝑃)) → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ 𝑊) = ((𝑄 ∨ (𝐹‘(𝐺‘𝑄))) ∧ 𝑊))
Theorem	cdlemg8b 36787	TODO: FIX COMMENT. (Contributed by NM, 29-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ (𝐺 ∈ 𝑇 ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) = (𝑃 ∨ 𝑄) ∧ (𝐹‘(𝐺‘𝑃)) ≠ 𝑃)) → (𝑃 ∨ (𝐹‘(𝐺‘𝑃))) = (𝑃 ∨ 𝑄))
Theorem	cdlemg8c 36788	TODO: FIX COMMENT. (Contributed by NM, 29-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ (𝐺 ∈ 𝑇 ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) = (𝑃 ∨ 𝑄) ∧ (𝐹‘(𝐺‘𝑃)) ≠ 𝑃)) → (𝑄 ∨ (𝐹‘(𝐺‘𝑄))) = (𝑃 ∨ 𝑄))
Theorem	cdlemg8d 36789	TODO: FIX COMMENT. (Contributed by NM, 29-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ (𝐺 ∈ 𝑇 ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) = (𝑃 ∨ 𝑄) ∧ (𝐹‘(𝐺‘𝑃)) ≠ 𝑃)) → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ 𝑊) = ((𝑄 ∨ (𝐹‘(𝐺‘𝑄))) ∧ 𝑊))
Theorem	cdlemg8 36790	TODO: FIX COMMENT. (Contributed by NM, 29-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ (𝐺 ∈ 𝑇 ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) = (𝑃 ∨ 𝑄))) → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ 𝑊) = ((𝑄 ∨ (𝐹‘(𝐺‘𝑄))) ∧ 𝑊))
Theorem	cdlemg9a 36791	TODO: FIX COMMENT. (Contributed by NM, 1-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄))) → ((𝑃 ∨ 𝑈) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ 𝑈)) ≤ ((𝐺‘𝑃) ∨ 𝑈))
Theorem	cdlemg9b 36792	The triples ⟨𝑃, (𝐹‘(𝐺‘𝑃)), (𝐹‘𝑃)⟩ and ⟨𝑄, (𝐹‘(𝐺‘𝑄)), (𝐹‘𝑄)⟩ are centrally perspective. TODO: FIX COMMENT. (Contributed by NM, 1-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄))) → ((𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄)))) ≤ ((𝐺‘𝑃) ∨ (𝐺‘𝑄)))
Theorem	cdlemg9 36793	The triples ⟨𝑃, (𝐹‘(𝐺‘𝑃)), (𝐹‘𝑃)⟩ and ⟨𝑄, (𝐹‘(𝐺‘𝑄)), (𝐹‘𝑄)⟩ are axially perspective by dalaw 36045. Part of Lemma G of [Crawley] p. 116, last 2 lines. TODO: FIX COMMENT. (Contributed by NM, 1-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄))) → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ (𝑄 ∨ (𝐹‘(𝐺‘𝑄)))) ≤ ((((𝐹‘(𝐺‘𝑃)) ∨ (𝐺‘𝑃)) ∧ ((𝐹‘(𝐺‘𝑄)) ∨ (𝐺‘𝑄))) ∨ (((𝐺‘𝑃) ∨ 𝑃) ∧ ((𝐺‘𝑄) ∨ 𝑄))))
Theorem	cdlemg10b 36794	TODO: FIX COMMENT. TODO: Can this be moved up as a stand-alone theorem in ltrn* area? (Contributed by NM, 4-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝐹 ∈ 𝑇) → (((𝐹‘𝑃) ∨ (𝐹‘𝑄)) ∧ 𝑊) = ((𝑃 ∨ 𝑄) ∧ 𝑊))
Theorem	cdlemg10bALTN 36795	TODO: FIX COMMENT. TODO: Can this be moved up as a stand-alone theorem in ltrn* area? TODO: Compare this proof to cdlemg2m 36763 and pick best, if moved to ltrn* area. (Contributed by NM, 4-May-2013.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐹 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (((𝐹‘𝑃) ∨ (𝐹‘𝑄)) ∧ 𝑊) = ((𝑃 ∨ 𝑄) ∧ 𝑊))
Theorem	cdlemg11a 36796	TODO: FIX COMMENT. (Contributed by NM, 4-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄))) → (𝐹‘(𝐺‘𝑃)) ≠ 𝑃)
Theorem	cdlemg11aq 36797	TODO: FIX COMMENT. TODO: can proof using this be restructured to use cdlemg11a 36796? (Contributed by NM, 4-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄))) → (𝐹‘(𝐺‘𝑄)) ≠ 𝑄)
Theorem	cdlemg10c 36798	TODO: FIX COMMENT. TODO: Can this be moved up as a stand-alone theorem in trl* area? (Contributed by NM, 4-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → ((𝑅‘𝐹) ≤ ((𝐺‘𝑃) ∨ (𝐺‘𝑄)) ↔ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄)))
Theorem	cdlemg10a 36799	TODO: FIX COMMENT. (Contributed by NM, 3-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ (𝑄 ∨ (𝐹‘(𝐺‘𝑄)))) ≤ ((𝑅‘𝐹) ∨ (𝑅‘𝐺)))
Theorem	cdlemg10 36800	TODO: FIX COMMENT. (Contributed by NM, 4-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ (𝑄 ∨ (𝐹‘(𝐺‘𝑄)))) ≤ 𝑊)