P. 401 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 40001-40100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dibval 40001*	The partial isomorphism B for a lattice 𝐾. (Contributed by NM, 8-Dec-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 0 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝐽 = ((DIsoA‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐽) → (𝐼‘𝑋) = ((𝐽‘𝑋) × { 0 }))
Theorem	dibopelvalN 40002*	Member of the partial isomorphism B. (Contributed by NM, 18-Jan-2014.) (Revised by Mario Carneiro, 6-May-2015.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 0 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝐽 = ((DIsoA‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐽) → (⟨𝐹, 𝑆⟩ ∈ (𝐼‘𝑋) ↔ (𝐹 ∈ (𝐽‘𝑋) ∧ 𝑆 = 0 )))
Theorem	dibval2 40003*	Value of the partial isomorphism B. (Contributed by NM, 18-Jan-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 0 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝐽 = ((DIsoA‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) = ((𝐽‘𝑋) × { 0 }))
Theorem	dibopelval2 40004*	Member of the partial isomorphism B. (Contributed by NM, 3-Mar-2014.) (Revised by Mario Carneiro, 6-May-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 0 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝐽 = ((DIsoA‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (⟨𝐹, 𝑆⟩ ∈ (𝐼‘𝑋) ↔ (𝐹 ∈ (𝐽‘𝑋) ∧ 𝑆 = 0 )))
Theorem	dibval3N 40005*	Value of the partial isomorphism B for a lattice 𝐾. (Contributed by NM, 24-Feb-2014.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 0 = (𝑔 ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) = ({𝑓 ∈ 𝑇 ∣ (𝑅‘𝑓) ≤ 𝑋} × { 0 }))
Theorem	dibelval3 40006*	Member of the partial isomorphism B. (Contributed by NM, 26-Feb-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 0 = (𝑔 ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝑌 ∈ (𝐼‘𝑋) ↔ ∃𝑓 ∈ 𝑇 (𝑌 = ⟨𝑓, 0 ⟩ ∧ (𝑅‘𝑓) ≤ 𝑋)))
Theorem	dibopelval3 40007*	Member of the partial isomorphism B. (Contributed by NM, 3-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 0 = (𝑔 ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (⟨𝐹, 𝑆⟩ ∈ (𝐼‘𝑋) ↔ ((𝐹 ∈ 𝑇 ∧ (𝑅‘𝐹) ≤ 𝑋) ∧ 𝑆 = 0 )))
Theorem	dibelval1st 40008	Membership in value of the partial isomorphism B for a lattice 𝐾. (Contributed by NM, 13-Feb-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐽 = ((DIsoA‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ (𝐼‘𝑋)) → (1st ‘𝑌) ∈ (𝐽‘𝑋))
Theorem	dibelval1st1 40009	Membership in value of the partial isomorphism B for a lattice 𝐾. (Contributed by NM, 13-Feb-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ (𝐼‘𝑋)) → (1st ‘𝑌) ∈ 𝑇)
Theorem	dibelval1st2N 40010	Membership in value of the partial isomorphism B for a lattice 𝐾. (Contributed by NM, 13-Feb-2014.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ (𝐼‘𝑋)) → (𝑅‘(1st ‘𝑌)) ≤ 𝑋)
Theorem	dibelval2nd 40011*	Membership in value of the partial isomorphism B for a lattice 𝐾. (Contributed by NM, 13-Feb-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 0 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ (𝐼‘𝑋)) → (2nd ‘𝑌) = 0 )
Theorem	dibn0 40012	The value of the partial isomorphism B is not empty. (Contributed by NM, 18-Jan-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) ≠ ∅)
Theorem	dibfna 40013	Functionality and domain of the partial isomorphism B. (Contributed by NM, 17-Jan-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐽 = ((DIsoA‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐼 Fn dom 𝐽)
Theorem	dibdiadm 40014	Domain of the partial isomorphism B. (Contributed by NM, 17-Jan-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐽 = ((DIsoA‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → dom 𝐼 = dom 𝐽)
Theorem	dibfnN 40015*	Functionality and domain of the partial isomorphism B. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐼 Fn {𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊})
Theorem	dibdmN 40016*	Domain of the partial isomorphism A. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → dom 𝐼 = {𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊})
Theorem	dibeldmN 40017	Member of domain of the partial isomorphism B. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → (𝑋 ∈ dom 𝐼 ↔ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)))
Theorem	dibord 40018	The isomorphism B for a lattice 𝐾 is order-preserving in the region under co-atom 𝑊. (Contributed by NM, 24-Feb-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → ((𝐼‘𝑋) ⊆ (𝐼‘𝑌) ↔ 𝑋 ≤ 𝑌))
Theorem	dib11N 40019	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 40020	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 40021	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 40022	The value of partial isomorphism B is a relation. (Contributed by NM, 8-Mar-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → Rel (𝐼‘𝑋))
Theorem	dib0 40023	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 40024*	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 40025*	Partial isomorphism B of a lattice glb. (Contributed by NM, 9-Mar-2014.) (New usage is discouraged.)
⊢ 𝐺 = (glb‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅)) → (𝐼‘(𝐺‘𝑆)) = ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))
Theorem	dibintclN 40026	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 40027*	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 40028	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 40029	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 40030*	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 40031	Extend class notation with isomorphism C.
class DIsoC
Definition	df-dic 40032*	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 unity. 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 40033*	The partial isomorphism C for a lattice 𝐾. (Contributed by NM, 15-Dec-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → (DIsoC‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑞 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑤} ↦ {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑔‘((oc‘𝐾)‘𝑤)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑤))})))
Theorem	dicfval 40034*	The partial isomorphism C for a lattice 𝐾. (Contributed by NM, 15-Dec-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐼 = (𝑞 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊} ↦ {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞)) ∧ 𝑠 ∈ 𝐸)}))
Theorem	dicval 40035*	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 40036*	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 40037*	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 40038*	The partial isomorphism C for a lattice 𝐾. (Contributed by NM, 20-Feb-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝐺 = (℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐼‘𝑄) = {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸)})
Theorem	dicelval3 40039*	Member of the partial isomorphism C. (Contributed by NM, 26-Feb-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝐺 = (℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝑌 ∈ (𝐼‘𝑄) ↔ ∃𝑠 ∈ 𝐸 𝑌 = ⟨(𝑠‘𝐺), 𝑠⟩))
Theorem	dicopelval2 40040*	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 40041*	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 40042*	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 40043*	Domain of the partial isomorphism C. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → dom 𝐼 = {𝑝 ∈ 𝐴 ∣ ¬ 𝑝 ≤ 𝑊})
Theorem	dicvalrelN 40044	The value of partial isomorphism C is a relation. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → Rel (𝐼‘𝑋))
Theorem	dicssdvh 40045	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 40046*	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 40047	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 40048	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 40049	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 40050	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 40051	The value of the partial isomorphism C is not empty. (Contributed by NM, 15-Feb-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐼‘𝑄) ≠ ∅)
Theorem	diclss 40052	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 40053*	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 40054*	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 40055*	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 40056*	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 40057*	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 40058*	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 40059*	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 40060	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 40061*	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 40062*	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 40063*	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 40064*	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 40065	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 40066*	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 40067*	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 40068*	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 40069*	Part of proof of Lemma N of [Crawley] p. 121 line 37. TODO: combine cdlemn11a 40066, cdlemn11b 40067, cdlemn11c 40068, 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 40070	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 40071	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 40072*	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 40073*	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 40074*	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 40075	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 40076	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 40077	Part of proof after Lemma N of [Crawley] p. 122. Forward ordering property. TODO: change (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 to 𝑄 ≤ 𝑋 using lhpmcvr3 38884, here and all theorems below. (Contributed by NM, 2-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)    &   ⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑅) ⊕ (𝐼‘(𝑌 ∧ 𝑊))))
Theorem	dihord2a 40078	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 40079	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 40080*	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 40081*	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 40082*	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 40083*	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 40084*	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 40085*	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 40086	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 40087	Extend class notation with isomorphism H.
class DIsoH
Definition	df-dih 40088*	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 40089*	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 40090*	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 40091*	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 40092*	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 40093	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 40094	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 40095	Value of isomorphism H for a lattice 𝐾 when ¬ 𝑋 ≤ 𝑊, given auxiliary atom 𝑄. TODO: Use dihvalcq2 40106 (with lhpmcvr3 38884 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 40096	Value of isomorphism H for a lattice 𝐾 when 𝑋 ≤ 𝑊. (Contributed by NM, 4-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝐷 = ((DIsoB‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) = (𝐷‘𝑋))
Theorem	dihopelvalbN 40097*	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 40098	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 40099*	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 40100*	Isomorphism H at an atom under 𝑊. (Contributed by NM, 27-Apr-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → ∃𝑓 ∈ 𝑇 (𝑓 ≠ ( I ↾ 𝐵) ∧ (𝐼‘𝑄) = (𝑁‘{⟨𝑓, 𝑂⟩})))