![]() |
Metamath
Proof Explorer Theorem List (p. 360 of 437) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28351) |
![]() (28352-29876) |
![]() (29877-43667) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ispointN 35901* | The predicate "is a point". (Contributed by NM, 2-Oct-2011.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑃 = (Points‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐷 → (𝑋 ∈ 𝑃 ↔ ∃𝑎 ∈ 𝐴 𝑋 = {𝑎})) | ||
Theorem | atpointN 35902 | The singleton of an atom is a point. (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑃 = (Points‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐴) → {𝑋} ∈ 𝑃) | ||
Theorem | psubspset 35903* | The set of projective subspaces in a Hilbert lattice. (Contributed by NM, 2-Oct-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐵 → 𝑆 = {𝑠 ∣ (𝑠 ⊆ 𝐴 ∧ ∀𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ∀𝑟 ∈ 𝐴 (𝑟 ≤ (𝑝 ∨ 𝑞) → 𝑟 ∈ 𝑠))}) | ||
Theorem | ispsubsp 35904* | The predicate "is a projective subspace". (Contributed by NM, 2-Oct-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐷 → (𝑋 ∈ 𝑆 ↔ (𝑋 ⊆ 𝐴 ∧ ∀𝑝 ∈ 𝑋 ∀𝑞 ∈ 𝑋 ∀𝑟 ∈ 𝐴 (𝑟 ≤ (𝑝 ∨ 𝑞) → 𝑟 ∈ 𝑋)))) | ||
Theorem | ispsubsp2 35905* | The predicate "is a projective subspace". (Contributed by NM, 13-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐷 → (𝑋 ∈ 𝑆 ↔ (𝑋 ⊆ 𝐴 ∧ ∀𝑝 ∈ 𝐴 (∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑋 𝑝 ≤ (𝑞 ∨ 𝑟) → 𝑝 ∈ 𝑋)))) | ||
Theorem | psubspi 35906* | Property of a projective subspace. (Contributed by NM, 13-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ (((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ∧ 𝑃 ∈ 𝐴) ∧ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑋 𝑃 ≤ (𝑞 ∨ 𝑟)) → 𝑃 ∈ 𝑋) | ||
Theorem | psubspi2N 35907 | Property of a projective subspace. (Contributed by NM, 13-Jan-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ (((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ∧ 𝑃 ∈ 𝐴) ∧ (𝑄 ∈ 𝑋 ∧ 𝑅 ∈ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑅))) → 𝑃 ∈ 𝑋) | ||
Theorem | 0psubN 35908 | The empty set is a projective subspace. Remark below Definition 15.1 of [MaedaMaeda] p. 61. (Contributed by NM, 13-Oct-2011.) (New usage is discouraged.) |
⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → ∅ ∈ 𝑆) | ||
Theorem | snatpsubN 35909 | The singleton of an atom is a projective subspace. (Contributed by NM, 9-Sep-2013.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) → {𝑃} ∈ 𝑆) | ||
Theorem | pointpsubN 35910 | A point (singleton of an atom) is a projective subspace. Remark below Definition 15.1 of [MaedaMaeda] p. 61. (Contributed by NM, 13-Oct-2011.) (New usage is discouraged.) |
⊢ 𝑃 = (Points‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝑃) → 𝑋 ∈ 𝑆) | ||
Theorem | linepsubN 35911 | A line is a projective subspace. (Contributed by NM, 16-Oct-2011.) (New usage is discouraged.) |
⊢ 𝑁 = (Lines‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝑁) → 𝑋 ∈ 𝑆) | ||
Theorem | atpsubN 35912 | The set of all atoms is a projective subspace. Remark below Definition 15.1 of [MaedaMaeda] p. 61. (Contributed by NM, 13-Oct-2011.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → 𝐴 ∈ 𝑆) | ||
Theorem | psubssat 35913 | A projective subspace consists of atoms. (Contributed by NM, 4-Nov-2011.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝑆) → 𝑋 ⊆ 𝐴) | ||
Theorem | psubatN 35914 | A member of a projective subspace is an atom. (Contributed by NM, 4-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑋) → 𝑌 ∈ 𝐴) | ||
Theorem | pmapfval 35915* | The projective map of a Hilbert lattice. (Contributed by NM, 2-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐶 → 𝑀 = (𝑥 ∈ 𝐵 ↦ {𝑎 ∈ 𝐴 ∣ 𝑎 ≤ 𝑥})) | ||
Theorem | pmapval 35916* | 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 35917 | Member of a projective map. (Contributed by NM, 27-Jan-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵) → (𝑃 ∈ (𝑀‘𝑋) ↔ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑋))) | ||
Theorem | pmapssat 35918 | The projective map of a Hilbert lattice is a set of atoms. (Contributed by NM, 14-Jan-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵) → (𝑀‘𝑋) ⊆ 𝐴) | ||
Theorem | pmapssbaN 35919 | A weakening of pmapssat 35918 to shorten some proofs. (Contributed by NM, 7-Mar-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵) → (𝑀‘𝑋) ⊆ 𝐵) | ||
Theorem | pmaple 35920 | 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 35921 | 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 35922 | The projective map of an atom. (Contributed by NM, 25-Jan-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴) → (𝑀‘𝑃) = {𝑃}) | ||
Theorem | elpmapat 35923 | Member of the projective map of an atom. (Contributed by NM, 27-Jan-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴) → (𝑋 ∈ (𝑀‘𝑃) ↔ 𝑋 = 𝑃)) | ||
Theorem | pmap0 35924 | 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 35925 | 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 35926 | Value of the projective map of a Hilbert lattice at lattice unit. 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 35927 | 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 35928* | The projective map of the GLB of a set of lattice elements. Index-set version of pmapglb 35929, where we read 𝑆 as 𝑆(𝑖). Theorem 15.5.2 of [MaedaMaeda] p. 62. (Contributed by NM, 5-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅) → (𝑀‘(𝐺‘{𝑦 ∣ ∃𝑖 ∈ 𝐼 𝑦 = 𝑆})) = ∩ 𝑖 ∈ 𝐼 (𝑀‘𝑆)) | ||
Theorem | pmapglb 35929* | 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 35930* | 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 35931* | The projective map of the GLB of a set of lattice elements. Index-set version of pmapglb2N 35930, 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 35932 | The projective map of a meet. (Contributed by NM, 25-Jan-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑃 = (pmap‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑃‘(𝑋 ∧ 𝑌)) = ((𝑃‘𝑋) ∩ (𝑃‘𝑌))) | ||
Theorem | isline2 35933* | Definition of line in terms of projective map. (Contributed by NM, 25-Jan-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑁 = (Lines‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ (𝐾 ∈ Lat → (𝑋 ∈ 𝑁 ↔ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (𝑝 ≠ 𝑞 ∧ 𝑋 = (𝑀‘(𝑝 ∨ 𝑞))))) | ||
Theorem | linepmap 35934 | A line described with a projective map. (Contributed by NM, 3-Feb-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑁 = (Lines‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ (((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → (𝑀‘(𝑃 ∨ 𝑄)) ∈ 𝑁) | ||
Theorem | isline3 35935* | Definition of line in terms of original lattice elements. (Contributed by NM, 29-Apr-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑁 = (Lines‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → ((𝑀‘𝑋) ∈ 𝑁 ↔ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (𝑝 ≠ 𝑞 ∧ 𝑋 = (𝑝 ∨ 𝑞)))) | ||
Theorem | isline4N 35936* | 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 35937 | 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 35938* | 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 35939* | 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 35940 | 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 35941 | A line covers the atoms it contains. (Contributed by NM, 30-Apr-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑁 = (Lines‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑀‘𝑋) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋)) → 𝑃𝐶𝑋) | ||
Theorem | lncmp 35942 | If two lines are comparable, they are equal. (Contributed by NM, 30-Apr-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑁 = (Lines‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑀‘𝑋) ∈ 𝑁 ∧ (𝑀‘𝑌) ∈ 𝑁)) → (𝑋 ≤ 𝑌 ↔ 𝑋 = 𝑌)) | ||
Theorem | 2lnat 35943 | Two intersecting lines intersect at an atom. (Contributed by NM, 30-Apr-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑁 = (Lines‘𝐾) & ⊢ 𝐹 = (pmap‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐹‘𝑋) ∈ 𝑁 ∧ (𝐹‘𝑌) ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → (𝑋 ∧ 𝑌) ∈ 𝐴) | ||
Theorem | 2atm2atN 35944 | 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 35945 | Generalization of 2llnma1 35946. (Contributed by NM, 26-Apr-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → ((𝑃 ∨ 𝑋) ∧ (𝑃 ∨ 𝑄)) = 𝑃) | ||
Theorem | 2llnma1 35946 | 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 35947 | 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 35948 | 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 35949 | 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 ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ((𝑃 ∨ 𝑅) ∧ (𝑄 ∨ 𝑅)) = 𝑅) | ||
Theorem | cdlema1N 35950 | 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 35951 | 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 35952 | Lemma for cdlemb 35953. (Contributed by NM, 8-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑉 = ((𝑃 ∨ 𝑄) ∧ 𝑋) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋)) ∧ (𝑢 ∈ 𝐴 ∧ (𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ (𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ (𝑃 ∨ 𝑢)))) → (¬ 𝑟 ≤ 𝑋 ∧ ¬ 𝑟 ≤ (𝑃 ∨ 𝑄))) | ||
Theorem | cdlemb 35953* | 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 35954 | Extend class notation with projective subspace sum. |
class +𝑃 | ||
Definition | df-padd 35955* | 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 35956* | Projective subspace sum operation. (Contributed by NM, 29-Dec-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐵 → + = (𝑚 ∈ 𝒫 𝐴, 𝑛 ∈ 𝒫 𝐴 ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟)}))) | ||
Theorem | paddval 35957* | Projective subspace sum operation value. (Contributed by NM, 29-Dec-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 + 𝑌) = ((𝑋 ∪ 𝑌) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝 ≤ (𝑞 ∨ 𝑟)})) | ||
Theorem | elpadd 35958* | Member of a projective subspace sum. (Contributed by NM, 29-Dec-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑆 ∈ (𝑋 + 𝑌) ↔ ((𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌) ∨ (𝑆 ∈ 𝐴 ∧ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑆 ≤ (𝑞 ∨ 𝑟))))) | ||
Theorem | elpaddn0 35959* | Member of projective subspace sum of nonempty sets. (Contributed by NM, 3-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → (𝑆 ∈ (𝑋 + 𝑌) ↔ (𝑆 ∈ 𝐴 ∧ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑆 ≤ (𝑞 ∨ 𝑟)))) | ||
Theorem | paddvaln0N 35960* | Projective subspace sum operation value for nonempty sets. (Contributed by NM, 27-Jan-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → (𝑋 + 𝑌) = {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝 ≤ (𝑞 ∨ 𝑟)}) | ||
Theorem | elpaddri 35961 | Condition implying membership in a projective subspace sum. (Contributed by NM, 8-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑄 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌) ∧ (𝑆 ∈ 𝐴 ∧ 𝑆 ≤ (𝑄 ∨ 𝑅))) → 𝑆 ∈ (𝑋 + 𝑌)) | ||
Theorem | elpaddatriN 35962 | 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 35963* | Membership in a projective subspace sum with a point. (Contributed by NM, 29-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑋 ≠ ∅) → (𝑆 ∈ (𝑋 + {𝑄}) ↔ (𝑆 ∈ 𝐴 ∧ ∃𝑝 ∈ 𝑋 𝑆 ≤ (𝑝 ∨ 𝑄)))) | ||
Theorem | elpaddatiN 35964* | 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 35965 | Membership in a projective subspace sum of two points. (Contributed by NM, 29-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) → (𝑆 ∈ ({𝑄} + {𝑅}) ↔ (𝑆 ∈ 𝐴 ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)))) | ||
Theorem | elpadd2at2 35966 | Membership in a projective subspace sum of two points. (Contributed by NM, 8-Mar-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → (𝑆 ∈ ({𝑄} + {𝑅}) ↔ 𝑆 ≤ (𝑄 ∨ 𝑅))) | ||
Theorem | paddunssN 35967 | Projective subspace sum includes the set union of its arguments. (Contributed by NM, 12-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 ∪ 𝑌) ⊆ (𝑋 + 𝑌)) | ||
Theorem | elpadd0 35968 | Member of projective subspace sum with at least one empty set. (Contributed by NM, 29-Dec-2011.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ ¬ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → (𝑆 ∈ (𝑋 + 𝑌) ↔ (𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌))) | ||
Theorem | paddval0 35969 | Projective subspace sum with at least one empty set. (Contributed by NM, 11-Jan-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ ¬ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → (𝑋 + 𝑌) = (𝑋 ∪ 𝑌)) | ||
Theorem | padd01 35970 | Projective subspace sum with an empty set. (Contributed by NM, 11-Jan-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴) → (𝑋 + ∅) = 𝑋) | ||
Theorem | padd02 35971 | Projective subspace sum with an empty set. (Contributed by NM, 11-Jan-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴) → (∅ + 𝑋) = 𝑋) | ||
Theorem | paddcom 35972 | Projective subspace sum commutes. (Contributed by NM, 3-Jan-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 + 𝑌) = (𝑌 + 𝑋)) | ||
Theorem | paddssat 35973 | A projective subspace sum is a set of atoms. (Contributed by NM, 3-Jan-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 + 𝑌) ⊆ 𝐴) | ||
Theorem | sspadd1 35974 | A projective subspace sum is a superset of its first summand. (ssun1 3999 analog.) (Contributed by NM, 3-Jan-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → 𝑋 ⊆ (𝑋 + 𝑌)) | ||
Theorem | sspadd2 35975 | A projective subspace sum is a superset of its second summand. (ssun2 4000 analog.) (Contributed by NM, 3-Jan-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → 𝑋 ⊆ (𝑌 + 𝑋)) | ||
Theorem | paddss1 35976 | Subset law for projective subspace sum. (unss1 4005 analog.) (Contributed by NM, 7-Mar-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) → (𝑋 ⊆ 𝑌 → (𝑋 + 𝑍) ⊆ (𝑌 + 𝑍))) | ||
Theorem | paddss2 35977 | Subset law for projective subspace sum. (unss2 4007 analog.) (Contributed by NM, 7-Mar-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) → (𝑋 ⊆ 𝑌 → (𝑍 + 𝑋) ⊆ (𝑍 + 𝑌))) | ||
Theorem | paddss12 35978 | Subset law for projective subspace sum. (unss12 4008 analog.) (Contributed by NM, 7-Mar-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴) → ((𝑋 ⊆ 𝑌 ∧ 𝑍 ⊆ 𝑊) → (𝑋 + 𝑍) ⊆ (𝑌 + 𝑊))) | ||
Theorem | paddasslem1 35979 | Lemma for paddass 35997. (Contributed by NM, 8-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≠ 𝑦) ∧ ¬ 𝑟 ≤ (𝑥 ∨ 𝑦)) → ¬ 𝑥 ≤ (𝑟 ∨ 𝑦)) | ||
Theorem | paddasslem2 35980 | Lemma for paddass 35997. (Contributed by NM, 8-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧))) → 𝑧 ≤ (𝑟 ∨ 𝑦)) | ||
Theorem | paddasslem3 35981* | Lemma for paddass 35997. Restate projective space axiom ps-2 35637. (Contributed by NM, 8-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑥 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (((¬ 𝑥 ≤ (𝑟 ∨ 𝑦) ∧ 𝑝 ≠ 𝑧) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑧 ≤ (𝑟 ∨ 𝑦))) → ∃𝑠 ∈ 𝐴 (𝑠 ≤ (𝑥 ∨ 𝑦) ∧ 𝑠 ≤ (𝑝 ∨ 𝑧)))) | ||
Theorem | paddasslem4 35982* | Lemma for paddass 35997. Combine paddasslem1 35979, paddasslem2 35980, and paddasslem3 35981. (Contributed by NM, 8-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ∧ ¬ 𝑟 ≤ (𝑥 ∨ 𝑦))) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧))) → ∃𝑠 ∈ 𝐴 (𝑠 ≤ (𝑥 ∨ 𝑦) ∧ 𝑠 ≤ (𝑝 ∨ 𝑧))) | ||
Theorem | paddasslem5 35983 | Lemma for paddass 35997. Show 𝑠 ≠ 𝑧 by contradiction. (Contributed by NM, 8-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧) ∧ 𝑠 ≤ (𝑥 ∨ 𝑦))) → 𝑠 ≠ 𝑧) | ||
Theorem | paddasslem6 35984 | Lemma for paddass 35997. (Contributed by NM, 8-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ (𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ (𝑠 ≠ 𝑧 ∧ 𝑠 ≤ (𝑝 ∨ 𝑧))) → 𝑝 ≤ (𝑠 ∨ 𝑧)) | ||
Theorem | paddasslem7 35985 | Lemma for paddass 35997. Combine paddasslem5 35983 and paddasslem6 35984. (Contributed by NM, 9-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧) ∧ 𝑠 ≤ (𝑥 ∨ 𝑦)) ∧ 𝑠 ≤ (𝑝 ∨ 𝑧))) → 𝑝 ≤ (𝑠 ∨ 𝑧)) | ||
Theorem | paddasslem8 35986 | Lemma for paddass 35997. (Contributed by NM, 8-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ 𝑠 ≤ (𝑥 ∨ 𝑦) ∧ 𝑝 ≤ (𝑠 ∨ 𝑧))) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍)) | ||
Theorem | paddasslem9 35987 | Lemma for paddass 35997. Combine paddasslem7 35985 and paddasslem8 35986. (Contributed by NM, 9-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)) ∧ (𝑠 ∈ 𝐴 ∧ 𝑠 ≤ (𝑥 ∨ 𝑦) ∧ 𝑠 ≤ (𝑝 ∨ 𝑧)))) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍)) | ||
Theorem | paddasslem10 35988 | Lemma for paddass 35997. Use paddasslem4 35982 to eliminate 𝑠 from paddasslem9 35987. (Contributed by NM, 9-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍)) | ||
Theorem | paddasslem11 35989 | Lemma for paddass 35997. The case when 𝑝 = 𝑧. (Contributed by NM, 11-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑝 = 𝑧) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) ∧ 𝑧 ∈ 𝑍) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍)) | ||
Theorem | paddasslem12 35990 | Lemma for paddass 35997. The case when 𝑥 = 𝑦. (Contributed by NM, 11-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍)) | ||
Theorem | paddasslem13 35991 | Lemma for paddass 35997. 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 35992 | Lemma for paddass 35997. Remove 𝑝 ≠ 𝑧, 𝑥 ≠ 𝑦, and ¬ 𝑟 ≤ (𝑥 ∨ 𝑦) from antecedent of paddasslem10 35988, using paddasslem11 35989, paddasslem12 35990, and paddasslem13 35991. (Contributed by NM, 11-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍)) | ||
Theorem | paddasslem15 35993 | Lemma for paddass 35997. Use elpaddn0 35959 to eliminate 𝑦 and 𝑧 from paddasslem14 35992. (Contributed by NM, 11-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅)) ∧ (𝑝 ∈ 𝐴 ∧ (𝑥 ∈ 𝑋 ∧ 𝑟 ∈ (𝑌 + 𝑍)) ∧ 𝑝 ≤ (𝑥 ∨ 𝑟))) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍)) | ||
Theorem | paddasslem16 35994 | Lemma for paddass 35997. Use elpaddn0 35959 to eliminate 𝑥 and 𝑟 from paddasslem15 35993. (Contributed by NM, 11-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍)) | ||
Theorem | paddasslem17 35995 | Lemma for paddass 35997. The case when at least one sum argument is empty. (Contributed by NM, 12-Jan-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ¬ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍)) | ||
Theorem | paddasslem18 35996 | Lemma for paddass 35997. Combine paddasslem16 35994 and paddasslem17 35995. (Contributed by NM, 12-Jan-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍)) | ||
Theorem | paddass 35997 | 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 35998 | Commutative/associative law for projective subspace sum. (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 + (𝑌 + 𝑍)) = (𝑌 + (𝑋 + 𝑍))) | ||
Theorem | padd4N 35999 | Rearrangement of 4 terms in a projective subspace sum. (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴)) → ((𝑋 + 𝑌) + (𝑍 + 𝑊)) = ((𝑋 + 𝑍) + (𝑌 + 𝑊))) | ||
Theorem | paddidm 36000 | Projective subspace sum is idempotent. Part of Lemma 16.2 of [MaedaMaeda] p. 68. (Contributed by NM, 13-Jan-2012.) |
⊢ 𝑆 = (PSubSp‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝑆) → (𝑋 + 𝑋) = 𝑋) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |