![]() |
Metamath
Proof Explorer Theorem List (p. 408 of 480) | < 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lclkrlem2u 40701 | Lemma for lclkr 40707. lclkrlem2t 40700 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 40702 | Lemma for lclkr 40707. When the hypotheses of lclkrlem2u 40701 and lclkrlem2u 40701 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 40642, which requires the orthomodular law dihoml4 40551 (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 40703 | Lemma for lclkr 40707. This is the same as lclkrlem2u 40701 and lclkrlem2u 40701 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 40704 | Lemma for lclkr 40707. Eliminate by cases the hypotheses of lclkrlem2u 40701, lclkrlem2u 40701 and lclkrlem2w 40703. (Contributed by NM, 18-Jan-2015.) |
β’ πΏ = (LKerβπ) & β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ πΉ = (LFnlβπ) & β’ π· = (LDualβπ) & β’ + = (+gβπ·) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β πΈ β πΉ) & β’ (π β πΊ β πΉ) & β’ (π β (πΏβπΈ) = ( β₯ β{π})) & β’ (π β (πΏβπΊ) = ( β₯ β{π})) β β’ (π β ( β₯ β( β₯ β(πΏβ(πΈ + πΊ)))) = (πΏβ(πΈ + πΊ))) | ||
Theorem | lclkrlem2y 40705 | Lemma for lclkr 40707. 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 40706* | The set of functionals having closed kernels is closed under vector (functional) addition. Lemmas lclkrlem2a 40681 through lclkrlem2y 40705 are used for the proof. Here we express lclkrlem2y 40705 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 40707* | 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 40708* | Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015.) |
β’ πΆ = {π β πΉ β£ (( β₯ β( β₯ β(πΏβπ))) = (πΏβπ) β§ ( β₯ β(πΏβπ)) β π)} β β’ (πΊ β πΆ β (πΊ β πΉ β§ ( β₯ β( β₯ β(πΏβπΊ))) = (πΏβπΊ) β§ ( β₯ β(πΏβπΊ)) β π)) | ||
Theorem | lcfls1N 40709* | Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015.) (New usage is discouraged.) |
β’ πΆ = {π β πΉ β£ (( β₯ β( β₯ β(πΏβπ))) = (πΏβπ) β§ ( β₯ β(πΏβπ)) β π)} & β’ (π β πΊ β πΉ) β β’ (π β (πΊ β πΆ β (( β₯ β( β₯ β(πΏβπΊ))) = (πΏβπΊ) β§ ( β₯ β(πΏβπΊ)) β π))) | ||
Theorem | lcfls1c 40710* | Property of a functional with a closed kernel. (Contributed by NM, 28-Jan-2015.) |
β’ πΆ = {π β πΉ β£ (( β₯ β( β₯ β(πΏβπ))) = (πΏβπ) β§ ( β₯ β(πΏβπ)) β π)} & β’ π· = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} β β’ (πΊ β πΆ β (πΊ β π· β§ ( β₯ β(πΏβπΊ)) β π)) | ||
Theorem | lclkrslem1 40711* | 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 40712* | 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 40713* | 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 40707 proof. Do we achieve overall shortening by breaking them out as subtheorems? Or make lclkr 40707 a special case of this? (Contributed by NM, 29-Jan-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (LSubSpβπ·) & β’ πΆ = {π β πΉ β£ (( β₯ β( β₯ β(πΏβπ))) = (πΏβπ) β§ ( β₯ β(πΏβπ)) β π )} & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β πΆ β π) | ||
Theorem | lclkrs2 40714* | 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 40802. (Contributed by NM, 12-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (LSubSpβπ·) & β’ πΆ = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} & β’ π = {π β πΉ β£ (( β₯ β( β₯ β(πΏβπ))) = (πΏβπ) β§ ( β₯ β(πΏβπ)) β π)} & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β (π β π β§ π β πΆ)) | ||
Theorem | lcfrvalsnN 40715* | 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 40716 | Lemma for lcfr 40759. 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 40717 | Lemma for lcfr 40759. (Contributed by NM, 27-Feb-2015.) |
β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ Γ = (.rβπ) & β’ 0 = (0gβπ) & β’ πΌ = (invrβπ) & β’ πΉ = (LFnlβπ) & β’ π· = (LDualβπ) & β’ Β· = ( Β·π βπ·) & β’ β = (-gβπ·) & β’ (π β π β LVec) & β’ (π β πΈ β πΉ) & β’ (π β πΊ β πΉ) & β’ (π β π β π) & β’ (π β (πΊβπ) β 0 ) & β’ π» = (πΈ β (((πΌβ(πΊβπ)) Γ (πΈβπ)) Β· πΊ)) & β’ πΏ = (LKerβπ) β β’ (π β ((πΏβπΈ) β© (πΏβπΊ)) β (πΏβπ»)) | ||
Theorem | lcfrlem3 40718 | Lemma for lcfr 40759. (Contributed by NM, 27-Feb-2015.) |
β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ Γ = (.rβπ) & β’ 0 = (0gβπ) & β’ πΌ = (invrβπ) & β’ πΉ = (LFnlβπ) & β’ π· = (LDualβπ) & β’ Β· = ( Β·π βπ·) & β’ β = (-gβπ·) & β’ (π β π β LVec) & β’ (π β πΈ β πΉ) & β’ (π β πΊ β πΉ) & β’ (π β π β π) & β’ (π β (πΊβπ) β 0 ) & β’ π» = (πΈ β (((πΌβ(πΊβπ)) Γ (πΈβπ)) Β· πΊ)) & β’ πΏ = (LKerβπ) β β’ (π β π β (πΏβπ»)) | ||
Theorem | lcfrlem4 40719* | Lemma for lcfr 40759. (Contributed by NM, 10-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (LSubSpβπ·) & β’ πΈ = βͺ π β πΊ ( β₯ β(πΏβπ)) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΊ β π) & β’ (π β π β πΈ) β β’ (π β π β π) | ||
Theorem | lcfrlem5 40720* | Lemma for lcfr 40759. 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 40721* | Lemma for lcfr 40759. 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 40722* | Lemma for lcfr 40759. 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 40723* | Lemma for lcf1o 40725 and lcfr 40759. (Contributed by NM, 21-Feb-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (0gβπ·) & β’ πΆ = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} & β’ π½ = (π₯ β (π β { 0 }) β¦ (π£ β π β¦ (β©π β π βπ€ β ( β₯ β{π₯})π£ = (π€ + (π Β· π₯))))) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) β β’ (π β (π½βπ) = (π£ β π β¦ (β©π β π βπ€ β ( β₯ β{π})π£ = (π€ + (π Β· π))))) | ||
Theorem | lcfrlem9 40724* | Lemma for lcf1o 40725. (This part has undesirable $d's on π½ and π that we remove in lcf1o 40725.) 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 40725* | 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 40726* | Lemma for lcfr 40759. (Contributed by NM, 23-Feb-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (0gβπ·) & β’ πΆ = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} & β’ π½ = (π₯ β (π β { 0 }) β¦ (π£ β π β¦ (β©π β π βπ€ β ( β₯ β{π₯})π£ = (π€ + (π Β· π₯))))) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) β β’ (π β (π½βπ) β πΉ) | ||
Theorem | lcfrlem11 40727* | Lemma for lcfr 40759. (Contributed by NM, 23-Feb-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (0gβπ·) & β’ πΆ = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} & β’ π½ = (π₯ β (π β { 0 }) β¦ (π£ β π β¦ (β©π β π βπ€ β ( β₯ β{π₯})π£ = (π€ + (π Β· π₯))))) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) β β’ (π β (πΏβ(π½βπ)) = ( β₯ β{π})) | ||
Theorem | lcfrlem12N 40728* | Lemma for lcfr 40759. (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 40729* | Lemma for lcfr 40759. (Contributed by NM, 8-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (0gβπ·) & β’ πΆ = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} & β’ π½ = (π₯ β (π β { 0 }) β¦ (π£ β π β¦ (β©π β π βπ€ β ( β₯ β{π₯})π£ = (π€ + (π Β· π₯))))) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) β β’ (π β (π½βπ) β (πΆ β {π})) | ||
Theorem | lcfrlem14 40730* | Lemma for lcfr 40759. (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 40731* | Lemma for lcfr 40759. (Contributed by NM, 9-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (0gβπ·) & β’ πΆ = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} & β’ π½ = (π₯ β (π β { 0 }) β¦ (π£ β π β¦ (β©π β π βπ€ β ( β₯ β{π₯})π£ = (π€ + (π Β· π₯))))) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) β β’ (π β π β ( β₯ β(πΏβ(π½βπ)))) | ||
Theorem | lcfrlem16 40732* | Lemma for lcfr 40759. (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 40733 | Lemma for lcfr 40759. 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 40734 | Lemma for lcfr 40759. (Contributed by NM, 24-Feb-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ{π}) β (πβ{π})) β β’ (π β ( β₯ β{π, π}) = (( β₯ β{π}) β© ( β₯ β{π}))) | ||
Theorem | lcfrlem19 40735 | Lemma for lcfr 40759. (Contributed by NM, 11-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ{π}) β (πβ{π})) β β’ (π β (Β¬ π β ( β₯ β{(π + π)}) β¨ Β¬ π β ( β₯ β{(π + π)}))) | ||
Theorem | lcfrlem20 40736 | Lemma for lcfr 40759. (Contributed by NM, 11-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β Β¬ π β ( β₯ β{(π + π)})) β β’ (π β ((πβ{π, π}) β© ( β₯ β{(π + π)})) β π΄) | ||
Theorem | lcfrlem21 40737 | Lemma for lcfr 40759. (Contributed by NM, 11-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ{π}) β (πβ{π})) β β’ (π β ((πβ{π, π}) β© ( β₯ β{(π + π)})) β π΄) | ||
Theorem | lcfrlem22 40738 | Lemma for lcfr 40759. (Contributed by NM, 24-Feb-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ{π}) β (πβ{π})) & β’ π΅ = ((πβ{π, π}) β© ( β₯ β{(π + π)})) β β’ (π β π΅ β π΄) | ||
Theorem | lcfrlem23 40739 | Lemma for lcfr 40759. 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 40740* | Lemma for lcfr 40759. (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 40741* | Lemma for lcfr 40759. Special case of lcfrlem35 40751 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 40742* | Lemma for lcfr 40759. Special case of lcfrlem36 40752 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 40743* | Lemma for lcfr 40759. Special case of lcfrlem37 40753 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 40744* | Lemma for lcfr 40759. 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 40745* | Lemma for lcfr 40759. (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 40746* | Lemma for lcfr 40759. (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 40747* | Lemma for lcfr 40759. (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 40748* | Lemma for lcfr 40759. (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 40749* | Lemma for lcfr 40759. (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 40750* | Lemma for lcfr 40759. (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 40751* | Lemma for lcfr 40759. (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 40752* | Lemma for lcfr 40759. (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 40753* | Lemma for lcfr 40759. (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 40754* | Lemma for lcfr 40759. Combine lcfrlem27 40743 and lcfrlem37 40753. (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 40755* | Lemma for lcfr 40759. 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 40756* | Lemma for lcfr 40759. 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 40757* | Lemma for lcfr 40759. 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 40758* | Lemma for lcfr 40759. Eliminate nonzero condition. (Contributed by NM, 11-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ + = (+gβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (LSubSpβπ·) & β’ πΆ = {π β (LFnlβπ) β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} & β’ πΈ = βͺ π β πΊ ( β₯ β(πΏβπ)) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΊ β π) & β’ (π β πΊ β πΆ) & β’ (π β π β πΈ) & β’ (π β π β πΈ) β β’ (π β (π + π) β πΈ) | ||
Theorem | lcfr 40759* | 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 40760 | Extend class notation with vector space of functionals with closed kernels. |
class LCDual | ||
Definition | df-lcdual 40761* | Dual vector space of functionals with closed kernels. Note: we could also define this directly without mapd by using mapdrn 40823. TODO: see if it makes sense to go back and replace some of the LDual stuff with this. TODO: We could simplify df-mapd 40799 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 40762* | 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 40763* | Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ (π β (πΎ β π β§ π β π»)) β β’ (π β πΆ = (π· βΎs {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)})) | ||
Theorem | lcdval2 40764* | Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ (π β (πΎ β π β§ π β π»)) & β’ π΅ = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} β β’ (π β πΆ = (π· βΎs π΅)) | ||
Theorem | lcdlvec 40765 | 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 40766 | 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 40767* | 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 40768 | 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 40769 | 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 β§ π β π»)) & β’ (π β π β π) β β’ (π β π β πΉ) | ||
Theorem | lcdvbasecl 40770 | Closure of the value of a vector (functional) in the closed kernel dual space. (Contributed by NM, 28-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΈ = (BaseβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β πΈ) & β’ (π β π β π) β β’ (π β (πΉβπ) β π ) | ||
Theorem | lcdvadd 40771 | Vector addition for the closed kernel vector space dual. (Contributed by NM, 10-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π· = (LDualβπ) & β’ + = (+gβπ·) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = (+gβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β β = + ) | ||
Theorem | lcdvaddval 40772 | The value of the value of vector addition in the closed kernel vector space dual. (Contributed by NM, 10-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ + = (+gβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ β = (+gβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β πΊ β π·) & β’ (π β π β π) β β’ (π β ((πΉ β πΊ)βπ) = ((πΉβπ) + (πΊβπ))) | ||
Theorem | lcdsca 40773 | The ring of scalars of the closed kernel dual space. (Contributed by NM, 16-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ π = (opprβπΉ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = (ScalarβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β π = π) | ||
Theorem | lcdsbase 40774 | Base set of scalar ring for the closed kernel dual of a vector space. (Contributed by NM, 18-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ πΏ = (BaseβπΉ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = (ScalarβπΆ) & β’ π = (Baseβπ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β π = πΏ) | ||
Theorem | lcdsadd 40775 | Scalar addition for the closed kernel vector space dual. (Contributed by NM, 6-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ + = (+gβπΉ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = (ScalarβπΆ) & β’ β = (+gβπ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β β = + ) | ||
Theorem | lcdsmul 40776 | Scalar multiplication for the closed kernel vector space dual. (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ πΏ = (BaseβπΉ) & β’ Β· = (.rβπΉ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = (ScalarβπΆ) & β’ β = (.rβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β πΏ) & β’ (π β π β πΏ) β β’ (π β (π β π) = (π Β· π)) | ||
Theorem | lcdvs 40777 | Scalar product for the closed kernel vector space dual. (Contributed by NM, 28-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π· = (LDualβπ) & β’ Β· = ( Β·π βπ·) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = ( Β·π βπΆ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β β = Β· ) | ||
Theorem | lcdvsval 40778 | Value of scalar product operation value for the closed kernel vector space dual. (Contributed by NM, 28-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ Β· = (.rβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ β = ( Β·π βπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π ) & β’ (π β πΊ β πΉ) & β’ (π β π΄ β π) β β’ (π β ((π β πΊ)βπ΄) = ((πΊβπ΄) Β· π)) | ||
Theorem | lcdvscl 40779 | The scalar product operation value is a functional. (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = (BaseβπΆ) & β’ Β· = ( Β·π βπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π ) & β’ (π β πΊ β π) β β’ (π β (π Β· πΊ) β π) | ||
Theorem | lcdlssvscl 40780 | Closure of scalar product in a closed kernel dual vector space. (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ π = (BaseβπΉ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = (BaseβπΆ) & β’ Β· = ( Β·π βπΆ) & β’ π = (LSubSpβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΏ β π) & β’ (π β π β π ) & β’ (π β π β πΏ) β β’ (π β (π Β· π) β πΏ) | ||
Theorem | lcdvsass 40781 | Associative law for scalar product in a closed kernel dual vector space. (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Scalarβπ) & β’ πΏ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ β = ( Β·π βπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β πΏ) & β’ (π β π β πΏ) & β’ (π β πΊ β πΉ) β β’ (π β ((π Β· π) β πΊ) = (π β (π β πΊ))) | ||
Theorem | lcd0 40782 | The zero scalar of the closed kernel dual of a vector space. (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ 0 = (0gβπΉ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = (ScalarβπΆ) & β’ π = (0gβπ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β π = 0 ) | ||
Theorem | lcd1 40783 | The unit scalar of the closed kernel dual of a vector space. (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ 1 = (1rβπΉ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = (ScalarβπΆ) & β’ πΌ = (1rβπ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β πΌ = 1 ) | ||
Theorem | lcdneg 40784 | The unit scalar of the closed kernel dual of a vector space. (Contributed by NM, 11-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Scalarβπ) & β’ π = (invgβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = (ScalarβπΆ) & β’ π = (invgβπ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β π = π) | ||
Theorem | lcd0v 40785 | The zero functional in the set of functionals with closed kernels. (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ 0 = (0gβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = (0gβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β π = (π Γ { 0 })) | ||
Theorem | lcd0v2 40786 | The zero functional in the set of functionals with closed kernels. (Contributed by NM, 27-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π· = (LDualβπ) & β’ 0 = (0gβπ·) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = (0gβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β π = 0 ) | ||
Theorem | lcd0vvalN 40787 | Value of the zero functional at any vector. (Contributed by NM, 28-Mar-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ 0 = (0gβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = (0gβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β (πβπ) = 0 ) | ||
Theorem | lcd0vcl 40788 | Closure of the zero functional in the set of functionals with closed kernels. (Contributed by NM, 15-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = (BaseβπΆ) & β’ π = (0gβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β π β π) | ||
Theorem | lcd0vs 40789 | A scalar zero times a functional is the zero functional. (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Scalarβπ) & β’ 0 = (0gβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = (BaseβπΆ) & β’ Β· = ( Β·π βπΆ) & β’ π = (0gβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΊ β π) β β’ (π β ( 0 Β· πΊ) = π) | ||
Theorem | lcdvs0N 40790 | A scalar times the zero functional is the zero functional. (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ Β· = ( Β·π βπΆ) & β’ 0 = (0gβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π ) β β’ (π β (π Β· 0 ) = 0 ) | ||
Theorem | lcdvsub 40791 | The value of vector subtraction in the closed kernel dual space. (Contributed by NM, 22-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Scalarβπ) & β’ π = (invgβπ) & β’ 1 = (1rβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = (BaseβπΆ) & β’ + = (+gβπΆ) & β’ Β· = ( Β·π βπΆ) & β’ β = (-gβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π) & β’ (π β πΊ β π) β β’ (π β (πΉ β πΊ) = (πΉ + ((πβ 1 ) Β· πΊ))) | ||
Theorem | lcdvsubval 40792 | The value of the value of vector addition in the closed kernel vector space dual. (Contributed by NM, 11-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ π = (-gβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ β = (-gβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β πΊ β π·) & β’ (π β π β π) β β’ (π β ((πΉ β πΊ)βπ) = ((πΉβπ)π(πΊβπ))) | ||
Theorem | lcdlss 40793* | Subspaces of a dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((ocHβπΎ)βπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = (LSubSpβπΆ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (LSubSpβπ·) & β’ π΅ = {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β π = (π β© π« π΅)) | ||
Theorem | lcdlss2N 40794 | Subspaces of a dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = (LSubSpβπΆ) & β’ π = (BaseβπΆ) & β’ π = ((DVecHβπΎ)βπ) & β’ π· = (LDualβπ) & β’ π = (LSubSpβπ·) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β π = (π β© π« π)) | ||
Theorem | lcdlsp 40795 | Span in the set of functionals with closed kernels. (Contributed by NM, 28-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π· = (LDualβπ) & β’ π = (LSpanβπ·) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΊ β πΉ) β β’ (π β (πβπΊ) = (πβπΊ)) | ||
Theorem | lcdlkreqN 40796 | Colinear functionals have equal kernels. (Contributed by NM, 28-Mar-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΏ = (LKerβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ 0 = (0gβπΆ) & β’ π = (LSpanβπΆ) & β’ π = (BaseβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΌ β π) & β’ (π β πΊ β (πβ{πΌ})) & β’ (π β πΊ β 0 ) β β’ (π β (πΏβπΊ) = (πΏβπΌ)) | ||
Theorem | lcdlkreq2N 40797 | Colinear functionals have equal kernels. (Contributed by NM, 28-Mar-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ πΏ = (LKerβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = (BaseβπΆ) & β’ Β· = ( Β·π βπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π΄ β (π β { 0 })) & β’ (π β πΌ β π) & β’ (π β πΊ = (π΄ Β· πΌ)) β β’ (π β (πΏβπΊ) = (πΏβπΌ)) | ||
Syntax | cmpd 40798 | Extend class notation with projectivity from subspaces of vector space H to subspaces of functionals with closed kernels. |
class mapd | ||
Definition | df-mapd 40799* | Extend class notation with a one-to-one onto (mapd1o 40822), order-preserving (mapdord 40812) map, called a projectivity (definition of projectivity in [Baer] p. 40), from subspaces of vector space H to those subspaces of the dual space having functionals with closed kernels. (Contributed by NM, 25-Jan-2015.) |
β’ mapd = (π β V β¦ (π€ β (LHypβπ) β¦ (π β (LSubSpβ((DVecHβπ)βπ€)) β¦ {π β (LFnlβ((DVecHβπ)βπ€)) β£ ((((ocHβπ)βπ€)β(((ocHβπ)βπ€)β((LKerβ((DVecHβπ)βπ€))βπ))) = ((LKerβ((DVecHβπ)βπ€))βπ) β§ (((ocHβπ)βπ€)β((LKerβ((DVecHβπ)βπ€))βπ)) β π )}))) | ||
Theorem | mapdffval 40800* | Projectivity from vector space H to dual space. (Contributed by NM, 25-Jan-2015.) |
β’ π» = (LHypβπΎ) β β’ (πΎ β π β (mapdβπΎ) = (π€ β π» β¦ (π β (LSubSpβ((DVecHβπΎ)βπ€)) β¦ {π β (LFnlβ((DVecHβπΎ)βπ€)) β£ ((((ocHβπΎ)βπ€)β(((ocHβπΎ)βπ€)β((LKerβ((DVecHβπΎ)βπ€))βπ))) = ((LKerβ((DVecHβπΎ)βπ€))βπ) β§ (((ocHβπΎ)βπ€)β((LKerβ((DVecHβπΎ)βπ€))βπ)) β π )}))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |