P. 427 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 42601-42700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dochsatshp 42601	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 42602	The orthocomplement of a subspace atom is a hyperplane. (Contributed by NM, 29-Oct-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ 𝑌 = (LSHyp‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑄 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑄 ∈ 𝐴 ↔ ( ⊥ ‘𝑄) ∈ 𝑌))
Theorem	dochsnshp 42603	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 42604	A hyperplane is closed iff its orthocomplement is an atom. (Contributed by NM, 29-Oct-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ 𝑌 = (LSHyp‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑌)    ⇒   ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ↔ ( ⊥ ‘𝑋) ∈ 𝐴))
Theorem	dochkrsat 42605	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 42606	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 42607	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 42608	The subspace sum of a closed subspace and a kernel orthocomplement is closed. (djhlsmcl 42564 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 42609	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 42610	Lemma for dochexmid 42618. 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 42611	Lemma for dochexmid 42618. (Contributed by NM, 14-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑝 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑞 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑟 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑞 ⊆ ( ⊥ ‘𝑋))    &   ⊢ (𝜑 → 𝑟 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝑝 ⊆ (𝑟 ⊕ 𝑞))    ⇒   ⊢ (𝜑 → 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋)))
Theorem	dochexmidlem3 42612	Lemma for dochexmid 42618. Use atom exchange lsatexch1 40196 to swap 𝑝 and 𝑞. (Contributed by NM, 14-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑝 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑞 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑟 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑞 ⊆ ( ⊥ ‘𝑋))    &   ⊢ (𝜑 → 𝑟 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝑞 ⊆ (𝑟 ⊕ 𝑝))    ⇒   ⊢ (𝜑 → 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋)))
Theorem	dochexmidlem4 42613	Lemma for dochexmid 42618. (Contributed by NM, 15-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑝 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑞 ∈ 𝐴)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑀 = (𝑋 ⊕ 𝑝)    &   ⊢ (𝜑 → 𝑋 ≠ { 0 })    &   ⊢ (𝜑 → 𝑞 ⊆ (( ⊥ ‘𝑋) ∩ 𝑀))    ⇒   ⊢ (𝜑 → 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋)))
Theorem	dochexmidlem5 42614	Lemma for dochexmid 42618. (Contributed by NM, 15-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑝 ∈ 𝐴)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑀 = (𝑋 ⊕ 𝑝)    &   ⊢ (𝜑 → 𝑋 ≠ { 0 })    &   ⊢ (𝜑 → ¬ 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋)))    ⇒   ⊢ (𝜑 → (( ⊥ ‘𝑋) ∩ 𝑀) = { 0 })
Theorem	dochexmidlem6 42615	Lemma for dochexmid 42618. (Contributed by NM, 15-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑝 ∈ 𝐴)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑀 = (𝑋 ⊕ 𝑝)    &   ⊢ (𝜑 → 𝑋 ≠ { 0 })    &   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋)    &   ⊢ (𝜑 → ¬ 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋)))    ⇒   ⊢ (𝜑 → 𝑀 = 𝑋)
Theorem	dochexmidlem7 42616	Lemma for dochexmid 42618. Contradict dochexmidlem6 42615. (Contributed by NM, 15-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑝 ∈ 𝐴)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑀 = (𝑋 ⊕ 𝑝)    &   ⊢ (𝜑 → 𝑋 ≠ { 0 })    &   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋)    &   ⊢ (𝜑 → ¬ 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋)))    ⇒   ⊢ (𝜑 → 𝑀 ≠ 𝑋)
Theorem	dochexmidlem8 42617	Lemma for dochexmid 42618. The contradiction of dochexmidlem6 42615 and dochexmidlem7 42616 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 42618	Excluded middle law for closed subspaces, which is equivalent to (and derived from) the orthomodular law dihoml4 42527. 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 41128 analog.) (Contributed by NM, 15-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋)    ⇒   ⊢ (𝜑 → (𝑋 ⊕ ( ⊥ ‘𝑋)) = 𝑉)
Theorem	dochsnkrlem1 42619	Lemma for dochsnkr 42622. (Contributed by NM, 1-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }))    ⇒   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉)
Theorem	dochsnkrlem2 42620	Lemma for dochsnkr 42622. (Contributed by NM, 1-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }))    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    ⇒   ⊢ (𝜑 → ( ⊥ ‘(𝐿‘𝐺)) ∈ 𝐴)
Theorem	dochsnkrlem3 42621	Lemma for dochsnkr 42622. (Contributed by NM, 2-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }))    ⇒   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺))
Theorem	dochsnkr 42622	A (closed) kernel expressed in terms of a nonzero vector in its orthocomplement. TODO: consolidate lemmas unless they're needed for something else (in which case break out as theorems). (Contributed by NM, 2-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑋}))
Theorem	dochsnkr2 42623*	Kernel of the explicit functional 𝐺 determined by a nonzero vector 𝑋. Compare the more general lshpkr 40267. (Contributed by NM, 27-Oct-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (Scalar‘𝑈)    &   ⊢ 𝑅 = (Base‘𝐷)    &   ⊢ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋))))    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑋}))
Theorem	dochsnkr2cl 42624*	The 𝑋 determining functional 𝐺 belongs to the atom formed by the orthocomplement of the kernel. (Contributed by NM, 4-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (Scalar‘𝑈)    &   ⊢ 𝑅 = (Base‘𝐷)    &   ⊢ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋))))    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → 𝑋 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }))
Theorem	dochflcl 42625*	Closure of the explicit functional 𝐺 determined by a nonzero vector 𝑋. Compare the more general lshpkrcl 40266. (Contributed by NM, 27-Oct-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐷 = (Scalar‘𝑈)    &   ⊢ 𝑅 = (Base‘𝐷)    &   ⊢ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋))))    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → 𝐺 ∈ 𝐹)
Theorem	dochfl1 42626*	The value of the explicit functional 𝐺 is 1 at the 𝑋 that determines it. (Contributed by NM, 27-Oct-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐷 = (Scalar‘𝑈)    &   ⊢ 𝑅 = (Base‘𝐷)    &   ⊢ 1 = (1r‘𝐷)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋))))    ⇒   ⊢ (𝜑 → (𝐺‘𝑋) = 1 )
Theorem	dochfln0 42627	The value of a functional is nonzero at a nonzero vector in the orthocomplement of its kernel. (Contributed by NM, 2-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝑁 = (0g‘𝑅)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝐺‘𝑋) ≠ 𝑁)
Theorem	dochkr1 42628*	A nonzero functional has a value of 1 at some argument belonging to the orthocomplement of its kernel (when its kernel is a closed hyperplane). Tighter version of lfl1 40220. (Contributed by NM, 2-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 })(𝐺‘𝑥) = 1 )
Theorem	dochkr1OLDN 42629*	A nonzero functional has a value of 1 at some argument belonging to the orthocomplement of its kernel (when its kernel is a closed hyperplane). Tighter version of lfl1 40220. (Contributed by NM, 2-Jan-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ( ⊥ ‘(𝐿‘𝐺))(𝐺‘𝑥) = 1 )
21.30.14  Construction of involution and inner product from a Hilbert lattice
Syntax	clpoN 42630	Extend class notation with all polarities of a left module or left vector space.
class LPol
Definition	df-lpolN 42631*	Define the set of all polarities of a left module or left vector space. A polarity is a kind of complementation operation on a subspace. The double polarity of a subspace is a closure operation. Based on Definition 3.2 of [Holland95] p. 214 for projective geometry polarities. For convenience, we open up the domain to include all vector subsets and not just subspaces, but any more restricted polarity can be converted to this one by taking the span of its argument. (Contributed by NM, 24-Nov-2014.)
⊢ LPol = (𝑤 ∈ V ↦ {𝑜 ∈ ((LSubSp‘𝑤) ↑m 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))})
Theorem	lpolsetN 42632*	The set of polarities of a left module or left vector space. (Contributed by NM, 24-Nov-2014.) (New usage is discouraged.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝑃 = (LPol‘𝑊)    ⇒   ⊢ (𝑊 ∈ 𝑋 → 𝑃 = {𝑜 ∈ (𝑆 ↑m 𝒫 𝑉) ∣ ((𝑜‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ((𝑜‘𝑥) ∈ 𝐻 ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))})
Theorem	islpolN 42633*	The predicate "is a polarity". (Contributed by NM, 24-Nov-2014.) (New usage is discouraged.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝑃 = (LPol‘𝑊)    ⇒   ⊢ (𝑊 ∈ 𝑋 → ( ⊥ ∈ 𝑃 ↔ ( ⊥ :𝒫 𝑉⟶𝑆 ∧ (( ⊥ ‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥ ‘𝑥)) = 𝑥)))))
Theorem	islpoldN 42634*	Properties that determine a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝑃 = (LPol‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → ⊥ :𝒫 𝑉⟶𝑆)    &   ⊢ (𝜑 → ( ⊥ ‘𝑉) = { 0 })    &   ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦)) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ( ⊥ ‘𝑥) ∈ 𝐻)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑥)) = 𝑥)    ⇒   ⊢ (𝜑 → ⊥ ∈ 𝑃)
Theorem	lpolfN 42635	Functionality of a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑃 = (LPol‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → ⊥ ∈ 𝑃)    ⇒   ⊢ (𝜑 → ⊥ :𝒫 𝑉⟶𝑆)
Theorem	lpolvN 42636	The polarity of the whole space is the zero subspace. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑃 = (LPol‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → ⊥ ∈ 𝑃)    ⇒   ⊢ (𝜑 → ( ⊥ ‘𝑉) = { 0 })
Theorem	lpolconN 42637	Contraposition property of a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑃 = (LPol‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → ⊥ ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑌)    ⇒   ⊢ (𝜑 → ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋))
Theorem	lpolsatN 42638	The polarity of an atomic subspace is a hyperplane. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.)
⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝑃 = (LPol‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → ⊥ ∈ 𝑃)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ( ⊥ ‘𝑄) ∈ 𝐻)
Theorem	lpolpolsatN 42639	Property of a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.)
⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ 𝑃 = (LPol‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → ⊥ ∈ 𝑃)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑄)) = 𝑄)
Theorem	dochpolN 42640	The subspace orthocomplement for the DVecH vector space is a polarity. (Contributed by NM, 27-Dec-2014.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑃 = (LPol‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → ⊥ ∈ 𝑃)
Theorem	lcfl1lem 42641*	Property of a functional with a closed kernel. (Contributed by NM, 28-Dec-2014.)
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    ⇒   ⊢ (𝐺 ∈ 𝐶 ↔ (𝐺 ∈ 𝐹 ∧ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺)))
Theorem	lcfl1 42642*	Property of a functional with a closed kernel. (Contributed by NM, 31-Dec-2014.)
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺)))
Theorem	lcfl2 42643*	Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉 ∨ (𝐿‘𝐺) = 𝑉)))
Theorem	lcfl3 42644*	Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ (( ⊥ ‘(𝐿‘𝐺)) ∈ 𝐴 ∨ (𝐿‘𝐺) = 𝑉)))
Theorem	lcfl4N 42645*	Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑌 = (LSHyp‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ∈ 𝑌 ∨ (𝐿‘𝐺) = 𝑉)))
Theorem	lcfl5 42646*	Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ (𝐿‘𝐺) ∈ ran 𝐼))
Theorem	lcfl5a 42647	Property of a functional with a closed kernel. TODO: Make lcfl5 42646 etc. obsolete and rewrite without 𝐶 hypothesis? (Contributed by NM, 29-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ↔ (𝐿‘𝐺) ∈ ran 𝐼))
Theorem	lcfl6lem 42648*	Lemma for lcfl6 42650. A functional 𝐺 (whose kernel is closed by dochsnkr 42622) is completely determined by a vector 𝑋 in the orthocomplement in its kernel at which the functional value is 1. Note that the ∖ { 0 } in the 𝑋 hypothesis is redundant by the last hypothesis but allows easier use of other theorems. (Contributed by NM, 3-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 1 = (1r‘𝑆)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }))    &   ⊢ (𝜑 → (𝐺‘𝑋) = 1 )    ⇒   ⊢ (𝜑 → 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋)))))
Theorem	lcfl7lem 42649*	Lemma for lcfl7N 42651. If two functionals 𝐺 and 𝐽 are equal, they are determined by the same vector. (Contributed by NM, 4-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋))))    &   ⊢ 𝐽 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑌})𝑣 = (𝑤 + (𝑘 · 𝑌))))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐺 = 𝐽)    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	lcfl6 42650*	Property of a functional with a closed kernel. Note that (𝐿‘𝐺) = 𝑉 means the functional is zero by lkr0f 40244. (Contributed by NM, 3-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ ((𝐿‘𝐺) = 𝑉 ∨ ∃𝑥 ∈ (𝑉 ∖ { 0 })𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))))
Theorem	lcfl7N 42651*	Property of a functional with a closed kernel. Every nonzero functional is determined by a unique nonzero vector. Note that (𝐿‘𝐺) = 𝑉 means the functional is zero by lkr0f 40244. (Contributed by NM, 4-Jan-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ ((𝐿‘𝐺) = 𝑉 ∨ ∃!𝑥 ∈ (𝑉 ∖ { 0 })𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))))
Theorem	lcfl8 42652*	Property of a functional with a closed kernel. (Contributed by NM, 17-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝑉 (𝐿‘𝐺) = ( ⊥ ‘{𝑥})))
Theorem	lcfl8a 42653*	Property of a functional with a closed kernel. (Contributed by NM, 17-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ↔ ∃𝑥 ∈ 𝑉 (𝐿‘𝐺) = ( ⊥ ‘{𝑥})))
Theorem	lcfl8b 42654*	Property of a nonzero functional with a closed kernel. (Contributed by NM, 4-Feb-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑌 = (0g‘𝐷)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 ∖ {𝑌}))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ (𝑉 ∖ { 0 })( ⊥ ‘(𝐿‘𝐺)) = (𝑁‘{𝑥}))
Theorem	lcfl9a 42655	Property implying that a functional has a closed kernel. (Contributed by NM, 16-Feb-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ⊆ (𝐿‘𝐺))    ⇒   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺))
Theorem	lclkrlem1 42656*	The set of functionals having closed kernels is closed under scalar product. (Contributed by NM, 28-Dec-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐶)    ⇒   ⊢ (𝜑 → (𝑋 · 𝐺) ∈ 𝐶)
Theorem	lclkrlem2a 42657	Lemma for lclkr 42683. Use lshpat 40206 to show that the intersection of a hyperplane with a noncomparable sum of atoms is an atom. (Contributed by NM, 16-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ≠ ( ⊥ ‘{𝑌}))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ ( ⊥ ‘{𝐵}))    ⇒   ⊢ (𝜑 → (((𝑁‘{𝑋}) ⊕ (𝑁‘{𝑌})) ∩ ( ⊥ ‘{𝐵})) ∈ 𝐴)
Theorem	lclkrlem2b 42658	Lemma for lclkr 42683. (Contributed by NM, 17-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ≠ ( ⊥ ‘{𝑌}))    &   ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵})))    ⇒   ⊢ (𝜑 → (((𝑁‘{𝑋}) ⊕ (𝑁‘{𝑌})) ∩ ( ⊥ ‘{𝐵})) ∈ 𝐴)
Theorem	lclkrlem2c 42659	Lemma for lclkr 42683. (Contributed by NM, 16-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ≠ ( ⊥ ‘{𝑌}))    &   ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵})))    &   ⊢ 𝐽 = (LSHyp‘𝑈)    ⇒   ⊢ (𝜑 → ((( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌})) ⊕ (𝑁‘{𝐵})) ∈ 𝐽)
Theorem	lclkrlem2d 42660	Lemma for lclkr 42683. (Contributed by NM, 16-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ≠ ( ⊥ ‘{𝑌}))    &   ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵})))    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    ⇒   ⊢ (𝜑 → ((( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌})) ⊕ (𝑁‘{𝐵})) ∈ ran 𝐼)
Theorem	lclkrlem2e 42661	Lemma for lclkr 42683. The kernel of the sum is closed when the kernels of the summands are equal and closed. (Contributed by NM, 17-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐸 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))    &   ⊢ (𝜑 → (𝐿‘𝐸) = (𝐿‘𝐺))    ⇒   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺)))
Theorem	lclkrlem2f 42662	Lemma for lclkr 42683. Construct a closed hyperplane under the kernel of the sum. (Contributed by NM, 16-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑄 = (0g‘𝑆)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐽 = (LSHyp‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐸 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))    &   ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌}))    &   ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝐵) = 𝑄)    &   ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵})))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝐿‘𝐸) ≠ (𝐿‘𝐺))    &   ⊢ (𝜑 → (𝐿‘(𝐸 + 𝐺)) ∈ 𝐽)    ⇒   ⊢ (𝜑 → (((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊕ (𝑁‘{𝐵})) ⊆ (𝐿‘(𝐸 + 𝐺)))
Theorem	lclkrlem2g 42663	Lemma for lclkr 42683. Comparable hyperplanes are equal, so the kernel of the sum is closed. (Contributed by NM, 16-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑄 = (0g‘𝑆)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐽 = (LSHyp‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐸 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))    &   ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌}))    &   ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝐵) = 𝑄)    &   ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵})))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝐿‘𝐸) ≠ (𝐿‘𝐺))    &   ⊢ (𝜑 → (𝐿‘(𝐸 + 𝐺)) ∈ 𝐽)    ⇒   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺)))
Theorem	lclkrlem2h 42664	Lemma for lclkr 42683. Eliminate the (𝐿‘(𝐸 + 𝐺)) ∈ 𝐽 hypothesis. (Contributed by NM, 16-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑄 = (0g‘𝑆)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐽 = (LSHyp‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐸 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))    &   ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌}))    &   ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝐵) = 𝑄)    &   ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵})))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝐿‘𝐸) ≠ (𝐿‘𝐺))    ⇒   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺)))
Theorem	lclkrlem2i 42665	Lemma for lclkr 42683. Eliminate the (𝐿‘𝐸) ≠ (𝐿‘𝐺) hypothesis. (Contributed by NM, 17-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑄 = (0g‘𝑆)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐽 = (LSHyp‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐸 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))    &   ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌}))    &   ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝐵) = 𝑄)    &   ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵})))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺)))
Theorem	lclkrlem2j 42666	Lemma for lclkr 42683. Kernel closure when 𝑌 is zero. (Contributed by NM, 18-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑄 = (0g‘𝑆)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐽 = (LSHyp‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐸 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))    &   ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌}))    &   ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝐵) = 𝑄)    &   ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵})))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 = 0 )    ⇒   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺)))
Theorem	lclkrlem2k 42667	Lemma for lclkr 42683. Kernel closure when 𝑋 is zero. (Contributed by NM, 18-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑄 = (0g‘𝑆)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐽 = (LSHyp‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐸 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))    &   ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌}))    &   ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝐵) = 𝑄)    &   ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵})))    &   ⊢ (𝜑 → 𝑋 = 0 )    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺)))
Theorem	lclkrlem2l 42668	Lemma for lclkr 42683. Eliminate the 𝑋 ≠ 0, 𝑌 ≠ 0 hypotheses. (Contributed by NM, 18-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑄 = (0g‘𝑆)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐽 = (LSHyp‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐸 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))    &   ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌}))    &   ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝐵) = 𝑄)    &   ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵})))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺)))
Theorem	lclkrlem2m 42669	Lemma for lclkr 42683. Construct a vector 𝐵 that makes the sum of functionals zero. Combine with 𝐵 ∈ 𝑉 to shorten overall proof. (Contributed by NM, 17-Jan-2015.)
⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ × = (.r‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐼 = (invr‘𝑆)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑈 ∈ LVec)    &   ⊢ 𝐵 = (𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌))    &   ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐵 ∈ 𝑉 ∧ ((𝐸 + 𝐺)‘𝐵) = 0 ))
Theorem	lclkrlem2n 42670	Lemma for lclkr 42683. (Contributed by NM, 12-Jan-2015.)
⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ × = (.r‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐼 = (invr‘𝑆)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ LVec)    &   ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑋) = 0 )    &   ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) = 0 )    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ⊆ (𝐿‘(𝐸 + 𝐺)))
Theorem	lclkrlem2o 42671	Lemma for lclkr 42683. When 𝐵 is nonzero, the vectors 𝑋 and 𝑌 can't both belong to the hyperplane generated by 𝐵. (Contributed by NM, 17-Jan-2015.)
⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ × = (.r‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐼 = (invr‘𝑆)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ 𝐵 = (𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌))    &   ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) ≠ 0 )    &   ⊢ (𝜑 → 𝐵 ≠ (0g‘𝑈))    ⇒   ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵})))
Theorem	lclkrlem2p 42672	Lemma for lclkr 42683. When 𝐵 is zero, 𝑋 and 𝑌 must colinear, so their orthocomplements must be comparable. (Contributed by NM, 17-Jan-2015.)
⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ × = (.r‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐼 = (invr‘𝑆)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ 𝐵 = (𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌))    &   ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) ≠ 0 )    &   ⊢ (𝜑 → 𝐵 = (0g‘𝑈))    ⇒   ⊢ (𝜑 → ( ⊥ ‘{𝑌}) ⊆ ( ⊥ ‘{𝑋}))
Theorem	lclkrlem2q 42673	Lemma for lclkr 42683. The sum has a closed kernel when 𝐵 is nonzero. (Contributed by NM, 18-Jan-2015.)
⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ × = (.r‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐼 = (invr‘𝑆)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))    &   ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌}))    &   ⊢ 𝐵 = (𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌))    &   ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) ≠ 0 )    &   ⊢ (𝜑 → 𝐵 ≠ (0g‘𝑈))    ⇒   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺)))
Theorem	lclkrlem2r 42674	Lemma for lclkr 42683. When 𝐵 is zero, i.e. when 𝑋 and 𝑌 are colinear, the intersection of the kernels of 𝐸 and 𝐺 equal the kernel of 𝐺, so the kernels of 𝐺 and the sum are comparable. (Contributed by NM, 18-Jan-2015.)
⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ × = (.r‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐼 = (invr‘𝑆)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))    &   ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌}))    &   ⊢ 𝐵 = (𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌))    &   ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) ≠ 0 )    &   ⊢ (𝜑 → 𝐵 = (0g‘𝑈))    ⇒   ⊢ (𝜑 → (𝐿‘𝐺) ⊆ (𝐿‘(𝐸 + 𝐺)))
Theorem	lclkrlem2s 42675	Lemma for lclkr 42683. Thus, the sum has a closed kernel when 𝐵 is zero. (Contributed by NM, 18-Jan-2015.)
⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ × = (.r‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐼 = (invr‘𝑆)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))    &   ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌}))    &   ⊢ 𝐵 = (𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌))    &   ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) ≠ 0 )    &   ⊢ (𝜑 → 𝐵 = (0g‘𝑈))    ⇒   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺)))
Theorem	lclkrlem2t 42676	Lemma for lclkr 42683. We eliminate all hypotheses with 𝐵 here. (Contributed by NM, 18-Jan-2015.)
⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ × = (.r‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐼 = (invr‘𝑆)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))    &   ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌}))    &   ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) ≠ 0 )    ⇒   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺)))
Theorem	lclkrlem2u 42677	Lemma for lclkr 42683. lclkrlem2t 42676 with 𝑋 and 𝑌 swapped. (Contributed by NM, 18-Jan-2015.)
⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ × = (.r‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐼 = (invr‘𝑆)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))    &   ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌}))    &   ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑋) ≠ 0 )    ⇒   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺)))
Theorem	lclkrlem2v 42678	Lemma for lclkr 42683. When the hypotheses of lclkrlem2u 42677 and lclkrlem2u 42677 are negated, the functional sum must be zero, so the kernel is the vector space. We make use of the law of excluded middle, dochexmid 42618, which requires the orthomodular law dihoml4 42527 (Lemma 3.3 of [Holland95] p. 214). (Contributed by NM, 16-Jan-2015.)
⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ × = (.r‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐼 = (invr‘𝑆)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))    &   ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌}))    &   ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑋) = 0 )    &   ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) = 0 )    ⇒   ⊢ (𝜑 → (𝐿‘(𝐸 + 𝐺)) = 𝑉)
Theorem	lclkrlem2w 42679	Lemma for lclkr 42683. This is the same as lclkrlem2u 42677 and lclkrlem2u 42677 with the inequality hypotheses negated. When the sum of two functionals is zero at each generating vector, the kernel is the vector space and therefore closed. (Contributed by NM, 16-Jan-2015.)
⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ × = (.r‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐼 = (invr‘𝑆)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))    &   ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌}))    &   ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑋) = 0 )    &   ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) = 0 )    ⇒   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺)))
Theorem	lclkrlem2x 42680	Lemma for lclkr 42683. Eliminate by cases the hypotheses of lclkrlem2u 42677, lclkrlem2u 42677 and lclkrlem2w 42679. (Contributed by NM, 18-Jan-2015.)
⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))    &   ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌}))    ⇒   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺)))
Theorem	lclkrlem2y 42681	Lemma for lclkr 42683. Restate the hypotheses for 𝐸 and 𝐺 to say their kernels are closed, in order to eliminate the generating vectors 𝑋 and 𝑌. (Contributed by NM, 18-Jan-2015.)
⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐸 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐸))) = (𝐿‘𝐸))    &   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺))    ⇒   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺)))
Theorem	lclkrlem2 42682*	The set of functionals having closed kernels is closed under vector (functional) addition. Lemmas lclkrlem2a 42657 through lclkrlem2y 42681 are used for the proof. Here we express lclkrlem2y 42681 in terms of membership in the set 𝐶 of functionals with closed kernels. (Contributed by NM, 18-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ + = (+g‘𝐷)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐸 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐶)    ⇒   ⊢ (𝜑 → (𝐸 + 𝐺) ∈ 𝐶)
Theorem	lclkr 42683*	The set of functionals with closed kernels is a subspace. Part of proof of Theorem 3.6 of [Holland95] p. 218, line 20, stating "The fM that arise this way generate a subspace F of E'". Our proof was suggested by Mario Carneiro, 5-Jan-2015. (Contributed by NM, 18-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝐷)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → 𝐶 ∈ 𝑆)
Theorem	lcfls1lem 42684*	Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015.)
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑄)}    ⇒   ⊢ (𝐺 ∈ 𝐶 ↔ (𝐺 ∈ 𝐹 ∧ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ∧ ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑄))
Theorem	lcfls1N 42685*	Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015.) (New usage is discouraged.)
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑄)}    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ∧ ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑄)))
Theorem	lcfls1c 42686*	Property of a functional with a closed kernel. (Contributed by NM, 28-Jan-2015.)
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑄)}    &   ⊢ 𝐷 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    ⇒   ⊢ (𝐺 ∈ 𝐶 ↔ (𝐺 ∈ 𝐷 ∧ ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑄))
Theorem	lclkrslem1 42687*	The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace 𝑄 is closed under scalar product. (Contributed by NM, 27-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑄)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑄 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · 𝐺) ∈ 𝐶)
Theorem	lclkrslem2 42688*	The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace 𝑄 is closed under scalar product. (Contributed by NM, 28-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑄)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑄 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐶)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐶)    ⇒   ⊢ (𝜑 → (𝐸 + 𝐺) ∈ 𝐶)
Theorem	lclkrs 42689*	The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace 𝑅 is a subspace of the dual space. TODO: This proof repeats large parts of the lclkr 42683 proof. Do we achieve overall shortening by breaking them out as subtheorems? Or make lclkr 42683 a special case of this? (Contributed by NM, 29-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑇 = (LSubSp‘𝐷)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑅)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝐶 ∈ 𝑇)
Theorem	lclkrs2 42690*	The set of functionals with closed kernels and majorizing the orthocomplement of a given subspace 𝑄 is a subspace of the dual space containing functionals with closed kernels. Note that 𝑅 is the value given by mapdval 42778. (Contributed by NM, 12-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑇 = (LSubSp‘𝐷)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ 𝑅 = {𝑔 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑔))) = (𝐿‘𝑔) ∧ ( ⊥ ‘(𝐿‘𝑔)) ⊆ 𝑄)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑄 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑅 ∈ 𝑇 ∧ 𝑅 ⊆ 𝐶))
Theorem	lcfrvalsnN 42691*	Reconstruction from the dual space span of a singleton. (Contributed by NM, 19-Feb-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝐷)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ 𝑄 = ∪ 𝑓 ∈ 𝑅 ( ⊥ ‘(𝐿‘𝑓))    &   ⊢ 𝑅 = (𝑁‘{𝐺})    ⇒   ⊢ (𝜑 → 𝑄 = ( ⊥ ‘(𝐿‘𝐺)))
Theorem	lcfrlem1 42692	Lemma for lcfr 42735. Note that 𝑋 is z in Mario's notes. (Contributed by NM, 27-Feb-2015.)
⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ × = (.r‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐼 = (invr‘𝑆)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ − = (-g‘𝐷)    &   ⊢ (𝜑 → 𝑈 ∈ LVec)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝐺‘𝑋) ≠ 0 )    &   ⊢ 𝐻 = (𝐸 − (((𝐼‘(𝐺‘𝑋)) × (𝐸‘𝑋)) · 𝐺))    ⇒   ⊢ (𝜑 → (𝐻‘𝑋) = 0 )
Theorem	lcfrlem2 42693	Lemma for lcfr 42735. (Contributed by NM, 27-Feb-2015.)
⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ × = (.r‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐼 = (invr‘𝑆)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ − = (-g‘𝐷)    &   ⊢ (𝜑 → 𝑈 ∈ LVec)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝐺‘𝑋) ≠ 0 )    &   ⊢ 𝐻 = (𝐸 − (((𝐼‘(𝐺‘𝑋)) × (𝐸‘𝑋)) · 𝐺))    &   ⊢ 𝐿 = (LKer‘𝑈)    ⇒   ⊢ (𝜑 → ((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊆ (𝐿‘𝐻))
Theorem	lcfrlem3 42694	Lemma for lcfr 42735. (Contributed by NM, 27-Feb-2015.)
⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ × = (.r‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐼 = (invr‘𝑆)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ − = (-g‘𝐷)    &   ⊢ (𝜑 → 𝑈 ∈ LVec)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝐺‘𝑋) ≠ 0 )    &   ⊢ 𝐻 = (𝐸 − (((𝐼‘(𝐺‘𝑋)) × (𝐸‘𝑋)) · 𝐺))    &   ⊢ 𝐿 = (LKer‘𝑈)    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐿‘𝐻))
Theorem	lcfrlem4 42695*	Lemma for lcfr 42735. (Contributed by NM, 10-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑄 = (LSubSp‘𝐷)    &   ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔))    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝑄)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐸)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝑉)
Theorem	lcfrlem5 42696*	Lemma for lcfr 42735. The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace 𝑄 is closed under scalar product. TODO: share hypotheses with others. Use more consistent variable names here or elsewhere when possible. (Contributed by NM, 5-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝐷)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑆)    &   ⊢ 𝑄 = ∪ 𝑓 ∈ 𝑅 ( ⊥ ‘(𝐿‘𝑓))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑄)    &   ⊢ 𝐶 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 · 𝑋) ∈ 𝑄)
Theorem	lcfrlem6 42697*	Lemma for lcfr 42735. Closure of vector sum with colinear vectors. TODO: Move down 𝑁 definition so top hypotheses can be shared. (Contributed by NM, 10-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑄 = (LSubSp‘𝐷)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝑄)    &   ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐸)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐸)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐸)
Theorem	lcfrlem7 42698*	Lemma for lcfr 42735. Closure of vector sum when one vector is zero. TODO: share hypotheses with others. (Contributed by NM, 11-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑄 = (LSubSp‘𝐷)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝑄)    &   ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐸)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ (𝜑 → 𝑌 = 0 )    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐸)
Theorem	lcfrlem8 42699*	Lemma for lcf1o 42701 and lcfr 42735. (Contributed by NM, 21-Feb-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑄 = (0g‘𝐷)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝐽‘𝑋) = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋)))))
Theorem	lcfrlem9 42700*	Lemma for lcf1o 42701. (This part has undesirable $d's on 𝐽 and 𝜑 that we remove in lcf1o 42701.) TODO: ugly proof; maybe have better subtheorems or abbreviate some ℩𝑘 expansions with 𝐽‘𝑧? TODO: Some redundant $d's? (Contributed by NM, 22-Feb-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑄 = (0g‘𝐷)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → 𝐽:(𝑉 ∖ { 0 })–1-1-onto→(𝐶 ∖ {𝑄}))