![]() |
Metamath
Proof Explorer Theorem List (p. 410 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lcfl1lem 40901* | Property of a functional with a closed kernel. (Contributed by NM, 28-Dec-2014.) |
β’ πΆ = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} β β’ (πΊ β πΆ β (πΊ β πΉ β§ ( β₯ β( β₯ β(πΏβπΊ))) = (πΏβπΊ))) | ||
Theorem | lcfl1 40902* | Property of a functional with a closed kernel. (Contributed by NM, 31-Dec-2014.) |
β’ πΆ = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} & β’ (π β πΊ β πΉ) β β’ (π β (πΊ β πΆ β ( β₯ β( β₯ β(πΏβπΊ))) = (πΏβπΊ))) | ||
Theorem | lcfl2 40903* | Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ πΆ = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΊ β πΉ) β β’ (π β (πΊ β πΆ β (( β₯ β( β₯ β(πΏβπΊ))) β π β¨ (πΏβπΊ) = π))) | ||
Theorem | lcfl3 40904* | Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ πΆ = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΊ β πΉ) β β’ (π β (πΊ β πΆ β (( β₯ β(πΏβπΊ)) β π΄ β¨ (πΏβπΊ) = π))) | ||
Theorem | lcfl4N 40905* | 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 40906* | Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.) |
β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ πΆ = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΊ β πΉ) β β’ (π β (πΊ β πΆ β (πΏβπΊ) β ran πΌ)) | ||
Theorem | lcfl5a 40907 | Property of a functional with a closed kernel. TODO: Make lcfl5 40906 etc. obsolete and rewrite without πΆ hypothesis? (Contributed by NM, 29-Jan-2015.) |
β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΊ β πΉ) β β’ (π β (( β₯ β( β₯ β(πΏβπΊ))) = (πΏβπΊ) β (πΏβπΊ) β ran πΌ)) | ||
Theorem | lcfl6lem 40908* | Lemma for lcfl6 40910. A functional πΊ (whose kernel is closed by dochsnkr 40882) 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 40909* | Lemma for lcfl7N 40911. 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 40910* | Property of a functional with a closed kernel. Note that (πΏβπΊ) = π means the functional is zero by lkr0f 38503. (Contributed by NM, 3-Jan-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ πΆ = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΊ β πΉ) β β’ (π β (πΊ β πΆ β ((πΏβπΊ) = π β¨ βπ₯ β (π β { 0 })πΊ = (π£ β π β¦ (β©π β π βπ€ β ( β₯ β{π₯})π£ = (π€ + (π Β· π₯))))))) | ||
Theorem | lcfl7N 40911* | 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 38503. (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 40912* | Property of a functional with a closed kernel. (Contributed by NM, 17-Jan-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ πΆ = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΊ β πΉ) β β’ (π β (πΊ β πΆ β βπ₯ β π (πΏβπΊ) = ( β₯ β{π₯}))) | ||
Theorem | lcfl8a 40913* | Property of a functional with a closed kernel. (Contributed by NM, 17-Jan-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΊ β πΉ) β β’ (π β (( β₯ β( β₯ β(πΏβπΊ))) = (πΏβπΊ) β βπ₯ β π (πΏβπΊ) = ( β₯ β{π₯}))) | ||
Theorem | lcfl8b 40914* | 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 40915 | Property implying that a functional has a closed kernel. (Contributed by NM, 16-Feb-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΊ β πΉ) & β’ (π β π β π) & β’ (π β ( β₯ β{π}) β (πΏβπΊ)) β β’ (π β ( β₯ β( β₯ β(πΏβπΊ))) = (πΏβπΊ)) | ||
Theorem | lclkrlem1 40916* | 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 40917 | Lemma for lclkr 40943. Use lshpat 38465 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 40918 | Lemma for lclkr 40943. (Contributed by NM, 17-Jan-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π΅ β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β ( β₯ β{π}) β ( β₯ β{π})) & β’ (π β (Β¬ π β ( β₯ β{π΅}) β¨ Β¬ π β ( β₯ β{π΅}))) β β’ (π β (((πβ{π}) β (πβ{π})) β© ( β₯ β{π΅})) β π΄) | ||
Theorem | lclkrlem2c 40919 | Lemma for lclkr 40943. (Contributed by NM, 16-Jan-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π΅ β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β ( β₯ β{π}) β ( β₯ β{π})) & β’ (π β (Β¬ π β ( β₯ β{π΅}) β¨ Β¬ π β ( β₯ β{π΅}))) & β’ π½ = (LSHypβπ) β β’ (π β ((( β₯ β{π}) β© ( β₯ β{π})) β (πβ{π΅})) β π½) | ||
Theorem | lclkrlem2d 40920 | Lemma for lclkr 40943. (Contributed by NM, 16-Jan-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π΅ β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β ( β₯ β{π}) β ( β₯ β{π})) & β’ (π β (Β¬ π β ( β₯ β{π΅}) β¨ Β¬ π β ( β₯ β{π΅}))) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (π β ((( β₯ β{π}) β© ( β₯ β{π})) β (πβ{π΅})) β ran πΌ) | ||
Theorem | lclkrlem2e 40921 | Lemma for lclkr 40943. 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 40922 | Lemma for lclkr 40943. 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 40923 | Lemma for lclkr 40943. 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 40924 | Lemma for lclkr 40943. 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 40925 | Lemma for lclkr 40943. 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 40926 | Lemma for lclkr 40943. 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 40927 | Lemma for lclkr 40943. 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 40928 | Lemma for lclkr 40943. 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 40929 | Lemma for lclkr 40943. 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 40930 | Lemma for lclkr 40943. (Contributed by NM, 12-Jan-2015.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ Γ = (.rβπ) & β’ 0 = (0gβπ) & β’ πΌ = (invrβπ) & β’ β = (-gβπ) & β’ πΉ = (LFnlβπ) & β’ π· = (LDualβπ) & β’ + = (+gβπ·) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β πΈ β πΉ) & β’ (π β πΊ β πΉ) & β’ π = (LSpanβπ) & β’ πΏ = (LKerβπ) & β’ (π β π β LVec) & β’ (π β ((πΈ + πΊ)βπ) = 0 ) & β’ (π β ((πΈ + πΊ)βπ) = 0 ) β β’ (π β (πβ{π, π}) β (πΏβ(πΈ + πΊ))) | ||
Theorem | lclkrlem2o 40931 | Lemma for lclkr 40943. 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 40932 | Lemma for lclkr 40943. 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 40933 | Lemma for lclkr 40943. 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 40934 | Lemma for lclkr 40943. 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 40935 | Lemma for lclkr 40943. 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 40936 | Lemma for lclkr 40943. 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 40937 | Lemma for lclkr 40943. lclkrlem2t 40936 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 40938 | Lemma for lclkr 40943. When the hypotheses of lclkrlem2u 40937 and lclkrlem2u 40937 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 40878, which requires the orthomodular law dihoml4 40787 (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 40939 | Lemma for lclkr 40943. This is the same as lclkrlem2u 40937 and lclkrlem2u 40937 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 40940 | Lemma for lclkr 40943. Eliminate by cases the hypotheses of lclkrlem2u 40937, lclkrlem2u 40937 and lclkrlem2w 40939. (Contributed by NM, 18-Jan-2015.) |
β’ πΏ = (LKerβπ) & β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ πΉ = (LFnlβπ) & β’ π· = (LDualβπ) & β’ + = (+gβπ·) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β πΈ β πΉ) & β’ (π β πΊ β πΉ) & β’ (π β (πΏβπΈ) = ( β₯ β{π})) & β’ (π β (πΏβπΊ) = ( β₯ β{π})) β β’ (π β ( β₯ β( β₯ β(πΏβ(πΈ + πΊ)))) = (πΏβ(πΈ + πΊ))) | ||
Theorem | lclkrlem2y 40941 | Lemma for lclkr 40943. 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 40942* | The set of functionals having closed kernels is closed under vector (functional) addition. Lemmas lclkrlem2a 40917 through lclkrlem2y 40941 are used for the proof. Here we express lclkrlem2y 40941 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 40943* | 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 40944* | Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015.) |
β’ πΆ = {π β πΉ β£ (( β₯ β( β₯ β(πΏβπ))) = (πΏβπ) β§ ( β₯ β(πΏβπ)) β π)} β β’ (πΊ β πΆ β (πΊ β πΉ β§ ( β₯ β( β₯ β(πΏβπΊ))) = (πΏβπΊ) β§ ( β₯ β(πΏβπΊ)) β π)) | ||
Theorem | lcfls1N 40945* | Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015.) (New usage is discouraged.) |
β’ πΆ = {π β πΉ β£ (( β₯ β( β₯ β(πΏβπ))) = (πΏβπ) β§ ( β₯ β(πΏβπ)) β π)} & β’ (π β πΊ β πΉ) β β’ (π β (πΊ β πΆ β (( β₯ β( β₯ β(πΏβπΊ))) = (πΏβπΊ) β§ ( β₯ β(πΏβπΊ)) β π))) | ||
Theorem | lcfls1c 40946* | Property of a functional with a closed kernel. (Contributed by NM, 28-Jan-2015.) |
β’ πΆ = {π β πΉ β£ (( β₯ β( β₯ β(πΏβπ))) = (πΏβπ) β§ ( β₯ β(πΏβπ)) β π)} & β’ π· = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} β β’ (πΊ β πΆ β (πΊ β π· β§ ( β₯ β(πΏβπΊ)) β π)) | ||
Theorem | lclkrslem1 40947* | 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 40948* | 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 40949* | 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 40943 proof. Do we achieve overall shortening by breaking them out as subtheorems? Or make lclkr 40943 a special case of this? (Contributed by NM, 29-Jan-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (LSubSpβπ·) & β’ πΆ = {π β πΉ β£ (( β₯ β( β₯ β(πΏβπ))) = (πΏβπ) β§ ( β₯ β(πΏβπ)) β π )} & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β πΆ β π) | ||
Theorem | lclkrs2 40950* | 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 41038. (Contributed by NM, 12-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (LSubSpβπ·) & β’ πΆ = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} & β’ π = {π β πΉ β£ (( β₯ β( β₯ β(πΏβπ))) = (πΏβπ) β§ ( β₯ β(πΏβπ)) β π)} & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β (π β π β§ π β πΆ)) | ||
Theorem | lcfrvalsnN 40951* | 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 40952 | Lemma for lcfr 40995. 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 40953 | Lemma for lcfr 40995. (Contributed by NM, 27-Feb-2015.) |
β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ Γ = (.rβπ) & β’ 0 = (0gβπ) & β’ πΌ = (invrβπ) & β’ πΉ = (LFnlβπ) & β’ π· = (LDualβπ) & β’ Β· = ( Β·π βπ·) & β’ β = (-gβπ·) & β’ (π β π β LVec) & β’ (π β πΈ β πΉ) & β’ (π β πΊ β πΉ) & β’ (π β π β π) & β’ (π β (πΊβπ) β 0 ) & β’ π» = (πΈ β (((πΌβ(πΊβπ)) Γ (πΈβπ)) Β· πΊ)) & β’ πΏ = (LKerβπ) β β’ (π β ((πΏβπΈ) β© (πΏβπΊ)) β (πΏβπ»)) | ||
Theorem | lcfrlem3 40954 | Lemma for lcfr 40995. (Contributed by NM, 27-Feb-2015.) |
β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ Γ = (.rβπ) & β’ 0 = (0gβπ) & β’ πΌ = (invrβπ) & β’ πΉ = (LFnlβπ) & β’ π· = (LDualβπ) & β’ Β· = ( Β·π βπ·) & β’ β = (-gβπ·) & β’ (π β π β LVec) & β’ (π β πΈ β πΉ) & β’ (π β πΊ β πΉ) & β’ (π β π β π) & β’ (π β (πΊβπ) β 0 ) & β’ π» = (πΈ β (((πΌβ(πΊβπ)) Γ (πΈβπ)) Β· πΊ)) & β’ πΏ = (LKerβπ) β β’ (π β π β (πΏβπ»)) | ||
Theorem | lcfrlem4 40955* | Lemma for lcfr 40995. (Contributed by NM, 10-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (LSubSpβπ·) & β’ πΈ = βͺ π β πΊ ( β₯ β(πΏβπ)) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΊ β π) & β’ (π β π β πΈ) β β’ (π β π β π) | ||
Theorem | lcfrlem5 40956* | Lemma for lcfr 40995. 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 40957* | Lemma for lcfr 40995. 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 40958* | Lemma for lcfr 40995. 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 40959* | Lemma for lcf1o 40961 and lcfr 40995. (Contributed by NM, 21-Feb-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (0gβπ·) & β’ πΆ = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} & β’ π½ = (π₯ β (π β { 0 }) β¦ (π£ β π β¦ (β©π β π βπ€ β ( β₯ β{π₯})π£ = (π€ + (π Β· π₯))))) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) β β’ (π β (π½βπ) = (π£ β π β¦ (β©π β π βπ€ β ( β₯ β{π})π£ = (π€ + (π Β· π))))) | ||
Theorem | lcfrlem9 40960* | Lemma for lcf1o 40961. (This part has undesirable $d's on π½ and π that we remove in lcf1o 40961.) 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 40961* | 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 40962* | Lemma for lcfr 40995. (Contributed by NM, 23-Feb-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (0gβπ·) & β’ πΆ = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} & β’ π½ = (π₯ β (π β { 0 }) β¦ (π£ β π β¦ (β©π β π βπ€ β ( β₯ β{π₯})π£ = (π€ + (π Β· π₯))))) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) β β’ (π β (π½βπ) β πΉ) | ||
Theorem | lcfrlem11 40963* | Lemma for lcfr 40995. (Contributed by NM, 23-Feb-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (0gβπ·) & β’ πΆ = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} & β’ π½ = (π₯ β (π β { 0 }) β¦ (π£ β π β¦ (β©π β π βπ€ β ( β₯ β{π₯})π£ = (π€ + (π Β· π₯))))) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) β β’ (π β (πΏβ(π½βπ)) = ( β₯ β{π})) | ||
Theorem | lcfrlem12N 40964* | Lemma for lcfr 40995. (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 40965* | Lemma for lcfr 40995. (Contributed by NM, 8-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (0gβπ·) & β’ πΆ = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} & β’ π½ = (π₯ β (π β { 0 }) β¦ (π£ β π β¦ (β©π β π βπ€ β ( β₯ β{π₯})π£ = (π€ + (π Β· π₯))))) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) β β’ (π β (π½βπ) β (πΆ β {π})) | ||
Theorem | lcfrlem14 40966* | Lemma for lcfr 40995. (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 40967* | Lemma for lcfr 40995. (Contributed by NM, 9-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (0gβπ·) & β’ πΆ = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} & β’ π½ = (π₯ β (π β { 0 }) β¦ (π£ β π β¦ (β©π β π βπ€ β ( β₯ β{π₯})π£ = (π€ + (π Β· π₯))))) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) β β’ (π β π β ( β₯ β(πΏβ(π½βπ)))) | ||
Theorem | lcfrlem16 40968* | Lemma for lcfr 40995. (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 40969 | Lemma for lcfr 40995. 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 40970 | Lemma for lcfr 40995. (Contributed by NM, 24-Feb-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ{π}) β (πβ{π})) β β’ (π β ( β₯ β{π, π}) = (( β₯ β{π}) β© ( β₯ β{π}))) | ||
Theorem | lcfrlem19 40971 | Lemma for lcfr 40995. (Contributed by NM, 11-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ{π}) β (πβ{π})) β β’ (π β (Β¬ π β ( β₯ β{(π + π)}) β¨ Β¬ π β ( β₯ β{(π + π)}))) | ||
Theorem | lcfrlem20 40972 | Lemma for lcfr 40995. (Contributed by NM, 11-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β Β¬ π β ( β₯ β{(π + π)})) β β’ (π β ((πβ{π, π}) β© ( β₯ β{(π + π)})) β π΄) | ||
Theorem | lcfrlem21 40973 | Lemma for lcfr 40995. (Contributed by NM, 11-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ{π}) β (πβ{π})) β β’ (π β ((πβ{π, π}) β© ( β₯ β{(π + π)})) β π΄) | ||
Theorem | lcfrlem22 40974 | Lemma for lcfr 40995. (Contributed by NM, 24-Feb-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ{π}) β (πβ{π})) & β’ π΅ = ((πβ{π, π}) β© ( β₯ β{(π + π)})) β β’ (π β π΅ β π΄) | ||
Theorem | lcfrlem23 40975 | Lemma for lcfr 40995. 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 40976* | Lemma for lcfr 40995. (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 40977* | Lemma for lcfr 40995. Special case of lcfrlem35 40987 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 40978* | Lemma for lcfr 40995. Special case of lcfrlem36 40988 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 40979* | Lemma for lcfr 40995. Special case of lcfrlem37 40989 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 40980* | Lemma for lcfr 40995. 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 40981* | Lemma for lcfr 40995. (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 40982* | Lemma for lcfr 40995. (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 40983* | Lemma for lcfr 40995. (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 40984* | Lemma for lcfr 40995. (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 40985* | Lemma for lcfr 40995. (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 40986* | Lemma for lcfr 40995. (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 40987* | Lemma for lcfr 40995. (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 40988* | Lemma for lcfr 40995. (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 40989* | Lemma for lcfr 40995. (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 40990* | Lemma for lcfr 40995. Combine lcfrlem27 40979 and lcfrlem37 40989. (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 40991* | Lemma for lcfr 40995. 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 40992* | Lemma for lcfr 40995. 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 40993* | Lemma for lcfr 40995. 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 40994* | Lemma for lcfr 40995. Eliminate nonzero condition. (Contributed by NM, 11-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ + = (+gβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (LSubSpβπ·) & β’ πΆ = {π β (LFnlβπ) β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} & β’ πΈ = βͺ π β πΊ ( β₯ β(πΏβπ)) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΊ β π) & β’ (π β πΊ β πΆ) & β’ (π β π β πΈ) & β’ (π β π β πΈ) β β’ (π β (π + π) β πΈ) | ||
Theorem | lcfr 40995* | 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 40996 | Extend class notation with vector space of functionals with closed kernels. |
class LCDual | ||
Definition | df-lcdual 40997* | Dual vector space of functionals with closed kernels. Note: we could also define this directly without mapd by using mapdrn 41059. TODO: see if it makes sense to go back and replace some of the LDual stuff with this. TODO: We could simplify df-mapd 41035 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 40998* | 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 40999* | Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ (π β (πΎ β π β§ π β π»)) β β’ (π β πΆ = (π· βΎs {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)})) | ||
Theorem | lcdval2 41000* | Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ (π β (πΎ β π β§ π β π»)) & β’ π΅ = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} β β’ (π β πΆ = (π· βΎs π΅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |