P. 402 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 40101-40200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ltrnldil 40101	A lattice translation is a lattice dilation. (Contributed by NM, 20-May-2012.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐷 = ((LDil‘𝐾)‘𝑊)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹 ∈ 𝐷)
Theorem	ltrnlaut 40102	A lattice translation is a lattice automorphism. (Contributed by NM, 20-May-2012.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹 ∈ 𝐼)
Theorem	ltrn1o 40103	A lattice translation is a one-to-one onto function. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹:𝐵–1-1-onto→𝐵)
Theorem	ltrncl 40104	Closure of a lattice translation. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ 𝐵)
Theorem	ltrn11 40105	One-to-one property of a lattice translation. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝐹‘𝑋) = (𝐹‘𝑌) ↔ 𝑋 = 𝑌))
Theorem	ltrncnvnid 40106	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 40107	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 40108	Less-than or equal property of a lattice translation. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ≤ 𝑌 ↔ (𝐹‘𝑋) ≤ (𝐹‘𝑌)))
Theorem	ltrncnvleN 40109	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 40110	Lattice translation of a meet. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(𝑋 ∧ 𝑌)) = ((𝐹‘𝑋) ∧ (𝐹‘𝑌)))
Theorem	ltrnj 40111	Lattice translation of a meet. TODO: change antecedent to 𝐾 ∈ HL (Contributed by NM, 25-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(𝑋 ∨ 𝑌)) = ((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
Theorem	ltrncvr 40112	Covering property of a lattice translation. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋𝐶𝑌 ↔ (𝐹‘𝑋)𝐶(𝐹‘𝑌)))
Theorem	ltrnval1 40113	Value of a lattice translation under its co-atom. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐹‘𝑋) = 𝑋)
Theorem	ltrnid 40114*	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 40115*	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 40116	The lattice translation of an atom is an atom. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐵) → (𝑃 ∈ 𝐴 ↔ (𝐹‘𝑃) ∈ 𝐴))
Theorem	ltrncnvatb 40117	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 40118	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 40119	The lattice translation of an atom is also an atom. TODO: See if this can shorten some ltrnel 40118 uses. (Contributed by NM, 25-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝐹‘𝑃) ∈ 𝐴)
Theorem	ltrncnvat 40120	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 40121	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 40122	Composition of lattice translations of an atom. TODO: See if this can shorten some ltrnel 40118 uses. (Contributed by NM, 1-May-2013.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘(𝐺‘𝑃)) ∈ 𝐴 ∧ ¬ (𝐹‘(𝐺‘𝑃)) ≤ 𝑊))
Theorem	ltrncoat 40123	Composition of lattice translations of an atom. TODO: See if this can shorten some ltrnel 40118, ltrnat 40119 uses. (Contributed by NM, 1-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → (𝐹‘(𝐺‘𝑃)) ∈ 𝐴)
Theorem	ltrncoval 40124	Two ways to express value of translation composition. (Contributed by NM, 31-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝑃) = (𝐹‘(𝐺‘𝑃)))
Theorem	ltrncnv 40125	The converse of a lattice translation is a lattice translation. (Contributed by NM, 10-May-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ◡𝐹 ∈ 𝑇)
Theorem	ltrn11at 40126	Frequently used one-to-one property of lattice translation atoms. (Contributed by NM, 5-May-2013.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄)) → (𝐹‘𝑃) ≠ (𝐹‘𝑄))
Theorem	ltrneq2 40127*	The equality of two translations is determined by their equality at atoms. (Contributed by NM, 2-Mar-2014.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (∀𝑝 ∈ 𝐴 (𝐹‘𝑝) = (𝐺‘𝑝) ↔ 𝐹 = 𝐺))
Theorem	ltrneq 40128*	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 40129	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 40130	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 40131*	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 40132*	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 40133*	The predicate "is a dilation". (Contributed by NM, 4-Feb-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝑊 = (WAtoms‘𝐾)    &   ⊢ 𝑀 = (PAut‘𝐾)    &   ⊢ 𝐿 = (Dil‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴) → (𝐹 ∈ (𝐿‘𝐷) ↔ (𝐹 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝑆 (𝑥 ⊆ (𝑊‘𝐷) → (𝐹‘𝑥) = 𝑥))))
Theorem	trnfsetN 40134*	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 40135*	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 40136*	The predicate "is a translation". (Contributed by NM, 4-Feb-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝑊 = (WAtoms‘𝐾)    &   ⊢ 𝑀 = (PAut‘𝐾)    &   ⊢ 𝐿 = (Dil‘𝐾)    &   ⊢ 𝑇 = (Trn‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴) → (𝐹 ∈ (𝑇‘𝐷) ↔ (𝐹 ∈ (𝐿‘𝐷) ∧ ∀𝑞 ∈ (𝑊‘𝐷)∀𝑟 ∈ (𝑊‘𝐷)((𝑞 + (𝐹‘𝑞)) ∩ ( ⊥ ‘{𝐷})) = ((𝑟 + (𝐹‘𝑟)) ∩ ( ⊥ ‘{𝐷})))))
Syntax	ctrl 40137	Extend class notation with set of all traces of lattice translations.
class trL
Definition	df-trl 40138*	Define trace of a lattice translation. (Contributed by NM, 20-May-2012.)
⊢ trL = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (℩𝑥 ∈ (Base‘𝑘)∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤 → 𝑥 = ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤))))))
Theorem	trlfset 40139*	The set of all traces of lattice translations for a lattice 𝐾. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐶 → (trL‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (℩𝑥 ∈ 𝐵 ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑤 → 𝑥 = ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤))))))
Theorem	trlset 40140*	The set of traces of lattice translations for a fiducial co-atom 𝑊. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝐶 ∧ 𝑊 ∈ 𝐻) → 𝑅 = (𝑓 ∈ 𝑇 ↦ (℩𝑥 ∈ 𝐵 ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → 𝑥 = ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑊)))))
Theorem	trlval 40141*	The value of the trace of a lattice translation. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘𝐹) = (℩𝑥 ∈ 𝐵 ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → 𝑥 = ((𝑝 ∨ (𝐹‘𝑝)) ∧ 𝑊))))
Theorem	trlval2 40142	The value of the trace of a lattice translation, given any atom 𝑃 not under the fiducial co-atom 𝑊. Note: this requires only the weaker assumption 𝐾 ∈ Lat; we use 𝐾 ∈ HL for convenience. (Contributed by NM, 20-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘𝐹) = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊))
Theorem	trlcl 40143	Closure of the trace of a lattice translation. (Contributed by NM, 22-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘𝐹) ∈ 𝐵)
Theorem	trlcnv 40144	The trace of the converse of a lattice translation. (Contributed by NM, 10-May-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘◡𝐹) = (𝑅‘𝐹))
Theorem	trljat1 40145	The value of a translation of an atom 𝑃 not under the fiducial co-atom 𝑊, joined with trace. Equation above Lemma C in [Crawley] p. 112. TODO: shorten with atmod3i1 39843? (Contributed by NM, 22-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ∨ (𝑅‘𝐹)) = (𝑃 ∨ (𝐹‘𝑃)))
Theorem	trljat2 40146	The value of a translation of an atom 𝑃 not under the fiducial co-atom 𝑊, joined with trace. Equation above Lemma C in [Crawley] p. 112. (Contributed by NM, 25-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ (𝑅‘𝐹)) = (𝑃 ∨ (𝐹‘𝑃)))
Theorem	trljat3 40147	The value of a translation of an atom 𝑃 not under the fiducial co-atom 𝑊, joined with trace. Equation above Lemma C in [Crawley] p. 112. (Contributed by NM, 22-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ∨ (𝑅‘𝐹)) = ((𝐹‘𝑃) ∨ (𝑅‘𝐹)))
Theorem	trlat 40148	If an atom differs from its translation, the trace is an atom. Equation above Lemma C in [Crawley] p. 112. (Contributed by NM, 23-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) ≠ 𝑃)) → (𝑅‘𝐹) ∈ 𝐴)
Theorem	trl0 40149	If an atom not under the fiducial co-atom 𝑊 equals its lattice translation, the trace of the translation is zero. (Contributed by NM, 24-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) = 𝑃)) → (𝑅‘𝐹) = 0 )
Theorem	trlator0 40150	The trace of a lattice translation is an atom or zero. (Contributed by NM, 5-May-2013.)
⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ((𝑅‘𝐹) ∈ 𝐴 ∨ (𝑅‘𝐹) = 0 ))
Theorem	trlatn0 40151	The trace of a lattice translation is an atom iff it is nonzero. (Contributed by NM, 14-Jun-2013.)
⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ((𝑅‘𝐹) ∈ 𝐴 ↔ (𝑅‘𝐹) ≠ 0 ))
Theorem	trlnidat 40152	The trace of a lattice translation other than the identity is an atom. Remark above Lemma C in [Crawley] p. 112. (Contributed by NM, 23-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) → (𝑅‘𝐹) ∈ 𝐴)
Theorem	ltrnnidn 40153	If a lattice translation is not the identity, then the translation of any atom not under the fiducial co-atom 𝑊 is different from the atom. Remark above Lemma C in [Crawley] p. 112. (Contributed by NM, 24-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹‘𝑃) ≠ 𝑃)
Theorem	ltrnideq 40154	Property of the identity lattice translation. (Contributed by NM, 27-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹 = ( I ↾ 𝐵) ↔ (𝐹‘𝑃) = 𝑃))
Theorem	trlid0 40155	The trace of the identity translation is zero. (Contributed by NM, 11-Jun-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑅‘( I ↾ 𝐵)) = 0 )
Theorem	trlnidatb 40156	A lattice translation is not the identity iff its trace is an atom. TODO: Can proofs be reorganized so this goes with trlnidat 40152? Why do both this and ltrnideq 40154 need trlnidat 40152? (Contributed by NM, 4-Jun-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝐹 ≠ ( I ↾ 𝐵) ↔ (𝑅‘𝐹) ∈ 𝐴))
Theorem	trlid0b 40157	A lattice translation is the identity iff its trace is zero. (Contributed by NM, 14-Jun-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝐹 = ( I ↾ 𝐵) ↔ (𝑅‘𝐹) = 0 ))
Theorem	trlnid 40158	Different translations with the same trace cannot be the identity. (Contributed by NM, 26-Jul-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ 𝐺 ∧ (𝑅‘𝐹) = (𝑅‘𝐺))) → 𝐹 ≠ ( I ↾ 𝐵))
Theorem	ltrn2ateq 40159	Property of the equality of a lattice translation with its value. (Contributed by NM, 27-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))) → ((𝐹‘𝑃) = 𝑃 ↔ (𝐹‘𝑄) = 𝑄))
Theorem	ltrnateq 40160	If any atom (under 𝑊) is not equal to its translation, so is any other atom. (Contributed by NM, 6-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → (𝐹‘𝑄) = 𝑄)
Theorem	ltrnatneq 40161	If any atom (under 𝑊) is not equal to its translation, so is any other atom. TODO: ¬ 𝑃 ≤ 𝑊 isn't needed to prove this. Will removing it shorten (and not lengthen) proofs using it? (Contributed by NM, 6-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝐹‘𝑄) ≠ 𝑄)
Theorem	ltrnatlw 40162	If the value of an atom equals the atom in a non-identity translation, the atom is under the fiducial hyperplane. (Contributed by NM, 15-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ ((𝐹‘𝑃) ≠ 𝑃 ∧ (𝐹‘𝑄) = 𝑄)) → 𝑄 ≤ 𝑊)
Theorem	trlle 40163	The trace of a lattice translation is less than the fiducial co-atom 𝑊. (Contributed by NM, 25-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘𝐹) ≤ 𝑊)
Theorem	trlne 40164	The trace of a lattice translation is not equal to any atom not under the fiducial co-atom 𝑊. Part of proof of Lemma C in [Crawley] p. 112. (Contributed by NM, 25-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑃 ≠ (𝑅‘𝐹))
Theorem	trlnle 40165	The atom not under the fiducial co-atom 𝑊 is not less than the trace of a lattice translation. Part of proof of Lemma C in [Crawley] p. 112. (Contributed by NM, 26-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ¬ 𝑃 ≤ (𝑅‘𝐹))
Theorem	trlval3 40166	The value of the trace of a lattice translation in terms of 2 atoms. TODO: Try to shorten proof. (Contributed by NM, 3-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) → (𝑅‘𝐹) = ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄))))
Theorem	trlval4 40167	The value of the trace of a lattice translation in terms of 2 atoms. (Contributed by NM, 3-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄))) → (𝑅‘𝐹) = ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄))))
Theorem	trlval5 40168	The value of the trace of a lattice translation in terms of itself. (Contributed by NM, 19-Jul-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘𝐹) = ((𝑃 ∨ (𝑅‘𝐹)) ∧ 𝑊))
Theorem	arglem1N 40169	Lemma for Desargues's law. Theorem 13.3 of [Crawley] p. 110, third and fourth lines from bottom. In these lemmas, 𝑃, 𝑄, 𝑅, 𝑆, 𝑇, 𝑈, 𝐶, 𝐷, 𝐸, 𝐹, and 𝐺 represent Crawley's a0, a1, a2, b0, b1, b2, c, z0, z1, z2, and p respectively. (Contributed by NM, 28-Jun-2012.) (New usage is discouraged.)
⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐹 = ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇))    &   ⊢ 𝐺 = ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇))    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇)) ∧ 𝐺 ∈ 𝐴) → 𝐹 ∈ 𝐴)
Theorem	cdlemc1 40170	Part of proof of Lemma C in [Crawley] p. 112. TODO: shorten with atmod3i1 39843? (Contributed by NM, 29-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ∨ ((𝑃 ∨ 𝑋) ∧ 𝑊)) = (𝑃 ∨ 𝑋))
Theorem	cdlemc2 40171	Part of proof of Lemma C in [Crawley] p. 112. (Contributed by NM, 25-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))) → (𝐹‘𝑄) ≤ ((𝐹‘𝑃) ∨ ((𝑃 ∨ 𝑄) ∧ 𝑊)))
Theorem	cdlemc3 40172	Part of proof of Lemma C in [Crawley] p. 113. (Contributed by NM, 26-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))) → ((𝐹‘𝑃) ≤ (𝑄 ∨ (𝑅‘𝐹)) → 𝑄 ≤ (𝑃 ∨ (𝐹‘𝑃))))
Theorem	cdlemc4 40173	Part of proof of Lemma C in [Crawley] p. 113. (Contributed by NM, 26-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ¬ 𝑄 ≤ (𝑃 ∨ (𝐹‘𝑃))) → (𝑄 ∨ (𝑅‘𝐹)) ≠ ((𝐹‘𝑃) ∨ ((𝑃 ∨ 𝑄) ∧ 𝑊)))
Theorem	cdlemc5 40174	Lemma for cdlemc 40176. (Contributed by NM, 26-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (¬ 𝑄 ≤ (𝑃 ∨ (𝐹‘𝑃)) ∧ (𝐹‘𝑃) ≠ 𝑃)) → (𝐹‘𝑄) = ((𝑄 ∨ (𝑅‘𝐹)) ∧ ((𝐹‘𝑃) ∨ ((𝑃 ∨ 𝑄) ∧ 𝑊))))
Theorem	cdlemc6 40175	Lemma for cdlemc 40176. (Contributed by NM, 26-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → (𝐹‘𝑄) = ((𝑄 ∨ (𝑅‘𝐹)) ∧ ((𝐹‘𝑃) ∨ ((𝑃 ∨ 𝑄) ∧ 𝑊))))
Theorem	cdlemc 40176	Lemma C in [Crawley] p. 113. (Contributed by NM, 26-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ¬ 𝑄 ≤ (𝑃 ∨ (𝐹‘𝑃))) → (𝐹‘𝑄) = ((𝑄 ∨ (𝑅‘𝐹)) ∧ ((𝐹‘𝑃) ∨ ((𝑃 ∨ 𝑄) ∧ 𝑊))))
Theorem	cdlemd1 40177	Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 29-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)))) → 𝑅 = ((𝑃 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊)) ∧ (𝑄 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑊))))
Theorem	cdlemd2 40178	Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 29-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝐹‘𝑅) = (𝐺‘𝑅))
Theorem	cdlemd3 40179	Part of proof of Lemma D in [Crawley] p. 113. The 𝑅 ≠ 𝑃 requirement is not mentioned in their proof. (Contributed by NM, 29-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≠ 𝑃)) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → ¬ 𝑅 ≤ (𝑃 ∨ 𝑆))
Theorem	cdlemd4 40180	Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 30-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≠ 𝑃)) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝐹‘𝑅) = (𝐺‘𝑅))
Theorem	cdlemd5 40181	Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 30-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑃 ≠ 𝑄) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝐹‘𝑅) = (𝐺‘𝑅))
Theorem	cdlemd6 40182	Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 31-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ ¬ 𝑄 ≤ (𝑃 ∨ (𝐹‘𝑃))) ∧ (𝐹‘𝑃) = (𝐺‘𝑃)) → (𝐹‘𝑄) = (𝐺‘𝑄))
Theorem	cdlemd7 40183	Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 1-Jun-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ ¬ 𝑄 ≤ (𝑃 ∨ (𝐹‘𝑃)))) → (𝐹‘𝑅) = (𝐺‘𝑅))
Theorem	cdlemd8 40184	Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 1-Jun-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑃) = 𝑃)) → (𝐹‘𝑅) = (𝐺‘𝑅))
Theorem	cdlemd9 40185	Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 2-Jun-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐹‘𝑃) = (𝐺‘𝑃)) → (𝐹‘𝑅) = (𝐺‘𝑅))
Theorem	cdlemd 40186	If two translations agree at any atom not under the fiducial co-atom 𝑊, then they are equal. Lemma D in [Crawley] p. 113. (Contributed by NM, 2-Jun-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐹‘𝑃) = (𝐺‘𝑃)) → 𝐹 = 𝐺)
Theorem	ltrneq3 40187	Two translations agree at any atom not under the fiducial co-atom 𝑊 iff they are equal. (Contributed by NM, 25-Jul-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) = (𝐺‘𝑃) ↔ 𝐹 = 𝐺))
Theorem	cdleme00a 40188	Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 14-Jun-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑅 ≠ 𝑃)
Theorem	cdleme0aa 40189	Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 14-Jun-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝐵 = (Base‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑈 ∈ 𝐵)
Theorem	cdleme0a 40190	Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 12-Jun-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄)) → 𝑈 ∈ 𝐴)
Theorem	cdleme0b 40191	Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 13-Jun-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) → 𝑈 ≠ 𝑃)
Theorem	cdleme0c 40192	Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 12-Jun-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → 𝑈 ≠ 𝑅)
Theorem	cdleme0cp 40193	Part of proof of Lemma E in [Crawley] p. 113. TODO: Reformat as in cdlemg3a 40576- swap consequent equality; make antecedent use df-3an 1088. (Contributed by NM, 13-Jun-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴)) → (𝑃 ∨ 𝑈) = (𝑃 ∨ 𝑄))
Theorem	cdleme0cq 40194	Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 25-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))) → (𝑄 ∨ 𝑈) = (𝑃 ∨ 𝑄))
Theorem	cdleme0dN 40195	Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 13-Jun-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑅) ∧ 𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ 𝑃 ≠ 𝑅)) → 𝑉 ∈ 𝐴)
Theorem	cdleme0e 40196	Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 13-Jun-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑅) ∧ 𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → 𝑈 ≠ 𝑉)
Theorem	cdleme0fN 40197	Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 14-Jun-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑅) ∧ 𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 𝑉 ≠ 𝑃)
Theorem	cdleme0gN 40198	Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 14-Jun-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑅) ∧ 𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝑉 ≠ 𝑄)
Theorem	cdlemeulpq 40199	Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 5-Dec-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → 𝑈 ≤ (𝑃 ∨ 𝑄))
Theorem	cdleme01N 40200	Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 5-Nov-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → ((𝑈 ≠ 𝑃 ∧ 𝑈 ≠ 𝑄 ∧ 𝑈 ≤ (𝑃 ∨ 𝑄)) ∧ 𝑈 ≤ 𝑊))