P. 418 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 41701-41800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dihlsprn 41701	The span of a vector belongs to the range of isomorphism H. (Contributed by NM, 27-Apr-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ ran 𝐼)
Theorem	dihlspsnssN 41702	A subspace included in a 1-dim subspace belongs to the range of isomorphism H. (Contributed by NM, 26-Apr-2014.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑇 ⊆ (𝑁‘{𝑋})) → (𝑇 ∈ 𝑆 ↔ 𝑇 ∈ ran 𝐼))
Theorem	dihlspsnat 41703	The inverse isomorphism H of the span of a singleton is a Hilbert lattice atom. (Contributed by NM, 27-Apr-2014.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → (◡𝐼‘(𝑁‘{𝑋})) ∈ 𝐴)
Theorem	dihatlat 41704	The isomorphism H of an atom is a 1-dim subspace. (Contributed by NM, 28-Apr-2014.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝐿 = (LSAtoms‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) → (𝐼‘𝑄) ∈ 𝐿)
Theorem	dihat 41705	There exists at least one atom in the subspaces of vector space H. (Contributed by NM, 12-Aug-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → (𝐼‘𝑃) ∈ 𝐴)
Theorem	dihpN 41706*	The value of isomorphism H at the fiducial atom 𝑃 is determined by the vector ⟨0, 𝑆⟩ (the zero translation ltrnid 40505 and a nonzero member of the endomorphism ring). In particular, 𝑆 can be replaced with the ring unity ( I ↾ 𝑇). (Contributed by NM, 26-Aug-2014.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂))    ⇒   ⊢ (𝜑 → (𝐼‘𝑃) = (𝑁‘{⟨( I ↾ 𝐵), 𝑆⟩}))
Theorem	dihlatat 41707	The reverse isomorphism H of a 1-dim subspace is an atom. (Contributed by NM, 28-Apr-2014.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝐿 = (LSAtoms‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐿) → (◡𝐼‘𝑄) ∈ 𝐴)
Theorem	dihatexv 41708*	There is a nonzero vector that maps to every lattice atom. (Contributed by NM, 16-Aug-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑄 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑄 ∈ 𝐴 ↔ ∃𝑥 ∈ (𝑉 ∖ { 0 })(𝐼‘𝑄) = (𝑁‘{𝑥})))
Theorem	dihatexv2 41709*	There is a nonzero vector that maps to every lattice atom. (Contributed by NM, 17-Aug-2014.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → (𝑄 ∈ 𝐴 ↔ ∃𝑥 ∈ (𝑉 ∖ { 0 })𝑄 = (◡𝐼‘(𝑁‘{𝑥}))))
Theorem	dihglblem6 41710*	Isomorphism H of a lattice glb. (Contributed by NM, 9-Apr-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑃 = (LSubSp‘𝑈)    &   ⊢ 𝐷 = (LSAtoms‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) → (𝐼‘(𝐺‘𝑆)) = ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))
Theorem	dihglb 41711*	Isomorphism H of a lattice glb. (Contributed by NM, 11-Apr-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) → (𝐼‘(𝐺‘𝑆)) = ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))
Theorem	dihglb2 41712*	Isomorphism H of a lattice glb. (Contributed by NM, 11-Apr-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝑉) → (𝐼‘(𝐺‘{𝑥 ∈ 𝐵 ∣ 𝑆 ⊆ (𝐼‘𝑥)})) = ∩ {𝑦 ∈ ran 𝐼 ∣ 𝑆 ⊆ 𝑦})
Theorem	dihmeet 41713	Isomorphism H of a lattice meet. (Contributed by NM, 13-Apr-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌)))
Theorem	dihintcl 41714	The intersection of closed subspaces (the range of isomorphism H) is a closed subspace. (Contributed by NM, 14-Apr-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → ∩ 𝑆 ∈ ran 𝐼)
Theorem	dihmeetcl 41715	Closure of closed subspace meet for DVecH vector space. (Contributed by NM, 5-Aug-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼)) → (𝑋 ∩ 𝑌) ∈ ran 𝐼)
Theorem	dihmeet2 41716	Reverse isomorphism H of a closed subspace intersection. (Contributed by NM, 15-Jan-2015.)
⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ ran 𝐼)    ⇒   ⊢ (𝜑 → (◡𝐼‘(𝑋 ∩ 𝑌)) = ((◡𝐼‘𝑋) ∧ (◡𝐼‘𝑌)))
Syntax	coch 41717	Extend class notation with subspace orthocomplement for DVecH vector space.
class ocH
Definition	df-doch 41718*	Define subspace orthocomplement for DVecH vector space. Temporarily, we are using the range of the isomorphism instead of the set of closed subspaces. Later, when inner product is introduced, we will show that these are the same. (Contributed by NM, 14-Mar-2014.)
⊢ ocH = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))))
Theorem	dochffval 41719*	Subspace orthocomplement for DVecH vector space. (Contributed by NM, 14-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → (ocH‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝐾)‘𝑤)) ↦ (((DIsoH‘𝐾)‘𝑤)‘( ⊥ ‘(𝐺‘{𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ (((DIsoH‘𝐾)‘𝑤)‘𝑦)}))))))
Theorem	dochfval 41720*	Subspace orthocomplement for DVecH vector space. (Contributed by NM, 14-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = ((ocH‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → 𝑁 = (𝑥 ∈ 𝒫 𝑉 ↦ (𝐼‘( ⊥ ‘(𝐺‘{𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ (𝐼‘𝑦)})))))
Theorem	dochval 41721*	Subspace orthocomplement for DVecH vector space. (Contributed by NM, 14-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = ((ocH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → (𝑁‘𝑋) = (𝐼‘( ⊥ ‘(𝐺‘{𝑦 ∈ 𝐵 ∣ 𝑋 ⊆ (𝐼‘𝑦)}))))
Theorem	dochval2 41722*	Subspace orthocomplement for DVecH vector space. (Contributed by NM, 14-Apr-2014.)
⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = ((ocH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → (𝑁‘𝑋) = (𝐼‘( ⊥ ‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧}))))
Theorem	dochcl 41723	Closure of subspace orthocomplement for DVecH vector space. (Contributed by NM, 9-Mar-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → ( ⊥ ‘𝑋) ∈ ran 𝐼)
Theorem	dochlss 41724	A subspace orthocomplement is a subspace of the DVecH vector space. (Contributed by NM, 22-Jul-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → ( ⊥ ‘𝑋) ∈ 𝑆)
Theorem	dochssv 41725	A subspace orthocomplement belongs to the DVecH vector space. (Contributed by NM, 22-Jul-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → ( ⊥ ‘𝑋) ⊆ 𝑉)
Theorem	dochfN 41726	Domain and codomain of the subspace orthocomplement for the DVecH vector space. (Contributed by NM, 27-Dec-2014.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → ⊥ :𝒫 𝑉⟶ran 𝐼)
Theorem	dochvalr 41727	Orthocomplement of a closed subspace. (Contributed by NM, 14-Mar-2014.)
⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑁 = ((ocH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ ran 𝐼) → (𝑁‘𝑋) = (𝐼‘( ⊥ ‘(◡𝐼‘𝑋))))
Theorem	doch0 41728	Orthocomplement of the zero subspace. (Contributed by NM, 19-Jun-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( ⊥ ‘{ 0 }) = 𝑉)
Theorem	doch1 41729	Orthocomplement of the unit subspace (all vectors). (Contributed by NM, 19-Jun-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( ⊥ ‘𝑉) = { 0 })
Theorem	dochoc0 41730	The zero subspace is closed. (Contributed by NM, 16-Feb-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘{ 0 })) = { 0 })
Theorem	dochoc1 41731	The unit subspace (all vectors) is closed. (Contributed by NM, 16-Feb-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑉)) = 𝑉)
Theorem	dochvalr2 41732	Orthocomplement of a closed subspace. (Contributed by NM, 21-Jul-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑁 = ((ocH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝑁‘(𝐼‘𝑋)) = (𝐼‘( ⊥ ‘𝑋)))
Theorem	dochvalr3 41733	Orthocomplement of a closed subspace. (Contributed by NM, 15-Jan-2015.)
⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑁 = ((ocH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐼)    ⇒   ⊢ (𝜑 → ( ⊥ ‘(◡𝐼‘𝑋)) = (◡𝐼‘(𝑁‘𝑋)))
Theorem	doch2val2 41734*	Double orthocomplement for DVecH vector space. (Contributed by NM, 26-Jul-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑉)    ⇒   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑋)) = ∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧})
Theorem	dochss 41735	Subset law for orthocomplement. (Contributed by NM, 16-Apr-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ⊆ 𝑉 ∧ 𝑋 ⊆ 𝑌) → ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋))
Theorem	dochocss 41736	Double negative law for orthocomplement of an arbitrary set of vectors. (Contributed by NM, 16-Apr-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → 𝑋 ⊆ ( ⊥ ‘( ⊥ ‘𝑋)))
Theorem	dochoc 41737	Double negative law for orthocomplement of a closed subspace. (Contributed by NM, 14-Mar-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ ran 𝐼) → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋)
Theorem	dochsscl 41738	If a set of vectors is included in a closed set, so is its closure. (Contributed by NM, 17-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ ran 𝐼)    ⇒   ⊢ (𝜑 → (𝑋 ⊆ 𝑌 ↔ ( ⊥ ‘( ⊥ ‘𝑋)) ⊆ 𝑌))
Theorem	dochoccl 41739	A set of vectors is closed iff it equals its double orthocomplent. (Contributed by NM, 1-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋 ∈ ran 𝐼 ↔ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋))
Theorem	dochord 41740	Ordering law for orthocomplement. (Contributed by NM, 12-Aug-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ ran 𝐼)    ⇒   ⊢ (𝜑 → (𝑋 ⊆ 𝑌 ↔ ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋)))
Theorem	dochord2N 41741	Ordering law for orthocomplement. (Contributed by NM, 29-Oct-2014.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ ran 𝐼)    ⇒   ⊢ (𝜑 → (( ⊥ ‘𝑋) ⊆ 𝑌 ↔ ( ⊥ ‘𝑌) ⊆ 𝑋))
Theorem	dochord3 41742	Ordering law for orthocomplement. (Contributed by NM, 9-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ ran 𝐼)    ⇒   ⊢ (𝜑 → (𝑋 ⊆ ( ⊥ ‘𝑌) ↔ 𝑌 ⊆ ( ⊥ ‘𝑋)))
Theorem	doch11 41743	Orthocomplement is one-to-one. (Contributed by NM, 12-Aug-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ ran 𝐼)    ⇒   ⊢ (𝜑 → (( ⊥ ‘𝑋) = ( ⊥ ‘𝑌) ↔ 𝑋 = 𝑌))
Theorem	dochsordN 41744	Strict ordering law for orthocomplement. (Contributed by NM, 12-Aug-2014.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ ran 𝐼)    ⇒   ⊢ (𝜑 → (𝑋 ⊊ 𝑌 ↔ ( ⊥ ‘𝑌) ⊊ ( ⊥ ‘𝑋)))
Theorem	dochn0nv 41745	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 41746	Version of dihoml4 41747 with closed subspaces. (Contributed by NM, 15-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ ran 𝐼)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑌)    ⇒   ⊢ (𝜑 → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = 𝑋)
Theorem	dihoml4 41747	Orthomodular law for constructed vector space H. Lemma 3.3(1) in [Holland95] p. 215. (poml4N 40323 analog.) (Contributed by NM, 15-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    &   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑌)) = 𝑌)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑌)    ⇒   ⊢ (𝜑 → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = ( ⊥ ‘( ⊥ ‘𝑋)))
Theorem	dochspss 41748	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 41749	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 41750	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 41751	The double orthocomplement of a singleton is its span. (Contributed by NM, 13-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘{𝑋})) = (𝑁‘{𝑋}))
Theorem	dochsncom 41752	Swap vectors in an orthocomplement of a singleton. (Contributed by NM, 17-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋 ∈ ( ⊥ ‘{𝑌}) ↔ 𝑌 ∈ ( ⊥ ‘{𝑋})))
Theorem	dochsat 41753	The double orthocomplement of an atom is an atom. (Contributed by NM, 29-Oct-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑄 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘𝑄)) ∈ 𝐴 ↔ 𝑄 ∈ 𝐴))
Theorem	dochshpncl 41754	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 41755	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 41756	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 41757	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 41758	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 41759	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 41760	De Morgan-like law for subspace orthocomplement. (Contributed by NM, 5-Aug-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉) → ( ⊥ ‘(𝑋 ∪ 𝑌)) = (( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑌)))
Theorem	dochnoncon 41761	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 41762	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 41763	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 41764	Extend class notation with subspace join for DVecH vector space.
class joinH
Definition	df-djh 41765*	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 41766*	Subspace join for DVecH vector space. (Contributed by NM, 19-Jul-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑋 → (joinH‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝐾)‘𝑤)), 𝑦 ∈ 𝒫 (Base‘((DVecH‘𝐾)‘𝑤)) ↦ (((ocH‘𝐾)‘𝑤)‘((((ocH‘𝐾)‘𝑤)‘𝑥) ∩ (((ocH‘𝐾)‘𝑤)‘𝑦))))))
Theorem	djhfval 41767*	Subspace join for DVecH vector space. (Contributed by NM, 19-Jul-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → ∨ = (𝑥 ∈ 𝒫 𝑉, 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘(( ⊥ ‘𝑥) ∩ ( ⊥ ‘𝑦)))))
Theorem	djhval 41768	Subspace join for DVecH vector space. (Contributed by NM, 19-Jul-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉)) → (𝑋 ∨ 𝑌) = ( ⊥ ‘(( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑌))))
Theorem	djhval2 41769	Value of subspace join for DVecH vector space. (Contributed by NM, 6-Aug-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉) → (𝑋 ∨ 𝑌) = ( ⊥ ‘( ⊥ ‘(𝑋 ∪ 𝑌))))
Theorem	djhcl 41770	Closure of subspace join for DVecH vector space. (Contributed by NM, 19-Jul-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉)) → (𝑋 ∨ 𝑌) ∈ ran 𝐼)
Theorem	djhlj 41771	Transfer lattice join to DVecH vector space closed subspace join. (Contributed by NM, 19-Jul-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝐽 = ((joinH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐼‘(𝑋 ∨ 𝑌)) = ((𝐼‘𝑋)𝐽(𝐼‘𝑌)))
Theorem	djhljjN 41772	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 41773	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 41774	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 41775	Subspace join commutes. (Contributed by NM, 8-Aug-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋))
Theorem	djhspss 41776	Subspace span of union is a subset of subspace join. (Contributed by NM, 6-Aug-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑉)    ⇒   ⊢ (𝜑 → (𝑁‘(𝑋 ∪ 𝑌)) ⊆ (𝑋 ∨ 𝑌))
Theorem	djhsumss 41777	Subspace sum is a subset of subspace join. (Contributed by NM, 6-Aug-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋 ⊕ 𝑌) ⊆ (𝑋 ∨ 𝑌))
Theorem	dihsumssj 41778	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 41779	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 41780	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 41781	Excluded middle property of DVecH vector space closed subspace join. (Contributed by NM, 22-Jul-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → (𝑋 ∨ ( ⊥ ‘𝑋)) = 𝑉)
Theorem	djh01 41782	Closed subspace join with zero. (Contributed by NM, 9-Aug-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐼)    ⇒   ⊢ (𝜑 → (𝑋 ∨ { 0 }) = 𝑋)
Theorem	djh02 41783	Closed subspace join with zero. (Contributed by NM, 9-Aug-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐼)    ⇒   ⊢ (𝜑 → ({ 0 } ∨ 𝑋) = 𝑋)
Theorem	djhlsmcl 41784	A closed subspace sum equals subspace join. (shjshseli 31580 analog.) (Contributed by NM, 13-Aug-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ((𝑋 ⊕ 𝑌) ∈ ran 𝐼 ↔ (𝑋 ⊕ 𝑌) = (𝑋 ∨ 𝑌)))
Theorem	djhcvat42 41785*	A covering property. (cvrat42 39814 analog.) (Contributed by NM, 17-Aug-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑆 ∈ ran 𝐼)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → ((𝑆 ≠ { 0 } ∧ (𝑁‘{𝑋}) ⊆ (𝑆 ∨ (𝑁‘{𝑌}))) → ∃𝑧 ∈ (𝑉 ∖ { 0 })((𝑁‘{𝑧}) ⊆ 𝑆 ∧ (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑧}) ∨ (𝑁‘{𝑌})))))
Theorem	dihjatb 41786	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 41787	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 41788	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 41789	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 41790*	Lemma for dihjatcc 41792. (Contributed by NM, 28-Sep-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑄) ∧ 𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))    &   ⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))    &   ⊢ 𝐶 = ((oc‘𝐾)‘𝑊)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐺 = (℩𝑑 ∈ 𝑇 (𝑑‘𝐶) = 𝑃)    &   ⊢ 𝐷 = (℩𝑑 ∈ 𝑇 (𝑑‘𝐶) = 𝑄)    ⇒   ⊢ (𝜑 → (𝑅‘(𝐺 ∘ ◡𝐷)) = 𝑉)
Theorem	dihjatcclem4 41791*	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 41792	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 41793	Isomorphism H of lattice join of two atoms. (Contributed by NM, 29-Sep-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)))
Theorem	dihprrnlem1N 41794	Lemma for dihprrn 41796, 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 41795	Lemma for dihprrn 41796. (Contributed by NM, 29-Sep-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    &   ⊢ (𝜑 → 𝑌 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ ran 𝐼)
Theorem	dihprrn 41796	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 41797	The sum of two subspace atoms equals their join. TODO: seems convoluted to go via dihprrn 41796; should we directly use dihjat 41793? (Contributed by NM, 13-Aug-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑁‘{𝑋}) ⊕ (𝑁‘{𝑌})) = ((𝑁‘{𝑋}) ∨ (𝑁‘{𝑌})))
Theorem	dihjat1lem 41798	Subspace sum of a closed subspace and an atom. (pmapjat1 40223 analog.) TODO: merge into dihjat1 41799? (Contributed by NM, 18-Aug-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐼)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝑋 ∨ (𝑁‘{𝑇})) = (𝑋 ⊕ (𝑁‘{𝑇})))
Theorem	dihjat1 41799	Subspace sum of a closed subspace and an atom. (pmapjat1 40223 analog.) (Contributed by NM, 1-Oct-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ∨ = ((joinH‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐼)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋 ∨ (𝑁‘{𝑇})) = (𝑋 ⊕ (𝑁‘{𝑇})))
Theorem	dihsmsprn 41800	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 𝐼)