![]() |
Metamath
Proof Explorer Theorem List (p. 373 of 437) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28347) |
![]() (28348-29872) |
![]() (29873-43661) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | diaelrnN 37201 | Any value of the partial isomorphism A is a set of translations i.e. a set of vectors. (Contributed by NM, 26-Nov-2013.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ ran 𝐼) → 𝑆 ⊆ 𝑇) | ||
Theorem | dialss 37202 | The value of partial isomorphism A is a subspace of partial vector space A. Part of Lemma M of [Crawley] p. 120 line 26. (Contributed by NM, 17-Jan-2014.) (Revised by Mario Carneiro, 23-Jun-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) ∈ 𝑆) | ||
Theorem | diaord 37203 | The partial isomorphism A for a lattice 𝐾 is order-preserving in the region under co-atom 𝑊. Part of Lemma M of [Crawley] p. 120 line 28. (Contributed by NM, 26-Nov-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → ((𝐼‘𝑋) ⊆ (𝐼‘𝑌) ↔ 𝑋 ≤ 𝑌)) | ||
Theorem | dia11N 37204 | The partial isomorphism A for a lattice 𝐾 is one-to-one in the region under co-atom 𝑊. Part of Lemma M of [Crawley] p. 120 line 28. (Contributed by NM, 25-Nov-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → ((𝐼‘𝑋) = (𝐼‘𝑌) ↔ 𝑋 = 𝑌)) | ||
Theorem | diaf11N 37205 | The partial isomorphism A for a lattice 𝐾 is a one-to-one function. Part of Lemma M of [Crawley] p. 120 line 27. (Contributed by NM, 4-Dec-2013.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐼:dom 𝐼–1-1-onto→ran 𝐼) | ||
Theorem | diaclN 37206 | Closure of partial isomorphism A for a lattice 𝐾. (Contributed by NM, 4-Dec-2013.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘𝑋) ∈ ran 𝐼) | ||
Theorem | diacnvclN 37207 | Closure of partial isomorphism A converse. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ ran 𝐼) → (◡𝐼‘𝑋) ∈ dom 𝐼) | ||
Theorem | dia0 37208 | The value of the partial isomorphism A at the lattice zero is the singleton of the identity translation i.e. the zero subspace. (Contributed by NM, 26-Nov-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝐼‘ 0 ) = {( I ↾ 𝐵)}) | ||
Theorem | dia1N 37209 | The value of the partial isomorphism A at the fiducial co-atom is the set of all translations i.e. the entire vector space. (Contributed by NM, 26-Nov-2013.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝐼‘𝑊) = 𝑇) | ||
Theorem | dia1elN 37210 | The largest subspace in the range of partial isomorphism A. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑇 ∈ ran 𝐼) | ||
Theorem | diaglbN 37211* | Partial isomorphism A of a lattice glb. (Contributed by NM, 3-Dec-2013.) (New usage is discouraged.) |
⊢ 𝐺 = (glb‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅)) → (𝐼‘(𝐺‘𝑆)) = ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)) | ||
Theorem | diameetN 37212 | Partial isomorphism A of a lattice meet. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.) |
⊢ ∧ = (meet‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) | ||
Theorem | diainN 37213 | Inverse partial isomorphism A of an intersection. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
⊢ ∧ = (meet‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼)) → (𝑋 ∩ 𝑌) = (𝐼‘((◡𝐼‘𝑋) ∧ (◡𝐼‘𝑌)))) | ||
Theorem | diaintclN 37214 | The intersection of partial isomorphism A closed subspaces is a closed subspace. (Contributed by NM, 3-Dec-2013.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → ∩ 𝑆 ∈ ran 𝐼) | ||
Theorem | diasslssN 37215 | The partial isomorphism A maps to subspaces of partial vector space A. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ran 𝐼 ⊆ 𝑆) | ||
Theorem | diassdvaN 37216 | The partial isomorphism A maps to a set of vectors in partial vector space A. (Contributed by NM, 1-Jan-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) ⇒ ⊢ (((𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) ⊆ 𝑉) | ||
Theorem | dia1dim 37217* | Two expressions for the 1-dimensional subspaces of partial vector space A (when 𝐹 is a nonzero vector i.e. non-identity translation). Remark after Lemma L in [Crawley] p. 120 line 21. (Contributed by NM, 15-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝐼‘(𝑅‘𝐹)) = {𝑔 ∣ ∃𝑠 ∈ 𝐸 𝑔 = (𝑠‘𝐹)}) | ||
Theorem | dia1dim2 37218 | Two expressions for a 1-dimensional subspace of partial vector space A (when 𝐹 is a nonzero vector i.e. non-identity translation). (Contributed by NM, 15-Jan-2014.) (Revised by Mario Carneiro, 22-Jun-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑈) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝐼‘(𝑅‘𝐹)) = (𝑁‘{𝐹})) | ||
Theorem | dia1dimid 37219 | A vector (translation) belongs to the 1-dim subspace it generates. (Contributed by NM, 8-Sep-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹 ∈ (𝐼‘(𝑅‘𝐹))) | ||
Theorem | dia2dimlem1 37220 | Lemma for dia2dim 37233. Show properties of the auxiliary atom 𝑄. Part of proof of Lemma M in [Crawley] p. 121 line 3. (Contributed by NM, 8-Sep-2014.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝑄 = ((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉)) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊)) & ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) & ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) & ⊢ (𝜑 → (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) ≠ 𝑃)) & ⊢ (𝜑 → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉)) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) & ⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑈) ⇒ ⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) | ||
Theorem | dia2dimlem2 37221 | Lemma for dia2dim 37233. Define a translation 𝐺 whose trace is atom 𝑈. Part of proof of Lemma M in [Crawley] p. 121 line 4. (Contributed by NM, 8-Sep-2014.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝑄 = ((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉)) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊)) & ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) & ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) & ⊢ (𝜑 → (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) ≠ 𝑃)) & ⊢ (𝜑 → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉)) & ⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝑇) & ⊢ (𝜑 → (𝐺‘𝑃) = 𝑄) ⇒ ⊢ (𝜑 → (𝑅‘𝐺) = 𝑈) | ||
Theorem | dia2dimlem3 37222 | Lemma for dia2dim 37233. Define a translation 𝐷 whose trace is atom 𝑉. Part of proof of Lemma M in [Crawley] p. 121 line 5. (Contributed by NM, 8-Sep-2014.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝑄 = ((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉)) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊)) & ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) & ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) & ⊢ (𝜑 → (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) ≠ 𝑃)) & ⊢ (𝜑 → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉)) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) & ⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑈) & ⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑇) & ⊢ (𝜑 → (𝐷‘𝑄) = (𝐹‘𝑃)) ⇒ ⊢ (𝜑 → (𝑅‘𝐷) = 𝑉) | ||
Theorem | dia2dimlem4 37223 | Lemma for dia2dim 37233. Show that the composition (sum) of translations (vectors) 𝐺 and 𝐷 equals 𝐹. Part of proof of Lemma M in [Crawley] p. 121 line 5. (Contributed by NM, 8-Sep-2014.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) & ⊢ (𝜑 → 𝐹 ∈ 𝑇) & ⊢ (𝜑 → 𝐺 ∈ 𝑇) & ⊢ (𝜑 → (𝐺‘𝑃) = 𝑄) & ⊢ (𝜑 → 𝐷 ∈ 𝑇) & ⊢ (𝜑 → (𝐷‘𝑄) = (𝐹‘𝑃)) ⇒ ⊢ (𝜑 → (𝐷 ∘ 𝐺) = 𝐹) | ||
Theorem | dia2dimlem5 37224 | Lemma for dia2dim 37233. The sum of vectors 𝐺 and 𝐷 belongs to the sum of the subspaces generated by them. Thus, 𝐹 = (𝐺 ∘ 𝐷) belongs to the subspace sum. Part of proof of Lemma M in [Crawley] p. 121 line 5. (Contributed by NM, 8-Sep-2014.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑌) & ⊢ ⊕ = (LSSum‘𝑌) & ⊢ 𝑁 = (LSpan‘𝑌) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝑄 = ((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉)) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊)) & ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) & ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) & ⊢ (𝜑 → (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) ≠ 𝑃)) & ⊢ (𝜑 → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉)) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) & ⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑈) & ⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝑇) & ⊢ (𝜑 → (𝐺‘𝑃) = 𝑄) & ⊢ (𝜑 → 𝐷 ∈ 𝑇) & ⊢ (𝜑 → (𝐷‘𝑄) = (𝐹‘𝑃)) ⇒ ⊢ (𝜑 → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))) | ||
Theorem | dia2dimlem6 37225 | Lemma for dia2dim 37233. Eliminate auxiliary translations 𝐺 and 𝐷. (Contributed by NM, 8-Sep-2014.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑌) & ⊢ ⊕ = (LSSum‘𝑌) & ⊢ 𝑁 = (LSpan‘𝑌) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝑄 = ((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉)) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊)) & ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) & ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) & ⊢ (𝜑 → (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) ≠ 𝑃)) & ⊢ (𝜑 → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉)) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) & ⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑈) & ⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑉) ⇒ ⊢ (𝜑 → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))) | ||
Theorem | dia2dimlem7 37226 | Lemma for dia2dim 37233. Eliminate (𝐹‘𝑃) ≠ 𝑃 condition. (Contributed by NM, 8-Sep-2014.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑌) & ⊢ ⊕ = (LSSum‘𝑌) & ⊢ 𝑁 = (LSpan‘𝑌) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝑄 = ((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉)) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊)) & ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) & ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) & ⊢ (𝜑 → 𝐹 ∈ 𝑇) & ⊢ (𝜑 → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉)) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) & ⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑈) & ⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑉) ⇒ ⊢ (𝜑 → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))) | ||
Theorem | dia2dimlem8 37227 | Lemma for dia2dim 37233. Eliminate no-longer used auxiliary atoms 𝑃 and 𝑄. (Contributed by NM, 8-Sep-2014.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑌) & ⊢ ⊕ = (LSSum‘𝑌) & ⊢ 𝑁 = (LSpan‘𝑌) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊)) & ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) & ⊢ (𝜑 → 𝐹 ∈ 𝑇) & ⊢ (𝜑 → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉)) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) & ⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑈) & ⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑉) ⇒ ⊢ (𝜑 → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))) | ||
Theorem | dia2dimlem9 37228 | Lemma for dia2dim 37233. Eliminate (𝑅‘𝐹) ≠ 𝑈, 𝑉 conditions. (Contributed by NM, 8-Sep-2014.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑌) & ⊢ ⊕ = (LSSum‘𝑌) & ⊢ 𝑁 = (LSpan‘𝑌) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊)) & ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) & ⊢ (𝜑 → 𝐹 ∈ 𝑇) & ⊢ (𝜑 → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉)) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) ⇒ ⊢ (𝜑 → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))) | ||
Theorem | dia2dimlem10 37229 | Lemma for dia2dim 37233. Convert membership in closed subspace (𝐼‘(𝑈 ∨ 𝑉)) to a lattice ordering. (Contributed by NM, 8-Sep-2014.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑌) & ⊢ 𝑁 = (LSpan‘𝑌) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊)) & ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) & ⊢ (𝜑 → 𝐹 ∈ 𝑇) & ⊢ (𝜑 → 𝐹 ∈ (𝐼‘(𝑈 ∨ 𝑉))) ⇒ ⊢ (𝜑 → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉)) | ||
Theorem | dia2dimlem11 37230 | Lemma for dia2dim 37233. Convert ordering hypothesis on 𝑅‘𝐹 to subspace membership 𝐹 ∈ (𝐼‘(𝑈 ∨ 𝑉)). (Contributed by NM, 8-Sep-2014.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑌) & ⊢ ⊕ = (LSSum‘𝑌) & ⊢ 𝑁 = (LSpan‘𝑌) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊)) & ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) & ⊢ (𝜑 → 𝐹 ∈ 𝑇) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ (𝐼‘(𝑈 ∨ 𝑉))) ⇒ ⊢ (𝜑 → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))) | ||
Theorem | dia2dimlem12 37231 | Lemma for dia2dim 37233. Obtain subset relation. (Contributed by NM, 8-Sep-2014.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑌) & ⊢ ⊕ = (LSSum‘𝑌) & ⊢ 𝑁 = (LSpan‘𝑌) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊)) & ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) ⇒ ⊢ (𝜑 → (𝐼‘(𝑈 ∨ 𝑉)) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))) | ||
Theorem | dia2dimlem13 37232 | Lemma for dia2dim 37233. Eliminate 𝑈 ≠ 𝑉 condition. (Contributed by NM, 8-Sep-2014.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑌) & ⊢ ⊕ = (LSSum‘𝑌) & ⊢ 𝑁 = (LSpan‘𝑌) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊)) & ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ⇒ ⊢ (𝜑 → (𝐼‘(𝑈 ∨ 𝑉)) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))) | ||
Theorem | dia2dim 37233 | A two-dimensional subspace of partial vector space A is closed, or equivalently, the isomorphism of a join of two atoms is a subset of the subspace sum of the isomorphisms of each atom (and thus they are equal, as shown later for the full vector space H). (Contributed by NM, 9-Sep-2014.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑌) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊)) & ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ⇒ ⊢ (𝜑 → (𝐼‘(𝑈 ∨ 𝑉)) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))) | ||
Syntax | cdvh 37234 | Extend class notation with constructed full vector space H. |
class DVecH | ||
Definition | df-dvech 37235* | Define constructed full vector space H. (Contributed by NM, 17-Oct-2013.) |
⊢ DVecH = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ ({〈(Base‘ndx), (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤))〉, 〈(+g‘ndx), (𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)), 𝑔 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ 〈((1st ‘𝑓) ∘ (1st ‘𝑔)), (ℎ ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ)))〉)〉, 〈(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)〉} ∪ {〈( ·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉)〉}))) | ||
Theorem | dvhfset 37236* | The constructed full vector space H for a lattice 𝐾. (Contributed by NM, 17-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → (DVecH‘𝐾) = (𝑤 ∈ 𝐻 ↦ ({〈(Base‘ndx), (((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤))〉, 〈(+g‘ndx), (𝑓 ∈ (((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤)), 𝑔 ∈ (((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤)) ↦ 〈((1st ‘𝑓) ∘ (1st ‘𝑔)), (ℎ ∈ ((LTrn‘𝐾)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ)))〉)〉, 〈(Scalar‘ndx), ((EDRing‘𝐾)‘𝑤)〉} ∪ {〈( ·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ (((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤)) ↦ 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉)〉}))) | ||
Theorem | dvhset 37237* | The constructed full vector space H for a lattice 𝐾. (Contributed by NM, 17-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝐷 = ((EDRing‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → 𝑈 = ({〈(Base‘ndx), (𝑇 × 𝐸)〉, 〈(+g‘ndx), (𝑓 ∈ (𝑇 × 𝐸), 𝑔 ∈ (𝑇 × 𝐸) ↦ 〈((1st ‘𝑓) ∘ (1st ‘𝑔)), (ℎ ∈ 𝑇 ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ)))〉)〉, 〈(Scalar‘ndx), 𝐷〉} ∪ {〈( ·𝑠 ‘ndx), (𝑠 ∈ 𝐸, 𝑓 ∈ (𝑇 × 𝐸) ↦ 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉)〉})) | ||
Theorem | dvhsca 37238 | The ring of scalars of the constructed full vector space H. (Contributed by NM, 22-Jun-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐷 = ((EDRing‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑈) ⇒ ⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → 𝐹 = 𝐷) | ||
Theorem | dvhbase 37239 | The ring base set of the constructed full vector space H. (Contributed by NM, 29-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑈) & ⊢ 𝐶 = (Base‘𝐹) ⇒ ⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → 𝐶 = 𝐸) | ||
Theorem | dvhfplusr 37240* | Ring addition operation for the constructed full vector space H. (Contributed by NM, 29-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑈) & ⊢ + = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))) & ⊢ ✚ = (+g‘𝐹) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → ✚ = + ) | ||
Theorem | dvhfmulr 37241* | Ring multiplication operation for the constructed full vector space H. (Contributed by NM, 29-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑈) & ⊢ · = (.r‘𝐹) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → · = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑠 ∘ 𝑡))) | ||
Theorem | dvhmulr 37242 | Ring multiplication operation for the constructed full vector space H. (Contributed by NM, 29-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑈) & ⊢ · = (.r‘𝐹) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐸 ∧ 𝑆 ∈ 𝐸)) → (𝑅 · 𝑆) = (𝑅 ∘ 𝑆)) | ||
Theorem | dvhvbase 37243 | The vectors (vector base set) of the constructed full vector space H are all translations (for a fiducial co-atom 𝑊). (Contributed by NM, 2-Nov-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) ⇒ ⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → 𝑉 = (𝑇 × 𝐸)) | ||
Theorem | dvhelvbasei 37244 | Vector membership in the constructed full vector space H. (Contributed by NM, 20-Feb-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) ⇒ ⊢ (((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸)) → 〈𝐹, 𝑆〉 ∈ 𝑉) | ||
Theorem | dvhvaddcbv 37245* | Change bound variables to isolate them later. (Contributed by NM, 3-Nov-2013.) |
⊢ + = (𝑓 ∈ (𝑇 × 𝐸), 𝑔 ∈ (𝑇 × 𝐸) ↦ 〈((1st ‘𝑓) ∘ (1st ‘𝑔)), ((2nd ‘𝑓) ⨣ (2nd ‘𝑔))〉) ⇒ ⊢ + = (ℎ ∈ (𝑇 × 𝐸), 𝑖 ∈ (𝑇 × 𝐸) ↦ 〈((1st ‘ℎ) ∘ (1st ‘𝑖)), ((2nd ‘ℎ) ⨣ (2nd ‘𝑖))〉) | ||
Theorem | dvhvaddval 37246* | The vector sum operation for the constructed full vector space H. (Contributed by NM, 26-Oct-2013.) |
⊢ + = (𝑓 ∈ (𝑇 × 𝐸), 𝑔 ∈ (𝑇 × 𝐸) ↦ 〈((1st ‘𝑓) ∘ (1st ‘𝑔)), ((2nd ‘𝑓) ⨣ (2nd ‘𝑔))〉) ⇒ ⊢ ((𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸)) → (𝐹 + 𝐺) = 〈((1st ‘𝐹) ∘ (1st ‘𝐺)), ((2nd ‘𝐹) ⨣ (2nd ‘𝐺))〉) | ||
Theorem | dvhfvadd 37247* | The vector sum operation for the constructed full vector space H. (Contributed by NM, 26-Oct-2013.) (Revised by Mario Carneiro, 23-Jun-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑈) & ⊢ ⨣ = (+g‘𝐷) & ⊢ ✚ = (𝑓 ∈ (𝑇 × 𝐸), 𝑔 ∈ (𝑇 × 𝐸) ↦ 〈((1st ‘𝑓) ∘ (1st ‘𝑔)), ((2nd ‘𝑓) ⨣ (2nd ‘𝑔))〉) & ⊢ + = (+g‘𝑈) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → + = ✚ ) | ||
Theorem | dvhvadd 37248 | The vector sum operation for the constructed full vector space H. (Contributed by NM, 11-Feb-2014.) (Revised by Mario Carneiro, 23-Jun-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ ⨣ = (+g‘𝐷) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸))) → (𝐹 + 𝐺) = 〈((1st ‘𝐹) ∘ (1st ‘𝐺)), ((2nd ‘𝐹) ⨣ (2nd ‘𝐺))〉) | ||
Theorem | dvhopvadd 37249 | The vector sum operation for the constructed full vector space H. (Contributed by NM, 21-Feb-2014.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ ⨣ = (+g‘𝐷) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐸) ∧ (𝐺 ∈ 𝑇 ∧ 𝑅 ∈ 𝐸)) → (〈𝐹, 𝑄〉 + 〈𝐺, 𝑅〉) = 〈(𝐹 ∘ 𝐺), (𝑄 ⨣ 𝑅)〉) | ||
Theorem | dvhopvadd2 37250* | The vector sum operation for the constructed full vector space H. TODO: check if this will shorten proofs that use dvhopvadd 37249 and/or dvhfplusr 37240. (Contributed by NM, 26-Sep-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ + = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ✚ = (+g‘𝑈) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐸) ∧ (𝐺 ∈ 𝑇 ∧ 𝑅 ∈ 𝐸)) → (〈𝐹, 𝑄〉 ✚ 〈𝐺, 𝑅〉) = 〈(𝐹 ∘ 𝐺), (𝑄 + 𝑅)〉) | ||
Theorem | dvhvaddcl 37251 | Closure of the vector sum operation for the constructed full vector space H. (Contributed by NM, 26-Oct-2013.) (Revised by Mario Carneiro, 23-Jun-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑈) & ⊢ ⨣ = (+g‘𝐷) & ⊢ + = (+g‘𝑈) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸))) → (𝐹 + 𝐺) ∈ (𝑇 × 𝐸)) | ||
Theorem | dvhvaddcomN 37252 | Commutativity of vector sum. (Contributed by NM, 26-Oct-2013.) (Revised by Mario Carneiro, 23-Jun-2014.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑈) & ⊢ ⨣ = (+g‘𝐷) & ⊢ + = (+g‘𝑈) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸))) → (𝐹 + 𝐺) = (𝐺 + 𝐹)) | ||
Theorem | dvhvaddass 37253 | Associativity of vector sum. (Contributed by NM, 31-Oct-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑈) & ⊢ ⨣ = (+g‘𝐷) & ⊢ + = (+g‘𝑈) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → ((𝐹 + 𝐺) + 𝐼) = (𝐹 + (𝐺 + 𝐼))) | ||
Theorem | dvhvscacbv 37254* | Change bound variables to isolate them later. (Contributed by NM, 20-Nov-2013.) |
⊢ · = (𝑠 ∈ 𝐸, 𝑓 ∈ (𝑇 × 𝐸) ↦ 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉) ⇒ ⊢ · = (𝑡 ∈ 𝐸, 𝑔 ∈ (𝑇 × 𝐸) ↦ 〈(𝑡‘(1st ‘𝑔)), (𝑡 ∘ (2nd ‘𝑔))〉) | ||
Theorem | dvhvscaval 37255* | The scalar product operation for the constructed full vector space H. (Contributed by NM, 20-Nov-2013.) |
⊢ · = (𝑠 ∈ 𝐸, 𝑓 ∈ (𝑇 × 𝐸) ↦ 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉) ⇒ ⊢ ((𝑈 ∈ 𝐸 ∧ 𝐹 ∈ (𝑇 × 𝐸)) → (𝑈 · 𝐹) = 〈(𝑈‘(1st ‘𝐹)), (𝑈 ∘ (2nd ‘𝐹))〉) | ||
Theorem | dvhfvsca 37256* | Scalar product operation for the constructed full vector space H. (Contributed by NM, 2-Nov-2013.) (Revised by Mario Carneiro, 23-Jun-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑈) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → · = (𝑠 ∈ 𝐸, 𝑓 ∈ (𝑇 × 𝐸) ↦ 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉)) | ||
Theorem | dvhvsca 37257 | Scalar product operation for the constructed full vector space H. (Contributed by NM, 2-Nov-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑈) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐸 ∧ 𝐹 ∈ (𝑇 × 𝐸))) → (𝑅 · 𝐹) = 〈(𝑅‘(1st ‘𝐹)), (𝑅 ∘ (2nd ‘𝐹))〉) | ||
Theorem | dvhopvsca 37258 | Scalar product operation for the constructed full vector space H. (Contributed by NM, 20-Feb-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑈) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝐸)) → (𝑅 · 〈𝐹, 𝑋〉) = 〈(𝑅‘𝐹), (𝑅 ∘ 𝑋)〉) | ||
Theorem | dvhvscacl 37259 | Closure of the scalar product operation for the constructed full vector space H. (Contributed by NM, 12-Feb-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑈) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐸 ∧ 𝐹 ∈ (𝑇 × 𝐸))) → (𝑅 · 𝐹) ∈ (𝑇 × 𝐸)) | ||
Theorem | tendoinvcl 37260* | Closure of multiplicative inverse for endomorphism. We use the scalar inverse of the vector space since it is much simpler than the direct inverse of cdleml8 37139. (Contributed by NM, 10-Apr-2014.) (Revised by Mario Carneiro, 23-Jun-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑈) & ⊢ 𝑁 = (invr‘𝐹) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂) → ((𝑁‘𝑆) ∈ 𝐸 ∧ (𝑁‘𝑆) ≠ 𝑂)) | ||
Theorem | tendolinv 37261* | Left multiplicative inverse for endomorphism. (Contributed by NM, 10-Apr-2014.) (Revised by Mario Carneiro, 23-Jun-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑈) & ⊢ 𝑁 = (invr‘𝐹) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂) → ((𝑁‘𝑆) ∘ 𝑆) = ( I ↾ 𝑇)) | ||
Theorem | tendorinv 37262* | Right multiplicative inverse for endomorphism. (Contributed by NM, 10-Apr-2014.) (Revised by Mario Carneiro, 23-Jun-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑈) & ⊢ 𝑁 = (invr‘𝐹) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂) → (𝑆 ∘ (𝑁‘𝑆)) = ( I ↾ 𝑇)) | ||
Theorem | dvhgrp 37263 | The full vector space 𝑈 constructed from a Hilbert lattice 𝐾 (given a fiducial hyperplane 𝑊) is a group. (Contributed by NM, 19-Oct-2013.) (Revised by Mario Carneiro, 24-Jun-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑈) & ⊢ ⨣ = (+g‘𝐷) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐼 = (invg‘𝐷) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑈 ∈ Grp) | ||
Theorem | dvhlveclem 37264 | Lemma for dvhlvec 37265. TODO: proof substituting inner part first shorter/longer than substituting outer part first? TODO: break up into smaller lemmas? TODO: does 𝜑 → method shorten proof? (Contributed by NM, 22-Oct-2013.) (Proof shortened by Mario Carneiro, 24-Jun-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑈) & ⊢ ⨣ = (+g‘𝐷) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐼 = (invg‘𝐷) & ⊢ × = (.r‘𝐷) & ⊢ · = ( ·𝑠 ‘𝑈) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑈 ∈ LVec) | ||
Theorem | dvhlvec 37265 | The full vector space 𝑈 constructed from a Hilbert lattice 𝐾 (given a fiducial hyperplane 𝑊) is a left module. (Contributed by NM, 23-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝑈 ∈ LVec) | ||
Theorem | dvhlmod 37266 | The full vector space 𝑈 constructed from a Hilbert lattice 𝐾 (given a fiducial hyperplane 𝑊) is a left module. (Contributed by NM, 23-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝑈 ∈ LMod) | ||
Theorem | dvh0g 37267* | The zero vector of vector space H has the zero translation as its first member and the zero trace-preserving endomorphism as the second. (Contributed by NM, 9-Mar-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 0 = 〈( I ↾ 𝐵), 𝑂〉) | ||
Theorem | dvheveccl 37268 | Properties of a unit vector that we will use later as a convenient reference vector. This vector is called "e" in the remark after Lemma M of [Crawley] p. 121. line 17. See also dvhopN 37272 and dihpN 37492. (Contributed by NM, 27-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐸 = 〈( I ↾ 𝐵), ( I ↾ 𝑇)〉 & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝐸 ∈ (𝑉 ∖ { 0 })) | ||
Theorem | dvhopclN 37269 | Closure of a DVecH vector expressed as ordered pair. (Contributed by NM, 20-Nov-2013.) (New usage is discouraged.) |
⊢ ((𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸) → 〈𝐹, 𝑈〉 ∈ (𝑇 × 𝐸)) | ||
Theorem | dvhopaddN 37270* | Sum of DVecH vectors expressed as ordered pair. (Contributed by NM, 20-Nov-2013.) (New usage is discouraged.) |
⊢ 𝐴 = (𝑓 ∈ (𝑇 × 𝐸), 𝑔 ∈ (𝑇 × 𝐸) ↦ 〈((1st ‘𝑓) ∘ (1st ‘𝑔)), ((2nd ‘𝑓)𝑃(2nd ‘𝑔))〉) ⇒ ⊢ (((𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸) ∧ (𝐺 ∈ 𝑇 ∧ 𝑉 ∈ 𝐸)) → (〈𝐹, 𝑈〉𝐴〈𝐺, 𝑉〉) = 〈(𝐹 ∘ 𝐺), (𝑈𝑃𝑉)〉) | ||
Theorem | dvhopspN 37271* | Scalar product of DVecH vector expressed as ordered pair. (Contributed by NM, 20-Nov-2013.) (New usage is discouraged.) |
⊢ 𝑆 = (𝑠 ∈ 𝐸, 𝑓 ∈ (𝑇 × 𝐸) ↦ 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉) ⇒ ⊢ ((𝑅 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸)) → (𝑅𝑆〈𝐹, 𝑈〉) = 〈(𝑅‘𝐹), (𝑅 ∘ 𝑈)〉) | ||
Theorem | dvhopN 37272* | Decompose a DVecH vector expressed as an ordered pair into the sum of two components, the first from the translation group vector base of DVecA and the other from the one-dimensional vector subspace 𝐸. Part of Lemma M of [Crawley] p. 121, line 18. We represent their e, sigma, f by 〈( I ↾ 𝐵), ( I ↾ 𝑇)〉, 𝑈, 〈𝐹, 𝑂〉. We swapped the order of vector sum (their juxtaposition i.e. composition) to show 〈𝐹, 𝑂〉 first. Note that 𝑂 and ( I ↾ 𝑇) are the zero and one of the division ring 𝐸, and ( I ↾ 𝐵) is the zero of the translation group. 𝑆 is the scalar product. (Contributed by NM, 21-Nov-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑃 = (𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (𝑐 ∈ 𝑇 ↦ ((𝑎‘𝑐) ∘ (𝑏‘𝑐)))) & ⊢ 𝐴 = (𝑓 ∈ (𝑇 × 𝐸), 𝑔 ∈ (𝑇 × 𝐸) ↦ 〈((1st ‘𝑓) ∘ (1st ‘𝑔)), ((2nd ‘𝑓)𝑃(2nd ‘𝑔))〉) & ⊢ 𝑆 = (𝑠 ∈ 𝐸, 𝑓 ∈ (𝑇 × 𝐸) ↦ 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉) & ⊢ 𝑂 = (𝑐 ∈ 𝑇 ↦ ( I ↾ 𝐵)) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸)) → 〈𝐹, 𝑈〉 = (〈𝐹, 𝑂〉𝐴(𝑈𝑆〈( I ↾ 𝐵), ( I ↾ 𝑇)〉))) | ||
Theorem | dvhopellsm 37273* | Ordered pair membership in a subspace sum. (Contributed by NM, 12-Mar-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ + = (+g‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (〈𝐹, 𝑇〉 ∈ (𝑋 ⊕ 𝑌) ↔ ∃𝑥∃𝑦∃𝑧∃𝑤((〈𝑥, 𝑦〉 ∈ 𝑋 ∧ 〈𝑧, 𝑤〉 ∈ 𝑌) ∧ 〈𝐹, 𝑇〉 = (〈𝑥, 𝑦〉 + 〈𝑧, 𝑤〉)))) | ||
Theorem | cdlemm10N 37274* | The image of the map 𝐺 is the entire one-dimensional subspace (𝐼‘𝑉). Remark after Lemma M of [Crawley] p. 121 line 23. (Contributed by NM, 24-Nov-2013.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝐶 = {𝑟 ∈ 𝐴 ∣ (𝑟 ≤ (𝑃 ∨ 𝑉) ∧ ¬ 𝑟 ≤ 𝑊)} & ⊢ 𝐹 = (℩𝑓 ∈ 𝑇 (𝑓‘𝑃) = 𝑠) & ⊢ 𝐺 = (𝑞 ∈ 𝐶 ↦ (℩𝑓 ∈ 𝑇 (𝑓‘𝑃) = 𝑞)) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) → ran 𝐺 = (𝐼‘𝑉)) | ||
Syntax | cocaN 37275 | Extend class notation with subspace orthocomplement for DVecA partial vector space. |
class ocA | ||
Definition | df-docaN 37276* | Define subspace orthocomplement for DVecA partial vector space. Temporarily, we are using the range of the isomorphism instead of the set of closed subspaces. Later, when inner product is introduced, we will show that these are the same. (Contributed by NM, 6-Dec-2013.) |
⊢ ocA = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤))))) | ||
Theorem | docaffvalN 37277* | Subspace orthocomplement for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → (ocA‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤) ↦ (((DIsoA‘𝐾)‘𝑤)‘((( ⊥ ‘(◡((DIsoA‘𝐾)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝐾)‘𝑤) ∣ 𝑥 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑤)) ∧ 𝑤))))) | ||
Theorem | docafvalN 37278* | Subspace orthocomplement for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝑁 = ((ocA‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝑁 = (𝑥 ∈ 𝒫 𝑇 ↦ (𝐼‘((( ⊥ ‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑥 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑊)) ∧ 𝑊)))) | ||
Theorem | docavalN 37279* | Subspace orthocomplement for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝑁 = ((ocA‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑇) → (𝑁‘𝑋) = (𝐼‘((( ⊥ ‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑊)) ∧ 𝑊))) | ||
Theorem | docaclN 37280 | Closure of subspace orthocomplement for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocA‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑇) → ( ⊥ ‘𝑋) ∈ ran 𝐼) | ||
Theorem | diaocN 37281 | Value of partial isomorphism A at lattice orthocomplement (using a Sasaki projection to get orthocomplement relative to the fiducial co-atom 𝑊). (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝑁 = ((ocA‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘((( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑊)) ∧ 𝑊)) = (𝑁‘(𝐼‘𝑋))) | ||
Theorem | doca2N 37282 | Double orthocomplement of partial isomorphism A. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocA‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → ( ⊥ ‘( ⊥ ‘(𝐼‘𝑋))) = (𝐼‘𝑋)) | ||
Theorem | doca3N 37283 | Double orthocomplement of partial isomorphism A. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocA‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ ran 𝐼) → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) | ||
Theorem | dvadiaN 37284 | Any closed subspace is a member of the range of partial isomorphism A, showing the isomorphism maps onto the set of closed subspaces of partial vector space A. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocA‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝑆 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋)) → 𝑋 ∈ ran 𝐼) | ||
Theorem | diarnN 37285* | Partial isomorphism A maps onto the set of all closed subspaces of partial vector space A. Part of Lemma M of [Crawley] p. 121 line 12, with closed subspaces rather than subspaces. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocA‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ran 𝐼 = {𝑥 ∈ 𝑆 ∣ ( ⊥ ‘( ⊥ ‘𝑥)) = 𝑥}) | ||
Theorem | diaf1oN 37286* | The partial isomorphism A for a lattice 𝐾 is a one-to-one, onto function. Part of Lemma M of [Crawley] p. 121 line 12, with closed subspaces rather than subspaces. See diadm 37191 for the domain. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocA‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐼:dom 𝐼–1-1-onto→{𝑥 ∈ 𝑆 ∣ ( ⊥ ‘( ⊥ ‘𝑥)) = 𝑥}) | ||
Syntax | cdjaN 37287 | Extend class notation with subspace join for DVecA partial vector space. |
class vA | ||
Definition | df-djaN 37288* | Define (closed) subspace join for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) |
⊢ vA = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤), 𝑦 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((ocA‘𝑘)‘𝑤)‘((((ocA‘𝑘)‘𝑤)‘𝑥) ∩ (((ocA‘𝑘)‘𝑤)‘𝑦)))))) | ||
Theorem | djaffvalN 37289* | Subspace join for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → (vA‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤), 𝑦 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤) ↦ (((ocA‘𝐾)‘𝑤)‘((((ocA‘𝐾)‘𝑤)‘𝑥) ∩ (((ocA‘𝐾)‘𝑤)‘𝑦)))))) | ||
Theorem | djafvalN 37290* | Subspace join for DVecA partial vector space. TODO: take out hypothesis .i, no longer used. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocA‘𝐾)‘𝑊) & ⊢ 𝐽 = ((vA‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐽 = (𝑥 ∈ 𝒫 𝑇, 𝑦 ∈ 𝒫 𝑇 ↦ ( ⊥ ‘(( ⊥ ‘𝑥) ∩ ( ⊥ ‘𝑦))))) | ||
Theorem | djavalN 37291 | Subspace join for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocA‘𝐾)‘𝑊) & ⊢ 𝐽 = ((vA‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑇 ∧ 𝑌 ⊆ 𝑇)) → (𝑋𝐽𝑌) = ( ⊥ ‘(( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑌)))) | ||
Theorem | djaclN 37292 | Closure of subspace join for DVecA partial vector space. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝐽 = ((vA‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑇 ∧ 𝑌 ⊆ 𝑇)) → (𝑋𝐽𝑌) ∈ ran 𝐼) | ||
Theorem | djajN 37293 | Transfer lattice join to DVecA partial vector space closed subspace join. Part of Lemma M of [Crawley] p. 120 line 29, with closed subspace join rather than subspace sum. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝐽 = ((vA‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘(𝑋 ∨ 𝑌)) = ((𝐼‘𝑋)𝐽(𝐼‘𝑌))) | ||
Syntax | cdib 37294 | Extend class notation with isomorphism B. |
class DIsoB | ||
Definition | df-dib 37295* | Isomorphism B is isomorphism A extended with an extra dimension set to the zero vector component i.e. the zero endormorphism. Its domain is lattice elements less than or equal to the fiducial co-atom 𝑤. (Contributed by NM, 8-Dec-2013.) |
⊢ DIsoB = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ dom ((DIsoA‘𝑘)‘𝑤) ↦ ((((DIsoA‘𝑘)‘𝑤)‘𝑥) × {(𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))})))) | ||
Theorem | dibffval 37296* | The partial isomorphism B for a lattice 𝐾. (Contributed by NM, 8-Dec-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → (DIsoB‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ dom ((DIsoA‘𝐾)‘𝑤) ↦ ((((DIsoA‘𝐾)‘𝑤)‘𝑥) × {(𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ ( I ↾ 𝐵))})))) | ||
Theorem | dibfval 37297* | The partial isomorphism B for a lattice 𝐾. (Contributed by NM, 8-Dec-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 0 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝐽 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐼 = (𝑥 ∈ dom 𝐽 ↦ ((𝐽‘𝑥) × { 0 }))) | ||
Theorem | dibval 37298* | The partial isomorphism B for a lattice 𝐾. (Contributed by NM, 8-Dec-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 0 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝐽 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐽) → (𝐼‘𝑋) = ((𝐽‘𝑋) × { 0 })) | ||
Theorem | dibopelvalN 37299* | Member of the partial isomorphism B. (Contributed by NM, 18-Jan-2014.) (Revised by Mario Carneiro, 6-May-2015.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 0 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝐽 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐽) → (〈𝐹, 𝑆〉 ∈ (𝐼‘𝑋) ↔ (𝐹 ∈ (𝐽‘𝑋) ∧ 𝑆 = 0 ))) | ||
Theorem | dibval2 37300* | Value of the partial isomorphism B. (Contributed by NM, 18-Jan-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 0 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝐽 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) = ((𝐽‘𝑋) × { 0 })) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |