P. 393 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39201-39300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lhpmcvr4N 39201	Specialization of lhpmcvr2 39199. (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝑌 ∈ 𝐵 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊 ∧ 𝑃 ≤ 𝑋)) → ¬ 𝑃 ≤ 𝑌)
Theorem	lhpmcvr5N 39202*	Specialization of lhpmcvr2 39199. (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → ∃𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑝 ≤ 𝑌 ∧ (𝑝 ∨ (𝑋 ∧ 𝑊)) = 𝑋))
Theorem	lhpmcvr6N 39203*	Specialization of lhpmcvr2 39199. (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → ∃𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑝 ≤ 𝑌 ∧ 𝑝 ≤ 𝑋))
Theorem	lhpm0atN 39204	If the meet of a lattice hyperplane with a nonzero element is zero, the element is an atom. (Contributed by NM, 28-Apr-2014.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ∧ (𝑋 ∧ 𝑊) = 0 )) → 𝑋 ∈ 𝐴)
Theorem	lhpmat 39205	An element covered by the lattice unity, when conjoined with an atom not under it, equals the lattice zero. (Contributed by NM, 6-Jun-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ∧ 𝑊) = 0 )
Theorem	lhpmatb 39206	An element covered by the lattice unity, when conjoined with an atom, equals zero iff the atom is not under it. (Contributed by NM, 15-Jun-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ∈ 𝐴) → (¬ 𝑃 ≤ 𝑊 ↔ (𝑃 ∧ 𝑊) = 0 ))
Theorem	lhp2at0 39207	Join and meet with different atoms under co-atom 𝑊. (Contributed by NM, 15-Jun-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑈 ≠ 𝑉) ∧ (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) → ((𝑃 ∨ 𝑈) ∧ 𝑉) = 0 )
Theorem	lhp2atnle 39208	Inequality for 2 different atoms under co-atom 𝑊. (Contributed by NM, 17-Jun-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑈 ≠ 𝑉) ∧ (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) → ¬ 𝑉 ≤ (𝑃 ∨ 𝑈))
Theorem	lhp2atne 39209	Inequality for joins with 2 different atoms under co-atom 𝑊. (Contributed by NM, 22-Jul-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ ((𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ 𝑈 ≠ 𝑉) → (𝑃 ∨ 𝑈) ≠ (𝑄 ∨ 𝑉))
Theorem	lhp2at0nle 39210	Inequality for 2 different atoms (or an atom and zero) under co-atom 𝑊. (Contributed by NM, 28-Jul-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑈 ≠ 𝑉) ∧ ((𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) → ¬ 𝑉 ≤ (𝑃 ∨ 𝑈))
Theorem	lhp2at0ne 39211	Inequality for joins with 2 different atoms (or an atom and zero) under co-atom 𝑊. (Contributed by NM, 28-Jul-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (((𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ 𝑈 ≠ 𝑉) → (𝑃 ∨ 𝑈) ≠ (𝑄 ∨ 𝑉))
Theorem	lhpelim 39212	Eliminate an atom not under a lattice hyperplane. TODO: Look at proofs using lhpmat 39205 to see if this can be used to shorten them. (Contributed by NM, 27-Apr-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑋 ∈ 𝐵) → ((𝑃 ∨ (𝑋 ∧ 𝑊)) ∧ 𝑊) = (𝑋 ∧ 𝑊))
Theorem	lhpmod2i2 39213	Modular law for hyperplanes analogous to atmod2i2 39037 for atoms. (Contributed by NM, 9-Feb-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑌 ≤ 𝑋) → ((𝑋 ∧ 𝑊) ∨ 𝑌) = (𝑋 ∧ (𝑊 ∨ 𝑌)))
Theorem	lhpmod6i1 39214	Modular law for hyperplanes analogous to complement of atmod2i1 39036 for atoms. (Contributed by NM, 1-Jun-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑊) → (𝑋 ∨ (𝑌 ∧ 𝑊)) = ((𝑋 ∨ 𝑌) ∧ 𝑊))
Theorem	lhprelat3N 39215*	The Hilbert lattice is relatively atomic with respect to co-atoms (lattice hyperplanes). Dual version of hlrelat3 38587. (Contributed by NM, 20-Jun-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ∃𝑤 ∈ 𝐻 (𝑋 ≤ (𝑌 ∧ 𝑤) ∧ (𝑌 ∧ 𝑤)𝐶𝑌))
Theorem	cdlemb2 39216*	Given two atoms not under the fiducial (reference) co-atom 𝑊, there is a third. Lemma B in [Crawley] p. 112. (Contributed by NM, 30-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ (𝑃 ∨ 𝑄)))
Theorem	lhple 39217	Property of a lattice element under a co-atom. (Contributed by NM, 28-Feb-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → ((𝑃 ∨ 𝑋) ∧ 𝑊) = 𝑋)
Theorem	lhpat 39218	Create an atom under a co-atom. Part of proof of Lemma B in [Crawley] p. 112. (Contributed by NM, 23-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄)) → ((𝑃 ∨ 𝑄) ∧ 𝑊) ∈ 𝐴)
Theorem	lhpat4N 39219	Property of an atom under a co-atom. (Contributed by NM, 24-Nov-2013.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊)) → ((𝑃 ∨ 𝑈) ∧ 𝑊) = 𝑈)
Theorem	lhpat2 39220	Create an atom under a co-atom. Part of proof of Lemma B in [Crawley] p. 112. (Contributed by NM, 21-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑅 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄)) → 𝑅 ∈ 𝐴)
Theorem	lhpat3 39221	There is only one atom under both 𝑃 ∨ 𝑄 and co-atom 𝑊. (Contributed by NM, 21-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑅 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ 𝑆 ≤ (𝑃 ∨ 𝑄))) → (¬ 𝑆 ≤ 𝑊 ↔ 𝑆 ≠ 𝑅))
Theorem	4atexlemk 39222	Lemma for 4atexlem7 39250. (Contributed by NM, 23-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    ⇒   ⊢ (𝜑 → 𝐾 ∈ HL)
Theorem	4atexlemw 39223	Lemma for 4atexlem7 39250. (Contributed by NM, 23-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    ⇒   ⊢ (𝜑 → 𝑊 ∈ 𝐻)
Theorem	4atexlempw 39224	Lemma for 4atexlem7 39250. (Contributed by NM, 23-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    ⇒   ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
Theorem	4atexlemp 39225	Lemma for 4atexlem7 39250. (Contributed by NM, 23-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    ⇒   ⊢ (𝜑 → 𝑃 ∈ 𝐴)
Theorem	4atexlemq 39226	Lemma for 4atexlem7 39250. (Contributed by NM, 23-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    ⇒   ⊢ (𝜑 → 𝑄 ∈ 𝐴)
Theorem	4atexlems 39227	Lemma for 4atexlem7 39250. (Contributed by NM, 23-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    ⇒   ⊢ (𝜑 → 𝑆 ∈ 𝐴)
Theorem	4atexlemt 39228	Lemma for 4atexlem7 39250. (Contributed by NM, 23-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    ⇒   ⊢ (𝜑 → 𝑇 ∈ 𝐴)
Theorem	4atexlemutvt 39229	Lemma for 4atexlem7 39250. (Contributed by NM, 23-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    ⇒   ⊢ (𝜑 → (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))
Theorem	4atexlempnq 39230	Lemma for 4atexlem7 39250. (Contributed by NM, 23-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    ⇒   ⊢ (𝜑 → 𝑃 ≠ 𝑄)
Theorem	4atexlemnslpq 39231	Lemma for 4atexlem7 39250. (Contributed by NM, 23-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    ⇒   ⊢ (𝜑 → ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))
Theorem	4atexlemkl 39232	Lemma for 4atexlem7 39250. (Contributed by NM, 23-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    ⇒   ⊢ (𝜑 → 𝐾 ∈ Lat)
Theorem	4atexlemkc 39233	Lemma for 4atexlem7 39250. (Contributed by NM, 23-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    ⇒   ⊢ (𝜑 → 𝐾 ∈ CvLat)
Theorem	4atexlemwb 39234	Lemma for 4atexlem7 39250. (Contributed by NM, 23-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (𝜑 → 𝑊 ∈ (Base‘𝐾))
Theorem	4atexlempsb 39235	Lemma for 4atexlem7 39250. (Contributed by NM, 23-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (𝜑 → (𝑃 ∨ 𝑆) ∈ (Base‘𝐾))
Theorem	4atexlemqtb 39236	Lemma for 4atexlem7 39250. (Contributed by NM, 24-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (𝜑 → (𝑄 ∨ 𝑇) ∈ (Base‘𝐾))
Theorem	4atexlempns 39237	Lemma for 4atexlem7 39250. (Contributed by NM, 23-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (𝜑 → 𝑃 ≠ 𝑆)
Theorem	4atexlemswapqr 39238	Lemma for 4atexlem7 39250. 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 39239	Lemma for 4atexlem7 39250. (Contributed by NM, 23-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    ⇒   ⊢ (𝜑 → 𝑈 ∈ 𝐴)
Theorem	4atexlemv 39240	Lemma for 4atexlem7 39250. (Contributed by NM, 23-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊)    ⇒   ⊢ (𝜑 → 𝑉 ∈ 𝐴)
Theorem	4atexlemunv 39241	Lemma for 4atexlem7 39250. (Contributed by NM, 21-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊)    ⇒   ⊢ (𝜑 → 𝑈 ≠ 𝑉)
Theorem	4atexlemtlw 39242	Lemma for 4atexlem7 39250. (Contributed by NM, 24-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊)    ⇒   ⊢ (𝜑 → 𝑇 ≤ 𝑊)
Theorem	4atexlemntlpq 39243	Lemma for 4atexlem7 39250. (Contributed by NM, 24-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊)    ⇒   ⊢ (𝜑 → ¬ 𝑇 ≤ (𝑃 ∨ 𝑄))
Theorem	4atexlemc 39244	Lemma for 4atexlem7 39250. (Contributed by NM, 24-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊)    &   ⊢ 𝐶 = ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))    ⇒   ⊢ (𝜑 → 𝐶 ∈ 𝐴)
Theorem	4atexlemnclw 39245	Lemma for 4atexlem7 39250. (Contributed by NM, 24-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊)    &   ⊢ 𝐶 = ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))    ⇒   ⊢ (𝜑 → ¬ 𝐶 ≤ 𝑊)
Theorem	4atexlemex2 39246*	Lemma for 4atexlem7 39250. Show that when 𝐶 ≠ 𝑆, 𝐶 satisfies the existence condition of the consequent. (Contributed by NM, 25-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊)    &   ⊢ 𝐶 = ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))    ⇒   ⊢ ((𝜑 ∧ 𝐶 ≠ 𝑆) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑃 ∨ 𝑧) = (𝑆 ∨ 𝑧)))
Theorem	4atexlemcnd 39247	Lemma for 4atexlem7 39250. (Contributed by NM, 24-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊)    &   ⊢ 𝐶 = ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))    &   ⊢ 𝐷 = ((𝑅 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))    ⇒   ⊢ (𝜑 → 𝐶 ≠ 𝐷)
Theorem	4atexlemex4 39248*	Lemma for 4atexlem7 39250. Show that when 𝐶 = 𝑆, 𝐷 satisfies the existence condition of the consequent. (Contributed by NM, 26-Nov-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊)    &   ⊢ 𝐶 = ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))    &   ⊢ 𝐷 = ((𝑅 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))    ⇒   ⊢ ((𝜑 ∧ 𝐶 = 𝑆) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑃 ∨ 𝑧) = (𝑆 ∨ 𝑧)))
Theorem	4atexlemex6 39249*	Lemma for 4atexlem7 39250. (Contributed by NM, 25-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ ((𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅) ∧ 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑃 ∨ 𝑧) = (𝑆 ∨ 𝑧)))
Theorem	4atexlem7 39250*	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 38517, our (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟) is a shorter way to express 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ (𝑃 ∨ 𝑄). With a longer proof, the condition ¬ 𝑆 ≤ (𝑃 ∨ 𝑄) could be eliminated (see 4atex 39251), although for some purposes this more restricted lemma may be adequate. (Contributed by NM, 25-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑃 ∨ 𝑧) = (𝑆 ∨ 𝑧)))
Theorem	4atex 39251*	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 38517, our (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟) is a shorter way to express 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ (𝑃 ∨ 𝑄). (Contributed by NM, 27-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑃 ∨ 𝑧) = (𝑆 ∨ 𝑧)))
Theorem	4atex2 39252*	More general version of 4atex 39251 for a line 𝑆 ∨ 𝑇 not necessarily connected to 𝑃 ∨ 𝑄. (Contributed by NM, 27-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑇 ∈ 𝐴 ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑆 ∨ 𝑧) = (𝑇 ∨ 𝑧)))
Theorem	4atex2-0aOLDN 39253*	Same as 4atex2 39252 except that 𝑆 is zero. (Contributed by NM, 27-May-2013.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 = (0.‘𝐾)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑆 ∨ 𝑧) = (𝑇 ∨ 𝑧)))
Theorem	4atex2-0bOLDN 39254*	Same as 4atex2 39252 except that 𝑇 is zero. (Contributed by NM, 27-May-2013.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑇 = (0.‘𝐾) ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑆 ∨ 𝑧) = (𝑇 ∨ 𝑧)))
Theorem	4atex2-0cOLDN 39255*	Same as 4atex2 39252 except that 𝑆 and 𝑇 are zero. TODO: do we need this one or 4atex2-0aOLDN 39253 or 4atex2-0bOLDN 39254? (Contributed by NM, 27-May-2013.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 = (0.‘𝐾)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑇 = (0.‘𝐾) ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑆 ∨ 𝑧) = (𝑇 ∨ 𝑧)))
Theorem	4atex3 39256*	More general version of 4atex 39251 for a line 𝑆 ∨ 𝑇 not necessarily connected to 𝑃 ∨ 𝑄. (Contributed by NM, 29-May-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇) ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑧 ≠ 𝑆 ∧ 𝑧 ≠ 𝑇 ∧ 𝑧 ≤ (𝑆 ∨ 𝑇))))
Theorem	lautset 39257*	The set of lattice automorphisms. (Contributed by NM, 11-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐴 → 𝐼 = {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑓‘𝑥) ≤ (𝑓‘𝑦)))})
Theorem	islaut 39258*	The predicate "is a lattice automorphism". (Contributed by NM, 11-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐴 → (𝐹 ∈ 𝐼 ↔ (𝐹:𝐵–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝐹‘𝑥) ≤ (𝐹‘𝑦)))))
Theorem	lautle 39259	Less-than or equal property of a lattice automorphism. (Contributed by NM, 19-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ≤ 𝑌 ↔ (𝐹‘𝑋) ≤ (𝐹‘𝑌)))
Theorem	laut1o 39260	A lattice automorphism is one-to-one and onto. (Contributed by NM, 19-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝐹 ∈ 𝐼) → 𝐹:𝐵–1-1-onto→𝐵)
Theorem	laut11 39261	One-to-one property of a lattice automorphism. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝐹‘𝑋) = (𝐹‘𝑌) ↔ 𝑋 = 𝑌))
Theorem	lautcl 39262	A lattice automorphism value belongs to the base set. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼) ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ 𝐵)
Theorem	lautcnvclN 39263	Reverse closure of a lattice automorphism. (Contributed by NM, 25-May-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼) ∧ 𝑋 ∈ 𝐵) → (◡𝐹‘𝑋) ∈ 𝐵)
Theorem	lautcnvle 39264	Less-than or equal property of lattice automorphism converse. (Contributed by NM, 19-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ≤ 𝑌 ↔ (◡𝐹‘𝑋) ≤ (◡𝐹‘𝑌)))
Theorem	lautcnv 39265	The converse of a lattice automorphism is a lattice automorphism. (Contributed by NM, 10-May-2013.)
⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼) → ◡𝐹 ∈ 𝐼)
Theorem	lautlt 39266	Less-than property of a lattice automorphism. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 < 𝑌 ↔ (𝐹‘𝑋) < (𝐹‘𝑌)))
Theorem	lautcvr 39267	Covering property of a lattice automorphism. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋𝐶𝑌 ↔ (𝐹‘𝑋)𝐶(𝐹‘𝑌)))
Theorem	lautj 39268	Meet property of a lattice automorphism. (Contributed by NM, 25-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(𝑋 ∨ 𝑌)) = ((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
Theorem	lautm 39269	Meet property of a lattice automorphism. (Contributed by NM, 19-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(𝑋 ∧ 𝑌)) = ((𝐹‘𝑋) ∧ (𝐹‘𝑌)))
Theorem	lauteq 39270*	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 39271	The identity function is a lattice automorphism. (Contributed by NM, 18-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐴 → ( I ↾ 𝐵) ∈ 𝐼)
Theorem	lautco 39272	The composition of two lattice automorphisms is a lattice automorphism. (Contributed by NM, 19-Apr-2013.)
⊢ 𝐼 = (LAut‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ∧ 𝐺 ∈ 𝐼) → (𝐹 ∘ 𝐺) ∈ 𝐼)
Theorem	pautsetN 39273*	The set of projective automorphisms. (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.)
⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝑀 = (PAut‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐵 → 𝑀 = {𝑓 ∣ (𝑓:𝑆–1-1-onto→𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 ⊆ 𝑦 ↔ (𝑓‘𝑥) ⊆ (𝑓‘𝑦)))})
Theorem	ispautN 39274*	The predicate "is a projective automorphism". (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.)
⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝑀 = (PAut‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐵 → (𝐹 ∈ 𝑀 ↔ (𝐹:𝑆–1-1-onto→𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 ⊆ 𝑦 ↔ (𝐹‘𝑥) ⊆ (𝐹‘𝑦)))))
Syntax	cldil 39275	Extend class notation with set of all lattice dilations.
class LDil
Syntax	cltrn 39276	Extend class notation with set of all lattice translations.
class LTrn
Syntax	cdilN 39277	Extend class notation with set of all dilations.
class Dil
Syntax	ctrnN 39278	Extend class notation with set of all translations.
class Trn
Definition	df-ldil 39279*	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 39280*	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 39281*	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 39282*	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 39283*	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 39284*	The set of lattice dilations for a fiducial co-atom 𝑊. (Contributed by NM, 11-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    &   ⊢ 𝐷 = ((LDil‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝐶 ∧ 𝑊 ∈ 𝐻) → 𝐷 = {𝑓 ∈ 𝐼 ∣ ∀𝑥 ∈ 𝐵 (𝑥 ≤ 𝑊 → (𝑓‘𝑥) = 𝑥)})
Theorem	isldil 39285*	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 39286	A lattice dilation is an automorphism. (Contributed by NM, 20-May-2012.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    &   ⊢ 𝐷 = ((LDil‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷) → 𝐹 ∈ 𝐼)
Theorem	ldil1o 39287	A lattice dilation is a one-to-one onto function. (Contributed by NM, 19-Apr-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐷 = ((LDil‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷) → 𝐹:𝐵–1-1-onto→𝐵)
Theorem	ldilval 39288	Value of a lattice dilation under its co-atom. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐷 = ((LDil‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷 ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐹‘𝑋) = 𝑋)
Theorem	idldil 39289	The identity function is a lattice dilation. (Contributed by NM, 18-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐷 = ((LDil‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝐵) ∈ 𝐷)
Theorem	ldilcnv 39290	The converse of a lattice dilation is a lattice dilation. (Contributed by NM, 10-May-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐷 = ((LDil‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷) → ◡𝐹 ∈ 𝐷)
Theorem	ldilco 39291	The composition of two lattice automorphisms is a lattice automorphism. (Contributed by NM, 19-Apr-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐷 = ((LDil‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷) → (𝐹 ∘ 𝐺) ∈ 𝐷)
Theorem	ltrnfset 39292*	The set of all lattice translations for a lattice 𝐾. (Contributed by NM, 11-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐶 → (LTrn‘𝐾) = (𝑤 ∈ 𝐻 ↦ {𝑓 ∈ ((LDil‘𝐾)‘𝑤) ∣ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤) → ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑤))}))
Theorem	ltrnset 39293*	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 39294*	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 39295*	The predicate "is a lattice translation". Version of isltrn 39294 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 39296	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 39297	A lattice translation is a lattice dilation. (Contributed by NM, 20-May-2012.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐷 = ((LDil‘𝐾)‘𝑊)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹 ∈ 𝐷)
Theorem	ltrnlaut 39298	A lattice translation is a lattice automorphism. (Contributed by NM, 20-May-2012.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = (LAut‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹 ∈ 𝐼)
Theorem	ltrn1o 39299	A lattice translation is a one-to-one onto function. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹:𝐵–1-1-onto→𝐵)
Theorem	ltrncl 39300	Closure of a lattice translation. (Contributed by NM, 20-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ 𝐵)