Home | Metamath
Proof Explorer Theorem List (p. 368 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | djh01 36701 | Closed subspace join with zero. (Contributed by NM, 9-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) ⇒ ⊢ (𝜑 → (𝑋 ∨ { 0 }) = 𝑋) | ||
Theorem | djh02 36702 | Closed subspace join with zero. (Contributed by NM, 9-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) ⇒ ⊢ (𝜑 → ({ 0 } ∨ 𝑋) = 𝑋) | ||
Theorem | djhlsmcl 36703 | A closed subspace sum equals subspace join. (shjshseli 28352 analog.) (Contributed by NM, 13-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝑋 ⊕ 𝑌) ∈ ran 𝐼 ↔ (𝑋 ⊕ 𝑌) = (𝑋 ∨ 𝑌))) | ||
Theorem | djhcvat42 36704* | A covering property. (cvrat42 34730 analog.) (Contributed by NM, 17-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑆 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → ((𝑆 ≠ { 0 } ∧ (𝑁‘{𝑋}) ⊆ (𝑆 ∨ (𝑁‘{𝑌}))) → ∃𝑧 ∈ (𝑉 ∖ { 0 })((𝑁‘{𝑧}) ⊆ 𝑆 ∧ (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑧}) ∨ (𝑁‘{𝑌}))))) | ||
Theorem | dihjatb 36705 | 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 36706 | 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 36707 | 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 36708 | 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 36709* | Lemma for dihjatcc 36711. (Contributed by NM, 28-Sep-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑉 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) & ⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) & ⊢ 𝐶 = ((oc‘𝐾)‘𝑊) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝐺 = (℩𝑑 ∈ 𝑇 (𝑑‘𝐶) = 𝑃) & ⊢ 𝐷 = (℩𝑑 ∈ 𝑇 (𝑑‘𝐶) = 𝑄) ⇒ ⊢ (𝜑 → (𝑅‘(𝐺 ∘ ◡𝐷)) = 𝑉) | ||
Theorem | dihjatcclem4 36710* | 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 36711 | 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 36712 | Isomorphism H of lattice join of two atoms. (Contributed by NM, 29-Sep-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑃 ∈ 𝐴) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑃) ⊕ (𝐼‘𝑄))) | ||
Theorem | dihprrnlem1N 36713 | Lemma for dihprrn 36715, 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 36714 | Lemma for dihprrn 36715. (Contributed by NM, 29-Sep-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → 𝑋 ≠ 0 ) & ⊢ (𝜑 → 𝑌 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ ran 𝐼) | ||
Theorem | dihprrn 36715 | 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 36716 | The sum of two subspace atoms equals their join. TODO: seems convoluted to go via dihprrn 36715; should we directly use dihjat 36712? (Contributed by NM, 13-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑋}) ⊕ (𝑁‘{𝑌})) = ((𝑁‘{𝑋}) ∨ (𝑁‘{𝑌}))) | ||
Theorem | dihjat1lem 36717 | Subspace sum of a closed subspace and an atom. (pmapjat1 35139 analog.) TODO: merge into dihjat1 36718? (Contributed by NM, 18-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝑋 ∨ (𝑁‘{𝑇})) = (𝑋 ⊕ (𝑁‘{𝑇}))) | ||
Theorem | dihjat1 36718 | Subspace sum of a closed subspace and an atom. (pmapjat1 35139 analog.) (Contributed by NM, 1-Oct-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋 ∨ (𝑁‘{𝑇})) = (𝑋 ⊕ (𝑁‘{𝑇}))) | ||
Theorem | dihsmsprn 36719 | 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 36720 | 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 36721 | Isomorphism H of lattice join with an atom. (Contributed by NM, 25-Apr-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑃 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐼‘(𝑋 ∨ 𝑃)) = ((𝐼‘𝑋) ⊕ (𝐼‘𝑃))) | ||
Theorem | dihjat4 36722 | 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 36723 | 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 36724 | 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 36725 | 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 36720. (Contributed by NM, 15-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑋 ⊕ 𝑄) ∈ ran 𝐼) | ||
Theorem | dihjat5N 36726 | 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 36727* | 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 36728* | 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 36729* | Given an atom, there exists another. (Contributed by NM, 25-Apr-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑃 ∈ 𝐴) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ 𝐴 𝑠 ≠ 𝑃) | ||
Theorem | dvh1dimat 36730* | There exists an atom. (Contributed by NM, 25-Apr-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → ∃𝑠 𝑠 ∈ 𝐴) | ||
Theorem | dvh1dim 36731* | There exists a nonzero vector. (Contributed by NM, 26-Apr-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 𝑧 ≠ 0 ) | ||
Theorem | dvh4dimlem 36732* | Lemma for dvh4dimN 36736. (Contributed by NM, 22-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → 𝑋 ≠ 0 ) & ⊢ (𝜑 → 𝑌 ≠ 0 ) & ⊢ (𝜑 → 𝑍 ≠ 0 ) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌, 𝑍})) | ||
Theorem | dvhdimlem 36733* | Lemma for dvh2dim 36734 and dvh3dim 36735. TODO: make this obsolete and use dvh4dimlem 36732 directly? (Contributed by NM, 24-Apr-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → 𝑋 ≠ 0 ) & ⊢ (𝜑 → 𝑌 ≠ 0 ) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌})) | ||
Theorem | dvh2dim 36734* | There is a vector that is outside the span of another. (Contributed by NM, 25-Apr-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝑋})) | ||
Theorem | dvh3dim 36735* | 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 36736* | 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 36737* | 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 36738* | There is a vector that is outside of 2 spans. TODO: decide to use either this or dvh3dim2 36737 everywhere. If this one is needed, make dvh3dim2 36737 into a lemma. (Contributed by NM, 21-May-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇}))) | ||
Theorem | dochsnnz 36739 | The orthocomplement of a singleton is nonzero. (Contributed by NM, 13-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ≠ { 0 }) | ||
Theorem | dochsatshp 36740 | 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 36741 | The orthocomplement of a subspace atom is a hyperplane. (Contributed by NM, 29-Oct-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ 𝑌 = (LSHyp‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑄 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑄 ∈ 𝐴 ↔ ( ⊥ ‘𝑄) ∈ 𝑌)) | ||
Theorem | dochsnshp 36742 | 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 36743 | A hyperplane is closed iff its orthocomplement is an atom. (Contributed by NM, 29-Oct-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ 𝑌 = (LSHyp‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑌) ⇒ ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ↔ ( ⊥ ‘𝑋) ∈ 𝐴)) | ||
Theorem | dochkrsat 36744 | 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 36745 | 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 36746 | 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 36747 | The subspace sum of a closed subspace and a kernel orthocomplement is closed. (djhlsmcl 36703 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 36748 | 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 36749 | Lemma for dochexmid 36757. 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 36750 | Lemma for dochexmid 36757. (Contributed by NM, 14-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑝 ∈ 𝐴) & ⊢ (𝜑 → 𝑞 ∈ 𝐴) & ⊢ (𝜑 → 𝑟 ∈ 𝐴) & ⊢ (𝜑 → 𝑞 ⊆ ( ⊥ ‘𝑋)) & ⊢ (𝜑 → 𝑟 ⊆ 𝑋) & ⊢ (𝜑 → 𝑝 ⊆ (𝑟 ⊕ 𝑞)) ⇒ ⊢ (𝜑 → 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋))) | ||
Theorem | dochexmidlem3 36751 | Lemma for dochexmid 36757. Use atom exchange lsatexch1 34333 to swap 𝑝 and 𝑞. (Contributed by NM, 14-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑝 ∈ 𝐴) & ⊢ (𝜑 → 𝑞 ∈ 𝐴) & ⊢ (𝜑 → 𝑟 ∈ 𝐴) & ⊢ (𝜑 → 𝑞 ⊆ ( ⊥ ‘𝑋)) & ⊢ (𝜑 → 𝑟 ⊆ 𝑋) & ⊢ (𝜑 → 𝑞 ⊆ (𝑟 ⊕ 𝑝)) ⇒ ⊢ (𝜑 → 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋))) | ||
Theorem | dochexmidlem4 36752 | Lemma for dochexmid 36757. (Contributed by NM, 15-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑝 ∈ 𝐴) & ⊢ (𝜑 → 𝑞 ∈ 𝐴) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑀 = (𝑋 ⊕ 𝑝) & ⊢ (𝜑 → 𝑋 ≠ { 0 }) & ⊢ (𝜑 → 𝑞 ⊆ (( ⊥ ‘𝑋) ∩ 𝑀)) ⇒ ⊢ (𝜑 → 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋))) | ||
Theorem | dochexmidlem5 36753 | Lemma for dochexmid 36757. (Contributed by NM, 15-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑝 ∈ 𝐴) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑀 = (𝑋 ⊕ 𝑝) & ⊢ (𝜑 → 𝑋 ≠ { 0 }) & ⊢ (𝜑 → ¬ 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋))) ⇒ ⊢ (𝜑 → (( ⊥ ‘𝑋) ∩ 𝑀) = { 0 }) | ||
Theorem | dochexmidlem6 36754 | Lemma for dochexmid 36757. (Contributed by NM, 15-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑝 ∈ 𝐴) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑀 = (𝑋 ⊕ 𝑝) & ⊢ (𝜑 → 𝑋 ≠ { 0 }) & ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) & ⊢ (𝜑 → ¬ 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋))) ⇒ ⊢ (𝜑 → 𝑀 = 𝑋) | ||
Theorem | dochexmidlem7 36755 | Lemma for dochexmid 36757. Contradict dochexmidlem6 36754. (Contributed by NM, 15-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑝 ∈ 𝐴) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑀 = (𝑋 ⊕ 𝑝) & ⊢ (𝜑 → 𝑋 ≠ { 0 }) & ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) & ⊢ (𝜑 → ¬ 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋))) ⇒ ⊢ (𝜑 → 𝑀 ≠ 𝑋) | ||
Theorem | dochexmidlem8 36756 | Lemma for dochexmid 36757. The contradiction of dochexmidlem6 36754 and dochexmidlem7 36755 shows that there can be no atom 𝑝 that is not in 𝑋 + ( ⊥ ‘𝑋), which is therefore the whole atom space. (Contributed by NM, 15-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → 𝑋 ≠ { 0 }) & ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) ⇒ ⊢ (𝜑 → (𝑋 ⊕ ( ⊥ ‘𝑋)) = 𝑉) | ||
Theorem | dochexmid 36757 | Excluded middle law for closed subspaces, which is equivalent to (and derived from) the orthomodular law dihoml4 36666. Lemma 3.3(2) in [Holland95] p. 215. In our proof, we use the variables 𝑋, 𝑀, 𝑝, 𝑞, 𝑟 in place of Hollands' l, m, P, Q, L respectively. (pexmidALTN 35264 analog.) (Contributed by NM, 15-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) ⇒ ⊢ (𝜑 → (𝑋 ⊕ ( ⊥ ‘𝑋)) = 𝑉) | ||
Theorem | dochsnkrlem1 36758 | Lemma for dochsnkr 36761. (Contributed by NM, 1-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 })) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉) | ||
Theorem | dochsnkrlem2 36759 | Lemma for dochsnkr 36761. (Contributed by NM, 1-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 })) & ⊢ 𝐴 = (LSAtoms‘𝑈) ⇒ ⊢ (𝜑 → ( ⊥ ‘(𝐿‘𝐺)) ∈ 𝐴) | ||
Theorem | dochsnkrlem3 36760 | Lemma for dochsnkr 36761. (Contributed by NM, 2-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 })) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺)) | ||
Theorem | dochsnkr 36761 | A (closed) kernel expressed in terms of a nonzero vector in its orthocomplement. TODO: consolidate lemmas unless they're needed for something else (in which case break out as theorems). (Contributed by NM, 2-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑋})) | ||
Theorem | dochsnkr2 36762* | Kernel of the explicit functional 𝐺 determined by a nonzero vector 𝑋. Compare the more general lshpkr 34404. (Contributed by NM, 27-Oct-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝐷) & ⊢ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋)))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑋})) | ||
Theorem | dochsnkr2cl 36763* | The 𝑋 determining functional 𝐺 belongs to the atom formed by the orthocomplement of the kernel. (Contributed by NM, 4-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝐷) & ⊢ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋)))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → 𝑋 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 })) | ||
Theorem | dochflcl 36764* | Closure of the explicit functional 𝐺 determined by a nonzero vector 𝑋. Compare the more general lshpkrcl 34403. (Contributed by NM, 27-Oct-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐷 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝐷) & ⊢ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋)))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝐹) | ||
Theorem | dochfl1 36765* | The value of the explicit functional 𝐺 is 1 at the 𝑋 that determines it. (Contributed by NM, 27-Oct-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐷 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝐷) & ⊢ 1 = (1r‘𝐷) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋)))) ⇒ ⊢ (𝜑 → (𝐺‘𝑋) = 1 ) | ||
Theorem | dochfln0 36766 | The value of a functional is nonzero at a nonzero vector in the orthocomplement of its kernel. (Contributed by NM, 2-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝑁 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐺‘𝑋) ≠ 𝑁) | ||
Theorem | dochkr1 36767* | A nonzero functional has a value of 1 at some argument belonging to the orthocomplement of its kernel (when its kernel is a closed hyperplane). Tighter version of lfl1 34357. (Contributed by NM, 2-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 })(𝐺‘𝑥) = 1 ) | ||
Theorem | dochkr1OLDN 36768* | A nonzero functional has a value of 1 at some argument belonging to the orthocomplement of its kernel (when its kernel is a closed hyperplane). Tighter version of lfl1 34357. (Contributed by NM, 2-Jan-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ( ⊥ ‘(𝐿‘𝐺))(𝐺‘𝑥) = 1 ) | ||
Syntax | clpoN 36769 | Extend class notation with all polarities of a left module or left vector space. |
class LPol | ||
Definition | df-lpolN 36770* | Define the set of all polarities of a left module or left vector space. A polarity is a kind of complementation operation on a subspace. The double polarity of a subspace is a closure operation. Based on Definition 3.2 of [Holland95] p. 214 for projective geometry polarities. For convenience, we open up the domain to include all vector subsets and not just subspaces, but any more restricted polarity can be converted to this one by taking the span of its argument. (Contributed by NM, 24-Nov-2014.) |
⊢ LPol = (𝑤 ∈ V ↦ {𝑜 ∈ ((LSubSp‘𝑤) ↑𝑚 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))}) | ||
Theorem | lpolsetN 36771* | The set of polarities of a left module or left vector space. (Contributed by NM, 24-Nov-2014.) (New usage is discouraged.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ 𝑃 = (LPol‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑋 → 𝑃 = {𝑜 ∈ (𝑆 ↑𝑚 𝒫 𝑉) ∣ ((𝑜‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ((𝑜‘𝑥) ∈ 𝐻 ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))}) | ||
Theorem | islpolN 36772* | The predicate "is a polarity". (Contributed by NM, 24-Nov-2014.) (New usage is discouraged.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ 𝑃 = (LPol‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑋 → ( ⊥ ∈ 𝑃 ↔ ( ⊥ :𝒫 𝑉⟶𝑆 ∧ (( ⊥ ‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥ ‘𝑥)) = 𝑥))))) | ||
Theorem | islpoldN 36773* | Properties that determine a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ 𝑃 = (LPol‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ (𝜑 → ⊥ :𝒫 𝑉⟶𝑆) & ⊢ (𝜑 → ( ⊥ ‘𝑉) = { 0 }) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦)) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ( ⊥ ‘𝑥) ∈ 𝐻) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑥)) = 𝑥) ⇒ ⊢ (𝜑 → ⊥ ∈ 𝑃) | ||
Theorem | lpolfN 36774 | Functionality of a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑃 = (LPol‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ (𝜑 → ⊥ ∈ 𝑃) ⇒ ⊢ (𝜑 → ⊥ :𝒫 𝑉⟶𝑆) | ||
Theorem | lpolvN 36775 | The polarity of the whole space is the zero subspace. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑃 = (LPol‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ (𝜑 → ⊥ ∈ 𝑃) ⇒ ⊢ (𝜑 → ( ⊥ ‘𝑉) = { 0 }) | ||
Theorem | lpolconN 36776 | Contraposition property of a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑃 = (LPol‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ (𝜑 → ⊥ ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ⊆ 𝑉) & ⊢ (𝜑 → 𝑌 ⊆ 𝑉) & ⊢ (𝜑 → 𝑋 ⊆ 𝑌) ⇒ ⊢ (𝜑 → ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋)) | ||
Theorem | lpolsatN 36777 | The polarity of an atomic subspace is a hyperplane. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.) |
⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ 𝑃 = (LPol‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ (𝜑 → ⊥ ∈ 𝑃) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ (𝜑 → ( ⊥ ‘𝑄) ∈ 𝐻) | ||
Theorem | lpolpolsatN 36778 | Property of a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.) |
⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ 𝑃 = (LPol‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ (𝜑 → ⊥ ∈ 𝑃) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑄)) = 𝑄) | ||
Theorem | dochpolN 36779 | The subspace orthocomplement for the DVecH vector space is a polarity. (Contributed by NM, 27-Dec-2014.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑃 = (LPol‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → ⊥ ∈ 𝑃) | ||
Theorem | lcfl1lem 36780* | Property of a functional with a closed kernel. (Contributed by NM, 28-Dec-2014.) |
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} ⇒ ⊢ (𝐺 ∈ 𝐶 ↔ (𝐺 ∈ 𝐹 ∧ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺))) | ||
Theorem | lcfl1 36781* | Property of a functional with a closed kernel. (Contributed by NM, 31-Dec-2014.) |
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺))) | ||
Theorem | lcfl2 36782* | Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉 ∨ (𝐿‘𝐺) = 𝑉))) | ||
Theorem | lcfl3 36783* | Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ (( ⊥ ‘(𝐿‘𝐺)) ∈ 𝐴 ∨ (𝐿‘𝐺) = 𝑉))) | ||
Theorem | lcfl4N 36784* | Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑌 = (LSHyp‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ∈ 𝑌 ∨ (𝐿‘𝐺) = 𝑉))) | ||
Theorem | lcfl5 36785* | Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ (𝐿‘𝐺) ∈ ran 𝐼)) | ||
Theorem | lcfl5a 36786 | Property of a functional with a closed kernel. TODO: Make lcfl5 36785 etc. obsolete and rewrite w/out 𝐶 hypothesis? (Contributed by NM, 29-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ↔ (𝐿‘𝐺) ∈ ran 𝐼)) | ||
Theorem | lcfl6lem 36787* | Lemma for lcfl6 36789. A functional 𝐺 (whose kernel is closed by dochsnkr 36761) is comletely determined by a vector 𝑋 in the orthocomplement in its kernel at which the functional value is 1. Note that the ∖ { 0 } in the 𝑋 hypothesis is redundant by the last hypothesis but allows easier use of other theorems. (Contributed by NM, 3-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 1 = (1r‘𝑆) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 })) & ⊢ (𝜑 → (𝐺‘𝑋) = 1 ) ⇒ ⊢ (𝜑 → 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋))))) | ||
Theorem | lcfl7lem 36788* | Lemma for lcfl7N 36790. If two functionals 𝐺 and 𝐽 are equal, they are determined by the same vector. (Contributed by NM, 4-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋)))) & ⊢ 𝐽 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑌})𝑣 = (𝑤 + (𝑘 · 𝑌)))) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐺 = 𝐽) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
Theorem | lcfl6 36789* | Property of a functional with a closed kernel. Note that (𝐿‘𝐺) = 𝑉 means the functional is zero by lkr0f 34381. (Contributed by NM, 3-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ ((𝐿‘𝐺) = 𝑉 ∨ ∃𝑥 ∈ (𝑉 ∖ { 0 })𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))))) | ||
Theorem | lcfl7N 36790* | Property of a functional with a closed kernel. Every nonzero functional is determined by a unique nonzero vector. Note that (𝐿‘𝐺) = 𝑉 means the functional is zero by lkr0f 34381. (Contributed by NM, 4-Jan-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ ((𝐿‘𝐺) = 𝑉 ∨ ∃!𝑥 ∈ (𝑉 ∖ { 0 })𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))))) | ||
Theorem | lcfl8 36791* | Property of a functional with a closed kernel. (Contributed by NM, 17-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝑉 (𝐿‘𝐺) = ( ⊥ ‘{𝑥}))) | ||
Theorem | lcfl8a 36792* | Property of a functional with a closed kernel. (Contributed by NM, 17-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ↔ ∃𝑥 ∈ 𝑉 (𝐿‘𝐺) = ( ⊥ ‘{𝑥}))) | ||
Theorem | lcfl8b 36793* | Property of a nonzero functional with a closed kernel. (Contributed by NM, 4-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑌 = (0g‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 ∖ {𝑌})) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ (𝑉 ∖ { 0 })( ⊥ ‘(𝐿‘𝐺)) = (𝑁‘{𝑥})) | ||
Theorem | lcfl9a 36794 | Property implying that a functional has a closed kernel. (Contributed by NM, 16-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ⊆ (𝐿‘𝐺)) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺)) | ||
Theorem | lclkrlem1 36795* | The set of functionals having closed kernels is closed under scalar product. (Contributed by NM, 28-Dec-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐶) ⇒ ⊢ (𝜑 → (𝑋 · 𝐺) ∈ 𝐶) | ||
Theorem | lclkrlem2a 36796 | Lemma for lclkr 36822. Use lshpat 34343 to show that the intersection of a hyperplane with a noncomparable sum of atoms is an atom. (Contributed by NM, 16-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ≠ ( ⊥ ‘{𝑌})) & ⊢ (𝜑 → ¬ 𝑋 ∈ ( ⊥ ‘{𝐵})) ⇒ ⊢ (𝜑 → (((𝑁‘{𝑋}) ⊕ (𝑁‘{𝑌})) ∩ ( ⊥ ‘{𝐵})) ∈ 𝐴) | ||
Theorem | lclkrlem2b 36797 | Lemma for lclkr 36822. (Contributed by NM, 17-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ≠ ( ⊥ ‘{𝑌})) & ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵}))) ⇒ ⊢ (𝜑 → (((𝑁‘{𝑋}) ⊕ (𝑁‘{𝑌})) ∩ ( ⊥ ‘{𝐵})) ∈ 𝐴) | ||
Theorem | lclkrlem2c 36798 | Lemma for lclkr 36822. (Contributed by NM, 16-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ≠ ( ⊥ ‘{𝑌})) & ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵}))) & ⊢ 𝐽 = (LSHyp‘𝑈) ⇒ ⊢ (𝜑 → ((( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌})) ⊕ (𝑁‘{𝐵})) ∈ 𝐽) | ||
Theorem | lclkrlem2d 36799 | Lemma for lclkr 36822. (Contributed by NM, 16-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ≠ ( ⊥ ‘{𝑌})) & ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵}))) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) ⇒ ⊢ (𝜑 → ((( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌})) ⊕ (𝑁‘{𝐵})) ∈ ran 𝐼) | ||
Theorem | lclkrlem2e 36800 | Lemma for lclkr 36822. The kernel of the sum is closed when the kernels of the summands are equal and closed. (Contributed by NM, 17-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋})) & ⊢ (𝜑 → (𝐿‘𝐸) = (𝐿‘𝐺)) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |