Home | Metamath
Proof Explorer Theorem List (p. 177 of 449) | < 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: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | joinfval 17601* | Value of join function for a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.) TODO: prove joinfval2 17602 first to reduce net proof size (existence part)? |
⊢ 𝑈 = (lub‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → ∨ = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝑈𝑧}) | ||
Theorem | joinfval2 17602* | Value of join function for a poset-type structure. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.) |
⊢ 𝑈 = (lub‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → ∨ = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ({𝑥, 𝑦} ∈ dom 𝑈 ∧ 𝑧 = (𝑈‘{𝑥, 𝑦}))}) | ||
Theorem | joindm 17603* | Domain of join function for a poset-type structure. (Contributed by NM, 16-Sep-2018.) |
⊢ 𝑈 = (lub‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → dom ∨ = {〈𝑥, 𝑦〉 ∣ {𝑥, 𝑦} ∈ dom 𝑈}) | ||
Theorem | joindef 17604 | Two ways to say that a join is defined. (Contributed by NM, 9-Sep-2018.) |
⊢ 𝑈 = (lub‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑊) & ⊢ (𝜑 → 𝑌 ∈ 𝑍) ⇒ ⊢ (𝜑 → (〈𝑋, 𝑌〉 ∈ dom ∨ ↔ {𝑋, 𝑌} ∈ dom 𝑈)) | ||
Theorem | joinval 17605 | Join value. Since both sides evaluate to ∅ when they don't exist, for convenience we drop the {𝑋, 𝑌} ∈ dom 𝑈 requirement. (Contributed by NM, 9-Sep-2018.) |
⊢ 𝑈 = (lub‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑊) & ⊢ (𝜑 → 𝑌 ∈ 𝑍) ⇒ ⊢ (𝜑 → (𝑋 ∨ 𝑌) = (𝑈‘{𝑋, 𝑌})) | ||
Theorem | joincl 17606 | Closure of join of elements in the domain. (Contributed by NM, 12-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ dom ∨ ) ⇒ ⊢ (𝜑 → (𝑋 ∨ 𝑌) ∈ 𝐵) | ||
Theorem | joindmss 17607 | Subset property of domain of join. (Contributed by NM, 12-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) ⇒ ⊢ (𝜑 → dom ∨ ⊆ (𝐵 × 𝐵)) | ||
Theorem | joinval2lem 17608* | Lemma for joinval2 17609 and joineu 17610. (Contributed by NM, 12-Sep-2018.) TODO: combine this through joineu 17610 into joinlem 17611? |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((∀𝑦 ∈ {𝑋, 𝑌}𝑦 ≤ 𝑥 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ {𝑋, 𝑌}𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧)) ↔ ((𝑋 ≤ 𝑥 ∧ 𝑌 ≤ 𝑥) ∧ ∀𝑧 ∈ 𝐵 ((𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧) → 𝑥 ≤ 𝑧)))) | ||
Theorem | joinval2 17609* | Value of join for a poset with LUB expanded. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 11-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ∨ 𝑌) = (℩𝑥 ∈ 𝐵 ((𝑋 ≤ 𝑥 ∧ 𝑌 ≤ 𝑥) ∧ ∀𝑧 ∈ 𝐵 ((𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧) → 𝑥 ≤ 𝑧)))) | ||
Theorem | joineu 17610* | Uniqueness of join of elements in the domain. (Contributed by NM, 12-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ dom ∨ ) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ 𝐵 ((𝑋 ≤ 𝑥 ∧ 𝑌 ≤ 𝑥) ∧ ∀𝑧 ∈ 𝐵 ((𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧) → 𝑥 ≤ 𝑧))) | ||
Theorem | joinlem 17611* | Lemma for join properties. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ dom ∨ ) ⇒ ⊢ (𝜑 → ((𝑋 ≤ (𝑋 ∨ 𝑌) ∧ 𝑌 ≤ (𝑋 ∨ 𝑌)) ∧ ∀𝑧 ∈ 𝐵 ((𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧) → (𝑋 ∨ 𝑌) ≤ 𝑧))) | ||
Theorem | lejoin1 17612 | A join's first argument is less than or equal to the join. (Contributed by NM, 16-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ dom ∨ ) ⇒ ⊢ (𝜑 → 𝑋 ≤ (𝑋 ∨ 𝑌)) | ||
Theorem | lejoin2 17613 | A join's second argument is less than or equal to the join. (Contributed by NM, 16-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ dom ∨ ) ⇒ ⊢ (𝜑 → 𝑌 ≤ (𝑋 ∨ 𝑌)) | ||
Theorem | joinle 17614 | A join is less than or equal to a third value iff each argument is less than or equal to the third value. (Contributed by NM, 16-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Poset) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ dom ∨ ) ⇒ ⊢ (𝜑 → ((𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍) ↔ (𝑋 ∨ 𝑌) ≤ 𝑍)) | ||
Theorem | meetfval 17615* | Value of meet function for a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.) TODO: prove meetfval2 17616 first to reduce net proof size (existence part)? |
⊢ 𝐺 = (glb‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → ∧ = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝐺𝑧}) | ||
Theorem | meetfval2 17616* | Value of meet function for a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.) |
⊢ 𝐺 = (glb‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → ∧ = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ({𝑥, 𝑦} ∈ dom 𝐺 ∧ 𝑧 = (𝐺‘{𝑥, 𝑦}))}) | ||
Theorem | meetdm 17617* | Domain of meet function for a poset-type structure. (Contributed by NM, 16-Sep-2018.) |
⊢ 𝐺 = (glb‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → dom ∧ = {〈𝑥, 𝑦〉 ∣ {𝑥, 𝑦} ∈ dom 𝐺}) | ||
Theorem | meetdef 17618 | Two ways to say that a meet is defined. (Contributed by NM, 9-Sep-2018.) |
⊢ 𝐺 = (glb‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑊) & ⊢ (𝜑 → 𝑌 ∈ 𝑍) ⇒ ⊢ (𝜑 → (〈𝑋, 𝑌〉 ∈ dom ∧ ↔ {𝑋, 𝑌} ∈ dom 𝐺)) | ||
Theorem | meetval 17619 | Meet value. Since both sides evaluate to ∅ when they don't exist, for convenience we drop the {𝑋, 𝑌} ∈ dom 𝐺 requirement. (Contributed by NM, 9-Sep-2018.) |
⊢ 𝐺 = (glb‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑊) & ⊢ (𝜑 → 𝑌 ∈ 𝑍) ⇒ ⊢ (𝜑 → (𝑋 ∧ 𝑌) = (𝐺‘{𝑋, 𝑌})) | ||
Theorem | meetcl 17620 | Closure of meet of elements in the domain. (Contributed by NM, 12-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ dom ∧ ) ⇒ ⊢ (𝜑 → (𝑋 ∧ 𝑌) ∈ 𝐵) | ||
Theorem | meetdmss 17621 | Subset property of domain of meet. (Contributed by NM, 12-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) ⇒ ⊢ (𝜑 → dom ∧ ⊆ (𝐵 × 𝐵)) | ||
Theorem | meetval2lem 17622* | Lemma for meetval2 17623 and meeteu 17624. (Contributed by NM, 12-Sep-2018.) TODO: combine this through meeteu 17624 into meetlem 17625? |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((∀𝑦 ∈ {𝑋, 𝑌}𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ {𝑋, 𝑌}𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥)) ↔ ((𝑥 ≤ 𝑋 ∧ 𝑥 ≤ 𝑌) ∧ ∀𝑧 ∈ 𝐵 ((𝑧 ≤ 𝑋 ∧ 𝑧 ≤ 𝑌) → 𝑧 ≤ 𝑥)))) | ||
Theorem | meetval2 17623* | Value of meet for a poset with LUB expanded. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 11-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ∧ 𝑌) = (℩𝑥 ∈ 𝐵 ((𝑥 ≤ 𝑋 ∧ 𝑥 ≤ 𝑌) ∧ ∀𝑧 ∈ 𝐵 ((𝑧 ≤ 𝑋 ∧ 𝑧 ≤ 𝑌) → 𝑧 ≤ 𝑥)))) | ||
Theorem | meeteu 17624* | Uniqueness of meet of elements in the domain. (Contributed by NM, 12-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ dom ∧ ) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ 𝐵 ((𝑥 ≤ 𝑋 ∧ 𝑥 ≤ 𝑌) ∧ ∀𝑧 ∈ 𝐵 ((𝑧 ≤ 𝑋 ∧ 𝑧 ≤ 𝑌) → 𝑧 ≤ 𝑥))) | ||
Theorem | meetlem 17625* | Lemma for meet properties. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ dom ∧ ) ⇒ ⊢ (𝜑 → (((𝑋 ∧ 𝑌) ≤ 𝑋 ∧ (𝑋 ∧ 𝑌) ≤ 𝑌) ∧ ∀𝑧 ∈ 𝐵 ((𝑧 ≤ 𝑋 ∧ 𝑧 ≤ 𝑌) → 𝑧 ≤ (𝑋 ∧ 𝑌)))) | ||
Theorem | lemeet1 17626 | A meet's first argument is less than or equal to the meet. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ dom ∧ ) ⇒ ⊢ (𝜑 → (𝑋 ∧ 𝑌) ≤ 𝑋) | ||
Theorem | lemeet2 17627 | A meet's second argument is less than or equal to the meet. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ dom ∧ ) ⇒ ⊢ (𝜑 → (𝑋 ∧ 𝑌) ≤ 𝑌) | ||
Theorem | meetle 17628 | A meet is less than or equal to a third value iff each argument is less than or equal to the third value. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Poset) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ dom ∧ ) ⇒ ⊢ (𝜑 → ((𝑍 ≤ 𝑋 ∧ 𝑍 ≤ 𝑌) ↔ 𝑍 ≤ (𝑋 ∧ 𝑌))) | ||
Theorem | joincomALT 17629 | The join of a poset commutes. (This may not be a theorem under other definitions of meet.) (Contributed by NM, 16-Sep-2011.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋)) | ||
Theorem | joincom 17630 | The join of a poset commutes. (The antecedent 〈𝑋, 𝑌〉 ∈ dom ∨ ∧ 〈𝑌, 𝑋〉 ∈ dom ∨ i.e. "the joins exist" could be omitted as an artifact of our particular join definition, but other definitions may require it.) (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (〈𝑋, 𝑌〉 ∈ dom ∨ ∧ 〈𝑌, 𝑋〉 ∈ dom ∨ )) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋)) | ||
Theorem | meetcomALT 17631 | The meet of a poset commutes. (This may not be a theorem under other definitions of meet.) (Contributed by NM, 17-Sep-2011.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) = (𝑌 ∧ 𝑋)) | ||
Theorem | meetcom 17632 | The meet of a poset commutes. (The antecedent 〈𝑋, 𝑌〉 ∈ dom ∧ ∧ 〈𝑌, 𝑋〉 ∈ dom ∧ i.e. "the meets exist" could be omitted as an artifact of our particular join definition, but other definitions may require it.) (Contributed by NM, 17-Sep-2011.) (Revised by NM, 12-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (〈𝑋, 𝑌〉 ∈ dom ∧ ∧ 〈𝑌, 𝑋〉 ∈ dom ∧ )) → (𝑋 ∧ 𝑌) = (𝑌 ∧ 𝑋)) | ||
Syntax | ctos 17633 | Extend class notation with the class of all tosets. |
class Toset | ||
Definition | df-toset 17634* | Define the class of totally ordered sets (tosets). (Contributed by FL, 17-Nov-2014.) |
⊢ Toset = {𝑓 ∈ Poset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑟𝑦 ∨ 𝑦𝑟𝑥)} | ||
Theorem | istos 17635* | The predicate "is a toset." (Contributed by FL, 17-Nov-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ (𝐾 ∈ Toset ↔ (𝐾 ∈ Poset ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥))) | ||
Theorem | tosso 17636 | Write the totally ordered set structure predicate in terms of the proper class strict order predicate. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → (𝐾 ∈ Toset ↔ ( < Or 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ ))) | ||
Syntax | cp0 17637 | Extend class notation with poset zero. |
class 0. | ||
Syntax | cp1 17638 | Extend class notation with poset unit. |
class 1. | ||
Definition | df-p0 17639 | Define poset zero. (Contributed by NM, 12-Oct-2011.) |
⊢ 0. = (𝑝 ∈ V ↦ ((glb‘𝑝)‘(Base‘𝑝))) | ||
Definition | df-p1 17640 | Define poset unit. (Contributed by NM, 22-Oct-2011.) |
⊢ 1. = (𝑝 ∈ V ↦ ((lub‘𝑝)‘(Base‘𝑝))) | ||
Theorem | p0val 17641 | Value of poset zero. (Contributed by NM, 12-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → 0 = (𝐺‘𝐵)) | ||
Theorem | p1val 17642 | Value of poset zero. (Contributed by NM, 22-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → 1 = (𝑈‘𝐵)) | ||
Theorem | p0le 17643 | Any element is less than or equal to a poset's upper bound (if defined). (Contributed by NM, 22-Oct-2011.) (Revised by NM, 13-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ dom 𝐺) ⇒ ⊢ (𝜑 → 0 ≤ 𝑋) | ||
Theorem | ple1 17644 | Any element is less than or equal to a poset's upper bound (if defined). (Contributed by NM, 22-Oct-2011.) (Revised by NM, 13-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ dom 𝑈) ⇒ ⊢ (𝜑 → 𝑋 ≤ 1 ) | ||
Syntax | clat 17645 | Extend class notation with the class of all lattices. |
class Lat | ||
Definition | df-lat 17646 | Define the class of all lattices. A lattice is a poset in which the join and meet of any two elements always exists. (Contributed by NM, 18-Oct-2012.) (Revised by NM, 12-Sep-2018.) |
⊢ Lat = {𝑝 ∈ Poset ∣ (dom (join‘𝑝) = ((Base‘𝑝) × (Base‘𝑝)) ∧ dom (meet‘𝑝) = ((Base‘𝑝) × (Base‘𝑝)))} | ||
Theorem | islat 17647 | The predicate "is a lattice." (Contributed by NM, 18-Oct-2012.) (Revised by NM, 12-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ (𝐾 ∈ Lat ↔ (𝐾 ∈ Poset ∧ (dom ∨ = (𝐵 × 𝐵) ∧ dom ∧ = (𝐵 × 𝐵)))) | ||
Theorem | latcl2 17648 | The join and meet of any two elements exist. (Contributed by NM, 14-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Lat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (〈𝑋, 𝑌〉 ∈ dom ∨ ∧ 〈𝑋, 𝑌〉 ∈ dom ∧ )) | ||
Theorem | latlem 17649 | Lemma for lattice properties. (Contributed by NM, 14-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∨ 𝑌) ∈ 𝐵 ∧ (𝑋 ∧ 𝑌) ∈ 𝐵)) | ||
Theorem | latpos 17650 | A lattice is a poset. (Contributed by NM, 17-Sep-2011.) |
⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset) | ||
Theorem | latjcl 17651 | Closure of join operation in a lattice. (chjcom 29211 analog.) (Contributed by NM, 14-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵) | ||
Theorem | latmcl 17652 | Closure of meet operation in a lattice. (incom 4177 analog.) (Contributed by NM, 14-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ∈ 𝐵) | ||
Theorem | latref 17653 | A lattice ordering is reflexive. (ssid 3988 analog.) (Contributed by NM, 8-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋) | ||
Theorem | latasymb 17654 | A lattice ordering is asymmetric. (eqss 3981 analog.) (Contributed by NM, 22-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) ↔ 𝑋 = 𝑌)) | ||
Theorem | latasym 17655 | A lattice ordering is asymmetric. (eqss 3981 analog.) (Contributed by NM, 8-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) → 𝑋 = 𝑌)) | ||
Theorem | lattr 17656 | A lattice ordering is transitive. (sstr 3974 analog.) (Contributed by NM, 17-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)) | ||
Theorem | latasymd 17657 | Deduce equality from lattice ordering. (eqssd 3983 analog.) (Contributed by NM, 18-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Lat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) & ⊢ (𝜑 → 𝑌 ≤ 𝑋) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
Theorem | lattrd 17658 | A lattice ordering is transitive. Deduction version of lattr 17656. (Contributed by NM, 3-Sep-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Lat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) & ⊢ (𝜑 → 𝑌 ≤ 𝑍) ⇒ ⊢ (𝜑 → 𝑋 ≤ 𝑍) | ||
Theorem | latjcom 17659 | The join of a lattice commutes. (chjcom 29211 analog.) (Contributed by NM, 16-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋)) | ||
Theorem | latlej1 17660 | A join's first argument is less than or equal to the join. (chub1 29212 analog.) (Contributed by NM, 17-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ≤ (𝑋 ∨ 𝑌)) | ||
Theorem | latlej2 17661 | A join's second argument is less than or equal to the join. (chub2 29213 analog.) (Contributed by NM, 17-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ≤ (𝑋 ∨ 𝑌)) | ||
Theorem | latjle12 17662 | A join is less than or equal to a third value iff each argument is less than or equal to the third value. (chlub 29214 analog.) (Contributed by NM, 17-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍) ↔ (𝑋 ∨ 𝑌) ≤ 𝑍)) | ||
Theorem | latleeqj1 17663 | "Less than or equal to" in terms of join. (chlejb1 29217 analog.) (Contributed by NM, 21-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ (𝑋 ∨ 𝑌) = 𝑌)) | ||
Theorem | latleeqj2 17664 | "Less than or equal to" in terms of join. (chlejb2 29218 analog.) (Contributed by NM, 14-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ (𝑌 ∨ 𝑋) = 𝑌)) | ||
Theorem | latjlej1 17665 | Add join to both sides of a lattice ordering. (chlej1i 29178 analog.) (Contributed by NM, 8-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑌 → (𝑋 ∨ 𝑍) ≤ (𝑌 ∨ 𝑍))) | ||
Theorem | latjlej2 17666 | Add join to both sides of a lattice ordering. (chlej2i 29179 analog.) (Contributed by NM, 8-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑌 → (𝑍 ∨ 𝑋) ≤ (𝑍 ∨ 𝑌))) | ||
Theorem | latjlej12 17667 | Add join to both sides of a lattice ordering. (chlej12i 29180 analog.) (Contributed by NM, 8-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑍 ≤ 𝑊) → (𝑋 ∨ 𝑍) ≤ (𝑌 ∨ 𝑊))) | ||
Theorem | latnlej 17668 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 28-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ ¬ 𝑋 ≤ (𝑌 ∨ 𝑍)) → (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍)) | ||
Theorem | latnlej1l 17669 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 19-Jul-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ ¬ 𝑋 ≤ (𝑌 ∨ 𝑍)) → 𝑋 ≠ 𝑌) | ||
Theorem | latnlej1r 17670 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 19-Jul-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ ¬ 𝑋 ≤ (𝑌 ∨ 𝑍)) → 𝑋 ≠ 𝑍) | ||
Theorem | latnlej2 17671 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 10-Jul-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ ¬ 𝑋 ≤ (𝑌 ∨ 𝑍)) → (¬ 𝑋 ≤ 𝑌 ∧ ¬ 𝑋 ≤ 𝑍)) | ||
Theorem | latnlej2l 17672 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 19-Jul-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ ¬ 𝑋 ≤ (𝑌 ∨ 𝑍)) → ¬ 𝑋 ≤ 𝑌) | ||
Theorem | latnlej2r 17673 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 19-Jul-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ ¬ 𝑋 ≤ (𝑌 ∨ 𝑍)) → ¬ 𝑋 ≤ 𝑍) | ||
Theorem | latjidm 17674 | Lattice join is idempotent. (Contributed by NM, 8-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵) → (𝑋 ∨ 𝑋) = 𝑋) | ||
Theorem | latmcom 17675 | The join of a lattice commutes. (Contributed by NM, 6-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) = (𝑌 ∧ 𝑋)) | ||
Theorem | latmle1 17676 | A meet is less than or equal to its first argument. (Contributed by NM, 21-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ≤ 𝑋) | ||
Theorem | latmle2 17677 | A meet is less than or equal to its second argument. (Contributed by NM, 21-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ≤ 𝑌) | ||
Theorem | latlem12 17678 | An element is less than or equal to a meet iff the element is less than or equal to each argument of the meet. (Contributed by NM, 21-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑋 ≤ 𝑍) ↔ 𝑋 ≤ (𝑌 ∧ 𝑍))) | ||
Theorem | latleeqm1 17679 | "Less than or equal to" in terms of meet. (Contributed by NM, 7-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ (𝑋 ∧ 𝑌) = 𝑋)) | ||
Theorem | latleeqm2 17680 | "Less than or equal to" in terms of meet. (Contributed by NM, 7-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ (𝑌 ∧ 𝑋) = 𝑋)) | ||
Theorem | latmlem1 17681 | Add meet to both sides of a lattice ordering. (Contributed by NM, 10-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑌 → (𝑋 ∧ 𝑍) ≤ (𝑌 ∧ 𝑍))) | ||
Theorem | latmlem2 17682 | Add meet to both sides of a lattice ordering. (sslin 4210 analog.) (Contributed by NM, 10-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑌 → (𝑍 ∧ 𝑋) ≤ (𝑍 ∧ 𝑌))) | ||
Theorem | latmlem12 17683 | Add join to both sides of a lattice ordering. (ss2in 4212 analog.) (Contributed by NM, 10-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑍 ≤ 𝑊) → (𝑋 ∧ 𝑍) ≤ (𝑌 ∧ 𝑊))) | ||
Theorem | latnlemlt 17684 | Negation of "less than or equal to" expressed in terms of meet and less-than. (nssinpss 4232 analog.) (Contributed by NM, 5-Feb-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (¬ 𝑋 ≤ 𝑌 ↔ (𝑋 ∧ 𝑌) < 𝑋)) | ||
Theorem | latnle 17685 | Equivalent expressions for "not less than" in a lattice. (chnle 29219 analog.) (Contributed by NM, 16-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (¬ 𝑌 ≤ 𝑋 ↔ 𝑋 < (𝑋 ∨ 𝑌))) | ||
Theorem | latmidm 17686 | Lattice join is idempotent. (inidm 4194 analog.) (Contributed by NM, 8-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ 𝑋) = 𝑋) | ||
Theorem | latabs1 17687 | Lattice absorption law. From definition of lattice in [Kalmbach] p. 14. (chabs1 29221 analog.) (Contributed by NM, 8-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ (𝑋 ∧ 𝑌)) = 𝑋) | ||
Theorem | latabs2 17688 | Lattice absorption law. From definition of lattice in [Kalmbach] p. 14. (chabs2 29222 analog.) (Contributed by NM, 8-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ (𝑋 ∨ 𝑌)) = 𝑋) | ||
Theorem | latledi 17689 | An ortholattice is distributive in one ordering direction. (ledi 29245 analog.) (Contributed by NM, 7-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)) ≤ (𝑋 ∧ (𝑌 ∨ 𝑍))) | ||
Theorem | latmlej11 17690 | Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ 𝑌) ≤ (𝑋 ∨ 𝑍)) | ||
Theorem | latmlej12 17691 | Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ 𝑌) ≤ (𝑍 ∨ 𝑋)) | ||
Theorem | latmlej21 17692 | Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 ∧ 𝑋) ≤ (𝑋 ∨ 𝑍)) | ||
Theorem | latmlej22 17693 | Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 ∧ 𝑋) ≤ (𝑍 ∨ 𝑋)) | ||
Theorem | lubsn 17694 | The least upper bound of a singleton. (chsupsn 29118 analog.) (Contributed by NM, 20-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵) → (𝑈‘{𝑋}) = 𝑋) | ||
Theorem | latjass 17695 | Lattice join is associative. Lemma 2.2 in [MegPav2002] p. 362. (chjass 29238 analog.) (Contributed by NM, 17-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ 𝑍) = (𝑋 ∨ (𝑌 ∨ 𝑍))) | ||
Theorem | latj12 17696 | Swap 1st and 2nd members of lattice join. (chj12 29239 analog.) (Contributed by NM, 4-Jun-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∨ (𝑌 ∨ 𝑍)) = (𝑌 ∨ (𝑋 ∨ 𝑍))) | ||
Theorem | latj32 17697 | Swap 2nd and 3rd members of lattice join. Lemma 2.2 in [MegPav2002] p. 362. (Contributed by NM, 2-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ 𝑍) = ((𝑋 ∨ 𝑍) ∨ 𝑌)) | ||
Theorem | latj13 17698 | Swap 1st and 3rd members of lattice join. (Contributed by NM, 4-Jun-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∨ (𝑌 ∨ 𝑍)) = (𝑍 ∨ (𝑌 ∨ 𝑋))) | ||
Theorem | latj31 17699 | Swap 2nd and 3rd members of lattice join. Lemma 2.2 in [MegPav2002] p. 362. (Contributed by NM, 23-Jun-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ 𝑍) = ((𝑍 ∨ 𝑌) ∨ 𝑋)) | ||
Theorem | latjrot 17700 | Rotate lattice join of 3 classes. (Contributed by NM, 23-Jul-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ 𝑍) = ((𝑍 ∨ 𝑋) ∨ 𝑌)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |