P. 381 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38001-38100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	4atexlempsb 38001	Lemma for 4atexlem7 38016. (Contributed by NM, 23-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (𝜑 → (𝑃 ∨ 𝑆) ∈ (Base‘𝐾))
Theorem	4atexlemqtb 38002	Lemma for 4atexlem7 38016. (Contributed by NM, 24-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (𝜑 → (𝑄 ∨ 𝑇) ∈ (Base‘𝐾))
Theorem	4atexlempns 38003	Lemma for 4atexlem7 38016. (Contributed by NM, 23-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (𝜑 → 𝑃 ≠ 𝑆)
Theorem	4atexlemswapqr 38004	Lemma for 4atexlem7 38016. Swap 𝑄 and 𝑅, so that theorems involving 𝐶 can be reused for 𝐷. Note that 𝑈 must be expanded because it involves 𝑄. (Contributed by NM, 25-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    ⇒   ⊢ (𝜑 → (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ∧ (𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑄)) ∧ (𝑇 ∈ 𝐴 ∧ (((𝑃 ∨ 𝑅) ∧ 𝑊) ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑅 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑅))))
Theorem	4atexlemu 38005	Lemma for 4atexlem7 38016. (Contributed by NM, 23-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    ⇒   ⊢ (𝜑 → 𝑈 ∈ 𝐴)
Theorem	4atexlemv 38006	Lemma for 4atexlem7 38016. (Contributed by NM, 23-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊)    ⇒   ⊢ (𝜑 → 𝑉 ∈ 𝐴)
Theorem	4atexlemunv 38007	Lemma for 4atexlem7 38016. (Contributed by NM, 21-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊)    ⇒   ⊢ (𝜑 → 𝑈 ≠ 𝑉)
Theorem	4atexlemtlw 38008	Lemma for 4atexlem7 38016. (Contributed by NM, 24-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊)    ⇒   ⊢ (𝜑 → 𝑇 ≤ 𝑊)
Theorem	4atexlemntlpq 38009	Lemma for 4atexlem7 38016. (Contributed by NM, 24-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊)    ⇒   ⊢ (𝜑 → ¬ 𝑇 ≤ (𝑃 ∨ 𝑄))
Theorem	4atexlemc 38010	Lemma for 4atexlem7 38016. (Contributed by NM, 24-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊)    &   ⊢ 𝐶 = ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))    ⇒   ⊢ (𝜑 → 𝐶 ∈ 𝐴)
Theorem	4atexlemnclw 38011	Lemma for 4atexlem7 38016. (Contributed by NM, 24-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊)    &   ⊢ 𝐶 = ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))    ⇒   ⊢ (𝜑 → ¬ 𝐶 ≤ 𝑊)
Theorem	4atexlemex2 38012*	Lemma for 4atexlem7 38016. Show that when 𝐶 ≠ 𝑆, 𝐶 satisfies the existence condition of the consequent. (Contributed by NM, 25-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊)    &   ⊢ 𝐶 = ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))    ⇒   ⊢ ((𝜑 ∧ 𝐶 ≠ 𝑆) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑃 ∨ 𝑧) = (𝑆 ∨ 𝑧)))
Theorem	4atexlemcnd 38013	Lemma for 4atexlem7 38016. (Contributed by NM, 24-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊)    &   ⊢ 𝐶 = ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))    &   ⊢ 𝐷 = ((𝑅 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))    ⇒   ⊢ (𝜑 → 𝐶 ≠ 𝐷)
Theorem	4atexlemex4 38014*	Lemma for 4atexlem7 38016. Show that when 𝐶 = 𝑆, 𝐷 satisfies the existence condition of the consequent. (Contributed by NM, 26-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊)    &   ⊢ 𝐶 = ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))    &   ⊢ 𝐷 = ((𝑅 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))    ⇒   ⊢ ((𝜑 ∧ 𝐶 = 𝑆) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑃 ∨ 𝑧) = (𝑆 ∨ 𝑧)))
Theorem	4atexlemex6 38015*	Lemma for 4atexlem7 38016. (Contributed by NM, 25-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ ((𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅) ∧ 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑃 ∨ 𝑧) = (𝑆 ∨ 𝑧)))
Theorem	4atexlem7 38016*	Whenever there are at least 4 atoms under 𝑃 ∨ 𝑄 (specifically, 𝑃, 𝑄, 𝑟, and (𝑃 ∨ 𝑄) ∧ 𝑊), there are also at least 4 atoms under 𝑃 ∨ 𝑆. This proves the statement in Lemma E of [Crawley] p. 114, last line, "...p ∨ q/0 and hence p ∨ s/0 contains at least four atoms..." Note that by cvlsupr2 37284, our (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟) is a shorter way to express 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ (𝑃 ∨ 𝑄). With a longer proof, the condition ¬ 𝑆 ≤ (𝑃 ∨ 𝑄) could be eliminated (see 4atex 38017), although for some purposes this more restricted lemma may be adequate. (Contributed by NM, 25-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑃 ∨ 𝑧) = (𝑆 ∨ 𝑧)))
Theorem	4atex 38017*	Whenever there are at least 4 atoms under 𝑃 ∨ 𝑄 (specifically, 𝑃, 𝑄, 𝑟, and (𝑃 ∨ 𝑄) ∧ 𝑊), there are also at least 4 atoms under 𝑃 ∨ 𝑆. This proves the statement in Lemma E of [Crawley] p. 114, last line, "...p ∨ q/0 and hence p ∨ s/0 contains at least four atoms..." Note that by cvlsupr2 37284, our (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟) is a shorter way to express 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ (𝑃 ∨ 𝑄). (Contributed by NM, 27-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑃 ∨ 𝑧) = (𝑆 ∨ 𝑧)))
Theorem	4atex2 38018*	More general version of 4atex 38017 for a line 𝑆 ∨ 𝑇 not necessarily connected to 𝑃 ∨ 𝑄. (Contributed by NM, 27-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑇 ∈ 𝐴 ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑆 ∨ 𝑧) = (𝑇 ∨ 𝑧)))
Theorem	4atex2-0aOLDN 38019*	Same as 4atex2 38018 except that 𝑆 is zero. (Contributed by NM, 27-May-2013.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 = (0.‘𝐾)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑆 ∨ 𝑧) = (𝑇 ∨ 𝑧)))
Theorem	4atex2-0bOLDN 38020*	Same as 4atex2 38018 except that 𝑇 is zero. (Contributed by NM, 27-May-2013.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑇 = (0.‘𝐾) ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑆 ∨ 𝑧) = (𝑇 ∨ 𝑧)))
Theorem	4atex2-0cOLDN 38021*	Same as 4atex2 38018 except that 𝑆 and 𝑇 are zero. TODO: do we need this one or 4atex2-0aOLDN 38019 or 4atex2-0bOLDN 38020? (Contributed by NM, 27-May-2013.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 = (0.‘𝐾)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑇 = (0.‘𝐾) ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑆 ∨ 𝑧) = (𝑇 ∨ 𝑧)))
Theorem	4atex3 38022*	More general version of 4atex 38017 for a line 𝑆 ∨ 𝑇 not necessarily connected to 𝑃 ∨ 𝑄. (Contributed by NM, 29-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇) ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑧 ≠ 𝑆 ∧ 𝑧 ≠ 𝑇 ∧ 𝑧 ≤ (𝑆 ∨ 𝑇))))
Theorem	lautset 38023*	The set of lattice automorphisms. (Contributed by NM, 11-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐴 → 𝐼 = {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑓‘𝑥) ≤ (𝑓‘𝑦)))})
Theorem	islaut 38024*	The predicate "is a lattice automorphism". (Contributed by NM, 11-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐴 → (𝐹 ∈ 𝐼 ↔ (𝐹:𝐵–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝐹‘𝑥) ≤ (𝐹‘𝑦)))))
Theorem	lautle 38025	Less-than or equal property of a lattice automorphism. (Contributed by NM, 19-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ≤ 𝑌 ↔ (𝐹‘𝑋) ≤ (𝐹‘𝑌)))
Theorem	laut1o 38026	A lattice automorphism is one-to-one and onto. (Contributed by NM, 19-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝐹 ∈ 𝐼) → 𝐹:𝐵–1-1-onto→𝐵)
Theorem	laut11 38027	One-to-one property of a lattice automorphism. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝐹‘𝑋) = (𝐹‘𝑌) ↔ 𝑋 = 𝑌))
Theorem	lautcl 38028	A lattice automorphism value belongs to the base set. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼) ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ 𝐵)
Theorem	lautcnvclN 38029	Reverse closure of a lattice automorphism. (Contributed by NM, 25-May-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼) ∧ 𝑋 ∈ 𝐵) → (◡𝐹‘𝑋) ∈ 𝐵)
Theorem	lautcnvle 38030	Less-than or equal property of lattice automorphism converse. (Contributed by NM, 19-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ≤ 𝑌 ↔ (◡𝐹‘𝑋) ≤ (◡𝐹‘𝑌)))
Theorem	lautcnv 38031	The converse of a lattice automorphism is a lattice automorphism. (Contributed by NM, 10-May-2013.)
⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼) → ◡𝐹 ∈ 𝐼)
Theorem	lautlt 38032	Less-than property of a lattice automorphism. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 < 𝑌 ↔ (𝐹‘𝑋) < (𝐹‘𝑌)))
Theorem	lautcvr 38033	Covering property of a lattice automorphism. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋𝐶𝑌 ↔ (𝐹‘𝑋)𝐶(𝐹‘𝑌)))
Theorem	lautj 38034	Meet property of a lattice automorphism. (Contributed by NM, 25-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(𝑋 ∨ 𝑌)) = ((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
Theorem	lautm 38035	Meet property of a lattice automorphism. (Contributed by NM, 19-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(𝑋 ∧ 𝑌)) = ((𝐹‘𝑋) ∧ (𝐹‘𝑌)))
Theorem	lauteq 38036*	A lattice automorphism argument is equal to its value if all atoms are equal to their values. (Contributed by NM, 24-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑝 ∈ 𝐴 (𝐹‘𝑝) = 𝑝) → (𝐹‘𝑋) = 𝑋)
Theorem	idlaut 38037	The identity function is a lattice automorphism. (Contributed by NM, 18-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐴 → ( I ↾ 𝐵) ∈ 𝐼)
Theorem	lautco 38038	The composition of two lattice automorphisms is a lattice automorphism. (Contributed by NM, 19-Apr-2013.)
⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ∧ 𝐺 ∈ 𝐼) → (𝐹 ∘ 𝐺) ∈ 𝐼)
Theorem	pautsetN 38039*	The set of projective automorphisms. (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.)
⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝑀 = (PAut‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐵 → 𝑀 = {𝑓 ∣ (𝑓:𝑆–1-1-onto→𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 ⊆ 𝑦 ↔ (𝑓‘𝑥) ⊆ (𝑓‘𝑦)))})
Theorem	ispautN 38040*	The predicate "is a projective automorphism". (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.)
⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝑀 = (PAut‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐵 → (𝐹 ∈ 𝑀 ↔ (𝐹:𝑆–1-1-onto→𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 ⊆ 𝑦 ↔ (𝐹‘𝑥) ⊆ (𝐹‘𝑦)))))
Syntax	cldil 38041	Extend class notation with set of all lattice dilations.
class LDil
Syntax	cltrn 38042	Extend class notation with set of all lattice translations.
class LTrn
Syntax	cdilN 38043	Extend class notation with set of all dilations.
class Dil
Syntax	ctrnN 38044	Extend class notation with set of all translations.
class Trn
Definition	df-ldil 38045*	Define set of all lattice dilations. Similar to definition of dilation in [Crawley] p. 111. (Contributed by NM, 11-May-2012.)
⊢ LDil = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∈ (LAut‘𝑘) ∣ ∀𝑥 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑤 → (𝑓‘𝑥) = 𝑥)}))
Definition	df-ltrn 38046*	Define set of all lattice translations. Similar to definition of translation in [Crawley] p. 111. (Contributed by NM, 11-May-2012.)
⊢ LTrn = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∈ ((LDil‘𝑘)‘𝑤) ∣ ∀𝑝 ∈ (Atoms‘𝑘)∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓‘𝑞))(meet‘𝑘)𝑤))}))
Definition	df-dilN 38047*	Define set of all dilations. Definition of dilation in [Crawley] p. 111. (Contributed by NM, 30-Jan-2012.)
⊢ Dil = (𝑘 ∈ V ↦ (𝑑 ∈ (Atoms‘𝑘) ↦ {𝑓 ∈ (PAut‘𝑘) ∣ ∀𝑥 ∈ (PSubSp‘𝑘)(𝑥 ⊆ ((WAtoms‘𝑘)‘𝑑) → (𝑓‘𝑥) = 𝑥)}))
Definition	df-trnN 38048*	Define set of all translations. Definition of translation in [Crawley] p. 111. (Contributed by NM, 4-Feb-2012.)
⊢ Trn = (𝑘 ∈ V ↦ (𝑑 ∈ (Atoms‘𝑘) ↦ {𝑓 ∈ ((Dil‘𝑘)‘𝑑) ∣ ∀𝑞 ∈ ((WAtoms‘𝑘)‘𝑑)∀𝑟 ∈ ((WAtoms‘𝑘)‘𝑑)((𝑞(+𝑃‘𝑘)(𝑓‘𝑞)) ∩ ((⊥𝑃‘𝑘)‘{𝑑})) = ((𝑟(+𝑃‘𝑘)(𝑓‘𝑟)) ∩ ((⊥𝑃‘𝑘)‘{𝑑}))}))
Theorem	ldilfset 38049*	The mapping from fiducial co-atom 𝑤 to its set of lattice dilations. (Contributed by NM, 11-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐶 → (LDil‘𝐾) = (𝑤 ∈ 𝐻 ↦ {𝑓 ∈ 𝐼 ∣ ∀𝑥 ∈ 𝐵 (𝑥 ≤ 𝑤 → (𝑓‘𝑥) = 𝑥)}))
Theorem	ldilset 38050*	The set of lattice dilations for a fiducial co-atom 𝑊. (Contributed by NM, 11-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    &   ⊢ 𝐷 = ((LDil‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝐶 ∧ 𝑊 ∈ 𝐻) → 𝐷 = {𝑓 ∈ 𝐼 ∣ ∀𝑥 ∈ 𝐵 (𝑥 ≤ 𝑊 → (𝑓‘𝑥) = 𝑥)})
Theorem	isldil 38051*	The predicate "is a lattice dilation". Similar to definition of dilation in [Crawley] p. 111. (Contributed by NM, 11-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    &   ⊢ 𝐷 = ((LDil‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝐶 ∧ 𝑊 ∈ 𝐻) → (𝐹 ∈ 𝐷 ↔ (𝐹 ∈ 𝐼 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ≤ 𝑊 → (𝐹‘𝑥) = 𝑥))))
Theorem	ldillaut 38052	A lattice dilation is an automorphism. (Contributed by NM, 20-May-2012.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    &   ⊢ 𝐷 = ((LDil‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷) → 𝐹 ∈ 𝐼)
Theorem	ldil1o 38053	A lattice dilation is a one-to-one onto function. (Contributed by NM, 19-Apr-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐷 = ((LDil‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷) → 𝐹:𝐵–1-1-onto→𝐵)
Theorem	ldilval 38054	Value of a lattice dilation under its co-atom. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐷 = ((LDil‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷 ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐹‘𝑋) = 𝑋)
Theorem	idldil 38055	The identity function is a lattice dilation. (Contributed by NM, 18-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐷 = ((LDil‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝐵) ∈ 𝐷)
Theorem	ldilcnv 38056	The converse of a lattice dilation is a lattice dilation. (Contributed by NM, 10-May-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐷 = ((LDil‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷) → ◡𝐹 ∈ 𝐷)
Theorem	ldilco 38057	The composition of two lattice automorphisms is a lattice automorphism. (Contributed by NM, 19-Apr-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐷 = ((LDil‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷) → (𝐹 ∘ 𝐺) ∈ 𝐷)
Theorem	ltrnfset 38058*	The set of all lattice translations for a lattice 𝐾. (Contributed by NM, 11-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐶 → (LTrn‘𝐾) = (𝑤 ∈ 𝐻 ↦ {𝑓 ∈ ((LDil‘𝐾)‘𝑤) ∣ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤) → ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑤))}))
Theorem	ltrnset 38059*	The set of lattice translations for a fiducial co-atom 𝑊. (Contributed by NM, 11-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐷 = ((LDil‘𝐾)‘𝑊)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑊 ∈ 𝐻) → 𝑇 = {𝑓 ∈ 𝐷 ∣ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊) → ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑊) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑊))})
Theorem	isltrn 38060*	The predicate "is a lattice translation". Similar to definition of translation in [Crawley] p. 111. (Contributed by NM, 11-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐷 = ((LDil‘𝐾)‘𝑊)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑊 ∈ 𝐻) → (𝐹 ∈ 𝑇 ↔ (𝐹 ∈ 𝐷 ∧ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊) → ((𝑝 ∨ (𝐹‘𝑝)) ∧ 𝑊) = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊)))))
Theorem	isltrn2N 38061*	The predicate "is a lattice translation". Version of isltrn 38060 that considers only different 𝑝 and 𝑞. TODO: Can this eliminate some separate proofs for the 𝑝 = 𝑞 case? (Contributed by NM, 22-Apr-2013.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐷 = ((LDil‘𝐾)‘𝑊)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑊 ∈ 𝐻) → (𝐹 ∈ 𝑇 ↔ (𝐹 ∈ 𝐷 ∧ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞) → ((𝑝 ∨ (𝐹‘𝑝)) ∧ 𝑊) = ((𝑞 ∨ (𝐹‘𝑞)) ∧ 𝑊)))))
Theorem	ltrnu 38062	Uniqueness property of a lattice translation value for atoms not under the fiducial co-atom 𝑊. Similar to definition of translation in [Crawley] p. 111. (Contributed by NM, 20-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ ((((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) = ((𝑄 ∨ (𝐹‘𝑄)) ∧ 𝑊))
Theorem	ltrnldil 38063	A lattice translation is a lattice dilation. (Contributed by NM, 20-May-2012.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐷 = ((LDil‘𝐾)‘𝑊)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹 ∈ 𝐷)
Theorem	ltrnlaut 38064	A lattice translation is a lattice automorphism. (Contributed by NM, 20-May-2012.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹 ∈ 𝐼)
Theorem	ltrn1o 38065	A lattice translation is a one-to-one onto function. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹:𝐵–1-1-onto→𝐵)
Theorem	ltrncl 38066	Closure of a lattice translation. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ 𝐵)
Theorem	ltrn11 38067	One-to-one property of a lattice translation. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝐹‘𝑋) = (𝐹‘𝑌) ↔ 𝑋 = 𝑌))
Theorem	ltrncnvnid 38068	If a translation is different from the identity, so is its converse. (Contributed by NM, 17-Jun-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) → ◡𝐹 ≠ ( I ↾ 𝐵))
Theorem	ltrncoidN 38069	Two translations are equal if the composition of one with the converse of the other is the zero translation. This is an analogue of vector subtraction. (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ((𝐹 ∘ ◡𝐺) = ( I ↾ 𝐵) ↔ 𝐹 = 𝐺))
Theorem	ltrnle 38070	Less-than or equal property of a lattice translation. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ≤ 𝑌 ↔ (𝐹‘𝑋) ≤ (𝐹‘𝑌)))
Theorem	ltrncnvleN 38071	Less-than or equal property of lattice translation converse. (Contributed by NM, 10-May-2013.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ≤ 𝑌 ↔ (◡𝐹‘𝑋) ≤ (◡𝐹‘𝑌)))
Theorem	ltrnm 38072	Lattice translation of a meet. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(𝑋 ∧ 𝑌)) = ((𝐹‘𝑋) ∧ (𝐹‘𝑌)))
Theorem	ltrnj 38073	Lattice translation of a meet. TODO: change antecedent to 𝐾 ∈ HL (Contributed by NM, 25-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(𝑋 ∨ 𝑌)) = ((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
Theorem	ltrncvr 38074	Covering property of a lattice translation. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋𝐶𝑌 ↔ (𝐹‘𝑋)𝐶(𝐹‘𝑌)))
Theorem	ltrnval1 38075	Value of a lattice translation under its co-atom. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐹‘𝑋) = 𝑋)
Theorem	ltrnid 38076*	A lattice translation is the identity function iff all atoms not under the fiducial co-atom 𝑊 are equal to their values. (Contributed by NM, 24-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → (𝐹‘𝑝) = 𝑝) ↔ 𝐹 = ( I ↾ 𝐵)))
Theorem	ltrnnid 38077*	If a lattice translation is not the identity, then there is an atom not under the fiducial co-atom 𝑊 and not equal to its translation. (Contributed by NM, 24-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) → ∃𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 ∧ (𝐹‘𝑝) ≠ 𝑝))
Theorem	ltrnatb 38078	The lattice translation of an atom is an atom. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐵) → (𝑃 ∈ 𝐴 ↔ (𝐹‘𝑃) ∈ 𝐴))
Theorem	ltrncnvatb 38079	The converse of the lattice translation of an atom is an atom. (Contributed by NM, 2-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐵) → (𝑃 ∈ 𝐴 ↔ (◡𝐹‘𝑃) ∈ 𝐴))
Theorem	ltrnel 38080	The lattice translation of an atom not under the fiducial co-atom is also an atom not under the fiducial co-atom. Remark below Lemma B in [Crawley] p. 112. (Contributed by NM, 22-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊))
Theorem	ltrnat 38081	The lattice translation of an atom is also an atom. TODO: See if this can shorten some ltrnel 38080 uses. (Contributed by NM, 25-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝐹‘𝑃) ∈ 𝐴)
Theorem	ltrncnvat 38082	The converse of the lattice translation of an atom is an atom. (Contributed by NM, 9-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (◡𝐹‘𝑃) ∈ 𝐴)
Theorem	ltrncnvel 38083	The converse of the lattice translation of an atom not under the fiducial co-atom. (Contributed by NM, 10-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((◡𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (◡𝐹‘𝑃) ≤ 𝑊))
Theorem	ltrncoelN 38084	Composition of lattice translations of an atom. TODO: See if this can shorten some ltrnel 38080 uses. (Contributed by NM, 1-May-2013.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘(𝐺‘𝑃)) ∈ 𝐴 ∧ ¬ (𝐹‘(𝐺‘𝑃)) ≤ 𝑊))
Theorem	ltrncoat 38085	Composition of lattice translations of an atom. TODO: See if this can shorten some ltrnel 38080, ltrnat 38081 uses. (Contributed by NM, 1-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → (𝐹‘(𝐺‘𝑃)) ∈ 𝐴)
Theorem	ltrncoval 38086	Two ways to express value of translation composition. (Contributed by NM, 31-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝑃) = (𝐹‘(𝐺‘𝑃)))
Theorem	ltrncnv 38087	The converse of a lattice translation is a lattice translation. (Contributed by NM, 10-May-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ◡𝐹 ∈ 𝑇)
Theorem	ltrn11at 38088	Frequently used one-to-one property of lattice translation atoms. (Contributed by NM, 5-May-2013.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄)) → (𝐹‘𝑃) ≠ (𝐹‘𝑄))
Theorem	ltrneq2 38089*	The equality of two translations is determined by their equality at atoms. (Contributed by NM, 2-Mar-2014.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (∀𝑝 ∈ 𝐴 (𝐹‘𝑝) = (𝐺‘𝑝) ↔ 𝐹 = 𝐺))
Theorem	ltrneq 38090*	The equality of two translations is determined by their equality at atoms not under co-atom 𝑊. (Contributed by NM, 20-Jun-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → (𝐹‘𝑝) = (𝐺‘𝑝)) ↔ 𝐹 = 𝐺))
Theorem	idltrn 38091	The identity function is a lattice translation. Remark below Lemma B in [Crawley] p. 112. (Contributed by NM, 18-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝐵) ∈ 𝑇)
Theorem	ltrnmw 38092	Property of lattice translation value. Remark below Lemma B in [Crawley] p. 112. TODO: Can this be used in more places? (Contributed by NM, 20-May-2012.) (Proof shortened by OpenAI, 25-Mar-2020.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∧ 𝑊) = 0 )
Theorem	dilfsetN 38093*	The mapping from fiducial atom to set of dilations. (Contributed by NM, 30-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝑊 = (WAtoms‘𝐾)    &   ⊢ 𝑀 = (PAut‘𝐾)    &   ⊢ 𝐿 = (Dil‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐵 → 𝐿 = (𝑑 ∈ 𝐴 ↦ {𝑓 ∈ 𝑀 ∣ ∀𝑥 ∈ 𝑆 (𝑥 ⊆ (𝑊‘𝑑) → (𝑓‘𝑥) = 𝑥)}))
Theorem	dilsetN 38094*	The set of dilations for a fiducial atom 𝐷. (Contributed by NM, 4-Feb-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝑊 = (WAtoms‘𝐾)    &   ⊢ 𝑀 = (PAut‘𝐾)    &   ⊢ 𝐿 = (Dil‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴) → (𝐿‘𝐷) = {𝑓 ∈ 𝑀 ∣ ∀𝑥 ∈ 𝑆 (𝑥 ⊆ (𝑊‘𝐷) → (𝑓‘𝑥) = 𝑥)})
Theorem	isdilN 38095*	The predicate "is a dilation". (Contributed by NM, 4-Feb-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝑊 = (WAtoms‘𝐾)    &   ⊢ 𝑀 = (PAut‘𝐾)    &   ⊢ 𝐿 = (Dil‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴) → (𝐹 ∈ (𝐿‘𝐷) ↔ (𝐹 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝑆 (𝑥 ⊆ (𝑊‘𝐷) → (𝐹‘𝑥) = 𝑥))))
Theorem	trnfsetN 38096*	The mapping from fiducial atom to set of translations. (Contributed by NM, 4-Feb-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝑊 = (WAtoms‘𝐾)    &   ⊢ 𝑀 = (PAut‘𝐾)    &   ⊢ 𝐿 = (Dil‘𝐾)    &   ⊢ 𝑇 = (Trn‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐶 → 𝑇 = (𝑑 ∈ 𝐴 ↦ {𝑓 ∈ (𝐿‘𝑑) ∣ ∀𝑞 ∈ (𝑊‘𝑑)∀𝑟 ∈ (𝑊‘𝑑)((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝑑})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝑑}))}))
Theorem	trnsetN 38097*	The set of translations for a fiducial atom 𝐷. (Contributed by NM, 4-Feb-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝑊 = (WAtoms‘𝐾)    &   ⊢ 𝑀 = (PAut‘𝐾)    &   ⊢ 𝐿 = (Dil‘𝐾)    &   ⊢ 𝑇 = (Trn‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴) → (𝑇‘𝐷) = {𝑓 ∈ (𝐿‘𝐷) ∣ ∀𝑞 ∈ (𝑊‘𝐷)∀𝑟 ∈ (𝑊‘𝐷)((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝐷})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝐷}))})
Theorem	istrnN 38098*	The predicate "is a translation". (Contributed by NM, 4-Feb-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝑊 = (WAtoms‘𝐾)    &   ⊢ 𝑀 = (PAut‘𝐾)    &   ⊢ 𝐿 = (Dil‘𝐾)    &   ⊢ 𝑇 = (Trn‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴) → (𝐹 ∈ (𝑇‘𝐷) ↔ (𝐹 ∈ (𝐿‘𝐷) ∧ ∀𝑞 ∈ (𝑊‘𝐷)∀𝑟 ∈ (𝑊‘𝐷)((𝑞 + (𝐹‘𝑞)) ∩ ( ⊥ ‘{𝐷})) = ((𝑟 + (𝐹‘𝑟)) ∩ ( ⊥ ‘{𝐷})))))
Syntax	ctrl 38099	Extend class notation with set of all traces of lattice translations.
class trL
Definition	df-trl 38100*	Define trace of a lattice translation. (Contributed by NM, 20-May-2012.)
⊢ trL = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (℩𝑥 ∈ (Base‘𝑘)∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤 → 𝑥 = ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤))))))