![]() |
Metamath
Proof Explorer Theorem List (p. 412 of 485) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30805) |
![]() (30806-32328) |
![]() (32329-48426) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lcfl5 41101* | Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ (𝐿‘𝐺) ∈ ran 𝐼)) | ||
Theorem | lcfl5a 41102 | Property of a functional with a closed kernel. TODO: Make lcfl5 41101 etc. obsolete and rewrite without 𝐶 hypothesis? (Contributed by NM, 29-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ↔ (𝐿‘𝐺) ∈ ran 𝐼)) | ||
Theorem | lcfl6lem 41103* | Lemma for lcfl6 41105. A functional 𝐺 (whose kernel is closed by dochsnkr 41077) 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 41104* | Lemma for lcfl7N 41106. 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 41105* | Property of a functional with a closed kernel. Note that (𝐿‘𝐺) = 𝑉 means the functional is zero by lkr0f 38698. (Contributed by NM, 3-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ ((𝐿‘𝐺) = 𝑉 ∨ ∃𝑥 ∈ (𝑉 ∖ { 0 })𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))))) | ||
Theorem | lcfl7N 41106* | 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 38698. (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 41107* | Property of a functional with a closed kernel. (Contributed by NM, 17-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝑉 (𝐿‘𝐺) = ( ⊥ ‘{𝑥}))) | ||
Theorem | lcfl8a 41108* | Property of a functional with a closed kernel. (Contributed by NM, 17-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ↔ ∃𝑥 ∈ 𝑉 (𝐿‘𝐺) = ( ⊥ ‘{𝑥}))) | ||
Theorem | lcfl8b 41109* | 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 41110 | Property implying that a functional has a closed kernel. (Contributed by NM, 16-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ⊆ (𝐿‘𝐺)) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺)) | ||
Theorem | lclkrlem1 41111* | 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 41112 | Lemma for lclkr 41138. Use lshpat 38660 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 41113 | Lemma for lclkr 41138. (Contributed by NM, 17-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ≠ ( ⊥ ‘{𝑌})) & ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵}))) ⇒ ⊢ (𝜑 → (((𝑁‘{𝑋}) ⊕ (𝑁‘{𝑌})) ∩ ( ⊥ ‘{𝐵})) ∈ 𝐴) | ||
Theorem | lclkrlem2c 41114 | Lemma for lclkr 41138. (Contributed by NM, 16-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ≠ ( ⊥ ‘{𝑌})) & ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵}))) & ⊢ 𝐽 = (LSHyp‘𝑈) ⇒ ⊢ (𝜑 → ((( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌})) ⊕ (𝑁‘{𝐵})) ∈ 𝐽) | ||
Theorem | lclkrlem2d 41115 | Lemma for lclkr 41138. (Contributed by NM, 16-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ≠ ( ⊥ ‘{𝑌})) & ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵}))) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) ⇒ ⊢ (𝜑 → ((( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌})) ⊕ (𝑁‘{𝐵})) ∈ ran 𝐼) | ||
Theorem | lclkrlem2e 41116 | Lemma for lclkr 41138. 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 41117 | Lemma for lclkr 41138. 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 41118 | Lemma for lclkr 41138. 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 41119 | Lemma for lclkr 41138. 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 41120 | Lemma for lclkr 41138. 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 41121 | Lemma for lclkr 41138. 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 41122 | Lemma for lclkr 41138. 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 41123 | Lemma for lclkr 41138. 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 41124 | Lemma for lclkr 41138. 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 41125 | Lemma for lclkr 41138. (Contributed by NM, 12-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ × = (.r‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐼 = (invr‘𝑆) & ⊢ − = (-g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ LVec) & ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑋) = 0 ) & ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) = 0 ) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ⊆ (𝐿‘(𝐸 + 𝐺))) | ||
Theorem | lclkrlem2o 41126 | Lemma for lclkr 41138. 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 41127 | Lemma for lclkr 41138. 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 41128 | Lemma for lclkr 41138. 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 41129 | Lemma for lclkr 41138. 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 41130 | Lemma for lclkr 41138. 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 41131 | Lemma for lclkr 41138. 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 41132 | Lemma for lclkr 41138. lclkrlem2t 41131 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 41133 | Lemma for lclkr 41138. When the hypotheses of lclkrlem2u 41132 and lclkrlem2u 41132 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 41073, which requires the orthomodular law dihoml4 40982 (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 41134 | Lemma for lclkr 41138. This is the same as lclkrlem2u 41132 and lclkrlem2u 41132 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 41135 | Lemma for lclkr 41138. Eliminate by cases the hypotheses of lclkrlem2u 41132, lclkrlem2u 41132 and lclkrlem2w 41134. (Contributed by NM, 18-Jan-2015.) |
⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋})) & ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌})) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺))) | ||
Theorem | lclkrlem2y 41136 | Lemma for lclkr 41138. 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 41137* | The set of functionals having closed kernels is closed under vector (functional) addition. Lemmas lclkrlem2a 41112 through lclkrlem2y 41136 are used for the proof. Here we express lclkrlem2y 41136 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 41138* | 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 41139* | Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015.) |
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑄)} ⇒ ⊢ (𝐺 ∈ 𝐶 ↔ (𝐺 ∈ 𝐹 ∧ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ∧ ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑄)) | ||
Theorem | lcfls1N 41140* | Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015.) (New usage is discouraged.) |
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑄)} & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ∧ ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑄))) | ||
Theorem | lcfls1c 41141* | Property of a functional with a closed kernel. (Contributed by NM, 28-Jan-2015.) |
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑄)} & ⊢ 𝐷 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} ⇒ ⊢ (𝐺 ∈ 𝐶 ↔ (𝐺 ∈ 𝐷 ∧ ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑄)) | ||
Theorem | lclkrslem1 41142* | 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 41143* | 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 41144* | 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 41138 proof. Do we achieve overall shortening by breaking them out as subtheorems? Or make lclkr 41138 a special case of this? (Contributed by NM, 29-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑇 = (LSubSp‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑅)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑅 ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝑇) | ||
Theorem | lclkrs2 41145* | 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 41233. (Contributed by NM, 12-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑇 = (LSubSp‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝑅 = {𝑔 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑔))) = (𝐿‘𝑔) ∧ ( ⊥ ‘(𝐿‘𝑔)) ⊆ 𝑄)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑄 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑅 ∈ 𝑇 ∧ 𝑅 ⊆ 𝐶)) | ||
Theorem | lcfrvalsnN 41146* | 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 41147 | Lemma for lcfr 41190. 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 41148 | Lemma for lcfr 41190. (Contributed by NM, 27-Feb-2015.) |
⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ × = (.r‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐼 = (invr‘𝑆) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ − = (-g‘𝐷) & ⊢ (𝜑 → 𝑈 ∈ LVec) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → (𝐺‘𝑋) ≠ 0 ) & ⊢ 𝐻 = (𝐸 − (((𝐼‘(𝐺‘𝑋)) × (𝐸‘𝑋)) · 𝐺)) & ⊢ 𝐿 = (LKer‘𝑈) ⇒ ⊢ (𝜑 → ((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊆ (𝐿‘𝐻)) | ||
Theorem | lcfrlem3 41149 | Lemma for lcfr 41190. (Contributed by NM, 27-Feb-2015.) |
⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ × = (.r‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐼 = (invr‘𝑆) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ − = (-g‘𝐷) & ⊢ (𝜑 → 𝑈 ∈ LVec) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → (𝐺‘𝑋) ≠ 0 ) & ⊢ 𝐻 = (𝐸 − (((𝐼‘(𝐺‘𝑋)) × (𝐸‘𝑋)) · 𝐺)) & ⊢ 𝐿 = (LKer‘𝑈) ⇒ ⊢ (𝜑 → 𝑋 ∈ (𝐿‘𝐻)) | ||
Theorem | lcfrlem4 41150* | Lemma for lcfr 41190. (Contributed by NM, 10-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (LSubSp‘𝐷) & ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝑄) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝑉) | ||
Theorem | lcfrlem5 41151* | Lemma for lcfr 41190. 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 41152* | Lemma for lcfr 41190. 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 41153* | Lemma for lcfr 41190. 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 41154* | Lemma for lcf1o 41156 and lcfr 41190. (Contributed by NM, 21-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (0g‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐽‘𝑋) = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋))))) | ||
Theorem | lcfrlem9 41155* | Lemma for lcf1o 41156. (This part has undesirable $d's on 𝐽 and 𝜑 that we remove in lcf1o 41156.) 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 41156* | 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 41157* | Lemma for lcfr 41190. (Contributed by NM, 23-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (0g‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐽‘𝑋) ∈ 𝐹) | ||
Theorem | lcfrlem11 41158* | Lemma for lcfr 41190. (Contributed by NM, 23-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (0g‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐿‘(𝐽‘𝑋)) = ( ⊥ ‘{𝑋})) | ||
Theorem | lcfrlem12N 41159* | Lemma for lcfr 41190. (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 41160* | Lemma for lcfr 41190. (Contributed by NM, 8-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (0g‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐽‘𝑋) ∈ (𝐶 ∖ {𝑄})) | ||
Theorem | lcfrlem14 41161* | Lemma for lcfr 41190. (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 41162* | Lemma for lcfr 41190. (Contributed by NM, 9-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (0g‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → 𝑋 ∈ ( ⊥ ‘(𝐿‘(𝐽‘𝑋)))) | ||
Theorem | lcfrlem16 41163* | Lemma for lcfr 41190. (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 41164 | Lemma for lcfr 41190. 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 41165 | Lemma for lcfr 41190. (Contributed by NM, 24-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → ( ⊥ ‘{𝑋, 𝑌}) = (( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌}))) | ||
Theorem | lcfrlem19 41166 | Lemma for lcfr 41190. (Contributed by NM, 11-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{(𝑋 + 𝑌)}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{(𝑋 + 𝑌)}))) | ||
Theorem | lcfrlem20 41167 | Lemma for lcfr 41190. (Contributed by NM, 11-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → ¬ 𝑋 ∈ ( ⊥ ‘{(𝑋 + 𝑌)})) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∈ 𝐴) | ||
Theorem | lcfrlem21 41168 | Lemma for lcfr 41190. (Contributed by NM, 11-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∈ 𝐴) | ||
Theorem | lcfrlem22 41169 | Lemma for lcfr 41190. (Contributed by NM, 24-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝐴) | ||
Theorem | lcfrlem23 41170 | Lemma for lcfr 41190. 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 41171* | Lemma for lcfr 41190. (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 41172* | Lemma for lcfr 41190. Special case of lcfrlem35 41182 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 41173* | Lemma for lcfr 41190. Special case of lcfrlem36 41183 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 41174* | Lemma for lcfr 41190. Special case of lcfrlem37 41184 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 41175* | Lemma for lcfr 41190. 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 41176* | Lemma for lcfr 41190. (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 41177* | Lemma for lcfr 41190. (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 41178* | Lemma for lcfr 41190. (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 41179* | Lemma for lcfr 41190. (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 41180* | Lemma for lcfr 41190. (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 41181* | Lemma for lcfr 41190. (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 41182* | Lemma for lcfr 41190. (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 41183* | Lemma for lcfr 41190. (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 41184* | Lemma for lcfr 41190. (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‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}) & ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ (𝜑 → 𝑌 ∈ 𝐸) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐸) | ||
Theorem | lcfrlem38 41185* | Lemma for lcfr 41190. Combine lcfrlem27 41174 and lcfrlem37 41184. (Contributed by NM, 11-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ + = (+g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (LSubSp‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝑄) & ⊢ (𝜑 → 𝐺 ⊆ 𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ (𝜑 → 𝑌 ∈ 𝐸) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → 𝑋 ≠ 0 ) & ⊢ (𝜑 → 𝑌 ≠ 0 ) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ (𝜑 → 𝐼 ≠ 0 ) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐸) | ||
Theorem | lcfrlem39 41186* | Lemma for lcfr 41190. Eliminate 𝐽. (Contributed by NM, 11-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ + = (+g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (LSubSp‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝑄) & ⊢ (𝜑 → 𝐺 ⊆ 𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ (𝜑 → 𝑌 ∈ 𝐸) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → 𝑋 ≠ 0 ) & ⊢ (𝜑 → 𝑌 ≠ 0 ) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ (𝜑 → 𝐼 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐸) | ||
Theorem | lcfrlem40 41187* | Lemma for lcfr 41190. Eliminate 𝐵 and 𝐼. (Contributed by NM, 11-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ + = (+g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (LSubSp‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝑄) & ⊢ (𝜑 → 𝐺 ⊆ 𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ (𝜑 → 𝑌 ∈ 𝐸) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → 𝑋 ≠ 0 ) & ⊢ (𝜑 → 𝑌 ≠ 0 ) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐸) | ||
Theorem | lcfrlem41 41188* | Lemma for lcfr 41190. Eliminate span condition. (Contributed by NM, 11-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ + = (+g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (LSubSp‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝑄) & ⊢ (𝜑 → 𝐺 ⊆ 𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ (𝜑 → 𝑌 ∈ 𝐸) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → 𝑋 ≠ 0 ) & ⊢ (𝜑 → 𝑌 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐸) | ||
Theorem | lcfrlem42 41189* | Lemma for lcfr 41190. Eliminate nonzero condition. (Contributed by NM, 11-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ + = (+g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (LSubSp‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝑄) & ⊢ (𝜑 → 𝐺 ⊆ 𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ (𝜑 → 𝑌 ∈ 𝐸) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐸) | ||
Theorem | lcfr 41190* | Reconstruction of a subspace from a dual subspace of functionals with closed kernels. Our proof was suggested by Mario Carneiro, 20-Feb-2015. (Contributed by NM, 5-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑇 = (LSubSp‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝑄 = ∪ 𝑔 ∈ 𝑅 ( ⊥ ‘(𝐿‘𝑔)) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑅 ∈ 𝑇) & ⊢ (𝜑 → 𝑅 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝑄 ∈ 𝑆) | ||
Syntax | clcd 41191 | Extend class notation with vector space of functionals with closed kernels. |
class LCDual | ||
Definition | df-lcdual 41192* | Dual vector space of functionals with closed kernels. Note: we could also define this directly without mapd by using mapdrn 41254. TODO: see if it makes sense to go back and replace some of the LDual stuff with this. TODO: We could simplify df-mapd 41230 using (Base‘((LCDual‘𝐾)‘𝑊)). (Contributed by NM, 13-Mar-2015.) |
⊢ LCDual = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ ((LDual‘((DVecH‘𝑘)‘𝑤)) ↾s {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)}))) | ||
Theorem | lcdfval 41193* | Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑋 → (LCDual‘𝐾) = (𝑤 ∈ 𝐻 ↦ ((LDual‘((DVecH‘𝐾)‘𝑤)) ↾s {𝑓 ∈ (LFnl‘((DVecH‘𝐾)‘𝑤)) ∣ (((ocH‘𝐾)‘𝑤)‘(((ocH‘𝐾)‘𝑤)‘((LKer‘((DVecH‘𝐾)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝐾)‘𝑤))‘𝑓)}))) | ||
Theorem | lcdval 41194* | Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝐶 = (𝐷 ↾s {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)})) | ||
Theorem | lcdval2 41195* | Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻)) & ⊢ 𝐵 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} ⇒ ⊢ (𝜑 → 𝐶 = (𝐷 ↾s 𝐵)) | ||
Theorem | lcdlvec 41196 | The dual vector space of functionals with closed kernels is a left vector space. (Contributed by NM, 14-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝐶 ∈ LVec) | ||
Theorem | lcdlmod 41197 | The dual vector space of functionals with closed kernels is a left module. (Contributed by NM, 13-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝐶 ∈ LMod) | ||
Theorem | lcdvbase 41198* | Vector base set of a dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝐶) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐵 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝑉 = 𝐵) | ||
Theorem | lcdvbasess 41199 | The vector base set of the closed kernel dual space is a set of functionals. (Contributed by NM, 15-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝐶) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝑉 ⊆ 𝐹) | ||
Theorem | lcdvbaselfl 41200 | A vector in the base set of the closed kernel dual space is a functional. (Contributed by NM, 28-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝐶) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝐹) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |