![]() |
Metamath
Proof Explorer Theorem List (p. 408 of 481) | < 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-30604) |
![]() (30605-32127) |
![]() (32128-48014) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dochocss 40701 | Double negative law for orthocomplement of an arbitrary set of vectors. (Contributed by NM, 16-Apr-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → 𝑋 ⊆ ( ⊥ ‘( ⊥ ‘𝑋))) | ||
Theorem | dochoc 40702 | Double negative law for orthocomplement of a closed subspace. (Contributed by NM, 14-Mar-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ ran 𝐼) → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) | ||
Theorem | dochsscl 40703 | If a set of vectors is included in a closed set, so is its closure. (Contributed by NM, 17-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ⊆ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ ran 𝐼) ⇒ ⊢ (𝜑 → (𝑋 ⊆ 𝑌 ↔ ( ⊥ ‘( ⊥ ‘𝑋)) ⊆ 𝑌)) | ||
Theorem | dochoccl 40704 | A set of vectors is closed iff it equals its double orthocomplent. (Contributed by NM, 1-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ⊆ 𝑉) ⇒ ⊢ (𝜑 → (𝑋 ∈ ran 𝐼 ↔ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋)) | ||
Theorem | dochord 40705 | Ordering law for orthocomplement. (Contributed by NM, 12-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑌 ∈ ran 𝐼) ⇒ ⊢ (𝜑 → (𝑋 ⊆ 𝑌 ↔ ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋))) | ||
Theorem | dochord2N 40706 | Ordering law for orthocomplement. (Contributed by NM, 29-Oct-2014.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑌 ∈ ran 𝐼) ⇒ ⊢ (𝜑 → (( ⊥ ‘𝑋) ⊆ 𝑌 ↔ ( ⊥ ‘𝑌) ⊆ 𝑋)) | ||
Theorem | dochord3 40707 | Ordering law for orthocomplement. (Contributed by NM, 9-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑌 ∈ ran 𝐼) ⇒ ⊢ (𝜑 → (𝑋 ⊆ ( ⊥ ‘𝑌) ↔ 𝑌 ⊆ ( ⊥ ‘𝑋))) | ||
Theorem | doch11 40708 | Orthocomplement is one-to-one. (Contributed by NM, 12-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑌 ∈ ran 𝐼) ⇒ ⊢ (𝜑 → (( ⊥ ‘𝑋) = ( ⊥ ‘𝑌) ↔ 𝑋 = 𝑌)) | ||
Theorem | dochsordN 40709 | Strict ordering law for orthocomplement. (Contributed by NM, 12-Aug-2014.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑌 ∈ ran 𝐼) ⇒ ⊢ (𝜑 → (𝑋 ⊊ 𝑌 ↔ ( ⊥ ‘𝑌) ⊊ ( ⊥ ‘𝑋))) | ||
Theorem | dochn0nv 40710 | An orthocomplement is nonzero iff the double orthocomplement is not the whole vector space. (Contributed by NM, 1-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ⊆ 𝑉) ⇒ ⊢ (𝜑 → (( ⊥ ‘𝑋) ≠ { 0 } ↔ ( ⊥ ‘( ⊥ ‘𝑋)) ≠ 𝑉)) | ||
Theorem | dihoml4c 40711 | Version of dihoml4 40712 with closed subspaces. (Contributed by NM, 15-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑌 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑋 ⊆ 𝑌) ⇒ ⊢ (𝜑 → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = 𝑋) | ||
Theorem | dihoml4 40712 | Orthomodular law for constructed vector space H. Lemma 3.3(1) in [Holland95] p. 215. (poml4N 39288 analog.) (Contributed by NM, 15-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) & ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑌)) = 𝑌) & ⊢ (𝜑 → 𝑋 ⊆ 𝑌) ⇒ ⊢ (𝜑 → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = ( ⊥ ‘( ⊥ ‘𝑋))) | ||
Theorem | dochspss 40713 | The span of a set of vectors is included in their double orthocomplement. (Contributed by NM, 26-Jul-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ⊆ 𝑉) ⇒ ⊢ (𝜑 → (𝑁‘𝑋) ⊆ ( ⊥ ‘( ⊥ ‘𝑋))) | ||
Theorem | dochocsp 40714 | The span of an orthocomplement equals the orthocomplement of the span. (Contributed by NM, 7-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ⊆ 𝑉) ⇒ ⊢ (𝜑 → ( ⊥ ‘(𝑁‘𝑋)) = ( ⊥ ‘𝑋)) | ||
Theorem | dochspocN 40715 | The span of an orthocomplement equals the orthocomplement of the span. (Contributed by NM, 7-Aug-2014.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ⊆ 𝑉) ⇒ ⊢ (𝜑 → (𝑁‘( ⊥ ‘𝑋)) = ( ⊥ ‘(𝑁‘𝑋))) | ||
Theorem | dochocsn 40716 | The double orthocomplement of a singleton is its span. (Contributed by NM, 13-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘{𝑋})) = (𝑁‘{𝑋})) | ||
Theorem | dochsncom 40717 | Swap vectors in an orthocomplement of a singleton. (Contributed by NM, 17-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋 ∈ ( ⊥ ‘{𝑌}) ↔ 𝑌 ∈ ( ⊥ ‘{𝑋}))) | ||
Theorem | dochsat 40718 | The double orthocomplement of an atom is an atom. (Contributed by NM, 29-Oct-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑄 ∈ 𝑆) ⇒ ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘𝑄)) ∈ 𝐴 ↔ 𝑄 ∈ 𝐴)) | ||
Theorem | dochshpncl 40719 | If a hyperplane is not closed, its closure equals the vector space. (Contributed by NM, 29-Oct-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑌 = (LSHyp‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑌) ⇒ ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘𝑋)) ≠ 𝑋 ↔ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑉)) | ||
Theorem | dochlkr 40720 | Equivalent conditions for the closure of a kernel to be a hyperplane. (Contributed by NM, 29-Oct-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝑌 = (LSHyp‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ∈ 𝑌 ↔ (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ∧ (𝐿‘𝐺) ∈ 𝑌))) | ||
Theorem | dochkrshp 40721 | The closure of a kernel is a hyperplane iff it doesn't contain all vectors. (Contributed by NM, 1-Nov-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑌 = (LSHyp‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉 ↔ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ∈ 𝑌)) | ||
Theorem | dochkrshp2 40722 | Properties of the closure of the kernel of a functional. (Contributed by NM, 1-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑌 = (LSHyp‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉 ↔ (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ∧ (𝐿‘𝐺) ∈ 𝑌))) | ||
Theorem | dochkrshp3 40723 | Properties of the closure of the kernel of a functional. (Contributed by NM, 1-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉 ↔ (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ∧ (𝐿‘𝐺) ≠ 𝑉))) | ||
Theorem | dochkrshp4 40724 | Properties of the closure of the kernel of a functional. (Contributed by NM, 1-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ↔ (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉 ∨ (𝐿‘𝐺) = 𝑉))) | ||
Theorem | dochdmj1 40725 | De Morgan-like law for subspace orthocomplement. (Contributed by NM, 5-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉) → ( ⊥ ‘(𝑋 ∪ 𝑌)) = (( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑌))) | ||
Theorem | dochnoncon 40726 | Law of noncontradiction. The intersection of a subspace and its orthocomplement is the zero subspace. (Contributed by NM, 16-Apr-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → (𝑋 ∩ ( ⊥ ‘𝑋)) = { 0 }) | ||
Theorem | dochnel2 40727 | A nonzero member of a subspace doesn't belong to the orthocomplement of the subspace. (Contributed by NM, 28-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ (𝑇 ∖ { 0 })) ⇒ ⊢ (𝜑 → ¬ 𝑋 ∈ ( ⊥ ‘𝑇)) | ||
Theorem | dochnel 40728 | A nonzero vector doesn't belong to the orthocomplement of its singleton. (Contributed by NM, 27-Oct-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → ¬ 𝑋 ∈ ( ⊥ ‘{𝑋})) | ||
Syntax | cdjh 40729 | Extend class notation with subspace join for DVecH vector space. |
class joinH | ||
Definition | df-djh 40730* | Define (closed) subspace join for DVecH vector space. (Contributed by NM, 19-Jul-2014.) |
⊢ joinH = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)), 𝑦 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((ocH‘𝑘)‘𝑤)‘((((ocH‘𝑘)‘𝑤)‘𝑥) ∩ (((ocH‘𝑘)‘𝑤)‘𝑦)))))) | ||
Theorem | djhffval 40731* | Subspace join for DVecH vector space. (Contributed by NM, 19-Jul-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑋 → (joinH‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝐾)‘𝑤)), 𝑦 ∈ 𝒫 (Base‘((DVecH‘𝐾)‘𝑤)) ↦ (((ocH‘𝐾)‘𝑤)‘((((ocH‘𝐾)‘𝑤)‘𝑥) ∩ (((ocH‘𝐾)‘𝑤)‘𝑦)))))) | ||
Theorem | djhfval 40732* | Subspace join for DVecH vector space. (Contributed by NM, 19-Jul-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → ∨ = (𝑥 ∈ 𝒫 𝑉, 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘(( ⊥ ‘𝑥) ∩ ( ⊥ ‘𝑦))))) | ||
Theorem | djhval 40733 | Subspace join for DVecH vector space. (Contributed by NM, 19-Jul-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉)) → (𝑋 ∨ 𝑌) = ( ⊥ ‘(( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑌)))) | ||
Theorem | djhval2 40734 | Value of subspace join for DVecH vector space. (Contributed by NM, 6-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉) → (𝑋 ∨ 𝑌) = ( ⊥ ‘( ⊥ ‘(𝑋 ∪ 𝑌)))) | ||
Theorem | djhcl 40735 | Closure of subspace join for DVecH vector space. (Contributed by NM, 19-Jul-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉)) → (𝑋 ∨ 𝑌) ∈ ran 𝐼) | ||
Theorem | djhlj 40736 | Transfer lattice join to DVecH vector space closed subspace join. (Contributed by NM, 19-Jul-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝐽 = ((joinH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐼‘(𝑋 ∨ 𝑌)) = ((𝐼‘𝑋)𝐽(𝐼‘𝑌))) | ||
Theorem | djhljjN 40737 | Lattice join in terms of DVecH vector space closed subspace join. (Contributed by NM, 17-Aug-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝐽 = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ∨ 𝑌) = (◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌)))) | ||
Theorem | djhjlj 40738 | DVecH vector space closed subspace join in terms of lattice join. (Contributed by NM, 9-Aug-2014.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝐽 = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑌 ∈ ran 𝐼) ⇒ ⊢ (𝜑 → (𝑋𝐽𝑌) = (𝐼‘((◡𝐼‘𝑋) ∨ (◡𝐼‘𝑌)))) | ||
Theorem | djhj 40739 | DVecH vector space closed subspace join in terms of lattice join. (Contributed by NM, 17-Aug-2014.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝐽 = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑌 ∈ ran 𝐼) ⇒ ⊢ (𝜑 → (◡𝐼‘(𝑋𝐽𝑌)) = ((◡𝐼‘𝑋) ∨ (◡𝐼‘𝑌))) | ||
Theorem | djhcom 40740 | Subspace join commutes. (Contributed by NM, 8-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ⊆ 𝑉) & ⊢ (𝜑 → 𝑌 ⊆ 𝑉) ⇒ ⊢ (𝜑 → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋)) | ||
Theorem | djhspss 40741 | Subspace span of union is a subset of subspace join. (Contributed by NM, 6-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ⊆ 𝑉) & ⊢ (𝜑 → 𝑌 ⊆ 𝑉) ⇒ ⊢ (𝜑 → (𝑁‘(𝑋 ∪ 𝑌)) ⊆ (𝑋 ∨ 𝑌)) | ||
Theorem | djhsumss 40742 | Subspace sum is a subset of subspace join. (Contributed by NM, 6-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ⊆ 𝑉) & ⊢ (𝜑 → 𝑌 ⊆ 𝑉) ⇒ ⊢ (𝜑 → (𝑋 ⊕ 𝑌) ⊆ (𝑋 ∨ 𝑌)) | ||
Theorem | dihsumssj 40743 | The subspace sum of two isomorphisms of lattice elements is less than the isomorphism of their lattice join. (Contributed by NM, 23-Sep-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝐼‘𝑋) ⊕ (𝐼‘𝑌)) ⊆ (𝐼‘(𝑋 ∨ 𝑌))) | ||
Theorem | djhunssN 40744 | Subspace union is a subset of subspace join. (Contributed by NM, 6-Aug-2014.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ⊆ 𝑉) & ⊢ (𝜑 → 𝑌 ⊆ 𝑉) ⇒ ⊢ (𝜑 → (𝑋 ∪ 𝑌) ⊆ (𝑋 ∨ 𝑌)) | ||
Theorem | dochdmm1 40745 | De Morgan-like law for closed subspace orthocomplement. (Contributed by NM, 13-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑌 ∈ ran 𝐼) ⇒ ⊢ (𝜑 → ( ⊥ ‘(𝑋 ∩ 𝑌)) = (( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌))) | ||
Theorem | djhexmid 40746 | Excluded middle property of DVecH vector space closed subspace join. (Contributed by NM, 22-Jul-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → (𝑋 ∨ ( ⊥ ‘𝑋)) = 𝑉) | ||
Theorem | djh01 40747 | Closed subspace join with zero. (Contributed by NM, 9-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) ⇒ ⊢ (𝜑 → (𝑋 ∨ { 0 }) = 𝑋) | ||
Theorem | djh02 40748 | Closed subspace join with zero. (Contributed by NM, 9-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) ⇒ ⊢ (𝜑 → ({ 0 } ∨ 𝑋) = 𝑋) | ||
Theorem | djhlsmcl 40749 | A closed subspace sum equals subspace join. (shjshseli 31179 analog.) (Contributed by NM, 13-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝑋 ⊕ 𝑌) ∈ ran 𝐼 ↔ (𝑋 ⊕ 𝑌) = (𝑋 ∨ 𝑌))) | ||
Theorem | djhcvat42 40750* | A covering property. (cvrat42 38779 analog.) (Contributed by NM, 17-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑆 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → ((𝑆 ≠ { 0 } ∧ (𝑁‘{𝑋}) ⊆ (𝑆 ∨ (𝑁‘{𝑌}))) → ∃𝑧 ∈ (𝑉 ∖ { 0 })((𝑁‘{𝑧}) ⊆ 𝑆 ∧ (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑧}) ∨ (𝑁‘{𝑌}))))) | ||
Theorem | dihjatb 40751 | Isomorphism H of lattice join of two atoms under the fiducial hyperplane. (Contributed by NM, 23-Sep-2014.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊)) & ⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ⇒ ⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑃) ⊕ (𝐼‘𝑄))) | ||
Theorem | dihjatc 40752 | Isomorphism H of lattice join of an element under the fiducial hyperplane with atom not under it. (Contributed by NM, 26-Aug-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) & ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ⇒ ⊢ (𝜑 → (𝐼‘(𝑋 ∨ 𝑃)) = ((𝐼‘𝑋) ⊕ (𝐼‘𝑃))) | ||
Theorem | dihjatcclem1 40753 | Lemma for isomorphism H of lattice join of two atoms not under the fiducial hyperplane. (Contributed by NM, 26-Sep-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑉 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) & ⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ⇒ ⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) = (((𝐼‘𝑃) ⊕ (𝐼‘𝑄)) ⊕ (𝐼‘𝑉))) | ||
Theorem | dihjatcclem2 40754 | Lemma for isomorphism H of lattice join of two atoms not under the fiducial hyperplane. (Contributed by NM, 26-Sep-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑉 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) & ⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) & ⊢ (𝜑 → (𝐼‘𝑉) ⊆ ((𝐼‘𝑃) ⊕ (𝐼‘𝑄))) ⇒ ⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑃) ⊕ (𝐼‘𝑄))) | ||
Theorem | dihjatcclem3 40755* | Lemma for dihjatcc 40757. (Contributed by NM, 28-Sep-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑉 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) & ⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) & ⊢ 𝐶 = ((oc‘𝐾)‘𝑊) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝐺 = (℩𝑑 ∈ 𝑇 (𝑑‘𝐶) = 𝑃) & ⊢ 𝐷 = (℩𝑑 ∈ 𝑇 (𝑑‘𝐶) = 𝑄) ⇒ ⊢ (𝜑 → (𝑅‘(𝐺 ∘ ◡𝐷)) = 𝑉) | ||
Theorem | dihjatcclem4 40756* | Lemma for isomorphism H of lattice join of two atoms not under the fiducial hyperplane. (Contributed by NM, 29-Sep-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑉 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) & ⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) & ⊢ 𝐶 = ((oc‘𝐾)‘𝑊) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝐺 = (℩𝑑 ∈ 𝑇 (𝑑‘𝐶) = 𝑃) & ⊢ 𝐷 = (℩𝑑 ∈ 𝑇 (𝑑‘𝐶) = 𝑄) & ⊢ 𝑁 = (𝑎 ∈ 𝐸 ↦ (𝑑 ∈ 𝑇 ↦ ◡(𝑎‘𝑑))) & ⊢ 0 = (𝑑 ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝐽 = (𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (𝑑 ∈ 𝑇 ↦ ((𝑎‘𝑑) ∘ (𝑏‘𝑑)))) ⇒ ⊢ (𝜑 → (𝐼‘𝑉) ⊆ ((𝐼‘𝑃) ⊕ (𝐼‘𝑄))) | ||
Theorem | dihjatcc 40757 | Isomorphism H of lattice join of two atoms not under the fiducial hyperplane. (Contributed by NM, 29-Sep-2014.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) & ⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ⇒ ⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑃) ⊕ (𝐼‘𝑄))) | ||
Theorem | dihjat 40758 | Isomorphism H of lattice join of two atoms. (Contributed by NM, 29-Sep-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑃 ∈ 𝐴) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑃) ⊕ (𝐼‘𝑄))) | ||
Theorem | dihprrnlem1N 40759 | Lemma for dihprrn 40761, showing one of 4 cases. (Contributed by NM, 30-Aug-2014.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ≤ = (le‘𝐾) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → 𝑌 ≠ 0 ) & ⊢ (𝜑 → (◡𝐼‘(𝑁‘{𝑋})) ≤ 𝑊) & ⊢ (𝜑 → ¬ (◡𝐼‘(𝑁‘{𝑌})) ≤ 𝑊) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ ran 𝐼) | ||
Theorem | dihprrnlem2 40760 | Lemma for dihprrn 40761. (Contributed by NM, 29-Sep-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → 𝑋 ≠ 0 ) & ⊢ (𝜑 → 𝑌 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ ran 𝐼) | ||
Theorem | dihprrn 40761 | The span of a vector pair belongs to the range of isomorphism H i.e. is a closed subspace. (Contributed by NM, 29-Sep-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ ran 𝐼) | ||
Theorem | djhlsmat 40762 | The sum of two subspace atoms equals their join. TODO: seems convoluted to go via dihprrn 40761; should we directly use dihjat 40758? (Contributed by NM, 13-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑋}) ⊕ (𝑁‘{𝑌})) = ((𝑁‘{𝑋}) ∨ (𝑁‘{𝑌}))) | ||
Theorem | dihjat1lem 40763 | Subspace sum of a closed subspace and an atom. (pmapjat1 39188 analog.) TODO: merge into dihjat1 40764? (Contributed by NM, 18-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝑋 ∨ (𝑁‘{𝑇})) = (𝑋 ⊕ (𝑁‘{𝑇}))) | ||
Theorem | dihjat1 40764 | Subspace sum of a closed subspace and an atom. (pmapjat1 39188 analog.) (Contributed by NM, 1-Oct-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋 ∨ (𝑁‘{𝑇})) = (𝑋 ⊕ (𝑁‘{𝑇}))) | ||
Theorem | dihsmsprn 40765 | Subspace sum of a closed subspace and the span of a singleton. (Contributed by NM, 17-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋 ⊕ (𝑁‘{𝑇})) ∈ ran 𝐼) | ||
Theorem | dihjat2 40766 | The subspace sum of a closed subspace and an atom is the same as their subspace join. (Contributed by NM, 1-Oct-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑋 ∨ 𝑄) = (𝑋 ⊕ 𝑄)) | ||
Theorem | dihjat3 40767 | Isomorphism H of lattice join with an atom. (Contributed by NM, 25-Apr-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑃 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐼‘(𝑋 ∨ 𝑃)) = ((𝐼‘𝑋) ⊕ (𝐼‘𝑃))) | ||
Theorem | dihjat4 40768 | Transfer the subspace sum of a closed subspace and an atom back to lattice join. (Contributed by NM, 25-Apr-2015.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑋 ⊕ 𝑄) = (𝐼‘((◡𝐼‘𝑋) ∨ (◡𝐼‘𝑄)))) | ||
Theorem | dihjat6 40769 | Transfer the subspace sum of a closed subspace and an atom back to lattice join. (Contributed by NM, 25-Apr-2015.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ (𝜑 → (◡𝐼‘(𝑋 ⊕ 𝑄)) = ((◡𝐼‘𝑋) ∨ (◡𝐼‘𝑄))) | ||
Theorem | dihsmsnrn 40770 | The subspace sum of two singleton spans is closed. (Contributed by NM, 27-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑋}) ⊕ (𝑁‘{𝑌})) ∈ ran 𝐼) | ||
Theorem | dihsmatrn 40771 | The subspace sum of a closed subspace and an atom is closed. TODO: see if proof at http://math.stackexchange.com/a/1233211/50776 and Mon, 13 Apr 2015 20:44:07 -0400 email could be used instead of this and dihjat2 40766. (Contributed by NM, 15-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑋 ⊕ 𝑄) ∈ ran 𝐼) | ||
Theorem | dihjat5N 40772 | Transfer lattice join with atom to subspace sum. (Contributed by NM, 25-Apr-2015.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑃 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑋 ∨ 𝑃) = (◡𝐼‘((𝐼‘𝑋) ⊕ (𝐼‘𝑃)))) | ||
Theorem | dvh4dimat 40773* | There is an atom that is outside the subspace sum of 3 others. (Contributed by NM, 25-Apr-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑃 ∈ 𝐴) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝐴) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ 𝐴 ¬ 𝑠 ⊆ ((𝑃 ⊕ 𝑄) ⊕ 𝑅)) | ||
Theorem | dvh3dimatN 40774* | There is an atom that is outside the subspace sum of 2 others. (Contributed by NM, 25-Apr-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑃 ∈ 𝐴) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ 𝐴 ¬ 𝑠 ⊆ (𝑃 ⊕ 𝑄)) | ||
Theorem | dvh2dimatN 40775* | Given an atom, there exists another. (Contributed by NM, 25-Apr-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑃 ∈ 𝐴) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ 𝐴 𝑠 ≠ 𝑃) | ||
Theorem | dvh1dimat 40776* | There exists an atom. (Contributed by NM, 25-Apr-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → ∃𝑠 𝑠 ∈ 𝐴) | ||
Theorem | dvh1dim 40777* | There exists a nonzero vector. (Contributed by NM, 26-Apr-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 𝑧 ≠ 0 ) | ||
Theorem | dvh4dimlem 40778* | Lemma for dvh4dimN 40782. (Contributed by NM, 22-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → 𝑋 ≠ 0 ) & ⊢ (𝜑 → 𝑌 ≠ 0 ) & ⊢ (𝜑 → 𝑍 ≠ 0 ) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌, 𝑍})) | ||
Theorem | dvhdimlem 40779* | Lemma for dvh2dim 40780 and dvh3dim 40781. TODO: make this obsolete and use dvh4dimlem 40778 directly? (Contributed by NM, 24-Apr-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → 𝑋 ≠ 0 ) & ⊢ (𝜑 → 𝑌 ≠ 0 ) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌})) | ||
Theorem | dvh2dim 40780* | There is a vector that is outside the span of another. (Contributed by NM, 25-Apr-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝑋})) | ||
Theorem | dvh3dim 40781* | There is a vector that is outside the span of 2 others. (Contributed by NM, 24-Apr-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌})) | ||
Theorem | dvh4dimN 40782* | There is a vector that is outside the span of 3 others. (Contributed by NM, 22-May-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌, 𝑍})) | ||
Theorem | dvh3dim2 40783* | There is a vector that is outside of 2 spans with a common vector. (Contributed by NM, 13-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑍}))) | ||
Theorem | dvh3dim3N 40784* | There is a vector that is outside of 2 spans. TODO: decide to use either this or dvh3dim2 40783 everywhere. If this one is needed, make dvh3dim2 40783 into a lemma. (Contributed by NM, 21-May-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇}))) | ||
Theorem | dochsnnz 40785 | The orthocomplement of a singleton is nonzero. (Contributed by NM, 13-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ≠ { 0 }) | ||
Theorem | dochsatshp 40786 | The orthocomplement of a subspace atom is a hyperplane. (Contributed by NM, 27-Jul-2014.) (Revised by Mario Carneiro, 1-Oct-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ 𝑌 = (LSHyp‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ (𝜑 → ( ⊥ ‘𝑄) ∈ 𝑌) | ||
Theorem | dochsatshpb 40787 | The orthocomplement of a subspace atom is a hyperplane. (Contributed by NM, 29-Oct-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ 𝑌 = (LSHyp‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑄 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑄 ∈ 𝐴 ↔ ( ⊥ ‘𝑄) ∈ 𝑌)) | ||
Theorem | dochsnshp 40788 | The orthocomplement of a nonzero singleton is a hyperplane. (Contributed by NM, 3-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑌 = (LSHyp‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ∈ 𝑌) | ||
Theorem | dochshpsat 40789 | A hyperplane is closed iff its orthocomplement is an atom. (Contributed by NM, 29-Oct-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ 𝑌 = (LSHyp‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑌) ⇒ ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ↔ ( ⊥ ‘𝑋) ∈ 𝐴)) | ||
Theorem | dochkrsat 40790 | The orthocomplement of a kernel is an atom iff it is nonzero. (Contributed by NM, 1-Nov-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (( ⊥ ‘(𝐿‘𝐺)) ≠ { 0 } ↔ ( ⊥ ‘(𝐿‘𝐺)) ∈ 𝐴)) | ||
Theorem | dochkrsat2 40791 | The orthocomplement of a kernel is an atom iff the double orthocomplement is not the vector space. (Contributed by NM, 1-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉 ↔ ( ⊥ ‘(𝐿‘𝐺)) ∈ 𝐴)) | ||
Theorem | dochsat0 40792 | The orthocomplement of a kernel is either an atom or zero. (Contributed by NM, 29-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (( ⊥ ‘(𝐿‘𝐺)) ∈ 𝐴 ∨ ( ⊥ ‘(𝐿‘𝐺)) = { 0 })) | ||
Theorem | dochkrsm 40793 | The subspace sum of a closed subspace and a kernel orthocomplement is closed. (djhlsmcl 40749 can be used to convert sum to join.) (Contributed by NM, 29-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝑋 ⊕ ( ⊥ ‘(𝐿‘𝐺))) ∈ ran 𝐼) | ||
Theorem | dochexmidat 40794 | Special case of excluded middle for the singleton of a vector. (Contributed by NM, 27-Oct-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (( ⊥ ‘{𝑋}) ⊕ (𝑁‘{𝑋})) = 𝑉) | ||
Theorem | dochexmidlem1 40795 | Lemma for dochexmid 40803. Holland's proof implicitly requires 𝑞 ≠ 𝑟, which we prove here. (Contributed by NM, 14-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑝 ∈ 𝐴) & ⊢ (𝜑 → 𝑞 ∈ 𝐴) & ⊢ (𝜑 → 𝑟 ∈ 𝐴) & ⊢ (𝜑 → 𝑞 ⊆ ( ⊥ ‘𝑋)) & ⊢ (𝜑 → 𝑟 ⊆ 𝑋) ⇒ ⊢ (𝜑 → 𝑞 ≠ 𝑟) | ||
Theorem | dochexmidlem2 40796 | Lemma for dochexmid 40803. (Contributed by NM, 14-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑝 ∈ 𝐴) & ⊢ (𝜑 → 𝑞 ∈ 𝐴) & ⊢ (𝜑 → 𝑟 ∈ 𝐴) & ⊢ (𝜑 → 𝑞 ⊆ ( ⊥ ‘𝑋)) & ⊢ (𝜑 → 𝑟 ⊆ 𝑋) & ⊢ (𝜑 → 𝑝 ⊆ (𝑟 ⊕ 𝑞)) ⇒ ⊢ (𝜑 → 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋))) | ||
Theorem | dochexmidlem3 40797 | Lemma for dochexmid 40803. Use atom exchange lsatexch1 38380 to swap 𝑝 and 𝑞. (Contributed by NM, 14-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑝 ∈ 𝐴) & ⊢ (𝜑 → 𝑞 ∈ 𝐴) & ⊢ (𝜑 → 𝑟 ∈ 𝐴) & ⊢ (𝜑 → 𝑞 ⊆ ( ⊥ ‘𝑋)) & ⊢ (𝜑 → 𝑟 ⊆ 𝑋) & ⊢ (𝜑 → 𝑞 ⊆ (𝑟 ⊕ 𝑝)) ⇒ ⊢ (𝜑 → 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋))) | ||
Theorem | dochexmidlem4 40798 | Lemma for dochexmid 40803. (Contributed by NM, 15-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑝 ∈ 𝐴) & ⊢ (𝜑 → 𝑞 ∈ 𝐴) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑀 = (𝑋 ⊕ 𝑝) & ⊢ (𝜑 → 𝑋 ≠ { 0 }) & ⊢ (𝜑 → 𝑞 ⊆ (( ⊥ ‘𝑋) ∩ 𝑀)) ⇒ ⊢ (𝜑 → 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋))) | ||
Theorem | dochexmidlem5 40799 | Lemma for dochexmid 40803. (Contributed by NM, 15-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑝 ∈ 𝐴) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑀 = (𝑋 ⊕ 𝑝) & ⊢ (𝜑 → 𝑋 ≠ { 0 }) & ⊢ (𝜑 → ¬ 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋))) ⇒ ⊢ (𝜑 → (( ⊥ ‘𝑋) ∩ 𝑀) = { 0 }) | ||
Theorem | dochexmidlem6 40800 | Lemma for dochexmid 40803. (Contributed by NM, 15-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑝 ∈ 𝐴) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑀 = (𝑋 ⊕ 𝑝) & ⊢ (𝜑 → 𝑋 ≠ { 0 }) & ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) & ⊢ (𝜑 → ¬ 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋))) ⇒ ⊢ (𝜑 → 𝑀 = 𝑋) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |