P. 421 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 42001-42100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dochord3 42001	Ordering law for orthocomplement. (Contributed by NM, 9-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ ran 𝐼)    ⇒   ⊢ (𝜑 → (𝑋 ⊆ ( ⊥ ‘𝑌) ↔ 𝑌 ⊆ ( ⊥ ‘𝑋)))
Theorem	doch11 42002	Orthocomplement is one-to-one. (Contributed by NM, 12-Aug-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ ran 𝐼)    ⇒   ⊢ (𝜑 → (( ⊥ ‘𝑋) = ( ⊥ ‘𝑌) ↔ 𝑋 = 𝑌))
Theorem	dochsordN 42003	Strict ordering law for orthocomplement. (Contributed by NM, 12-Aug-2014.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ ran 𝐼)    ⇒   ⊢ (𝜑 → (𝑋 ⊊ 𝑌 ↔ ( ⊥ ‘𝑌) ⊊ ( ⊥ ‘𝑋)))
Theorem	dochn0nv 42004	An orthocomplement is nonzero iff the double orthocomplement is not the whole vector space. (Contributed by NM, 1-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑉)    ⇒   ⊢ (𝜑 → (( ⊥ ‘𝑋) ≠ { 0 } ↔ ( ⊥ ‘( ⊥ ‘𝑋)) ≠ 𝑉))
Theorem	dihoml4c 42005	Version of dihoml4 42006 with closed subspaces. (Contributed by NM, 15-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ ran 𝐼)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑌)    ⇒   ⊢ (𝜑 → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = 𝑋)
Theorem	dihoml4 42006	Orthomodular law for constructed vector space H. Lemma 3.3(1) in [Holland95] p. 215. (poml4N 40582 analog.) (Contributed by NM, 15-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    &   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑌)) = 𝑌)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑌)    ⇒   ⊢ (𝜑 → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = ( ⊥ ‘( ⊥ ‘𝑋)))
Theorem	dochspss 42007	The span of a set of vectors is included in their double orthocomplement. (Contributed by NM, 26-Jul-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑉)    ⇒   ⊢ (𝜑 → (𝑁‘𝑋) ⊆ ( ⊥ ‘( ⊥ ‘𝑋)))
Theorem	dochocsp 42008	The span of an orthocomplement equals the orthocomplement of the span. (Contributed by NM, 7-Aug-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑉)    ⇒   ⊢ (𝜑 → ( ⊥ ‘(𝑁‘𝑋)) = ( ⊥ ‘𝑋))
Theorem	dochspocN 42009	The span of an orthocomplement equals the orthocomplement of the span. (Contributed by NM, 7-Aug-2014.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑉)    ⇒   ⊢ (𝜑 → (𝑁‘( ⊥ ‘𝑋)) = ( ⊥ ‘(𝑁‘𝑋)))
Theorem	dochocsn 42010	The double orthocomplement of a singleton is its span. (Contributed by NM, 13-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘{𝑋})) = (𝑁‘{𝑋}))
Theorem	dochsncom 42011	Swap vectors in an orthocomplement of a singleton. (Contributed by NM, 17-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋 ∈ ( ⊥ ‘{𝑌}) ↔ 𝑌 ∈ ( ⊥ ‘{𝑋})))
Theorem	dochsat 42012	The double orthocomplement of an atom is an atom. (Contributed by NM, 29-Oct-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑄 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘𝑄)) ∈ 𝐴 ↔ 𝑄 ∈ 𝐴))
Theorem	dochshpncl 42013	If a hyperplane is not closed, its closure equals the vector space. (Contributed by NM, 29-Oct-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑌 = (LSHyp‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑌)    ⇒   ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘𝑋)) ≠ 𝑋 ↔ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑉))
Theorem	dochlkr 42014	Equivalent conditions for the closure of a kernel to be a hyperplane. (Contributed by NM, 29-Oct-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝑌 = (LSHyp‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ∈ 𝑌 ↔ (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ∧ (𝐿‘𝐺) ∈ 𝑌)))
Theorem	dochkrshp 42015	The closure of a kernel is a hyperplane iff it doesn't contain all vectors. (Contributed by NM, 1-Nov-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑌 = (LSHyp‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉 ↔ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ∈ 𝑌))
Theorem	dochkrshp2 42016	Properties of the closure of the kernel of a functional. (Contributed by NM, 1-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑌 = (LSHyp‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉 ↔ (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ∧ (𝐿‘𝐺) ∈ 𝑌)))
Theorem	dochkrshp3 42017	Properties of the closure of the kernel of a functional. (Contributed by NM, 1-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉 ↔ (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ∧ (𝐿‘𝐺) ≠ 𝑉)))
Theorem	dochkrshp4 42018	Properties of the closure of the kernel of a functional. (Contributed by NM, 1-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ↔ (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉 ∨ (𝐿‘𝐺) = 𝑉)))
Theorem	dochdmj1 42019	De Morgan-like law for subspace orthocomplement. (Contributed by NM, 5-Aug-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉) → ( ⊥ ‘(𝑋 ∪ 𝑌)) = (( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑌)))
Theorem	dochnoncon 42020	Law of noncontradiction. The intersection of a subspace and its orthocomplement is the zero subspace. (Contributed by NM, 16-Apr-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → (𝑋 ∩ ( ⊥ ‘𝑋)) = { 0 })
Theorem	dochnel2 42021	A nonzero member of a subspace doesn't belong to the orthocomplement of the subspace. (Contributed by NM, 28-Feb-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑇 ∖ { 0 }))    ⇒   ⊢ (𝜑 → ¬ 𝑋 ∈ ( ⊥ ‘𝑇))
Theorem	dochnel 42022	A nonzero vector doesn't belong to the orthocomplement of its singleton. (Contributed by NM, 27-Oct-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → ¬ 𝑋 ∈ ( ⊥ ‘{𝑋}))
Syntax	cdjh 42023	Extend class notation with subspace join for DVecH vector space.
class joinH
Definition	df-djh 42024*	Define (closed) subspace join for DVecH vector space. (Contributed by NM, 19-Jul-2014.)
⊢ joinH = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)), 𝑦 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((ocH‘𝑘)‘𝑤)‘((((ocH‘𝑘)‘𝑤)‘𝑥) ∩ (((ocH‘𝑘)‘𝑤)‘𝑦))))))
Theorem	djhffval 42025*	Subspace join for DVecH vector space. (Contributed by NM, 19-Jul-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑋 → (joinH‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝐾)‘𝑤)), 𝑦 ∈ 𝒫 (Base‘((DVecH‘𝐾)‘𝑤)) ↦ (((ocH‘𝐾)‘𝑤)‘((((ocH‘𝐾)‘𝑤)‘𝑥) ∩ (((ocH‘𝐾)‘𝑤)‘𝑦))))))
Theorem	djhfval 42026*	Subspace join for DVecH vector space. (Contributed by NM, 19-Jul-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → ∨ = (𝑥 ∈ 𝒫 𝑉, 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘(( ⊥ ‘𝑥) ∩ ( ⊥ ‘𝑦)))))
Theorem	djhval 42027	Subspace join for DVecH vector space. (Contributed by NM, 19-Jul-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉)) → (𝑋 ∨ 𝑌) = ( ⊥ ‘(( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑌))))
Theorem	djhval2 42028	Value of subspace join for DVecH vector space. (Contributed by NM, 6-Aug-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉) → (𝑋 ∨ 𝑌) = ( ⊥ ‘( ⊥ ‘(𝑋 ∪ 𝑌))))
Theorem	djhcl 42029	Closure of subspace join for DVecH vector space. (Contributed by NM, 19-Jul-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉)) → (𝑋 ∨ 𝑌) ∈ ran 𝐼)
Theorem	djhlj 42030	Transfer lattice join to DVecH vector space closed subspace join. (Contributed by NM, 19-Jul-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝐽 = ((joinH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐼‘(𝑋 ∨ 𝑌)) = ((𝐼‘𝑋)𝐽(𝐼‘𝑌)))
Theorem	djhljjN 42031	Lattice join in terms of DVecH vector space closed subspace join. (Contributed by NM, 17-Aug-2014.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝐽 = ((joinH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∨ 𝑌) = (◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌))))
Theorem	djhjlj 42032	DVecH vector space closed subspace join in terms of lattice join. (Contributed by NM, 9-Aug-2014.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝐽 = ((joinH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ ran 𝐼)    ⇒   ⊢ (𝜑 → (𝑋𝐽𝑌) = (𝐼‘((◡𝐼‘𝑋) ∨ (◡𝐼‘𝑌))))
Theorem	djhj 42033	DVecH vector space closed subspace join in terms of lattice join. (Contributed by NM, 17-Aug-2014.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝐽 = ((joinH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ ran 𝐼)    ⇒   ⊢ (𝜑 → (◡𝐼‘(𝑋𝐽𝑌)) = ((◡𝐼‘𝑋) ∨ (◡𝐼‘𝑌)))
Theorem	djhcom 42034	Subspace join commutes. (Contributed by NM, 8-Aug-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋))
Theorem	djhspss 42035	Subspace span of union is a subset of subspace join. (Contributed by NM, 6-Aug-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑉)    ⇒   ⊢ (𝜑 → (𝑁‘(𝑋 ∪ 𝑌)) ⊆ (𝑋 ∨ 𝑌))
Theorem	djhsumss 42036	Subspace sum is a subset of subspace join. (Contributed by NM, 6-Aug-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋 ⊕ 𝑌) ⊆ (𝑋 ∨ 𝑌))
Theorem	dihsumssj 42037	The subspace sum of two isomorphisms of lattice elements is less than the isomorphism of their lattice join. (Contributed by NM, 23-Sep-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝐼‘𝑋) ⊕ (𝐼‘𝑌)) ⊆ (𝐼‘(𝑋 ∨ 𝑌)))
Theorem	djhunssN 42038	Subspace union is a subset of subspace join. (Contributed by NM, 6-Aug-2014.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋 ∪ 𝑌) ⊆ (𝑋 ∨ 𝑌))
Theorem	dochdmm1 42039	De Morgan-like law for closed subspace orthocomplement. (Contributed by NM, 13-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ ran 𝐼)    ⇒   ⊢ (𝜑 → ( ⊥ ‘(𝑋 ∩ 𝑌)) = (( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌)))
Theorem	djhexmid 42040	Excluded middle property of DVecH vector space closed subspace join. (Contributed by NM, 22-Jul-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → (𝑋 ∨ ( ⊥ ‘𝑋)) = 𝑉)
Theorem	djh01 42041	Closed subspace join with zero. (Contributed by NM, 9-Aug-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐼)    ⇒   ⊢ (𝜑 → (𝑋 ∨ { 0 }) = 𝑋)
Theorem	djh02 42042	Closed subspace join with zero. (Contributed by NM, 9-Aug-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐼)    ⇒   ⊢ (𝜑 → ({ 0 } ∨ 𝑋) = 𝑋)
Theorem	djhlsmcl 42043	A closed subspace sum equals subspace join. (shjshseli 31703 analog.) (Contributed by NM, 13-Aug-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ((𝑋 ⊕ 𝑌) ∈ ran 𝐼 ↔ (𝑋 ⊕ 𝑌) = (𝑋 ∨ 𝑌)))
Theorem	djhcvat42 42044*	A covering property. (cvrat42 40073 analog.) (Contributed by NM, 17-Aug-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑆 ∈ ran 𝐼)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → ((𝑆 ≠ { 0 } ∧ (𝑁‘{𝑋}) ⊆ (𝑆 ∨ (𝑁‘{𝑌}))) → ∃𝑧 ∈ (𝑉 ∖ { 0 })((𝑁‘{𝑧}) ⊆ 𝑆 ∧ (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑧}) ∨ (𝑁‘{𝑌})))))
Theorem	dihjatb 42045	Isomorphism H of lattice join of two atoms under the fiducial hyperplane. (Contributed by NM, 23-Sep-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊))    &   ⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊))    ⇒   ⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)))
Theorem	dihjatc 42046	Isomorphism H of lattice join of an element under the fiducial hyperplane with atom not under it. (Contributed by NM, 26-Aug-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊))    &   ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))    ⇒   ⊢ (𝜑 → (𝐼‘(𝑋 ∨ 𝑃)) = ((𝐼‘𝑋) ⊕ (𝐼‘𝑃)))
Theorem	dihjatcclem1 42047	Lemma for isomorphism H of lattice join of two atoms not under the fiducial hyperplane. (Contributed by NM, 26-Sep-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))    &   ⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))    ⇒   ⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) = (((𝐼‘𝑃) ⊕ (𝐼‘𝑄)) ⊕ (𝐼‘𝑉)))
Theorem	dihjatcclem2 42048	Lemma for isomorphism H of lattice join of two atoms not under the fiducial hyperplane. (Contributed by NM, 26-Sep-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))    &   ⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))    &   ⊢ (𝜑 → (𝐼‘𝑉) ⊆ ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)))    ⇒   ⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)))
Theorem	dihjatcclem3 42049*	Lemma for dihjatcc 42051. (Contributed by NM, 28-Sep-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))    &   ⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))    &   ⊢ 𝐶 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐺 = (℩𝑑 ∈ 𝑇 (𝑑‘𝐶) = 𝑃)    &   ⊢ 𝐷 = (℩𝑑 ∈ 𝑇 (𝑑‘𝐶) = 𝑄)    ⇒   ⊢ (𝜑 → (𝑅‘(𝐺 ∘ ◡𝐷)) = 𝑉)
Theorem	dihjatcclem4 42050*	Lemma for isomorphism H of lattice join of two atoms not under the fiducial hyperplane. (Contributed by NM, 29-Sep-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))    &   ⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))    &   ⊢ 𝐶 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐺 = (℩𝑑 ∈ 𝑇 (𝑑‘𝐶) = 𝑃)    &   ⊢ 𝐷 = (℩𝑑 ∈ 𝑇 (𝑑‘𝐶) = 𝑄)    &   ⊢ 𝑁 = (𝑎 ∈ 𝐸 ↦ (𝑑 ∈ 𝑇 ↦ ◡(𝑎‘𝑑)))    &   ⊢ 0 = (𝑑 ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝐽 = (𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (𝑑 ∈ 𝑇 ↦ ((𝑎‘𝑑) ∘ (𝑏‘𝑑))))    ⇒   ⊢ (𝜑 → (𝐼‘𝑉) ⊆ ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)))
Theorem	dihjatcc 42051	Isomorphism H of lattice join of two atoms not under the fiducial hyperplane. (Contributed by NM, 29-Sep-2014.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))    &   ⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))    ⇒   ⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)))
Theorem	dihjat 42052	Isomorphism H of lattice join of two atoms. (Contributed by NM, 29-Sep-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)))
Theorem	dihprrnlem1N 42053	Lemma for dihprrn 42055, showing one of 4 cases. (Contributed by NM, 30-Aug-2014.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ (𝜑 → 𝑌 ≠ 0 )    &   ⊢ (𝜑 → (◡𝐼‘(𝑁‘{𝑋})) ≤ 𝑊)    &   ⊢ (𝜑 → ¬ (◡𝐼‘(𝑁‘{𝑌})) ≤ 𝑊)    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ ran 𝐼)
Theorem	dihprrnlem2 42054	Lemma for dihprrn 42055. (Contributed by NM, 29-Sep-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    &   ⊢ (𝜑 → 𝑌 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ ran 𝐼)
Theorem	dihprrn 42055	The span of a vector pair belongs to the range of isomorphism H i.e. is a closed subspace. (Contributed by NM, 29-Sep-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ ran 𝐼)
Theorem	djhlsmat 42056	The sum of two subspace atoms equals their join. TODO: seems convoluted to go via dihprrn 42055; should we directly use dihjat 42052? (Contributed by NM, 13-Aug-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑁‘{𝑋}) ⊕ (𝑁‘{𝑌})) = ((𝑁‘{𝑋}) ∨ (𝑁‘{𝑌})))
Theorem	dihjat1lem 42057	Subspace sum of a closed subspace and an atom. (pmapjat1 40482 analog.) TODO: merge into dihjat1 42058? (Contributed by NM, 18-Aug-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐼)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝑋 ∨ (𝑁‘{𝑇})) = (𝑋 ⊕ (𝑁‘{𝑇})))
Theorem	dihjat1 42058	Subspace sum of a closed subspace and an atom. (pmapjat1 40482 analog.) (Contributed by NM, 1-Oct-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐼)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋 ∨ (𝑁‘{𝑇})) = (𝑋 ⊕ (𝑁‘{𝑇})))
Theorem	dihsmsprn 42059	Subspace sum of a closed subspace and the span of a singleton. (Contributed by NM, 17-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐼)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋 ⊕ (𝑁‘{𝑇})) ∈ ran 𝐼)
Theorem	dihjat2 42060	The subspace sum of a closed subspace and an atom is the same as their subspace join. (Contributed by NM, 1-Oct-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐼)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑋 ∨ 𝑄) = (𝑋 ⊕ 𝑄))
Theorem	dihjat3 42061	Isomorphism H of lattice join with an atom. (Contributed by NM, 25-Apr-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑃 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝐼‘(𝑋 ∨ 𝑃)) = ((𝐼‘𝑋) ⊕ (𝐼‘𝑃)))
Theorem	dihjat4 42062	Transfer the subspace sum of a closed subspace and an atom back to lattice join. (Contributed by NM, 25-Apr-2015.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐼)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑋 ⊕ 𝑄) = (𝐼‘((◡𝐼‘𝑋) ∨ (◡𝐼‘𝑄))))
Theorem	dihjat6 42063	Transfer the subspace sum of a closed subspace and an atom back to lattice join. (Contributed by NM, 25-Apr-2015.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐼)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (◡𝐼‘(𝑋 ⊕ 𝑄)) = ((◡𝐼‘𝑋) ∨ (◡𝐼‘𝑄)))
Theorem	dihsmsnrn 42064	The subspace sum of two singleton spans is closed. (Contributed by NM, 27-Feb-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑁‘{𝑋}) ⊕ (𝑁‘{𝑌})) ∈ ran 𝐼)
Theorem	dihsmatrn 42065	The subspace sum of a closed subspace and an atom is closed. TODO: see if proof at https://math.stackexchange.com/a/1233211/50776 and Mon, 13 Apr 2015 20:44:07 -0400 email could be used instead of this and dihjat2 42060. (Contributed by NM, 15-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐼)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑋 ⊕ 𝑄) ∈ ran 𝐼)
Theorem	dihjat5N 42066	Transfer lattice join with atom to subspace sum. (Contributed by NM, 25-Apr-2015.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑃 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑋 ∨ 𝑃) = (◡𝐼‘((𝐼‘𝑋) ⊕ (𝐼‘𝑃))))
Theorem	dvh4dimat 42067*	There is an atom that is outside the subspace sum of 3 others. (Contributed by NM, 25-Apr-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ 𝐴 ¬ 𝑠 ⊆ ((𝑃 ⊕ 𝑄) ⊕ 𝑅))
Theorem	dvh3dimatN 42068*	There is an atom that is outside the subspace sum of 2 others. (Contributed by NM, 25-Apr-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ 𝐴 ¬ 𝑠 ⊆ (𝑃 ⊕ 𝑄))
Theorem	dvh2dimatN 42069*	Given an atom, there exists another. (Contributed by NM, 25-Apr-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ 𝐴 𝑠 ≠ 𝑃)
Theorem	dvh1dimat 42070*	There exists an atom. (Contributed by NM, 25-Apr-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → ∃𝑠 𝑠 ∈ 𝐴)
Theorem	dvh1dim 42071*	There exists a nonzero vector. (Contributed by NM, 26-Apr-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 𝑧 ≠ 0 )
Theorem	dvh4dimlem 42072*	Lemma for dvh4dimN 42076. (Contributed by NM, 22-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    &   ⊢ (𝜑 → 𝑌 ≠ 0 )    &   ⊢ (𝜑 → 𝑍 ≠ 0 )    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌, 𝑍}))
Theorem	dvhdimlem 42073*	Lemma for dvh2dim 42074 and dvh3dim 42075. TODO: make this obsolete and use dvh4dimlem 42072 directly? (Contributed by NM, 24-Apr-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    &   ⊢ (𝜑 → 𝑌 ≠ 0 )    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}))
Theorem	dvh2dim 42074*	There is a vector that is outside the span of another. (Contributed by NM, 25-Apr-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝑋}))
Theorem	dvh3dim 42075*	There is a vector that is outside the span of 2 others. (Contributed by NM, 24-Apr-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}))
Theorem	dvh4dimN 42076*	There is a vector that is outside the span of 3 others. (Contributed by NM, 22-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌, 𝑍}))
Theorem	dvh3dim2 42077*	There is a vector that is outside of 2 spans with a common vector. (Contributed by NM, 13-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑍})))
Theorem	dvh3dim3N 42078*	There is a vector that is outside of 2 spans. TODO: decide to use either this or dvh3dim2 42077 everywhere. If this one is needed, make dvh3dim2 42077 into a lemma. (Contributed by NM, 21-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇})))
Theorem	dochsnnz 42079	The orthocomplement of a singleton is nonzero. (Contributed by NM, 13-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ≠ { 0 })
Theorem	dochsatshp 42080	The orthocomplement of a subspace atom is a hyperplane. (Contributed by NM, 27-Jul-2014.) (Revised by Mario Carneiro, 1-Oct-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ 𝑌 = (LSHyp‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ( ⊥ ‘𝑄) ∈ 𝑌)
Theorem	dochsatshpb 42081	The orthocomplement of a subspace atom is a hyperplane. (Contributed by NM, 29-Oct-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ 𝑌 = (LSHyp‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑄 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑄 ∈ 𝐴 ↔ ( ⊥ ‘𝑄) ∈ 𝑌))
Theorem	dochsnshp 42082	The orthocomplement of a nonzero singleton is a hyperplane. (Contributed by NM, 3-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑌 = (LSHyp‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ∈ 𝑌)
Theorem	dochshpsat 42083	A hyperplane is closed iff its orthocomplement is an atom. (Contributed by NM, 29-Oct-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ 𝑌 = (LSHyp‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑌)    ⇒   ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ↔ ( ⊥ ‘𝑋) ∈ 𝐴))
Theorem	dochkrsat 42084	The orthocomplement of a kernel is an atom iff it is nonzero. (Contributed by NM, 1-Nov-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (( ⊥ ‘(𝐿‘𝐺)) ≠ { 0 } ↔ ( ⊥ ‘(𝐿‘𝐺)) ∈ 𝐴))
Theorem	dochkrsat2 42085	The orthocomplement of a kernel is an atom iff the double orthocomplement is not the vector space. (Contributed by NM, 1-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉 ↔ ( ⊥ ‘(𝐿‘𝐺)) ∈ 𝐴))
Theorem	dochsat0 42086	The orthocomplement of a kernel is either an atom or zero. (Contributed by NM, 29-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (( ⊥ ‘(𝐿‘𝐺)) ∈ 𝐴 ∨ ( ⊥ ‘(𝐿‘𝐺)) = { 0 }))
Theorem	dochkrsm 42087	The subspace sum of a closed subspace and a kernel orthocomplement is closed. (djhlsmcl 42043 can be used to convert sum to join.) (Contributed by NM, 29-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐼)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝑋 ⊕ ( ⊥ ‘(𝐿‘𝐺))) ∈ ran 𝐼)
Theorem	dochexmidat 42088	Special case of excluded middle for the singleton of a vector. (Contributed by NM, 27-Oct-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (( ⊥ ‘{𝑋}) ⊕ (𝑁‘{𝑋})) = 𝑉)
Theorem	dochexmidlem1 42089	Lemma for dochexmid 42097. Holland's proof implicitly requires 𝑞 ≠ 𝑟, which we prove here. (Contributed by NM, 14-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑝 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑞 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑟 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑞 ⊆ ( ⊥ ‘𝑋))    &   ⊢ (𝜑 → 𝑟 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → 𝑞 ≠ 𝑟)
Theorem	dochexmidlem2 42090	Lemma for dochexmid 42097. (Contributed by NM, 14-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑝 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑞 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑟 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑞 ⊆ ( ⊥ ‘𝑋))    &   ⊢ (𝜑 → 𝑟 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝑝 ⊆ (𝑟 ⊕ 𝑞))    ⇒   ⊢ (𝜑 → 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋)))
Theorem	dochexmidlem3 42091	Lemma for dochexmid 42097. Use atom exchange lsatexch1 39675 to swap 𝑝 and 𝑞. (Contributed by NM, 14-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑝 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑞 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑟 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑞 ⊆ ( ⊥ ‘𝑋))    &   ⊢ (𝜑 → 𝑟 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝑞 ⊆ (𝑟 ⊕ 𝑝))    ⇒   ⊢ (𝜑 → 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋)))
Theorem	dochexmidlem4 42092	Lemma for dochexmid 42097. (Contributed by NM, 15-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑝 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑞 ∈ 𝐴)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑀 = (𝑋 ⊕ 𝑝)    &   ⊢ (𝜑 → 𝑋 ≠ { 0 })    &   ⊢ (𝜑 → 𝑞 ⊆ (( ⊥ ‘𝑋) ∩ 𝑀))    ⇒   ⊢ (𝜑 → 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋)))
Theorem	dochexmidlem5 42093	Lemma for dochexmid 42097. (Contributed by NM, 15-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑝 ∈ 𝐴)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑀 = (𝑋 ⊕ 𝑝)    &   ⊢ (𝜑 → 𝑋 ≠ { 0 })    &   ⊢ (𝜑 → ¬ 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋)))    ⇒   ⊢ (𝜑 → (( ⊥ ‘𝑋) ∩ 𝑀) = { 0 })
Theorem	dochexmidlem6 42094	Lemma for dochexmid 42097. (Contributed by NM, 15-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑝 ∈ 𝐴)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑀 = (𝑋 ⊕ 𝑝)    &   ⊢ (𝜑 → 𝑋 ≠ { 0 })    &   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋)    &   ⊢ (𝜑 → ¬ 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋)))    ⇒   ⊢ (𝜑 → 𝑀 = 𝑋)
Theorem	dochexmidlem7 42095	Lemma for dochexmid 42097. Contradict dochexmidlem6 42094. (Contributed by NM, 15-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑝 ∈ 𝐴)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑀 = (𝑋 ⊕ 𝑝)    &   ⊢ (𝜑 → 𝑋 ≠ { 0 })    &   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋)    &   ⊢ (𝜑 → ¬ 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋)))    ⇒   ⊢ (𝜑 → 𝑀 ≠ 𝑋)
Theorem	dochexmidlem8 42096	Lemma for dochexmid 42097. The contradiction of dochexmidlem6 42094 and dochexmidlem7 42095 shows that there can be no atom 𝑝 that is not in 𝑋 + ( ⊥ ‘𝑋), which is therefore the whole atom space. (Contributed by NM, 15-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ (𝜑 → 𝑋 ≠ { 0 })    &   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋)    ⇒   ⊢ (𝜑 → (𝑋 ⊕ ( ⊥ ‘𝑋)) = 𝑉)
Theorem	dochexmid 42097	Excluded middle law for closed subspaces, which is equivalent to (and derived from) the orthomodular law dihoml4 42006. Lemma 3.3(2) in [Holland95] p. 215. In our proof, we use the variables 𝑋, 𝑀, 𝑝, 𝑞, 𝑟 in place of Hollands' l, m, P, Q, L respectively. (pexmidALTN 40607 analog.) (Contributed by NM, 15-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋)    ⇒   ⊢ (𝜑 → (𝑋 ⊕ ( ⊥ ‘𝑋)) = 𝑉)
Theorem	dochsnkrlem1 42098	Lemma for dochsnkr 42101. (Contributed by NM, 1-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }))    ⇒   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉)
Theorem	dochsnkrlem2 42099	Lemma for dochsnkr 42101. (Contributed by NM, 1-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }))    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    ⇒   ⊢ (𝜑 → ( ⊥ ‘(𝐿‘𝐺)) ∈ 𝐴)
Theorem	dochsnkrlem3 42100	Lemma for dochsnkr 42101. (Contributed by NM, 2-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }))    ⇒   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺))