P. 403 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 40201-40300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	psubatN 40201	A member of a projective subspace is an atom. (Contributed by NM, 4-Nov-2011.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑋) → 𝑌 ∈ 𝐴)
Theorem	pmapfval 40202*	The projective map of a Hilbert lattice. (Contributed by NM, 2-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐶 → 𝑀 = (𝑥 ∈ 𝐵 ↦ {𝑎 ∈ 𝐴 ∣ 𝑎 ≤ 𝑥}))
Theorem	pmapval 40203*	Value of the projective map of a Hilbert lattice. Definition in Theorem 15.5 of [MaedaMaeda] p. 62. (Contributed by NM, 2-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵) → (𝑀‘𝑋) = {𝑎 ∈ 𝐴 ∣ 𝑎 ≤ 𝑋})
Theorem	elpmap 40204	Member of a projective map. (Contributed by NM, 27-Jan-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵) → (𝑃 ∈ (𝑀‘𝑋) ↔ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑋)))
Theorem	pmapssat 40205	The projective map of a Hilbert lattice is a set of atoms. (Contributed by NM, 14-Jan-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵) → (𝑀‘𝑋) ⊆ 𝐴)
Theorem	pmapssbaN 40206	A weakening of pmapssat 40205 to shorten some proofs. (Contributed by NM, 7-Mar-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵) → (𝑀‘𝑋) ⊆ 𝐵)
Theorem	pmaple 40207	The projective map of a Hilbert lattice preserves ordering. Part of Theorem 15.5 of [MaedaMaeda] p. 62. (Contributed by NM, 22-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ (𝑀‘𝑋) ⊆ (𝑀‘𝑌)))
Theorem	pmap11 40208	The projective map of a Hilbert lattice is one-to-one. Part of Theorem 15.5 of [MaedaMaeda] p. 62. (Contributed by NM, 22-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑀‘𝑋) = (𝑀‘𝑌) ↔ 𝑋 = 𝑌))
Theorem	pmapat 40209	The projective map of an atom. (Contributed by NM, 25-Jan-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴) → (𝑀‘𝑃) = {𝑃})
Theorem	elpmapat 40210	Member of the projective map of an atom. (Contributed by NM, 27-Jan-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴) → (𝑋 ∈ (𝑀‘𝑃) ↔ 𝑋 = 𝑃))
Theorem	pmap0 40211	Value of the projective map of a Hilbert lattice at lattice zero. Part of Theorem 15.5.1 of [MaedaMaeda] p. 62. (Contributed by NM, 17-Oct-2011.)
⊢ 0 = (0.‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ (𝐾 ∈ AtLat → (𝑀‘ 0 ) = ∅)
Theorem	pmapeq0 40212	A projective map value is zero iff its argument is lattice zero. (Contributed by NM, 27-Jan-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → ((𝑀‘𝑋) = ∅ ↔ 𝑋 = 0 ))
Theorem	pmap1N 40213	Value of the projective map of a Hilbert lattice at lattice unity. Part of Theorem 15.5.1 of [MaedaMaeda] p. 62. (Contributed by NM, 22-Oct-2011.) (New usage is discouraged.)
⊢ 1 = (1.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ (𝐾 ∈ OP → (𝑀‘ 1 ) = 𝐴)
Theorem	pmapsub 40214	The projective map of a Hilbert lattice maps to projective subspaces. Part of Theorem 15.5 of [MaedaMaeda] p. 62. (Contributed by NM, 17-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵) → (𝑀‘𝑋) ∈ 𝑆)
Theorem	pmapglbx 40215*	The projective map of the GLB of a set of lattice elements. Index-set version of pmapglb 40216, where we read 𝑆 as 𝑆(𝑖). Theorem 15.5.2 of [MaedaMaeda] p. 62. (Contributed by NM, 5-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅) → (𝑀‘(𝐺‘{𝑦 ∣ ∃𝑖 ∈ 𝐼 𝑦 = 𝑆})) = ∩ 𝑖 ∈ 𝐼 (𝑀‘𝑆))
Theorem	pmapglb 40216*	The projective map of the GLB of a set of lattice elements 𝑆. Variant of Theorem 15.5.2 of [MaedaMaeda] p. 62. (Contributed by NM, 5-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) → (𝑀‘(𝐺‘𝑆)) = ∩ 𝑥 ∈ 𝑆 (𝑀‘𝑥))
Theorem	pmapglb2N 40217*	The projective map of the GLB of a set of lattice elements 𝑆. Variant of Theorem 15.5.2 of [MaedaMaeda] p. 62. Allows 𝑆 = ∅. (Contributed by NM, 21-Jan-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) → (𝑀‘(𝐺‘𝑆)) = (𝐴 ∩ ∩ 𝑥 ∈ 𝑆 (𝑀‘𝑥)))
Theorem	pmapglb2xN 40218*	The projective map of the GLB of a set of lattice elements. Index-set version of pmapglb2N 40217, where we read 𝑆 as 𝑆(𝑖). Extension of Theorem 15.5.2 of [MaedaMaeda] p. 62 that allows 𝐼 = ∅. (Contributed by NM, 21-Jan-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵) → (𝑀‘(𝐺‘{𝑦 ∣ ∃𝑖 ∈ 𝐼 𝑦 = 𝑆})) = (𝐴 ∩ ∩ 𝑖 ∈ 𝐼 (𝑀‘𝑆)))
Theorem	pmapmeet 40219	The projective map of a meet. (Contributed by NM, 25-Jan-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑃 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑃‘(𝑋 ∧ 𝑌)) = ((𝑃‘𝑋) ∩ (𝑃‘𝑌)))
Theorem	isline2 40220*	Definition of line in terms of projective map. (Contributed by NM, 25-Jan-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (Lines‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ (𝐾 ∈ Lat → (𝑋 ∈ 𝑁 ↔ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (𝑝 ≠ 𝑞 ∧ 𝑋 = (𝑀‘(𝑝 ∨ 𝑞)))))
Theorem	linepmap 40221	A line described with a projective map. (Contributed by NM, 3-Feb-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (Lines‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ (((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → (𝑀‘(𝑃 ∨ 𝑄)) ∈ 𝑁)
Theorem	isline3 40222*	Definition of line in terms of original lattice elements. (Contributed by NM, 29-Apr-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (Lines‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → ((𝑀‘𝑋) ∈ 𝑁 ↔ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (𝑝 ≠ 𝑞 ∧ 𝑋 = (𝑝 ∨ 𝑞))))
Theorem	isline4N 40223*	Definition of line in terms of original lattice elements. (Contributed by NM, 16-Jun-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (Lines‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → ((𝑀‘𝑋) ∈ 𝑁 ↔ ∃𝑝 ∈ 𝐴 𝑝𝐶𝑋))
Theorem	lneq2at 40224	A line equals the join of any two of its distinct points (atoms). (Contributed by NM, 29-Apr-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (Lines‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ (𝑀‘𝑋) ∈ 𝑁) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋)) → 𝑋 = (𝑃 ∨ 𝑄))
Theorem	lnatexN 40225*	There is an atom in a line different from any other. (Contributed by NM, 30-Apr-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (Lines‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ (𝑀‘𝑋) ∈ 𝑁) → ∃𝑞 ∈ 𝐴 (𝑞 ≠ 𝑃 ∧ 𝑞 ≤ 𝑋))
Theorem	lnjatN 40226*	Given an atom in a line, there is another atom which when joined equals the line. (Contributed by NM, 30-Apr-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (Lines‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑀‘𝑋) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋)) → ∃𝑞 ∈ 𝐴 (𝑞 ≠ 𝑃 ∧ 𝑋 = (𝑃 ∨ 𝑞)))
Theorem	lncvrelatN 40227	A lattice element covered by a line is an atom. (Contributed by NM, 28-Apr-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (Lines‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ ((𝑀‘𝑋) ∈ 𝑁 ∧ 𝑃𝐶𝑋)) → 𝑃 ∈ 𝐴)
Theorem	lncvrat 40228	A line covers the atoms it contains. (Contributed by NM, 30-Apr-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (Lines‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑀‘𝑋) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋)) → 𝑃𝐶𝑋)
Theorem	lncmp 40229	If two lines are comparable, they are equal. (Contributed by NM, 30-Apr-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑁 = (Lines‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑀‘𝑋) ∈ 𝑁 ∧ (𝑀‘𝑌) ∈ 𝑁)) → (𝑋 ≤ 𝑌 ↔ 𝑋 = 𝑌))
Theorem	2lnat 40230	Two intersecting lines intersect at an atom. (Contributed by NM, 30-Apr-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (Lines‘𝐾)    &   ⊢ 𝐹 = (pmap‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐹‘𝑋) ∈ 𝑁 ∧ (𝐹‘𝑌) ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → (𝑋 ∧ 𝑌) ∈ 𝐴)
Theorem	2atm2atN 40231	Two joins with a common atom have a nonzero meet. (Contributed by NM, 4-Jul-2012.) (New usage is discouraged.)
⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑅 ∨ 𝑃) ∧ (𝑅 ∨ 𝑄)) ≠ 0 )
Theorem	2llnma1b 40232	Generalization of 2llnma1 40233. (Contributed by NM, 26-Apr-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → ((𝑃 ∨ 𝑋) ∧ (𝑃 ∨ 𝑄)) = 𝑃)
Theorem	2llnma1 40233	Two different intersecting lines (expressed in terms of atoms) meet at their common point (atom). (Contributed by NM, 11-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ((𝑄 ∨ 𝑃) ∧ (𝑄 ∨ 𝑅)) = 𝑄)
Theorem	2llnma3r 40234	Two different intersecting lines (expressed in terms of atoms) meet at their common point (atom). (Contributed by NM, 30-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ∨ 𝑅) ≠ (𝑄 ∨ 𝑅)) → ((𝑃 ∨ 𝑅) ∧ (𝑄 ∨ 𝑅)) = 𝑅)
Theorem	2llnma2 40235	Two different intersecting lines (expressed in terms of atoms) meet at their common point (atom). (Contributed by NM, 28-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ((𝑅 ∨ 𝑃) ∧ (𝑅 ∨ 𝑄)) = 𝑅)
Theorem	2llnma2rN 40236	Two different intersecting lines (expressed in terms of atoms) meet at their common point (atom). (Contributed by NM, 2-May-2013.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ((𝑃 ∨ 𝑅) ∧ (𝑄 ∨ 𝑅)) = 𝑅)
21.28.13  Construction of a vector space from a Hilbert lattice
Theorem	cdlema1N 40237	A condition for required for proof of Lemma A in [Crawley] p. 112. (Contributed by NM, 29-Apr-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (Lines‘𝐾)    &   ⊢ 𝐹 = (pmap‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ((𝑅 ≠ 𝑃 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌) ∧ ((𝐹‘𝑌) ∈ 𝑁 ∧ (𝑋 ∧ 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋))) → (𝑋 ∨ 𝑅) = (𝑋 ∨ 𝑌))
Theorem	cdlema2N 40238	A condition for required for proof of Lemma A in [Crawley] p. 112. (Contributed by NM, 9-May-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ((𝑅 ≠ 𝑃 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋))) → (𝑅 ∧ 𝑋) = 0 )
Theorem	cdlemblem 40239	Lemma for cdlemb 40240. (Contributed by NM, 8-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑄) ∧ 𝑋)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋)) ∧ (𝑢 ∈ 𝐴 ∧ (𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ (𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ (𝑃 ∨ 𝑢)))) → (¬ 𝑟 ≤ 𝑋 ∧ ¬ 𝑟 ≤ (𝑃 ∨ 𝑄)))
Theorem	cdlemb 40240*	Given two atoms not less than or equal to an element covered by 1, there is a third. Lemma B in [Crawley] p. 112. (Contributed by NM, 8-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋)) → ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑋 ∧ ¬ 𝑟 ≤ (𝑃 ∨ 𝑄)))
Syntax	cpadd 40241	Extend class notation with projective subspace sum.
class +𝑃
Definition	df-padd 40242*	Define projective sum of two subspaces (or more generally two sets of atoms), which is the union of all lines generated by pairs of atoms from each subspace. Lemma 16.2 of [MaedaMaeda] p. 68. For convenience, our definition is generalized to apply to empty sets. (Contributed by NM, 29-Dec-2011.)
⊢ +𝑃 = (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙), 𝑛 ∈ 𝒫 (Atoms‘𝑙) ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)})))
Theorem	paddfval 40243*	Projective subspace sum operation. (Contributed by NM, 29-Dec-2011.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐵 → + = (𝑚 ∈ 𝒫 𝐴, 𝑛 ∈ 𝒫 𝐴 ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟)})))
Theorem	paddval 40244*	Projective subspace sum operation value. (Contributed by NM, 29-Dec-2011.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 + 𝑌) = ((𝑋 ∪ 𝑌) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝 ≤ (𝑞 ∨ 𝑟)}))
Theorem	elpadd 40245*	Member of a projective subspace sum. (Contributed by NM, 29-Dec-2011.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑆 ∈ (𝑋 + 𝑌) ↔ ((𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌) ∨ (𝑆 ∈ 𝐴 ∧ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑆 ≤ (𝑞 ∨ 𝑟)))))
Theorem	elpaddn0 40246*	Member of projective subspace sum of nonempty sets. (Contributed by NM, 3-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → (𝑆 ∈ (𝑋 + 𝑌) ↔ (𝑆 ∈ 𝐴 ∧ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑆 ≤ (𝑞 ∨ 𝑟))))
Theorem	paddvaln0N 40247*	Projective subspace sum operation value for nonempty sets. (Contributed by NM, 27-Jan-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → (𝑋 + 𝑌) = {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝 ≤ (𝑞 ∨ 𝑟)})
Theorem	elpaddri 40248	Condition implying membership in a projective subspace sum. (Contributed by NM, 8-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑄 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌) ∧ (𝑆 ∈ 𝐴 ∧ 𝑆 ≤ (𝑄 ∨ 𝑅))) → 𝑆 ∈ (𝑋 + 𝑌))
Theorem	elpaddatriN 40249	Condition implying membership in a projective subspace sum with a point. (Contributed by NM, 1-Feb-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝐴 ∧ 𝑆 ≤ (𝑅 ∨ 𝑄))) → 𝑆 ∈ (𝑋 + {𝑄}))
Theorem	elpaddat 40250*	Membership in a projective subspace sum with a point. (Contributed by NM, 29-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑋 ≠ ∅) → (𝑆 ∈ (𝑋 + {𝑄}) ↔ (𝑆 ∈ 𝐴 ∧ ∃𝑝 ∈ 𝑋 𝑆 ≤ (𝑝 ∨ 𝑄))))
Theorem	elpaddatiN 40251*	Consequence of membership in a projective subspace sum with a point. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑅 ∈ (𝑋 + {𝑄}))) → ∃𝑝 ∈ 𝑋 𝑅 ≤ (𝑝 ∨ 𝑄))
Theorem	elpadd2at 40252	Membership in a projective subspace sum of two points. (Contributed by NM, 29-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) → (𝑆 ∈ ({𝑄} + {𝑅}) ↔ (𝑆 ∈ 𝐴 ∧ 𝑆 ≤ (𝑄 ∨ 𝑅))))
Theorem	elpadd2at2 40253	Membership in a projective subspace sum of two points. (Contributed by NM, 8-Mar-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → (𝑆 ∈ ({𝑄} + {𝑅}) ↔ 𝑆 ≤ (𝑄 ∨ 𝑅)))
Theorem	paddunssN 40254	Projective subspace sum includes the set union of its arguments. (Contributed by NM, 12-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 ∪ 𝑌) ⊆ (𝑋 + 𝑌))
Theorem	elpadd0 40255	Member of projective subspace sum with at least one empty set. (Contributed by NM, 29-Dec-2011.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ ¬ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → (𝑆 ∈ (𝑋 + 𝑌) ↔ (𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌)))
Theorem	paddval0 40256	Projective subspace sum with at least one empty set. (Contributed by NM, 11-Jan-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ ¬ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → (𝑋 + 𝑌) = (𝑋 ∪ 𝑌))
Theorem	padd01 40257	Projective subspace sum with an empty set. (Contributed by NM, 11-Jan-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴) → (𝑋 + ∅) = 𝑋)
Theorem	padd02 40258	Projective subspace sum with an empty set. (Contributed by NM, 11-Jan-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴) → (∅ + 𝑋) = 𝑋)
Theorem	paddcom 40259	Projective subspace sum commutes. (Contributed by NM, 3-Jan-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
Theorem	paddssat 40260	A projective subspace sum is a set of atoms. (Contributed by NM, 3-Jan-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 + 𝑌) ⊆ 𝐴)
Theorem	sspadd1 40261	A projective subspace sum is a superset of its first summand. (ssun1 4119 analog.) (Contributed by NM, 3-Jan-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → 𝑋 ⊆ (𝑋 + 𝑌))
Theorem	sspadd2 40262	A projective subspace sum is a superset of its second summand. (ssun2 4120 analog.) (Contributed by NM, 3-Jan-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → 𝑋 ⊆ (𝑌 + 𝑋))
Theorem	paddss1 40263	Subset law for projective subspace sum. (unss1 4126 analog.) (Contributed by NM, 7-Mar-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) → (𝑋 ⊆ 𝑌 → (𝑋 + 𝑍) ⊆ (𝑌 + 𝑍)))
Theorem	paddss2 40264	Subset law for projective subspace sum. (unss2 4128 analog.) (Contributed by NM, 7-Mar-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) → (𝑋 ⊆ 𝑌 → (𝑍 + 𝑋) ⊆ (𝑍 + 𝑌)))
Theorem	paddss12 40265	Subset law for projective subspace sum. (unss12 4129 analog.) (Contributed by NM, 7-Mar-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴) → ((𝑋 ⊆ 𝑌 ∧ 𝑍 ⊆ 𝑊) → (𝑋 + 𝑍) ⊆ (𝑌 + 𝑊)))
Theorem	paddasslem1 40266	Lemma for paddass 40284. (Contributed by NM, 8-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≠ 𝑦) ∧ ¬ 𝑟 ≤ (𝑥 ∨ 𝑦)) → ¬ 𝑥 ≤ (𝑟 ∨ 𝑦))
Theorem	paddasslem2 40267	Lemma for paddass 40284. (Contributed by NM, 8-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧))) → 𝑧 ≤ (𝑟 ∨ 𝑦))
Theorem	paddasslem3 40268*	Lemma for paddass 40284. Restate projective space axiom ps-2 39924. (Contributed by NM, 8-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑥 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (((¬ 𝑥 ≤ (𝑟 ∨ 𝑦) ∧ 𝑝 ≠ 𝑧) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑧 ≤ (𝑟 ∨ 𝑦))) → ∃𝑠 ∈ 𝐴 (𝑠 ≤ (𝑥 ∨ 𝑦) ∧ 𝑠 ≤ (𝑝 ∨ 𝑧))))
Theorem	paddasslem4 40269*	Lemma for paddass 40284. Combine paddasslem1 40266, paddasslem2 40267, and paddasslem3 40268. (Contributed by NM, 8-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ∧ ¬ 𝑟 ≤ (𝑥 ∨ 𝑦))) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧))) → ∃𝑠 ∈ 𝐴 (𝑠 ≤ (𝑥 ∨ 𝑦) ∧ 𝑠 ≤ (𝑝 ∨ 𝑧)))
Theorem	paddasslem5 40270	Lemma for paddass 40284. Show 𝑠 ≠ 𝑧 by contradiction. (Contributed by NM, 8-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧) ∧ 𝑠 ≤ (𝑥 ∨ 𝑦))) → 𝑠 ≠ 𝑧)
Theorem	paddasslem6 40271	Lemma for paddass 40284. (Contributed by NM, 8-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ (𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ (𝑠 ≠ 𝑧 ∧ 𝑠 ≤ (𝑝 ∨ 𝑧))) → 𝑝 ≤ (𝑠 ∨ 𝑧))
Theorem	paddasslem7 40272	Lemma for paddass 40284. Combine paddasslem5 40270 and paddasslem6 40271. (Contributed by NM, 9-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧) ∧ 𝑠 ≤ (𝑥 ∨ 𝑦)) ∧ 𝑠 ≤ (𝑝 ∨ 𝑧))) → 𝑝 ≤ (𝑠 ∨ 𝑧))
Theorem	paddasslem8 40273	Lemma for paddass 40284. (Contributed by NM, 8-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ 𝑠 ≤ (𝑥 ∨ 𝑦) ∧ 𝑝 ≤ (𝑠 ∨ 𝑧))) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍))
Theorem	paddasslem9 40274	Lemma for paddass 40284. Combine paddasslem7 40272 and paddasslem8 40273. (Contributed by NM, 9-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)) ∧ (𝑠 ∈ 𝐴 ∧ 𝑠 ≤ (𝑥 ∨ 𝑦) ∧ 𝑠 ≤ (𝑝 ∨ 𝑧)))) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍))
Theorem	paddasslem10 40275	Lemma for paddass 40284. Use paddasslem4 40269 to eliminate 𝑠 from paddasslem9 40274. (Contributed by NM, 9-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍))
Theorem	paddasslem11 40276	Lemma for paddass 40284. The case when 𝑝 = 𝑧. (Contributed by NM, 11-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑝 = 𝑧) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) ∧ 𝑧 ∈ 𝑍) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍))
Theorem	paddasslem12 40277	Lemma for paddass 40284. The case when 𝑥 = 𝑦. (Contributed by NM, 11-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍))
Theorem	paddasslem13 40278	Lemma for paddass 40284. The case when 𝑟 ≤ (𝑥 ∨ 𝑦). (Unlike the proof in Maeda and Maeda, we don't need 𝑥 ≠ 𝑦.) (Contributed by NM, 11-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) ∧ (𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑝 ≤ (𝑥 ∨ 𝑟)))) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍))
Theorem	paddasslem14 40279	Lemma for paddass 40284. Remove 𝑝 ≠ 𝑧, 𝑥 ≠ 𝑦, and ¬ 𝑟 ≤ (𝑥 ∨ 𝑦) from antecedent of paddasslem10 40275, using paddasslem11 40276, paddasslem12 40277, and paddasslem13 40278. (Contributed by NM, 11-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍))
Theorem	paddasslem15 40280	Lemma for paddass 40284. Use elpaddn0 40246 to eliminate 𝑦 and 𝑧 from paddasslem14 40279. (Contributed by NM, 11-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅)) ∧ (𝑝 ∈ 𝐴 ∧ (𝑥 ∈ 𝑋 ∧ 𝑟 ∈ (𝑌 + 𝑍)) ∧ 𝑝 ≤ (𝑥 ∨ 𝑟))) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍))
Theorem	paddasslem16 40281	Lemma for paddass 40284. Use elpaddn0 40246 to eliminate 𝑥 and 𝑟 from paddasslem15 40280. (Contributed by NM, 11-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍))
Theorem	paddasslem17 40282	Lemma for paddass 40284. The case when at least one sum argument is empty. (Contributed by NM, 12-Jan-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ¬ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍))
Theorem	paddasslem18 40283	Lemma for paddass 40284. Combine paddasslem16 40281 and paddasslem17 40282. (Contributed by NM, 12-Jan-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍))
Theorem	paddass 40284	Projective subspace sum is associative. Equation 16.2.1 of [MaedaMaeda] p. 68. In our version, the subspaces do not have to be nonempty. (Contributed by NM, 29-Dec-2011.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
Theorem	padd12N 40285	Commutative/associative law for projective subspace sum. (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 + (𝑌 + 𝑍)) = (𝑌 + (𝑋 + 𝑍)))
Theorem	padd4N 40286	Rearrangement of 4 terms in a projective subspace sum. (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴)) → ((𝑋 + 𝑌) + (𝑍 + 𝑊)) = ((𝑋 + 𝑍) + (𝑌 + 𝑊)))
Theorem	paddidm 40287	Projective subspace sum is idempotent. Part of Lemma 16.2 of [MaedaMaeda] p. 68. (Contributed by NM, 13-Jan-2012.)
⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝑆) → (𝑋 + 𝑋) = 𝑋)
Theorem	paddclN 40288	The projective sum of two subspaces is a subspace. Part of Lemma 16.2 of [MaedaMaeda] p. 68. (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.)
⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝑋 + 𝑌) ∈ 𝑆)
Theorem	paddssw1 40289	Subset law for projective subspace sum valid for all subsets of atoms. (Contributed by NM, 14-Mar-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((𝑋 ⊆ 𝑍 ∧ 𝑌 ⊆ 𝑍) → (𝑋 + 𝑌) ⊆ (𝑍 + 𝑍)))
Theorem	paddssw2 40290	Subset law for projective subspace sum valid for all subsets of atoms. (Contributed by NM, 14-Mar-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((𝑋 + 𝑌) ⊆ 𝑍 → (𝑋 ⊆ 𝑍 ∧ 𝑌 ⊆ 𝑍)))
Theorem	paddss 40291	Subset law for projective subspace sum. (unss 4131 analog.) (Contributed by NM, 7-Mar-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆)) → ((𝑋 ⊆ 𝑍 ∧ 𝑌 ⊆ 𝑍) ↔ (𝑋 + 𝑌) ⊆ 𝑍))
Theorem	pmodlem1 40292*	Lemma for pmod1i 40294. (Contributed by NM, 9-Mar-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) → 𝑝 ∈ (𝑋 + (𝑌 ∩ 𝑍)))
Theorem	pmodlem2 40293	Lemma for pmod1i 40294. (Contributed by NM, 9-Mar-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆) ∧ 𝑋 ⊆ 𝑍) → ((𝑋 + 𝑌) ∩ 𝑍) ⊆ (𝑋 + (𝑌 ∩ 𝑍)))
Theorem	pmod1i 40294	The modular law holds in a projective subspace. (Contributed by NM, 10-Mar-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆)) → (𝑋 ⊆ 𝑍 → ((𝑋 + 𝑌) ∩ 𝑍) = (𝑋 + (𝑌 ∩ 𝑍))))
Theorem	pmod2iN 40295	Dual of the modular law. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑍 ⊆ 𝑋 → ((𝑋 ∩ 𝑌) + 𝑍) = (𝑋 ∩ (𝑌 + 𝑍))))
Theorem	pmodN 40296	The modular law for projective subspaces. (Contributed by NM, 26-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 ∩ (𝑌 + (𝑋 ∩ 𝑍))) = ((𝑋 ∩ 𝑌) + (𝑋 ∩ 𝑍)))
Theorem	pmodl42N 40297	Lemma derived from modular law. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.)
⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆)) → (((𝑋 + 𝑌) + 𝑍) ∩ ((𝑋 + 𝑌) + 𝑊)) = ((𝑋 + 𝑌) + ((𝑋 + 𝑍) ∩ (𝑌 + 𝑊))))
Theorem	pmapjoin 40298	The projective map of the join of two lattice elements. Part of Equation 15.5.3 of [MaedaMaeda] p. 63. (Contributed by NM, 27-Jan-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑀‘𝑋) + (𝑀‘𝑌)) ⊆ (𝑀‘(𝑋 ∨ 𝑌)))
Theorem	pmapjat1 40299	The projective map of the join of a lattice element and an atom. (Contributed by NM, 28-Jan-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴) → (𝑀‘(𝑋 ∨ 𝑄)) = ((𝑀‘𝑋) + (𝑀‘𝑄)))
Theorem	pmapjat2 40300	The projective map of the join of an atom with a lattice element. (Contributed by NM, 12-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴) → (𝑀‘(𝑄 ∨ 𝑋)) = ((𝑀‘𝑄) + (𝑀‘𝑋)))