P. 411 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 41001-41100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	erngdvlem4-rN 41001*	Lemma for erngdv 40995. (Contributed by NM, 11-Aug-2013.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐷 = ((EDRingR‘𝐾)‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑃 = (𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑎‘𝑓) ∘ (𝑏‘𝑓))))    &   ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝐼 = (𝑎 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ◡(𝑎‘𝑓)))    &   ⊢ 𝑀 = (𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (𝑏 ∘ 𝑎))    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝑄 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑍 = ((𝑄 ∨ (𝑅‘𝑏)) ∧ ((ℎ‘𝑄) ∨ (𝑅‘(𝑏 ∘ ◡(𝑠‘ℎ)))))    &   ⊢ 𝑌 = ((𝑄 ∨ (𝑅‘𝑔)) ∧ (𝑍 ∨ (𝑅‘(𝑔 ∘ ◡𝑏))))    &   ⊢ 𝑋 = (℩𝑧 ∈ 𝑇 ∀𝑏 ∈ 𝑇 ((𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘(𝑠‘ℎ)) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝑔)) → (𝑧‘𝑄) = 𝑌))    &   ⊢ 𝑈 = (𝑔 ∈ 𝑇 ↦ if((𝑠‘ℎ) = ℎ, 𝑔, 𝑋))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵))) → 𝐷 ∈ DivRing)
Theorem	erngring-rN 41002	An endomorphism ring is a ring. TODO: fix comment. (Contributed by NM, 4-Aug-2013.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐷 = ((EDRingR‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐷 ∈ Ring)
Theorem	erngdv-rN 41003	An endomorphism ring is a division ring. TODO: fix comment. (Contributed by NM, 11-Aug-2013.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐷 = ((EDRingR‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐷 ∈ DivRing)
Syntax	cdveca 41004	Extend class notation with constructed vector space A.
class DVecA
Definition	df-dveca 41005*	Define constructed partial vector space A. (Contributed by NM, 8-Oct-2013.)
⊢ DVecA = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ ({⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))⟩, ⟨(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠‘𝑓))⟩})))
Theorem	dvafset 41006*	The constructed partial vector space A for a lattice 𝐾. (Contributed by NM, 8-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → (DVecA‘𝐾) = (𝑤 ∈ 𝐻 ↦ ({⟨(Base‘ndx), ((LTrn‘𝐾)‘𝑤)⟩, ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))⟩, ⟨(Scalar‘ndx), ((EDRing‘𝐾)‘𝑤)⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑠‘𝑓))⟩})))
Theorem	dvaset 41007*	The constructed partial vector space A for a lattice 𝐾. (Contributed by NM, 8-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐷 = ((EDRing‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → 𝑈 = ({⟨(Base‘ndx), 𝑇⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑇, 𝑔 ∈ 𝑇 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(Scalar‘ndx), 𝐷⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑠 ∈ 𝐸, 𝑓 ∈ 𝑇 ↦ (𝑠‘𝑓))⟩}))
Theorem	dvasca 41008	The ring base set of the constructed partial vector space A are all translation group endomorphisms (for a fiducial co-atom 𝑊). (Contributed by NM, 22-Jun-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐷 = ((EDRing‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑈)    ⇒   ⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → 𝐹 = 𝐷)
Theorem	dvabase 41009	The ring base set of the constructed partial vector space A are all translation group endomorphisms (for a fiducial co-atom 𝑊). (Contributed by NM, 9-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑈)    &   ⊢ 𝐶 = (Base‘𝐹)    ⇒   ⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → 𝐶 = 𝐸)
Theorem	dvafplusg 41010*	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‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑈)    &   ⊢ + = (+g‘𝐹)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → + = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))))
Theorem	dvaplusg 41011*	Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑈)    &   ⊢ + = (+g‘𝐹)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐸 ∧ 𝑆 ∈ 𝐸)) → (𝑅 + 𝑆) = (𝑓 ∈ 𝑇 ↦ ((𝑅‘𝑓) ∘ (𝑆‘𝑓))))
Theorem	dvaplusgv 41012	Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑈)    &   ⊢ + = (+g‘𝐹)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐸 ∧ 𝑆 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇)) → ((𝑅 + 𝑆)‘𝐺) = ((𝑅‘𝐺) ∘ (𝑆‘𝐺)))
Theorem	dvafmulr 41013*	Ring multiplication 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‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑈)    &   ⊢ · = (.r‘𝐹)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → · = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑠 ∘ 𝑡)))
Theorem	dvamulr 41014	Ring multiplication operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑈)    &   ⊢ · = (.r‘𝐹)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐸 ∧ 𝑆 ∈ 𝐸)) → (𝑅 · 𝑆) = (𝑅 ∘ 𝑆))
Theorem	dvavbase 41015	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 41016*	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 41017	Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝑈)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → (𝐹 + 𝐺) = (𝐹 ∘ 𝐺))
Theorem	dvafvsca 41018*	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 41019	Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑈)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇)) → (𝑅 · 𝐹) = (𝑅‘𝐹))
Theorem	tendospcl 41020	Closure of endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → (𝑈‘𝐹) ∈ 𝑇)
Theorem	tendospass 41021	Associative law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇)) → ((𝑈 ∘ 𝑉)‘𝐹) = (𝑈‘(𝑉‘𝐹)))
Theorem	tendospdi1 41022	Forward distributive law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → (𝑈‘(𝐹 ∘ 𝐺)) = ((𝑈‘𝐹) ∘ (𝑈‘𝐺)))
Theorem	tendocnv 41023	Converse of a trace-preserving endomorphism value. (Contributed by NM, 7-Apr-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → ◡(𝑆‘𝐹) = (𝑆‘◡𝐹))
Theorem	tendospdi2 41024*	Reverse distributive law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.)
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))    ⇒   ⊢ ((𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → ((𝑈𝑃𝑉)‘𝐹) = ((𝑈‘𝐹) ∘ (𝑉‘𝐹)))
Theorem	tendospcanN 41025*	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 41026	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 41027	Lemma for dvalvec 41028. (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 41028	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 41029	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 41030	Extend class notation with partial isomorphism A.
class DIsoA
Definition	df-disoa 41031*	Define partial isomorphism A. (Contributed by NM, 15-Oct-2013.)
⊢ DIsoA = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} ↦ {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥})))
Theorem	diaffval 41032*	The partial isomorphism A for a lattice 𝐾. (Contributed by NM, 15-Oct-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → (DIsoA‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) ≤ 𝑥})))
Theorem	diafval 41033*	The partial isomorphism A for a lattice 𝐾. (Contributed by NM, 15-Oct-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐼 = (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑊} ↦ {𝑓 ∈ 𝑇 ∣ (𝑅‘𝑓) ≤ 𝑥}))
Theorem	diaval 41034*	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 41035	Member of the partial isomorphism A for a lattice 𝐾. (Contributed by NM, 3-Dec-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐹 ∈ (𝐼‘𝑋) ↔ (𝐹 ∈ 𝑇 ∧ (𝑅‘𝐹) ≤ 𝑋)))
Theorem	diafn 41036*	Functionality and domain of the partial isomorphism A. (Contributed by NM, 26-Nov-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐼 Fn {𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊})
Theorem	diadm 41037*	Domain of the partial isomorphism A. (Contributed by NM, 3-Dec-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → dom 𝐼 = {𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊})
Theorem	diaeldm 41038	Member of domain of the partial isomorphism A. (Contributed by NM, 4-Dec-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → (𝑋 ∈ dom 𝐼 ↔ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)))
Theorem	diadmclN 41039	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 41040	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 41041	The value of the partial isomorphism A is not empty. (Contributed by NM, 17-Jan-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) ≠ ∅)
Theorem	dia0eldmN 41042	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 41043	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 41044	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 41045	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 41046	Trace of a member of the partial isomorphism A. (Contributed by NM, 17-Jan-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ (𝐼‘𝑋)) → (𝑅‘𝐹) ≤ 𝑋)
Theorem	diaelrnN 41047	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 41048	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 41049	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 41050	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 41051	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 41052	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 41053	Closure of partial isomorphism A converse. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ ran 𝐼) → (◡𝐼‘𝑋) ∈ dom 𝐼)
Theorem	dia0 41054	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 41055	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 41056	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 41057*	Partial isomorphism A of a lattice glb. (Contributed by NM, 3-Dec-2013.) (New usage is discouraged.)
⊢ 𝐺 = (glb‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅)) → (𝐼‘(𝐺‘𝑆)) = ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))
Theorem	diameetN 41058	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 41059	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 41060	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 41061	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 41062	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 41063*	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 41064	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 41065	A vector (translation) belongs to the 1-dim subspace it generates. (Contributed by NM, 8-Sep-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹 ∈ (𝐼‘(𝑅‘𝐹)))
Theorem	dia2dimlem1 41066	Lemma for dia2dim 41079. 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 41067	Lemma for dia2dim 41079. 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 41068	Lemma for dia2dim 41079. 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 41069	Lemma for dia2dim 41079. 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 41070	Lemma for dia2dim 41079. 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 41071	Lemma for dia2dim 41079. 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 41072	Lemma for dia2dim 41079. Eliminate (𝐹‘𝑃) ≠ 𝑃 condition. (Contributed by NM, 8-Sep-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑌)    &   ⊢ ⊕ = (LSSum‘𝑌)    &   ⊢ 𝑁 = (LSpan‘𝑌)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    &   ⊢ 𝑄 = ((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉))    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))    &   ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))    &   ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))    &   ⊢ (𝜑 → 𝐹 ∈ 𝑇)    &   ⊢ (𝜑 → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉))    &   ⊢ (𝜑 → 𝑈 ≠ 𝑉)    &   ⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑈)    &   ⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑉)    ⇒   ⊢ (𝜑 → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
Theorem	dia2dimlem8 41073	Lemma for dia2dim 41079. 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 41074	Lemma for dia2dim 41079. Eliminate (𝑅‘𝐹) ≠ 𝑈, 𝑉 conditions. (Contributed by NM, 8-Sep-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑌)    &   ⊢ ⊕ = (LSSum‘𝑌)    &   ⊢ 𝑁 = (LSpan‘𝑌)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))    &   ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))    &   ⊢ (𝜑 → 𝐹 ∈ 𝑇)    &   ⊢ (𝜑 → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉))    &   ⊢ (𝜑 → 𝑈 ≠ 𝑉)    ⇒   ⊢ (𝜑 → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
Theorem	dia2dimlem10 41075	Lemma for dia2dim 41079. 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 41076	Lemma for dia2dim 41079. 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 41077	Lemma for dia2dim 41079. Obtain subset relation. (Contributed by NM, 8-Sep-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑌)    &   ⊢ ⊕ = (LSSum‘𝑌)    &   ⊢ 𝑁 = (LSpan‘𝑌)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))    &   ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))    &   ⊢ (𝜑 → 𝑈 ≠ 𝑉)    ⇒   ⊢ (𝜑 → (𝐼‘(𝑈 ∨ 𝑉)) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
Theorem	dia2dimlem13 41078	Lemma for dia2dim 41079. Eliminate 𝑈 ≠ 𝑉 condition. (Contributed by NM, 8-Sep-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑌)    &   ⊢ ⊕ = (LSSum‘𝑌)    &   ⊢ 𝑁 = (LSpan‘𝑌)    &   ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))    &   ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))    ⇒   ⊢ (𝜑 → (𝐼‘(𝑈 ∨ 𝑉)) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
Theorem	dia2dim 41079	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 41080	Extend class notation with constructed full vector space H.
class DVecH
Definition	df-dvech 41081*	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 41082*	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 41083*	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 41084	The ring of scalars of the constructed full vector space H. (Contributed by NM, 22-Jun-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐷 = ((EDRing‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑈)    ⇒   ⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → 𝐹 = 𝐷)
Theorem	dvhbase 41085	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 41086*	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 41087*	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 41088	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 41089	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 41090	Vector membership in the constructed full vector space H. (Contributed by NM, 20-Feb-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    ⇒   ⊢ (((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸)) → ⟨𝐹, 𝑆⟩ ∈ 𝑉)
Theorem	dvhvaddcbv 41091*	Change bound variables to isolate them later. (Contributed by NM, 3-Nov-2013.)
⊢ + = (𝑓 ∈ (𝑇 × 𝐸), 𝑔 ∈ (𝑇 × 𝐸) ↦ ⟨((1st ‘𝑓) ∘ (1st ‘𝑔)), ((2nd ‘𝑓) ⨣ (2nd ‘𝑔))⟩)    ⇒   ⊢ + = (ℎ ∈ (𝑇 × 𝐸), 𝑖 ∈ (𝑇 × 𝐸) ↦ ⟨((1st ‘ℎ) ∘ (1st ‘𝑖)), ((2nd ‘ℎ) ⨣ (2nd ‘𝑖))⟩)
Theorem	dvhvaddval 41092*	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 41093*	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 41094	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 41095	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 41096*	The vector sum operation for the constructed full vector space H. TODO: check if this will shorten proofs that use dvhopvadd 41095 and/or dvhfplusr 41086. (Contributed by NM, 26-Sep-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ + = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ✚ = (+g‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐸) ∧ (𝐺 ∈ 𝑇 ∧ 𝑅 ∈ 𝐸)) → (⟨𝐹, 𝑄⟩ ✚ ⟨𝐺, 𝑅⟩) = ⟨(𝐹 ∘ 𝐺), (𝑄 + 𝑅)⟩)
Theorem	dvhvaddcl 41097	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 41098	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 41099	Associativity of vector sum. (Contributed by NM, 31-Oct-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑈)    &   ⊢ ⨣ = (+g‘𝐷)    &   ⊢ + = (+g‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → ((𝐹 + 𝐺) + 𝐼) = (𝐹 + (𝐺 + 𝐼)))
Theorem	dvhvscacbv 41100*	Change bound variables to isolate them later. (Contributed by NM, 20-Nov-2013.)
⊢ · = (𝑠 ∈ 𝐸, 𝑓 ∈ (𝑇 × 𝐸) ↦ ⟨(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))⟩)    ⇒   ⊢ · = (𝑡 ∈ 𝐸, 𝑔 ∈ (𝑇 × 𝐸) ↦ ⟨(𝑡‘(1st ‘𝑔)), (𝑡 ∘ (2nd ‘𝑔))⟩)