P. 396 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39501-39600   *Has distinct variable group(s)

Type	Label	Description
Statement
20.24.14  Construction of involution and inner product from a Hilbert lattice
Syntax	clpoN 39501	Extend class notation with all polarities of a left module or left vector space.
class LPol
Definition	df-lpolN 39502*	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 39503*	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 39504*	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 39505*	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 39506	Functionality of a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑃 = (LPol‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → ⊥ ∈ 𝑃)    ⇒   ⊢ (𝜑 → ⊥ :𝒫 𝑉⟶𝑆)
Theorem	lpolvN 39507	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 39508	Contraposition property of a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑃 = (LPol‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → ⊥ ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑌)    ⇒   ⊢ (𝜑 → ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋))
Theorem	lpolsatN 39509	The polarity of an atomic subspace is a hyperplane. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.)
⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝑃 = (LPol‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → ⊥ ∈ 𝑃)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ( ⊥ ‘𝑄) ∈ 𝐻)
Theorem	lpolpolsatN 39510	Property of a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.)
⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ 𝑃 = (LPol‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → ⊥ ∈ 𝑃)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑄)) = 𝑄)
Theorem	dochpolN 39511	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 39512*	Property of a functional with a closed kernel. (Contributed by NM, 28-Dec-2014.)
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    ⇒   ⊢ (𝐺 ∈ 𝐶 ↔ (𝐺 ∈ 𝐹 ∧ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺)))
Theorem	lcfl1 39513*	Property of a functional with a closed kernel. (Contributed by NM, 31-Dec-2014.)
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺)))
Theorem	lcfl2 39514*	Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉 ∨ (𝐿‘𝐺) = 𝑉)))
Theorem	lcfl3 39515*	Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ (( ⊥ ‘(𝐿‘𝐺)) ∈ 𝐴 ∨ (𝐿‘𝐺) = 𝑉)))
Theorem	lcfl4N 39516*	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 39517*	Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ (𝐿‘𝐺) ∈ ran 𝐼))
Theorem	lcfl5a 39518	Property of a functional with a closed kernel. TODO: Make lcfl5 39517 etc. obsolete and rewrite without 𝐶 hypothesis? (Contributed by NM, 29-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ↔ (𝐿‘𝐺) ∈ ran 𝐼))
Theorem	lcfl6lem 39519*	Lemma for lcfl6 39521. A functional 𝐺 (whose kernel is closed by dochsnkr 39493) is comletely 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 39520*	Lemma for lcfl7N 39522. 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 39521*	Property of a functional with a closed kernel. Note that (𝐿‘𝐺) = 𝑉 means the functional is zero by lkr0f 37115. (Contributed by NM, 3-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ ((𝐿‘𝐺) = 𝑉 ∨ ∃𝑥 ∈ (𝑉 ∖ { 0 })𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))))
Theorem	lcfl7N 39522*	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 37115. (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 39523*	Property of a functional with a closed kernel. (Contributed by NM, 17-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝑉 (𝐿‘𝐺) = ( ⊥ ‘{𝑥})))
Theorem	lcfl8a 39524*	Property of a functional with a closed kernel. (Contributed by NM, 17-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ↔ ∃𝑥 ∈ 𝑉 (𝐿‘𝐺) = ( ⊥ ‘{𝑥})))
Theorem	lcfl8b 39525*	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 39526	Property implying that a functional has a closed kernel. (Contributed by NM, 16-Feb-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ⊆ (𝐿‘𝐺))    ⇒   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺))
Theorem	lclkrlem1 39527*	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 39528	Lemma for lclkr 39554. Use lshpat 37077 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 39529	Lemma for lclkr 39554. (Contributed by NM, 17-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ≠ ( ⊥ ‘{𝑌}))    &   ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵})))    ⇒   ⊢ (𝜑 → (((𝑁‘{𝑋}) ⊕ (𝑁‘{𝑌})) ∩ ( ⊥ ‘{𝐵})) ∈ 𝐴)
Theorem	lclkrlem2c 39530	Lemma for lclkr 39554. (Contributed by NM, 16-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ≠ ( ⊥ ‘{𝑌}))    &   ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵})))    &   ⊢ 𝐽 = (LSHyp‘𝑈)    ⇒   ⊢ (𝜑 → ((( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌})) ⊕ (𝑁‘{𝐵})) ∈ 𝐽)
Theorem	lclkrlem2d 39531	Lemma for lclkr 39554. (Contributed by NM, 16-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ≠ ( ⊥ ‘{𝑌}))    &   ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵})))    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    ⇒   ⊢ (𝜑 → ((( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌})) ⊕ (𝑁‘{𝐵})) ∈ ran 𝐼)
Theorem	lclkrlem2e 39532	Lemma for lclkr 39554. 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 39533	Lemma for lclkr 39554. 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 39534	Lemma for lclkr 39554. 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 39535	Lemma for lclkr 39554. 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 39536	Lemma for lclkr 39554. 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 39537	Lemma for lclkr 39554. 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 39538	Lemma for lclkr 39554. 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 39539	Lemma for lclkr 39554. 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 39540	Lemma for lclkr 39554. 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 39541	Lemma for lclkr 39554. (Contributed by NM, 12-Jan-2015.)
⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ × = (.r‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐼 = (invr‘𝑆)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ LVec)    &   ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑋) = 0 )    &   ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) = 0 )    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ⊆ (𝐿‘(𝐸 + 𝐺)))
Theorem	lclkrlem2o 39542	Lemma for lclkr 39554. 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 39543	Lemma for lclkr 39554. 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 39544	Lemma for lclkr 39554. 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 39545	Lemma for lclkr 39554. 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 39546	Lemma for lclkr 39554. 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 39547	Lemma for lclkr 39554. 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 39548	Lemma for lclkr 39554. lclkrlem2t 39547 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 39549	Lemma for lclkr 39554. When the hypotheses of lclkrlem2u 39548 and lclkrlem2u 39548 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 39489, which requires the orthomodular law dihoml4 39398 (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 39550	Lemma for lclkr 39554. This is the same as lclkrlem2u 39548 and lclkrlem2u 39548 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 39551	Lemma for lclkr 39554. Eliminate by cases the hypotheses of lclkrlem2u 39548, lclkrlem2u 39548 and lclkrlem2w 39550. (Contributed by NM, 18-Jan-2015.)
⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))    &   ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌}))    ⇒   ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺)))
Theorem	lclkrlem2y 39552	Lemma for lclkr 39554. 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 39553*	The set of functionals having closed kernels is closed under vector (functional) addition. Lemmas lclkrlem2a 39528 through lclkrlem2y 39552 are used for the proof. Here we express lclkrlem2y 39552 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 39554*	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 39555*	Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015.)
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑄)}    ⇒   ⊢ (𝐺 ∈ 𝐶 ↔ (𝐺 ∈ 𝐹 ∧ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ∧ ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑄))
Theorem	lcfls1N 39556*	Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015.) (New usage is discouraged.)
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑄)}    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ∧ ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑄)))
Theorem	lcfls1c 39557*	Property of a functional with a closed kernel. (Contributed by NM, 28-Jan-2015.)
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑄)}    &   ⊢ 𝐷 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    ⇒   ⊢ (𝐺 ∈ 𝐶 ↔ (𝐺 ∈ 𝐷 ∧ ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑄))
Theorem	lclkrslem1 39558*	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 39559*	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 39560*	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 39554 proof. Do we achieve overall shortening by breaking them out as subtheorems? Or make lclkr 39554 a special case of this? (Contributed by NM, 29-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑇 = (LSubSp‘𝐷)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑅)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝐶 ∈ 𝑇)
Theorem	lclkrs2 39561*	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 39649. (Contributed by NM, 12-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑇 = (LSubSp‘𝐷)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ 𝑅 = {𝑔 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑔))) = (𝐿‘𝑔) ∧ ( ⊥ ‘(𝐿‘𝑔)) ⊆ 𝑄)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑄 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑅 ∈ 𝑇 ∧ 𝑅 ⊆ 𝐶))
Theorem	lcfrvalsnN 39562*	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 39563	Lemma for lcfr 39606. 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 39564	Lemma for lcfr 39606. (Contributed by NM, 27-Feb-2015.)
⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ × = (.r‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐼 = (invr‘𝑆)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ − = (-g‘𝐷)    &   ⊢ (𝜑 → 𝑈 ∈ LVec)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝐺‘𝑋) ≠ 0 )    &   ⊢ 𝐻 = (𝐸 − (((𝐼‘(𝐺‘𝑋)) × (𝐸‘𝑋)) · 𝐺))    &   ⊢ 𝐿 = (LKer‘𝑈)    ⇒   ⊢ (𝜑 → ((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊆ (𝐿‘𝐻))
Theorem	lcfrlem3 39565	Lemma for lcfr 39606. (Contributed by NM, 27-Feb-2015.)
⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ × = (.r‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐼 = (invr‘𝑆)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ − = (-g‘𝐷)    &   ⊢ (𝜑 → 𝑈 ∈ LVec)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝐺‘𝑋) ≠ 0 )    &   ⊢ 𝐻 = (𝐸 − (((𝐼‘(𝐺‘𝑋)) × (𝐸‘𝑋)) · 𝐺))    &   ⊢ 𝐿 = (LKer‘𝑈)    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐿‘𝐻))
Theorem	lcfrlem4 39566*	Lemma for lcfr 39606. (Contributed by NM, 10-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑄 = (LSubSp‘𝐷)    &   ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔))    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝑄)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐸)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝑉)
Theorem	lcfrlem5 39567*	Lemma for lcfr 39606. 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 39568*	Lemma for lcfr 39606. 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 39569*	Lemma for lcfr 39606. 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 39570*	Lemma for lcf1o 39572 and lcfr 39606. (Contributed by NM, 21-Feb-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑄 = (0g‘𝐷)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝐽‘𝑋) = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋)))))
Theorem	lcfrlem9 39571*	Lemma for lcf1o 39572. (This part has undesirable $d's on 𝐽 and 𝜑 that we remove in lcf1o 39572.) 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→(𝐶 ∖ {𝑄}))
Theorem	lcf1o 39572*	Define a function 𝐽 that provides a bijection from nonzero vectors 𝑉 to nonzero functionals with closed kernels 𝐶. (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→(𝐶 ∖ {𝑄}))
Theorem	lcfrlem10 39573*	Lemma for lcfr 39606. (Contributed by NM, 23-Feb-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑄 = (0g‘𝐷)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝐽‘𝑋) ∈ 𝐹)
Theorem	lcfrlem11 39574*	Lemma for lcfr 39606. (Contributed by NM, 23-Feb-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑄 = (0g‘𝐷)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝐿‘(𝐽‘𝑋)) = ( ⊥ ‘{𝑋}))
Theorem	lcfrlem12N 39575*	Lemma for lcfr 39606. (Contributed by NM, 23-Feb-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑄 = (0g‘𝐷)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ 𝐵 = (0g‘𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ ( ⊥ ‘{𝑋}))    ⇒   ⊢ (𝜑 → ((𝐽‘𝑋)‘𝑌) = 𝐵)
Theorem	lcfrlem13 39576*	Lemma for lcfr 39606. (Contributed by NM, 8-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑄 = (0g‘𝐷)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝐽‘𝑋) ∈ (𝐶 ∖ {𝑄}))
Theorem	lcfrlem14 39577*	Lemma for lcfr 39606. (Contributed by NM, 10-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑄 = (0g‘𝐷)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ 𝑁 = (LSpan‘𝑈)    ⇒   ⊢ (𝜑 → ( ⊥ ‘(𝐿‘(𝐽‘𝑋))) = (𝑁‘{𝑋}))
Theorem	lcfrlem15 39578*	Lemma for lcfr 39606. (Contributed by NM, 9-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑄 = (0g‘𝐷)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → 𝑋 ∈ ( ⊥ ‘(𝐿‘(𝐽‘𝑋))))
Theorem	lcfrlem16 39579*	Lemma for lcfr 39606. (Contributed by NM, 8-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑄 = (0g‘𝐷)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ 𝑃 = (LSubSp‘𝐷)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ⊆ 𝐶)    &   ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐸 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝐽‘𝑋) ∈ 𝐺)
Theorem	lcfrlem17 39580	Lemma for lcfr 39606. Condition needed more than once. (Contributed by NM, 11-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝑉 ∖ { 0 }))
Theorem	lcfrlem18 39581	Lemma for lcfr 39606. (Contributed by NM, 24-Feb-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → ( ⊥ ‘{𝑋, 𝑌}) = (( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌})))
Theorem	lcfrlem19 39582	Lemma for lcfr 39606. (Contributed by NM, 11-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{(𝑋 + 𝑌)}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{(𝑋 + 𝑌)})))
Theorem	lcfrlem20 39583	Lemma for lcfr 39606. (Contributed by NM, 11-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ ( ⊥ ‘{(𝑋 + 𝑌)}))    ⇒   ⊢ (𝜑 → ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∈ 𝐴)
Theorem	lcfrlem21 39584	Lemma for lcfr 39606. (Contributed by NM, 11-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∈ 𝐴)
Theorem	lcfrlem22 39585	Lemma for lcfr 39606. (Contributed by NM, 24-Feb-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)}))    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝐴)
Theorem	lcfrlem23 39586	Lemma for lcfr 39606. TODO: this proof was built from other proof pieces that may change 𝑁‘{𝑋, 𝑌} into subspace sum and back unnecessarily, or similar things. (Contributed by NM, 1-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)}))    &   ⊢ ⊕ = (LSSum‘𝑈)    ⇒   ⊢ (𝜑 → (( ⊥ ‘{𝑋, 𝑌}) ⊕ 𝐵) = ( ⊥ ‘{(𝑋 + 𝑌)}))
Theorem	lcfrlem24 39587*	Lemma for lcfr 39606. (Contributed by NM, 24-Feb-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)}))    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑄 = (0g‘𝑆)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    &   ⊢ 𝐿 = (LKer‘𝑈)    ⇒   ⊢ (𝜑 → ( ⊥ ‘{𝑋, 𝑌}) = ((𝐿‘(𝐽‘𝑋)) ∩ (𝐿‘(𝐽‘𝑌))))
Theorem	lcfrlem25 39588*	Lemma for lcfr 39606. Special case of lcfrlem35 39598 when ((𝐽‘𝑌)‘𝐼) is zero. (Contributed by NM, 11-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)}))    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑄 = (0g‘𝑆)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) = 𝑄)    &   ⊢ (𝜑 → 𝐼 ≠ 0 )    ⇒   ⊢ (𝜑 → ( ⊥ ‘{(𝑋 + 𝑌)}) = (𝐿‘(𝐽‘𝑌)))
Theorem	lcfrlem26 39589*	Lemma for lcfr 39606. Special case of lcfrlem36 39599 when ((𝐽‘𝑌)‘𝐼) is zero. (Contributed by NM, 11-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)}))    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑄 = (0g‘𝑆)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) = 𝑄)    &   ⊢ (𝜑 → 𝐼 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ ( ⊥ ‘(𝐿‘(𝐽‘𝑌))))
Theorem	lcfrlem27 39590*	Lemma for lcfr 39606. Special case of lcfrlem37 39600 when ((𝐽‘𝑌)‘𝐼) is zero. (Contributed by NM, 11-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)}))    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑄 = (0g‘𝑆)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) = 𝑄)    &   ⊢ (𝜑 → 𝐼 ≠ 0 )    &   ⊢ (𝜑 → 𝐺 ∈ (LSubSp‘𝐷))    &   ⊢ (𝜑 → 𝐺 ⊆ {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)})    &   ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐸)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐸)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐸)
Theorem	lcfrlem28 39591*	Lemma for lcfr 39606. TODO: This can be a hypothesis since the zero version of (𝐽‘𝑌)‘𝐼 needs it. (Contributed by NM, 9-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)}))    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑄 = (0g‘𝑆)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄)    ⇒   ⊢ (𝜑 → 𝐼 ≠ 0 )
Theorem	lcfrlem29 39592*	Lemma for lcfr 39606. (Contributed by NM, 9-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)}))    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑄 = (0g‘𝑆)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄)    &   ⊢ 𝐹 = (invr‘𝑆)    ⇒   ⊢ (𝜑 → ((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼)) ∈ 𝑅)
Theorem	lcfrlem30 39593*	Lemma for lcfr 39606. (Contributed by NM, 6-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)}))    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑄 = (0g‘𝑆)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄)    &   ⊢ 𝐹 = (invr‘𝑆)    &   ⊢ − = (-g‘𝐷)    &   ⊢ 𝐶 = ((𝐽‘𝑋) − (((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠 ‘𝐷)(𝐽‘𝑌)))    ⇒   ⊢ (𝜑 → 𝐶 ∈ (LFnl‘𝑈))
Theorem	lcfrlem31 39594*	Lemma for lcfr 39606. (Contributed by NM, 10-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)}))    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑄 = (0g‘𝑆)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄)    &   ⊢ 𝐹 = (invr‘𝑆)    &   ⊢ − = (-g‘𝐷)    &   ⊢ 𝐶 = ((𝐽‘𝑋) − (((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠 ‘𝐷)(𝐽‘𝑌)))    &   ⊢ (𝜑 → ((𝐽‘𝑋)‘𝐼) ≠ 𝑄)    &   ⊢ (𝜑 → 𝐶 = (0g‘𝐷))    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{𝑌}))
Theorem	lcfrlem32 39595*	Lemma for lcfr 39606. (Contributed by NM, 10-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)}))    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑄 = (0g‘𝑆)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄)    &   ⊢ 𝐹 = (invr‘𝑆)    &   ⊢ − = (-g‘𝐷)    &   ⊢ 𝐶 = ((𝐽‘𝑋) − (((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠 ‘𝐷)(𝐽‘𝑌)))    &   ⊢ (𝜑 → ((𝐽‘𝑋)‘𝐼) ≠ 𝑄)    ⇒   ⊢ (𝜑 → 𝐶 ≠ (0g‘𝐷))
Theorem	lcfrlem33 39596*	Lemma for lcfr 39606. (Contributed by NM, 10-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)}))    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑄 = (0g‘𝑆)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄)    &   ⊢ 𝐹 = (invr‘𝑆)    &   ⊢ − = (-g‘𝐷)    &   ⊢ 𝐶 = ((𝐽‘𝑋) − (((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠 ‘𝐷)(𝐽‘𝑌)))    &   ⊢ (𝜑 → ((𝐽‘𝑋)‘𝐼) = 𝑄)    ⇒   ⊢ (𝜑 → 𝐶 ≠ (0g‘𝐷))
Theorem	lcfrlem34 39597*	Lemma for lcfr 39606. (Contributed by NM, 10-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)}))    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑄 = (0g‘𝑆)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄)    &   ⊢ 𝐹 = (invr‘𝑆)    &   ⊢ − = (-g‘𝐷)    &   ⊢ 𝐶 = ((𝐽‘𝑋) − (((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠 ‘𝐷)(𝐽‘𝑌)))    ⇒   ⊢ (𝜑 → 𝐶 ≠ (0g‘𝐷))
Theorem	lcfrlem35 39598*	Lemma for lcfr 39606. (Contributed by NM, 2-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)}))    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑄 = (0g‘𝑆)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄)    &   ⊢ 𝐹 = (invr‘𝑆)    &   ⊢ − = (-g‘𝐷)    &   ⊢ 𝐶 = ((𝐽‘𝑋) − (((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠 ‘𝐷)(𝐽‘𝑌)))    ⇒   ⊢ (𝜑 → ( ⊥ ‘{(𝑋 + 𝑌)}) = (𝐿‘𝐶))
Theorem	lcfrlem36 39599*	Lemma for lcfr 39606. (Contributed by NM, 6-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)}))    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑄 = (0g‘𝑆)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄)    &   ⊢ 𝐹 = (invr‘𝑆)    &   ⊢ − = (-g‘𝐷)    &   ⊢ 𝐶 = ((𝐽‘𝑋) − (((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠 ‘𝐷)(𝐽‘𝑌)))    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ ( ⊥ ‘(𝐿‘𝐶)))
Theorem	lcfrlem37 39600*	Lemma for lcfr 39606. (Contributed by NM, 8-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)}))    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑄 = (0g‘𝑆)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄)    &   ⊢ 𝐹 = (invr‘𝑆)    &   ⊢ − = (-g‘𝐷)    &   ⊢ 𝐶 = ((𝐽‘𝑋) − (((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠 ‘𝐷)(𝐽‘𝑌)))    &   ⊢ (𝜑 → 𝐺 ∈ (LSubSp‘𝐷))    &   ⊢ (𝜑 → 𝐺 ⊆ {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)})    &   ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐸)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐸)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐸)