Home | Metamath
Proof Explorer Theorem List (p. 385 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-28622) |
Hilbert Space Explorer
(28623-30145) |
Users' Mathboxes
(30146-44834) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dochlkr 38401 | 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 38402 | 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 38403 | 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 38404 | 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 38405 | 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 38406 | De Morgan-like law for subspace orthocomplement. (Contributed by NM, 5-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉) → ( ⊥ ‘(𝑋 ∪ 𝑌)) = (( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑌))) | ||
Theorem | dochnoncon 38407 | 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 38408 | 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 38409 | 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 38410 | Extend class notation with subspace join for DVecH vector space. |
class joinH | ||
Definition | df-djh 38411* | 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 38412* | Subspace join for DVecH vector space. (Contributed by NM, 19-Jul-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑋 → (joinH‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝐾)‘𝑤)), 𝑦 ∈ 𝒫 (Base‘((DVecH‘𝐾)‘𝑤)) ↦ (((ocH‘𝐾)‘𝑤)‘((((ocH‘𝐾)‘𝑤)‘𝑥) ∩ (((ocH‘𝐾)‘𝑤)‘𝑦)))))) | ||
Theorem | djhfval 38413* | Subspace join for DVecH vector space. (Contributed by NM, 19-Jul-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → ∨ = (𝑥 ∈ 𝒫 𝑉, 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘(( ⊥ ‘𝑥) ∩ ( ⊥ ‘𝑦))))) | ||
Theorem | djhval 38414 | Subspace join for DVecH vector space. (Contributed by NM, 19-Jul-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉)) → (𝑋 ∨ 𝑌) = ( ⊥ ‘(( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑌)))) | ||
Theorem | djhval2 38415 | Value of subspace join for DVecH vector space. (Contributed by NM, 6-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉) → (𝑋 ∨ 𝑌) = ( ⊥ ‘( ⊥ ‘(𝑋 ∪ 𝑌)))) | ||
Theorem | djhcl 38416 | Closure of subspace join for DVecH vector space. (Contributed by NM, 19-Jul-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉)) → (𝑋 ∨ 𝑌) ∈ ran 𝐼) | ||
Theorem | djhlj 38417 | Transfer lattice join to DVecH vector space closed subspace join. (Contributed by NM, 19-Jul-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝐽 = ((joinH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐼‘(𝑋 ∨ 𝑌)) = ((𝐼‘𝑋)𝐽(𝐼‘𝑌))) | ||
Theorem | djhljjN 38418 | 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 38419 | 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 38420 | 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 38421 | Subspace join commutes. (Contributed by NM, 8-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ⊆ 𝑉) & ⊢ (𝜑 → 𝑌 ⊆ 𝑉) ⇒ ⊢ (𝜑 → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋)) | ||
Theorem | djhspss 38422 | Subspace span of union is a subset of subspace join. (Contributed by NM, 6-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ⊆ 𝑉) & ⊢ (𝜑 → 𝑌 ⊆ 𝑉) ⇒ ⊢ (𝜑 → (𝑁‘(𝑋 ∪ 𝑌)) ⊆ (𝑋 ∨ 𝑌)) | ||
Theorem | djhsumss 38423 | Subspace sum is a subset of subspace join. (Contributed by NM, 6-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ⊆ 𝑉) & ⊢ (𝜑 → 𝑌 ⊆ 𝑉) ⇒ ⊢ (𝜑 → (𝑋 ⊕ 𝑌) ⊆ (𝑋 ∨ 𝑌)) | ||
Theorem | dihsumssj 38424 | 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 38425 | 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 38426 | 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 38427 | Excluded middle property of DVecH vector space closed subspace join. (Contributed by NM, 22-Jul-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → (𝑋 ∨ ( ⊥ ‘𝑋)) = 𝑉) | ||
Theorem | djh01 38428 | Closed subspace join with zero. (Contributed by NM, 9-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) ⇒ ⊢ (𝜑 → (𝑋 ∨ { 0 }) = 𝑋) | ||
Theorem | djh02 38429 | Closed subspace join with zero. (Contributed by NM, 9-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) ⇒ ⊢ (𝜑 → ({ 0 } ∨ 𝑋) = 𝑋) | ||
Theorem | djhlsmcl 38430 | A closed subspace sum equals subspace join. (shjshseli 29197 analog.) (Contributed by NM, 13-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝑋 ⊕ 𝑌) ∈ ran 𝐼 ↔ (𝑋 ⊕ 𝑌) = (𝑋 ∨ 𝑌))) | ||
Theorem | djhcvat42 38431* | A covering property. (cvrat42 36460 analog.) (Contributed by NM, 17-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑆 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → ((𝑆 ≠ { 0 } ∧ (𝑁‘{𝑋}) ⊆ (𝑆 ∨ (𝑁‘{𝑌}))) → ∃𝑧 ∈ (𝑉 ∖ { 0 })((𝑁‘{𝑧}) ⊆ 𝑆 ∧ (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑧}) ∨ (𝑁‘{𝑌}))))) | ||
Theorem | dihjatb 38432 | 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 38433 | 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 38434 | 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 38435 | 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 38436* | Lemma for dihjatcc 38438. (Contributed by NM, 28-Sep-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑉 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) & ⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) & ⊢ 𝐶 = ((oc‘𝐾)‘𝑊) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝐺 = (℩𝑑 ∈ 𝑇 (𝑑‘𝐶) = 𝑃) & ⊢ 𝐷 = (℩𝑑 ∈ 𝑇 (𝑑‘𝐶) = 𝑄) ⇒ ⊢ (𝜑 → (𝑅‘(𝐺 ∘ ◡𝐷)) = 𝑉) | ||
Theorem | dihjatcclem4 38437* | 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 38438 | 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 38439 | Isomorphism H of lattice join of two atoms. (Contributed by NM, 29-Sep-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑃 ∈ 𝐴) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑃) ⊕ (𝐼‘𝑄))) | ||
Theorem | dihprrnlem1N 38440 | Lemma for dihprrn 38442, 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 38441 | Lemma for dihprrn 38442. (Contributed by NM, 29-Sep-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → 𝑋 ≠ 0 ) & ⊢ (𝜑 → 𝑌 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ ran 𝐼) | ||
Theorem | dihprrn 38442 | 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 38443 | The sum of two subspace atoms equals their join. TODO: seems convoluted to go via dihprrn 38442; should we directly use dihjat 38439? (Contributed by NM, 13-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑋}) ⊕ (𝑁‘{𝑌})) = ((𝑁‘{𝑋}) ∨ (𝑁‘{𝑌}))) | ||
Theorem | dihjat1lem 38444 | Subspace sum of a closed subspace and an atom. (pmapjat1 36869 analog.) TODO: merge into dihjat1 38445? (Contributed by NM, 18-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝑋 ∨ (𝑁‘{𝑇})) = (𝑋 ⊕ (𝑁‘{𝑇}))) | ||
Theorem | dihjat1 38445 | Subspace sum of a closed subspace and an atom. (pmapjat1 36869 analog.) (Contributed by NM, 1-Oct-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ∨ = ((joinH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋 ∨ (𝑁‘{𝑇})) = (𝑋 ⊕ (𝑁‘{𝑇}))) | ||
Theorem | dihsmsprn 38446 | 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 38447 | 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 38448 | Isomorphism H of lattice join with an atom. (Contributed by NM, 25-Apr-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑃 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐼‘(𝑋 ∨ 𝑃)) = ((𝐼‘𝑋) ⊕ (𝐼‘𝑃))) | ||
Theorem | dihjat4 38449 | 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 38450 | 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 38451 | 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 38452 | 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 38447. (Contributed by NM, 15-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑋 ⊕ 𝑄) ∈ ran 𝐼) | ||
Theorem | dihjat5N 38453 | 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 38454* | 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 38455* | 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 38456* | Given an atom, there exists another. (Contributed by NM, 25-Apr-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑃 ∈ 𝐴) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ 𝐴 𝑠 ≠ 𝑃) | ||
Theorem | dvh1dimat 38457* | There exists an atom. (Contributed by NM, 25-Apr-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → ∃𝑠 𝑠 ∈ 𝐴) | ||
Theorem | dvh1dim 38458* | There exists a nonzero vector. (Contributed by NM, 26-Apr-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 𝑧 ≠ 0 ) | ||
Theorem | dvh4dimlem 38459* | Lemma for dvh4dimN 38463. (Contributed by NM, 22-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → 𝑋 ≠ 0 ) & ⊢ (𝜑 → 𝑌 ≠ 0 ) & ⊢ (𝜑 → 𝑍 ≠ 0 ) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌, 𝑍})) | ||
Theorem | dvhdimlem 38460* | Lemma for dvh2dim 38461 and dvh3dim 38462. TODO: make this obsolete and use dvh4dimlem 38459 directly? (Contributed by NM, 24-Apr-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → 𝑋 ≠ 0 ) & ⊢ (𝜑 → 𝑌 ≠ 0 ) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌})) | ||
Theorem | dvh2dim 38461* | There is a vector that is outside the span of another. (Contributed by NM, 25-Apr-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝑋})) | ||
Theorem | dvh3dim 38462* | 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 38463* | 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 38464* | 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 38465* | There is a vector that is outside of 2 spans. TODO: decide to use either this or dvh3dim2 38464 everywhere. If this one is needed, make dvh3dim2 38464 into a lemma. (Contributed by NM, 21-May-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇}))) | ||
Theorem | dochsnnz 38466 | The orthocomplement of a singleton is nonzero. (Contributed by NM, 13-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ≠ { 0 }) | ||
Theorem | dochsatshp 38467 | 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 38468 | The orthocomplement of a subspace atom is a hyperplane. (Contributed by NM, 29-Oct-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ 𝑌 = (LSHyp‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑄 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑄 ∈ 𝐴 ↔ ( ⊥ ‘𝑄) ∈ 𝑌)) | ||
Theorem | dochsnshp 38469 | 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 38470 | A hyperplane is closed iff its orthocomplement is an atom. (Contributed by NM, 29-Oct-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ 𝑌 = (LSHyp‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑌) ⇒ ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ↔ ( ⊥ ‘𝑋) ∈ 𝐴)) | ||
Theorem | dochkrsat 38471 | 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 38472 | 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 38473 | 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 38474 | The subspace sum of a closed subspace and a kernel orthocomplement is closed. (djhlsmcl 38430 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 38475 | 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 38476 | Lemma for dochexmid 38484. 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 38477 | Lemma for dochexmid 38484. (Contributed by NM, 14-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑝 ∈ 𝐴) & ⊢ (𝜑 → 𝑞 ∈ 𝐴) & ⊢ (𝜑 → 𝑟 ∈ 𝐴) & ⊢ (𝜑 → 𝑞 ⊆ ( ⊥ ‘𝑋)) & ⊢ (𝜑 → 𝑟 ⊆ 𝑋) & ⊢ (𝜑 → 𝑝 ⊆ (𝑟 ⊕ 𝑞)) ⇒ ⊢ (𝜑 → 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋))) | ||
Theorem | dochexmidlem3 38478 | Lemma for dochexmid 38484. Use atom exchange lsatexch1 36062 to swap 𝑝 and 𝑞. (Contributed by NM, 14-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑝 ∈ 𝐴) & ⊢ (𝜑 → 𝑞 ∈ 𝐴) & ⊢ (𝜑 → 𝑟 ∈ 𝐴) & ⊢ (𝜑 → 𝑞 ⊆ ( ⊥ ‘𝑋)) & ⊢ (𝜑 → 𝑟 ⊆ 𝑋) & ⊢ (𝜑 → 𝑞 ⊆ (𝑟 ⊕ 𝑝)) ⇒ ⊢ (𝜑 → 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋))) | ||
Theorem | dochexmidlem4 38479 | Lemma for dochexmid 38484. (Contributed by NM, 15-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑝 ∈ 𝐴) & ⊢ (𝜑 → 𝑞 ∈ 𝐴) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑀 = (𝑋 ⊕ 𝑝) & ⊢ (𝜑 → 𝑋 ≠ { 0 }) & ⊢ (𝜑 → 𝑞 ⊆ (( ⊥ ‘𝑋) ∩ 𝑀)) ⇒ ⊢ (𝜑 → 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋))) | ||
Theorem | dochexmidlem5 38480 | Lemma for dochexmid 38484. (Contributed by NM, 15-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑝 ∈ 𝐴) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑀 = (𝑋 ⊕ 𝑝) & ⊢ (𝜑 → 𝑋 ≠ { 0 }) & ⊢ (𝜑 → ¬ 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋))) ⇒ ⊢ (𝜑 → (( ⊥ ‘𝑋) ∩ 𝑀) = { 0 }) | ||
Theorem | dochexmidlem6 38481 | Lemma for dochexmid 38484. (Contributed by NM, 15-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑝 ∈ 𝐴) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑀 = (𝑋 ⊕ 𝑝) & ⊢ (𝜑 → 𝑋 ≠ { 0 }) & ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) & ⊢ (𝜑 → ¬ 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋))) ⇒ ⊢ (𝜑 → 𝑀 = 𝑋) | ||
Theorem | dochexmidlem7 38482 | Lemma for dochexmid 38484. Contradict dochexmidlem6 38481. (Contributed by NM, 15-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑝 ∈ 𝐴) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑀 = (𝑋 ⊕ 𝑝) & ⊢ (𝜑 → 𝑋 ≠ { 0 }) & ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) & ⊢ (𝜑 → ¬ 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋))) ⇒ ⊢ (𝜑 → 𝑀 ≠ 𝑋) | ||
Theorem | dochexmidlem8 38483 | Lemma for dochexmid 38484. The contradiction of dochexmidlem6 38481 and dochexmidlem7 38482 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 38484 | Excluded middle law for closed subspaces, which is equivalent to (and derived from) the orthomodular law dihoml4 38393. 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 36994 analog.) (Contributed by NM, 15-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) ⇒ ⊢ (𝜑 → (𝑋 ⊕ ( ⊥ ‘𝑋)) = 𝑉) | ||
Theorem | dochsnkrlem1 38485 | Lemma for dochsnkr 38488. (Contributed by NM, 1-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 })) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉) | ||
Theorem | dochsnkrlem2 38486 | Lemma for dochsnkr 38488. (Contributed by NM, 1-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 })) & ⊢ 𝐴 = (LSAtoms‘𝑈) ⇒ ⊢ (𝜑 → ( ⊥ ‘(𝐿‘𝐺)) ∈ 𝐴) | ||
Theorem | dochsnkrlem3 38487 | Lemma for dochsnkr 38488. (Contributed by NM, 2-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 })) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺)) | ||
Theorem | dochsnkr 38488 | 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 38489* | Kernel of the explicit functional 𝐺 determined by a nonzero vector 𝑋. Compare the more general lshpkr 36133. (Contributed by NM, 27-Oct-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝐷) & ⊢ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋)))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑋})) | ||
Theorem | dochsnkr2cl 38490* | 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 38491* | Closure of the explicit functional 𝐺 determined by a nonzero vector 𝑋. Compare the more general lshpkrcl 36132. (Contributed by NM, 27-Oct-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐷 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝐷) & ⊢ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋)))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝐹) | ||
Theorem | dochfl1 38492* | 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 38493 | 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 38494* | 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 36086. (Contributed by NM, 2-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 })(𝐺‘𝑥) = 1 ) | ||
Theorem | dochkr1OLDN 38495* | 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 36086. (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 38496 | Extend class notation with all polarities of a left module or left vector space. |
class LPol | ||
Definition | df-lpolN 38497* | 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‘𝑤) ↑m 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))}) | ||
Theorem | lpolsetN 38498* | 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‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑋 → 𝑃 = {𝑜 ∈ (𝑆 ↑m 𝒫 𝑉) ∣ ((𝑜‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ((𝑜‘𝑥) ∈ 𝐻 ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))}) | ||
Theorem | islpolN 38499* | 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 38500* | Properties that determine a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ 𝑃 = (LPol‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ (𝜑 → ⊥ :𝒫 𝑉⟶𝑆) & ⊢ (𝜑 → ( ⊥ ‘𝑉) = { 0 }) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦)) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ( ⊥ ‘𝑥) ∈ 𝐻) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑥)) = 𝑥) ⇒ ⊢ (𝜑 → ⊥ ∈ 𝑃) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |