P. 392 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39101-39200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dib11N 39101	The isomorphism B for a lattice 𝐾 is one-to-one in the region under co-atom 𝑊. (Contributed by NM, 24-Feb-2014.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → ((𝐼‘𝑋) = (𝐼‘𝑌) ↔ 𝑋 = 𝑌))
Theorem	dibf11N 39102	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‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐼:dom 𝐼–1-1-onto→ran 𝐼)
Theorem	dibclN 39103	Closure of partial isomorphism B for a lattice 𝐾. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘𝑋) ∈ ran 𝐼)
Theorem	dibvalrel 39104	The value of partial isomorphism B is a relation. (Contributed by NM, 8-Mar-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → Rel (𝐼‘𝑋))
Theorem	dib0 39105	The value of partial isomorphism B at the lattice zero is the singleton of the zero vector i.e. the zero subspace. (Contributed by NM, 27-Mar-2014.)
⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (0g‘𝑈)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝐼‘ 0 ) = {𝑂})
Theorem	dib1dim 39106*	Two expressions for the 1-dimensional subspaces of vector space H. (Contributed by NM, 24-Feb-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝐼‘(𝑅‘𝐹)) = {𝑔 ∈ (𝑇 × 𝐸) ∣ ∃𝑠 ∈ 𝐸 𝑔 = ⟨(𝑠‘𝐹), 𝑂⟩})
Theorem	dibglbN 39107*	Partial isomorphism B of a lattice glb. (Contributed by NM, 9-Mar-2014.) (New usage is discouraged.)
⊢ 𝐺 = (glb‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅)) → (𝐼‘(𝐺‘𝑆)) = ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))
Theorem	dibintclN 39108	The intersection of partial isomorphism B closed subspaces is a closed subspace. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → ∩ 𝑆 ∈ ran 𝐼)
Theorem	dib1dim2 39109*	Two expressions for a 1-dimensional subspace of vector space H (when 𝐹 is a nonzero vector i.e. non-identity translation). (Contributed by NM, 24-Feb-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝐼‘(𝑅‘𝐹)) = (𝑁‘{⟨𝐹, 𝑂⟩}))
Theorem	dibss 39110	The partial isomorphism B maps to a set of vectors in full vector space H. (Contributed by NM, 1-Jan-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) ⊆ 𝑉)
Theorem	diblss 39111	The value of partial isomorphism B is a subspace of partial vector space H. TODO: use dib* specific theorems instead of dia* ones to shorten proof? (Contributed by NM, 11-Feb-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) ∈ 𝑆)
Theorem	diblsmopel 39112*	Membership in subspace sum for partial isomorphism B. (Contributed by NM, 21-Sep-2014.) (Revised by Mario Carneiro, 6-May-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝑉 = ((DVecA‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑉)    &   ⊢ ✚ = (LSSum‘𝑈)    &   ⊢ 𝐽 = ((DIsoA‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊))    &   ⊢ (𝜑 → (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊))    ⇒   ⊢ (𝜑 → (⟨𝐹, 𝑆⟩ ∈ ((𝐼‘𝑋) ✚ (𝐼‘𝑌)) ↔ (𝐹 ∈ ((𝐽‘𝑋) ⊕ (𝐽‘𝑌)) ∧ 𝑆 = 𝑂)))
Syntax	cdic 39113	Extend class notation with isomorphism C.
class DIsoC
Definition	df-dic 39114*	Isomorphism C has domain of lattice atoms that are not less than or equal to the fiducial co-atom 𝑤. The value is a one-dimensional subspace generated by the pair consisting of the ℩ vector below and the endomorphism ring unit. Definition of phi(q) in [Crawley] p. 121. Note that we use the fixed atom ((oc k ) 𝑤) to represent the p in their "Choose an atom p..." on line 21. (Contributed by NM, 15-Dec-2013.)
⊢ DIsoC = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑞 ∈ {𝑟 ∈ (Atoms‘𝑘) ∣ ¬ 𝑟(le‘𝑘)𝑤} ↦ {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ ((LTrn‘𝑘)‘𝑤)(𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝑘)‘𝑤))})))
Theorem	dicffval 39115*	The partial isomorphism C for a lattice 𝐾. (Contributed by NM, 15-Dec-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → (DIsoC‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑞 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑤} ↦ {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑔‘((oc‘𝐾)‘𝑤)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑤))})))
Theorem	dicfval 39116*	The partial isomorphism C for a lattice 𝐾. (Contributed by NM, 15-Dec-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐼 = (𝑞 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊} ↦ {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞)) ∧ 𝑠 ∈ 𝐸)}))
Theorem	dicval 39117*	The partial isomorphism C for a lattice 𝐾. (Contributed by NM, 15-Dec-2013.) (Revised by Mario Carneiro, 22-Sep-2015.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐼‘𝑄) = {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸)})
Theorem	dicopelval 39118*	Membership in value of the partial isomorphism C for a lattice 𝐾. (Contributed by NM, 15-Feb-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝐹 ∈ V    &   ⊢ 𝑆 ∈ V    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (⟨𝐹, 𝑆⟩ ∈ (𝐼‘𝑄) ↔ (𝐹 = (𝑆‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑆 ∈ 𝐸)))
Theorem	dicelvalN 39119*	Membership in value of the partial isomorphism C for a lattice 𝐾. (Contributed by NM, 25-Feb-2014.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝑌 ∈ (𝐼‘𝑄) ↔ (𝑌 ∈ (V × V) ∧ ((1st ‘𝑌) = ((2nd ‘𝑌)‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ (2nd ‘𝑌) ∈ 𝐸))))
Theorem	dicval2 39120*	The partial isomorphism C for a lattice 𝐾. (Contributed by NM, 20-Feb-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝐺 = (℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐼‘𝑄) = {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸)})
Theorem	dicelval3 39121*	Member of the partial isomorphism C. (Contributed by NM, 26-Feb-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝐺 = (℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝑌 ∈ (𝐼‘𝑄) ↔ ∃𝑠 ∈ 𝐸 𝑌 = ⟨(𝑠‘𝐺), 𝑠⟩))
Theorem	dicopelval2 39122*	Membership in value of the partial isomorphism C for a lattice 𝐾. (Contributed by NM, 20-Feb-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝐺 = (℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)    &   ⊢ 𝐹 ∈ V    &   ⊢ 𝑆 ∈ V    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (⟨𝐹, 𝑆⟩ ∈ (𝐼‘𝑄) ↔ (𝐹 = (𝑆‘𝐺) ∧ 𝑆 ∈ 𝐸)))
Theorem	dicelval2N 39123*	Membership in value of the partial isomorphism C for a lattice 𝐾. (Contributed by NM, 25-Feb-2014.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝐺 = (℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝑌 ∈ (𝐼‘𝑄) ↔ (𝑌 ∈ (V × V) ∧ ((1st ‘𝑌) = ((2nd ‘𝑌)‘𝐺) ∧ (2nd ‘𝑌) ∈ 𝐸))))
Theorem	dicfnN 39124*	Functionality and domain of the partial isomorphism C. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐼 Fn {𝑝 ∈ 𝐴 ∣ ¬ 𝑝 ≤ 𝑊})
Theorem	dicdmN 39125*	Domain of the partial isomorphism C. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → dom 𝐼 = {𝑝 ∈ 𝐴 ∣ ¬ 𝑝 ≤ 𝑊})
Theorem	dicvalrelN 39126	The value of partial isomorphism C is a relation. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → Rel (𝐼‘𝑋))
Theorem	dicssdvh 39127	The partial isomorphism C maps to a set of vectors in full vector space H. (Contributed by NM, 19-Jan-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐼‘𝑄) ⊆ 𝑉)
Theorem	dicelval1sta 39128*	Membership in value of the partial isomorphism C for a lattice 𝐾. (Contributed by NM, 16-Feb-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑌 ∈ (𝐼‘𝑄)) → (1st ‘𝑌) = ((2nd ‘𝑌)‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)))
Theorem	dicelval1stN 39129	Membership in value of the partial isomorphism C for a lattice 𝐾. (Contributed by NM, 16-Feb-2014.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑌 ∈ (𝐼‘𝑄)) → (1st ‘𝑌) ∈ 𝑇)
Theorem	dicelval2nd 39130	Membership in value of the partial isomorphism C for a lattice 𝐾. (Contributed by NM, 16-Feb-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑌 ∈ (𝐼‘𝑄)) → (2nd ‘𝑌) ∈ 𝐸)
Theorem	dicvaddcl 39131	Membership in value of the partial isomorphism C is closed under vector sum. (Contributed by NM, 16-Feb-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑋 ∈ (𝐼‘𝑄) ∧ 𝑌 ∈ (𝐼‘𝑄))) → (𝑋 + 𝑌) ∈ (𝐼‘𝑄))
Theorem	dicvscacl 39132	Membership in value of the partial isomorphism C is closed under scalar product. (Contributed by NM, 16-Feb-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑋 ∈ 𝐸 ∧ 𝑌 ∈ (𝐼‘𝑄))) → (𝑋 · 𝑌) ∈ (𝐼‘𝑄))
Theorem	dicn0 39133	The value of the partial isomorphism C is not empty. (Contributed by NM, 15-Feb-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐼‘𝑄) ≠ ∅)
Theorem	diclss 39134	The value of partial isomorphism C is a subspace of partial vector space H. (Contributed by NM, 16-Feb-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐼‘𝑄) ∈ 𝑆)
Theorem	diclspsn 39135*	The value of isomorphism C is spanned by vector 𝐹. Part of proof of Lemma N of [Crawley] p. 121 line 29. (Contributed by NM, 21-Feb-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐹 = (℩𝑓 ∈ 𝑇 (𝑓‘𝑃) = 𝑄)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐼‘𝑄) = (𝑁‘{⟨𝐹, ( I ↾ 𝑇)⟩}))
Theorem	cdlemn2 39136*	Part of proof of Lemma N of [Crawley] p. 121 line 30. (Contributed by NM, 21-Feb-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (℩ℎ ∈ 𝑇 (ℎ‘𝑄) = 𝑆)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑋)) → (𝑅‘𝐹) ≤ 𝑋)
Theorem	cdlemn2a 39137*	Part of proof of Lemma N of [Crawley] p. 121. (Contributed by NM, 24-Feb-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐹 = (℩ℎ ∈ 𝑇 (ℎ‘𝑄) = 𝑆)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑋)) → (𝑁‘{⟨𝐹, 𝑂⟩}) ⊆ (𝐼‘𝑋))
Theorem	cdlemn3 39138*	Part of proof of Lemma N of [Crawley] p. 121 line 31. (Contributed by NM, 21-Feb-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑄)    &   ⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑅)    &   ⊢ 𝐽 = (℩ℎ ∈ 𝑇 (ℎ‘𝑄) = 𝑅)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → (𝐽 ∘ 𝐹) = 𝐺)
Theorem	cdlemn4 39139*	Part of proof of Lemma N of [Crawley] p. 121 line 31. (Contributed by NM, 21-Feb-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑄)    &   ⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑅)    &   ⊢ 𝐽 = (℩ℎ ∈ 𝑇 (ℎ‘𝑄) = 𝑅)    &   ⊢ + = (+g‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → ⟨𝐺, ( I ↾ 𝑇)⟩ = (⟨𝐹, ( I ↾ 𝑇)⟩ + ⟨𝐽, 𝑂⟩))
Theorem	cdlemn4a 39140*	Part of proof of Lemma N of [Crawley] p. 121 line 32. (Contributed by NM, 24-Feb-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑄)    &   ⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑅)    &   ⊢ 𝐽 = (℩ℎ ∈ 𝑇 (ℎ‘𝑄) = 𝑅)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → (𝑁‘{⟨𝐺, ( I ↾ 𝑇)⟩}) ⊆ ((𝑁‘{⟨𝐹, ( I ↾ 𝑇)⟩}) ⊕ (𝑁‘{⟨𝐽, 𝑂⟩})))
Theorem	cdlemn5pre 39141*	Part of proof of Lemma N of [Crawley] p. 121 line 32. (Contributed by NM, 25-Feb-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐹 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑄)    &   ⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑅)    &   ⊢ 𝑀 = (℩ℎ ∈ 𝑇 (ℎ‘𝑄) = 𝑅)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑄 ∨ 𝑋)) → (𝐽‘𝑅) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋)))
Theorem	cdlemn5 39142	Part of proof of Lemma N of [Crawley] p. 121 line 32. (Contributed by NM, 25-Feb-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑄 ∨ 𝑋)) → (𝐽‘𝑅) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋)))
Theorem	cdlemn6 39143*	Part of proof of Lemma N of [Crawley] p. 121 line 35. (Contributed by NM, 26-Feb-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝐹 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑄)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → (⟨(𝑠‘𝐹), 𝑠⟩ + ⟨𝑔, 𝑂⟩) = ⟨((𝑠‘𝐹) ∘ 𝑔), 𝑠⟩)
Theorem	cdlemn7 39144*	Part of proof of Lemma N of [Crawley] p. 121 line 36. (Contributed by NM, 26-Feb-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝐹 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑄)    &   ⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑅)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ∧ ⟨𝐺, ( I ↾ 𝑇)⟩ = (⟨(𝑠‘𝐹), 𝑠⟩ + ⟨𝑔, 𝑂⟩))) → (𝐺 = ((𝑠‘𝐹) ∘ 𝑔) ∧ ( I ↾ 𝑇) = 𝑠))
Theorem	cdlemn8 39145*	Part of proof of Lemma N of [Crawley] p. 121 line 36. (Contributed by NM, 26-Feb-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝐹 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑄)    &   ⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑅)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ∧ ⟨𝐺, ( I ↾ 𝑇)⟩ = (⟨(𝑠‘𝐹), 𝑠⟩ + ⟨𝑔, 𝑂⟩))) → 𝑔 = (𝐺 ∘ ◡𝐹))
Theorem	cdlemn9 39146*	Part of proof of Lemma N of [Crawley] p. 121 line 36. (Contributed by NM, 27-Feb-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝐹 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑄)    &   ⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑅)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ∧ ⟨𝐺, ( I ↾ 𝑇)⟩ = (⟨(𝑠‘𝐹), 𝑠⟩ + ⟨𝑔, 𝑂⟩))) → (𝑔‘𝑄) = 𝑅)
Theorem	cdlemn10 39147	Part of proof of Lemma N of [Crawley] p. 121 line 36. (Contributed by NM, 27-Feb-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑄) = 𝑆 ∧ (𝑅‘𝑔) ≤ 𝑋)) → 𝑆 ≤ (𝑄 ∨ 𝑋))
Theorem	cdlemn11a 39148*	Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐹 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑄)    &   ⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑁)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → ⟨𝐺, ( I ↾ 𝑇)⟩ ∈ (𝐽‘𝑁))
Theorem	cdlemn11b 39149*	Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐹 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑄)    &   ⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑁)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → ⟨𝐺, ( I ↾ 𝑇)⟩ ∈ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋)))
Theorem	cdlemn11c 39150*	Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐹 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑄)    &   ⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑁)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → ∃𝑦 ∈ (𝐽‘𝑄)∃𝑧 ∈ (𝐼‘𝑋)⟨𝐺, ( I ↾ 𝑇)⟩ = (𝑦 + 𝑧))
Theorem	cdlemn11pre 39151*	Part of proof of Lemma N of [Crawley] p. 121 line 37. TODO: combine cdlemn11a 39148, cdlemn11b 39149, cdlemn11c 39150, cdlemn11pre into one? (Contributed by NM, 27-Feb-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐹 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑄)    &   ⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑁)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → 𝑁 ≤ (𝑄 ∨ 𝑋))
Theorem	cdlemn11 39152	Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑅) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → 𝑅 ≤ (𝑄 ∨ 𝑋))
Theorem	cdlemn 39153	Lemma N of [Crawley] p. 121 line 27. (Contributed by NM, 27-Feb-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊))) → (𝑅 ≤ (𝑄 ∨ 𝑋) ↔ (𝐽‘𝑅) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))))
Theorem	dihordlem6 39154*	Part of proof of Lemma N of [Crawley] p. 122 line 35. (Contributed by NM, 3-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑅)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → (⟨(𝑠‘𝐺), 𝑠⟩ + ⟨𝑔, 𝑂⟩) = ⟨((𝑠‘𝐺) ∘ 𝑔), 𝑠⟩)
Theorem	dihordlem7 39155*	Part of proof of Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑅)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ∧ ⟨𝑓, 𝑂⟩ = (⟨(𝑠‘𝐺), 𝑠⟩ + ⟨𝑔, 𝑂⟩))) → (𝑓 = ((𝑠‘𝐺) ∘ 𝑔) ∧ 𝑂 = 𝑠))
Theorem	dihordlem7b 39156*	Part of proof of Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑅)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ∧ ⟨𝑓, 𝑂⟩ = (⟨(𝑠‘𝐺), 𝑠⟩ + ⟨𝑔, 𝑂⟩))) → (𝑓 = 𝑔 ∧ 𝑂 = 𝑠))
Theorem	dihjustlem 39157	Part of proof after Lemma N of [Crawley] p. 122 line 4, "the definition of phi(x) is independent of the atom q." (Contributed by NM, 2-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ 𝑋 ∈ 𝐵) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = (𝑅 ∨ (𝑋 ∧ 𝑊))) → ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑅) ⊕ (𝐼‘(𝑋 ∧ 𝑊))))
Theorem	dihjust 39158	Part of proof after Lemma N of [Crawley] p. 122 line 4, "the definition of phi(x) is independent of the atom q." (Contributed by NM, 2-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ 𝑋 ∈ 𝐵) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = (𝑅 ∨ (𝑋 ∧ 𝑊))) → ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) = ((𝐽‘𝑅) ⊕ (𝐼‘(𝑋 ∧ 𝑊))))
Theorem	dihord1 39159	Part of proof after Lemma N of [Crawley] p. 122. Forward ordering property. TODO: change (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 to 𝑄 ≤ 𝑋 using lhpmcvr3 37966, here and all theorems below. (Contributed by NM, 2-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑅) ⊕ (𝐼‘(𝑌 ∧ 𝑊))))
Theorem	dihord2a 39160	Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑅) ⊕ (𝐼‘(𝑌 ∧ 𝑊))))) → 𝑄 ≤ (𝑅 ∨ (𝑌 ∧ 𝑊)))
Theorem	dihord2b 39161	Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑅) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) → (𝐼‘(𝑋 ∧ 𝑊)) ⊆ ((𝐽‘𝑅) ⊕ (𝐼‘(𝑌 ∧ 𝑊))))
Theorem	dihord2cN 39162*	Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. TODO: needed? shorten other proof with it? (Contributed by NM, 3-Mar-2014.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → ⟨𝑓, 𝑂⟩ ∈ (𝐼‘(𝑋 ∧ 𝑊)))
Theorem	dihord11b 39163*	Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑁)    ⇒   ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → ⟨𝑓, 𝑂⟩ ∈ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊))))
Theorem	dihord10 39164*	Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑁)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ ((𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) ∧ (𝑅‘𝑔) ≤ (𝑌 ∧ 𝑊) ∧ ⟨𝑓, 𝑂⟩ = (⟨(𝑠‘𝐺), 𝑠⟩ + ⟨𝑔, 𝑂⟩))) → (𝑅‘𝑓) ≤ (𝑌 ∧ 𝑊))
Theorem	dihord11c 39165*	Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑁)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊))) ∧ 𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → ∃𝑦 ∈ (𝐽‘𝑁)∃𝑧 ∈ (𝐼‘(𝑌 ∧ 𝑊))⟨𝑓, 𝑂⟩ = (𝑦 + 𝑧))
Theorem	dihord2pre 39166*	Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑁)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) → (𝑋 ∧ 𝑊) ≤ (𝑌 ∧ 𝑊))
Theorem	dihord2pre2 39167*	Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 4-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑁)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑁 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊))))) → (𝑄 ∨ (𝑋 ∧ 𝑊)) ≤ (𝑁 ∨ (𝑌 ∧ 𝑊)))
Theorem	dihord2 39168	Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. TODO: do we need ¬ 𝑋 ≤ 𝑊 and ¬ 𝑌 ≤ 𝑊? (Contributed by NM, 4-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑁 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊))))) → 𝑋 ≤ 𝑌)
Syntax	cdih 39169	Extend class notation with isomorphism H.
class DIsoH
Definition	df-dih 39170*	Define isomorphism H. (Contributed by NM, 28-Jan-2014.)
⊢ DIsoH = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ (Base‘𝑘) ↦ if(𝑥(le‘𝑘)𝑤, (((DIsoB‘𝑘)‘𝑤)‘𝑥), (℩𝑢 ∈ (LSubSp‘((DVecH‘𝑘)‘𝑤))∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑞(le‘𝑘)𝑤 ∧ (𝑞(join‘𝑘)(𝑥(meet‘𝑘)𝑤)) = 𝑥) → 𝑢 = ((((DIsoC‘𝑘)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝑘)‘𝑤))(((DIsoB‘𝑘)‘𝑤)‘(𝑥(meet‘𝑘)𝑤)))))))))
Theorem	dihffval 39171*	The isomorphism H for a lattice 𝐾. Definition of isomorphism map in [Crawley] p. 122 line 3. (Contributed by NM, 28-Jan-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → (DIsoH‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝐵 ↦ if(𝑥 ≤ 𝑤, (((DIsoB‘𝐾)‘𝑤)‘𝑥), (℩𝑢 ∈ (LSubSp‘((DVecH‘𝐾)‘𝑤))∀𝑞 ∈ 𝐴 ((¬ 𝑞 ≤ 𝑤 ∧ (𝑞 ∨ (𝑥 ∧ 𝑤)) = 𝑥) → 𝑢 = ((((DIsoC‘𝐾)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝐾)‘𝑤))(((DIsoB‘𝐾)‘𝑤)‘(𝑥 ∧ 𝑤)))))))))
Theorem	dihfval 39172*	Isomorphism H for a lattice 𝐾. Definition of isomorphism map in [Crawley] p. 122 line 3. (Contributed by NM, 28-Jan-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝐷 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝐶 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐼 = (𝑥 ∈ 𝐵 ↦ if(𝑥 ≤ 𝑊, (𝐷‘𝑥), (℩𝑢 ∈ 𝑆 ∀𝑞 ∈ 𝐴 ((¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑢 = ((𝐶‘𝑞) ⊕ (𝐷‘(𝑥 ∧ 𝑊))))))))
Theorem	dihval 39173*	Value of isomorphism H for a lattice 𝐾. Definition of isomorphism map in [Crawley] p. 122 line 3. (Contributed by NM, 3-Feb-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝐷 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝐶 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐼‘𝑋) = if(𝑋 ≤ 𝑊, (𝐷‘𝑋), (℩𝑢 ∈ 𝑆 ∀𝑞 ∈ 𝐴 ((¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ (𝑋 ∧ 𝑊)) = 𝑋) → 𝑢 = ((𝐶‘𝑞) ⊕ (𝐷‘(𝑋 ∧ 𝑊)))))))
Theorem	dihvalc 39174*	Value of isomorphism H for a lattice 𝐾 when ¬ 𝑋 ≤ 𝑊. (Contributed by NM, 4-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝐷 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝐶 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) = (℩𝑢 ∈ 𝑆 ∀𝑞 ∈ 𝐴 ((¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ (𝑋 ∧ 𝑊)) = 𝑋) → 𝑢 = ((𝐶‘𝑞) ⊕ (𝐷‘(𝑋 ∧ 𝑊))))))
Theorem	dihlsscpre 39175	Closure of isomorphism H for a lattice 𝐾 when ¬ 𝑋 ≤ 𝑊. (Contributed by NM, 6-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝐷 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝐶 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) ∈ 𝑆)
Theorem	dihvalcqpre 39176	Value of isomorphism H for a lattice 𝐾 when ¬ 𝑋 ≤ 𝑊, given auxiliary atom 𝑄. (Contributed by NM, 6-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝐷 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝐶 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝐼‘𝑋) = ((𝐶‘𝑄) ⊕ (𝐷‘(𝑋 ∧ 𝑊))))
Theorem	dihvalcq 39177	Value of isomorphism H for a lattice 𝐾 when ¬ 𝑋 ≤ 𝑊, given auxiliary atom 𝑄. TODO: Use dihvalcq2 39188 (with lhpmcvr3 37966 for (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 simplification) that changes 𝐶 and 𝐷 to 𝐼 and make this obsolete. Do to other theorems as well. (Contributed by NM, 6-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝐷 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝐶 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝐼‘𝑋) = ((𝐶‘𝑄) ⊕ (𝐷‘(𝑋 ∧ 𝑊))))
Theorem	dihvalb 39178	Value of isomorphism H for a lattice 𝐾 when 𝑋 ≤ 𝑊. (Contributed by NM, 4-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝐷 = ((DIsoB‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) = (𝐷‘𝑋))
Theorem	dihopelvalbN 39179*	Ordered pair member of the partial isomorphism H for argument under 𝑊. (Contributed by NM, 21-Mar-2014.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (𝑔 ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (⟨𝐹, 𝑆⟩ ∈ (𝐼‘𝑋) ↔ ((𝐹 ∈ 𝑇 ∧ (𝑅‘𝐹) ≤ 𝑋) ∧ 𝑆 = 𝑂)))
Theorem	dihvalcqat 39180	Value of isomorphism H for a lattice 𝐾 at an atom not under 𝑊. (Contributed by NM, 27-Mar-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐼‘𝑄) = (𝐽‘𝑄))
Theorem	dih1dimb 39181*	Two expressions for a 1-dimensional subspace of vector space H (when 𝐹 is a nonzero vector i.e. non-identity translation). (Contributed by NM, 27-Apr-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝐼‘(𝑅‘𝐹)) = (𝑁‘{⟨𝐹, 𝑂⟩}))
Theorem	dih1dimb2 39182*	Isomorphism H at an atom under 𝑊. (Contributed by NM, 27-Apr-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → ∃𝑓 ∈ 𝑇 (𝑓 ≠ ( I ↾ 𝐵) ∧ (𝐼‘𝑄) = (𝑁‘{⟨𝑓, 𝑂⟩})))
Theorem	dih1dimc 39183*	Isomorphism H at an atom not under 𝑊. (Contributed by NM, 27-Apr-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐹 = (℩𝑓 ∈ 𝑇 (𝑓‘𝑃) = 𝑄)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐼‘𝑄) = (𝑁‘{⟨𝐹, ( I ↾ 𝑇)⟩}))
Theorem	dib2dim 39184	Extend dia2dim 39018 to partial isomorphism B. (Contributed by NM, 22-Sep-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊))    &   ⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊))    ⇒   ⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) ⊆ ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)))
Theorem	dih2dimb 39185	Extend dib2dim 39184 to isomorphism H. (Contributed by NM, 22-Sep-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊))    &   ⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊))    ⇒   ⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) ⊆ ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)))
Theorem	dih2dimbALTN 39186	Extend dia2dim 39018 to isomorphism H. (This version combines dib2dim 39184 and dih2dimb 39185 for shorter overall proof, but may be less easy to understand. TODO: decide which to use.) (Contributed by NM, 22-Sep-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊))    &   ⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊))    ⇒   ⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) ⊆ ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)))
Theorem	dihopelvalcqat 39187*	Ordered pair member of the partial isomorphism H for atom argument not under 𝑊. TODO: remove .t hypothesis. (Contributed by NM, 30-Mar-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝐺 = (℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)    &   ⊢ 𝐹 ∈ V    &   ⊢ 𝑆 ∈ V    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (⟨𝐹, 𝑆⟩ ∈ (𝐼‘𝑄) ↔ (𝐹 = (𝑆‘𝐺) ∧ 𝑆 ∈ 𝐸)))
Theorem	dihvalcq2 39188	Value of isomorphism H for a lattice 𝐾 when ¬ 𝑋 ≤ 𝑊, given auxiliary atom 𝑄. (Contributed by NM, 26-Sep-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ 𝑋)) → (𝐼‘𝑋) = ((𝐼‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))))
Theorem	dihopelvalcpre 39189*	Member of value of isomorphism H for a lattice 𝐾 when ¬ 𝑋 ≤ 𝑊, given auxiliary atom 𝑄. TODO: refactor to be shorter and more understandable; add lemmas? (Contributed by NM, 13-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝐺 = (℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)    &   ⊢ 𝐹 ∈ V    &   ⊢ 𝑆 ∈ V    &   ⊢ 𝑍 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝑁 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝐶 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝑉 = (LSubSp‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑂 = (𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (ℎ ∈ 𝑇 ↦ ((𝑎‘ℎ) ∘ (𝑏‘ℎ))))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (⟨𝐹, 𝑆⟩ ∈ (𝐼‘𝑋) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘(𝐹 ∘ ◡(𝑆‘𝐺))) ≤ 𝑋)))
Theorem	dihopelvalc 39190*	Member of value of isomorphism H for a lattice 𝐾 when ¬ 𝑋 ≤ 𝑊, given auxiliary atom 𝑄. (Contributed by NM, 13-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝐺 = (℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)    &   ⊢ 𝐹 ∈ V    &   ⊢ 𝑆 ∈ V    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (⟨𝐹, 𝑆⟩ ∈ (𝐼‘𝑋) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘(𝐹 ∘ ◡(𝑆‘𝐺))) ≤ 𝑋)))
Theorem	dihlss 39191	The value of isomorphism H is a subspace. (Contributed by NM, 6-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐼‘𝑋) ∈ 𝑆)
Theorem	dihss 39192	The value of isomorphism H is a set of vectors. (Contributed by NM, 14-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐼‘𝑋) ⊆ 𝑉)
Theorem	dihssxp 39193	An isomorphism H value is included in the vector space (expressed as 𝑇 × 𝐸). (Contributed by NM, 26-Sep-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) ⊆ (𝑇 × 𝐸))
Theorem	dihopcl 39194	Closure of an ordered pair (vector) member of a value of isomorphism H. (Contributed by NM, 26-Sep-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → ⟨𝐹, 𝑆⟩ ∈ (𝐼‘𝑋))    ⇒   ⊢ (𝜑 → (𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸))
Theorem	xihopellsmN 39195*	Ordered pair membership in a subspace sum of isomorphism H values. (Contributed by NM, 26-Sep-2014.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐴 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐿 = (LSubSp‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (⟨𝐹, 𝑆⟩ ∈ ((𝐼‘𝑋) ⊕ (𝐼‘𝑌)) ↔ ∃𝑔∃𝑡∃ℎ∃𝑢((⟨𝑔, 𝑡⟩ ∈ (𝐼‘𝑋) ∧ ⟨ℎ, 𝑢⟩ ∈ (𝐼‘𝑌)) ∧ (𝐹 = (𝑔 ∘ ℎ) ∧ 𝑆 = (𝑡𝐴𝑢)))))
Theorem	dihopellsm 39196*	Ordered pair membership in a subspace sum of isomorphism H values. (Contributed by NM, 26-Sep-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐴 = (𝑣 ∈ 𝐸, 𝑤 ∈ 𝐸 ↦ (𝑖 ∈ 𝑇 ↦ ((𝑣‘𝑖) ∘ (𝑤‘𝑖))))    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐿 = (LSubSp‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (⟨𝐹, 𝑆⟩ ∈ ((𝐼‘𝑋) ⊕ (𝐼‘𝑌)) ↔ ∃𝑔∃𝑡∃ℎ∃𝑢((⟨𝑔, 𝑡⟩ ∈ (𝐼‘𝑋) ∧ ⟨ℎ, 𝑢⟩ ∈ (𝐼‘𝑌)) ∧ (𝐹 = (𝑔 ∘ ℎ) ∧ 𝑆 = (𝑡𝐴𝑢)))))
Theorem	dihord6apre 39197*	Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑞)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌)) → 𝑋 ≤ 𝑌)
Theorem	dihord3 39198	The isomorphism H for a lattice 𝐾 is order-preserving in the region under co-atom 𝑊. (Contributed by NM, 6-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → ((𝐼‘𝑋) ⊆ (𝐼‘𝑌) ↔ 𝑋 ≤ 𝑌))
Theorem	dihord4 39199	The isomorphism H for a lattice 𝐾 is order-preserving in the region not under co-atom 𝑊. TODO: reformat (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) to eliminate adant*. (Contributed by NM, 6-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) → ((𝐼‘𝑋) ⊆ (𝐼‘𝑌) ↔ 𝑋 ≤ 𝑌))
Theorem	dihord5b 39200	Part of proof that isomorphism H is order-preserving. TODO: eliminate 3ad2ant1; combine with other way to have one lhpmcvr2 . (Contributed by NM, 7-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ 𝑋 ≤ 𝑌) → (𝐼‘𝑋) ⊆ (𝐼‘𝑌))