P. 417 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 41601-41700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dvavbase 41601	The vectors (vector base set) of the constructed partial vector space A are all translations (for a fiducial co-atom 𝑊). (Contributed by NM, 9-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    ⇒   ⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → 𝑉 = 𝑇)
Theorem	dvafvadd 41602*	The vector sum operation for the constructed partial vector space A. (Contributed by NM, 9-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝑈)    ⇒   ⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → + = (𝑓 ∈ 𝑇, 𝑔 ∈ 𝑇 ↦ (𝑓 ∘ 𝑔)))
Theorem	dvavadd 41603	Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝑈)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → (𝐹 + 𝐺) = (𝐹 ∘ 𝐺))
Theorem	dvafvsca 41604*	Ring addition operation for the constructed partial vector space A. (Contributed by NM, 9-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑈)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → · = (𝑠 ∈ 𝐸, 𝑓 ∈ 𝑇 ↦ (𝑠‘𝑓)))
Theorem	dvavsca 41605	Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑈)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇)) → (𝑅 · 𝐹) = (𝑅‘𝐹))
Theorem	tendospcl 41606	Closure of endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → (𝑈‘𝐹) ∈ 𝑇)
Theorem	tendospass 41607	Associative law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇)) → ((𝑈 ∘ 𝑉)‘𝐹) = (𝑈‘(𝑉‘𝐹)))
Theorem	tendospdi1 41608	Forward distributive law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → (𝑈‘(𝐹 ∘ 𝐺)) = ((𝑈‘𝐹) ∘ (𝑈‘𝐺)))
Theorem	tendocnv 41609	Converse of a trace-preserving endomorphism value. (Contributed by NM, 7-Apr-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → ◡(𝑆‘𝐹) = (𝑆‘◡𝐹))
Theorem	tendospdi2 41610*	Reverse distributive law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.)
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))    ⇒   ⊢ ((𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → ((𝑈𝑃𝑉)‘𝐹) = ((𝑈‘𝐹) ∘ (𝑉‘𝐹)))
Theorem	tendospcanN 41611*	Cancellation law for trace-preserving endomorphism values (used as scalar product). (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → ((𝑆‘𝐹) = (𝑆‘𝐺) ↔ 𝐹 = 𝐺))
Theorem	dvaabl 41612	The constructed partial vector space A for a lattice 𝐾 is an abelian group. (Contributed by NM, 11-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑈 ∈ Abel)
Theorem	dvalveclem 41613	Lemma for dvalvec 41614. (Contributed by NM, 11-Oct-2013.) (Proof shortened by Mario Carneiro, 22-Jun-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⨣ = (+g‘𝐷)    &   ⊢ × = (.r‘𝐷)    &   ⊢ · = ( ·𝑠 ‘𝑈)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑈 ∈ LVec)
Theorem	dvalvec 41614	The constructed partial vector space A for a lattice 𝐾 is a left vector space. (Contributed by NM, 11-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑈 ∈ LVec)
Theorem	dva0g 41615	The zero vector of partial vector space A. (Contributed by NM, 9-Sep-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊)    &   ⊢ 0 = (0g‘𝑈)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 0 = ( I ↾ 𝐵))
Syntax	cdia 41616	Extend class notation with partial isomorphism A.
class DIsoA
Definition	df-disoa 41617*	Define partial isomorphism A. (Contributed by NM, 15-Oct-2013.)
⊢ DIsoA = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} ↦ {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥})))
Theorem	diaffval 41618*	The partial isomorphism A for a lattice 𝐾. (Contributed by NM, 15-Oct-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → (DIsoA‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) ≤ 𝑥})))
Theorem	diafval 41619*	The partial isomorphism A for a lattice 𝐾. (Contributed by NM, 15-Oct-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐼 = (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑊} ↦ {𝑓 ∈ 𝑇 ∣ (𝑅‘𝑓) ≤ 𝑥}))
Theorem	diaval 41620*	The partial isomorphism A for a lattice 𝐾. Definition of isomorphism map in [Crawley] p. 120 line 24. (Contributed by NM, 15-Oct-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) = {𝑓 ∈ 𝑇 ∣ (𝑅‘𝑓) ≤ 𝑋})
Theorem	diaelval 41621	Member of the partial isomorphism A for a lattice 𝐾. (Contributed by NM, 3-Dec-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐹 ∈ (𝐼‘𝑋) ↔ (𝐹 ∈ 𝑇 ∧ (𝑅‘𝐹) ≤ 𝑋)))
Theorem	diafn 41622*	Functionality and domain of the partial isomorphism A. (Contributed by NM, 26-Nov-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐼 Fn {𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊})
Theorem	diadm 41623*	Domain of the partial isomorphism A. (Contributed by NM, 3-Dec-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → dom 𝐼 = {𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊})
Theorem	diaeldm 41624	Member of domain of the partial isomorphism A. (Contributed by NM, 4-Dec-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → (𝑋 ∈ dom 𝐼 ↔ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)))
Theorem	diadmclN 41625	A member of domain of the partial isomorphism A is a lattice element. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → 𝑋 ∈ 𝐵)
Theorem	diadmleN 41626	A member of domain of the partial isomorphism A is under the fiducial hyperplane. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → 𝑋 ≤ 𝑊)
Theorem	dian0 41627	The value of the partial isomorphism A is not empty. (Contributed by NM, 17-Jan-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) ≠ ∅)
Theorem	dia0eldmN 41628	The lattice zero belongs to the domain of partial isomorphism A. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.)
⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 0 ∈ dom 𝐼)
Theorem	dia1eldmN 41629	The fiducial hyperplane (the largest allowed lattice element) belongs to the domain of partial isomorphism A. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ dom 𝐼)
Theorem	diass 41630	The value of the partial isomorphism A is a set of translations, i.e., a set of vectors. (Contributed by NM, 26-Nov-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) ⊆ 𝑇)
Theorem	diael 41631	A member of the value of the partial isomorphism A is a translation, i.e., a vector. (Contributed by NM, 17-Jan-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ (𝐼‘𝑋)) → 𝐹 ∈ 𝑇)
Theorem	diatrl 41632	Trace of a member of the partial isomorphism A. (Contributed by NM, 17-Jan-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ (𝐼‘𝑋)) → (𝑅‘𝐹) ≤ 𝑋)
Theorem	diaelrnN 41633	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 41634	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 41635	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 41636	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 41637	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 41638	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 41639	Closure of partial isomorphism A converse. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ ran 𝐼) → (◡𝐼‘𝑋) ∈ dom 𝐼)
Theorem	dia0 41640	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 41641	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 41642	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 41643*	Partial isomorphism A of a lattice glb. (Contributed by NM, 3-Dec-2013.) (New usage is discouraged.)
⊢ 𝐺 = (glb‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅)) → (𝐼‘(𝐺‘𝑆)) = ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))
Theorem	diameetN 41644	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 41645	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 41646	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 41647	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 41648	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 41649*	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 41650	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 41651	A vector (translation) belongs to the 1-dim subspace it generates. (Contributed by NM, 8-Sep-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹 ∈ (𝐼‘(𝑅‘𝐹)))
Theorem	dia2dimlem1 41652	Lemma for dia2dim 41665. 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 41653	Lemma for dia2dim 41665. 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 41654	Lemma for dia2dim 41665. 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 41655	Lemma for dia2dim 41665. 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 41656	Lemma for dia2dim 41665. 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 41657	Lemma for dia2dim 41665. 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 41658	Lemma for dia2dim 41665. Eliminate (𝐹‘𝑃) ≠ 𝑃 condition. (Contributed by NM, 8-Sep-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑌)    &   ⊢ ⊕ = (LSSum‘𝑌)    &   ⊢ 𝑁 = (LSpan‘𝑌)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    &   ⊢ 𝑄 = ((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉))    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))    &   ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))    &   ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))    &   ⊢ (𝜑 → 𝐹 ∈ 𝑇)    &   ⊢ (𝜑 → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉))    &   ⊢ (𝜑 → 𝑈 ≠ 𝑉)    &   ⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑈)    &   ⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑉)    ⇒   ⊢ (𝜑 → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
Theorem	dia2dimlem8 41659	Lemma for dia2dim 41665. 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 41660	Lemma for dia2dim 41665. Eliminate (𝑅‘𝐹) ≠ 𝑈, 𝑉 conditions. (Contributed by NM, 8-Sep-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑌)    &   ⊢ ⊕ = (LSSum‘𝑌)    &   ⊢ 𝑁 = (LSpan‘𝑌)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))    &   ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))    &   ⊢ (𝜑 → 𝐹 ∈ 𝑇)    &   ⊢ (𝜑 → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉))    &   ⊢ (𝜑 → 𝑈 ≠ 𝑉)    ⇒   ⊢ (𝜑 → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
Theorem	dia2dimlem10 41661	Lemma for dia2dim 41665. 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 41662	Lemma for dia2dim 41665. 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 41663	Lemma for dia2dim 41665. Obtain subset relation. (Contributed by NM, 8-Sep-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑌)    &   ⊢ ⊕ = (LSSum‘𝑌)    &   ⊢ 𝑁 = (LSpan‘𝑌)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))    &   ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))    &   ⊢ (𝜑 → 𝑈 ≠ 𝑉)    ⇒   ⊢ (𝜑 → (𝐼‘(𝑈 ∨ 𝑉)) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
Theorem	dia2dimlem13 41664	Lemma for dia2dim 41665. Eliminate 𝑈 ≠ 𝑉 condition. (Contributed by NM, 8-Sep-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑌)    &   ⊢ ⊕ = (LSSum‘𝑌)    &   ⊢ 𝑁 = (LSpan‘𝑌)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))    &   ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))    ⇒   ⊢ (𝜑 → (𝐼‘(𝑈 ∨ 𝑉)) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
Theorem	dia2dim 41665	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 41666	Extend class notation with constructed full vector space H.
class DVecH
Definition	df-dvech 41667*	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 41668*	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 41669*	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 41670	The ring of scalars of the constructed full vector space H. (Contributed by NM, 22-Jun-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐷 = ((EDRing‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑈)    ⇒   ⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → 𝐹 = 𝐷)
Theorem	dvhbase 41671	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 41672*	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 41673*	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 41674	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 41675	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 41676	Vector membership in the constructed full vector space H. (Contributed by NM, 20-Feb-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    ⇒   ⊢ (((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸)) → ⟨𝐹, 𝑆⟩ ∈ 𝑉)
Theorem	dvhvaddcbv 41677*	Change bound variables to isolate them later. (Contributed by NM, 3-Nov-2013.)
⊢ + = (𝑓 ∈ (𝑇 × 𝐸), 𝑔 ∈ (𝑇 × 𝐸) ↦ ⟨((1st ‘𝑓) ∘ (1st ‘𝑔)), ((2nd ‘𝑓) ⨣ (2nd ‘𝑔))⟩)    ⇒   ⊢ + = (ℎ ∈ (𝑇 × 𝐸), 𝑖 ∈ (𝑇 × 𝐸) ↦ ⟨((1st ‘ℎ) ∘ (1st ‘𝑖)), ((2nd ‘ℎ) ⨣ (2nd ‘𝑖))⟩)
Theorem	dvhvaddval 41678*	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 41679*	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 41680	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 41681	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 41682*	The vector sum operation for the constructed full vector space H. TODO: check if this will shorten proofs that use dvhopvadd 41681 and/or dvhfplusr 41672. (Contributed by NM, 26-Sep-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ + = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ✚ = (+g‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐸) ∧ (𝐺 ∈ 𝑇 ∧ 𝑅 ∈ 𝐸)) → (⟨𝐹, 𝑄⟩ ✚ ⟨𝐺, 𝑅⟩) = ⟨(𝐹 ∘ 𝐺), (𝑄 + 𝑅)⟩)
Theorem	dvhvaddcl 41683	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 41684	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 41685	Associativity of vector sum. (Contributed by NM, 31-Oct-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑈)    &   ⊢ ⨣ = (+g‘𝐷)    &   ⊢ + = (+g‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → ((𝐹 + 𝐺) + 𝐼) = (𝐹 + (𝐺 + 𝐼)))
Theorem	dvhvscacbv 41686*	Change bound variables to isolate them later. (Contributed by NM, 20-Nov-2013.)
⊢ · = (𝑠 ∈ 𝐸, 𝑓 ∈ (𝑇 × 𝐸) ↦ ⟨(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))⟩)    ⇒   ⊢ · = (𝑡 ∈ 𝐸, 𝑔 ∈ (𝑇 × 𝐸) ↦ ⟨(𝑡‘(1st ‘𝑔)), (𝑡 ∘ (2nd ‘𝑔))⟩)
Theorem	dvhvscaval 41687*	The scalar product operation for the constructed full vector space H. (Contributed by NM, 20-Nov-2013.)
⊢ · = (𝑠 ∈ 𝐸, 𝑓 ∈ (𝑇 × 𝐸) ↦ ⟨(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))⟩)    ⇒   ⊢ ((𝑈 ∈ 𝐸 ∧ 𝐹 ∈ (𝑇 × 𝐸)) → (𝑈 · 𝐹) = ⟨(𝑈‘(1st ‘𝐹)), (𝑈 ∘ (2nd ‘𝐹))⟩)
Theorem	dvhfvsca 41688*	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 41689	Scalar product operation for the constructed full vector space H. (Contributed by NM, 2-Nov-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑈)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐸 ∧ 𝐹 ∈ (𝑇 × 𝐸))) → (𝑅 · 𝐹) = ⟨(𝑅‘(1st ‘𝐹)), (𝑅 ∘ (2nd ‘𝐹))⟩)
Theorem	dvhopvsca 41690	Scalar product operation for the constructed full vector space H. (Contributed by NM, 20-Feb-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑈)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝐸)) → (𝑅 · ⟨𝐹, 𝑋⟩) = ⟨(𝑅‘𝐹), (𝑅 ∘ 𝑋)⟩)
Theorem	dvhvscacl 41691	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 41692*	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 41571. (Contributed by NM, 10-Apr-2014.) (Revised by Mario Carneiro, 23-Jun-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑈)    &   ⊢ 𝑁 = (invr‘𝐹)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂) → ((𝑁‘𝑆) ∈ 𝐸 ∧ (𝑁‘𝑆) ≠ 𝑂))
Theorem	tendolinv 41693*	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 41694*	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 41695	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 41696	Lemma for dvhlvec 41697. 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 41697	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 41698	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 41699*	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 41700	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 41704 and dihpN 41924. (Contributed by NM, 27-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐸 = ⟨( I ↾ 𝐵), ( I ↾ 𝑇)⟩    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → 𝐸 ∈ (𝑉 ∖ { 0 }))