![]() |
Metamath
Proof Explorer Theorem List (p. 405 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lclkrlem2x 40401 | Lemma for lclkr 40404. Eliminate by cases the hypotheses of lclkrlem2u 40398, lclkrlem2u 40398 and lclkrlem2w 40400. (Contributed by NM, 18-Jan-2015.) |
β’ πΏ = (LKerβπ) & β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ πΉ = (LFnlβπ) & β’ π· = (LDualβπ) & β’ + = (+gβπ·) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β πΈ β πΉ) & β’ (π β πΊ β πΉ) & β’ (π β (πΏβπΈ) = ( β₯ β{π})) & β’ (π β (πΏβπΊ) = ( β₯ β{π})) β β’ (π β ( β₯ β( β₯ β(πΏβ(πΈ + πΊ)))) = (πΏβ(πΈ + πΊ))) | ||
Theorem | lclkrlem2y 40402 | Lemma for lclkr 40404. 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 40403* | The set of functionals having closed kernels is closed under vector (functional) addition. Lemmas lclkrlem2a 40378 through lclkrlem2y 40402 are used for the proof. Here we express lclkrlem2y 40402 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 40404* | 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 40405* | Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015.) |
β’ πΆ = {π β πΉ β£ (( β₯ β( β₯ β(πΏβπ))) = (πΏβπ) β§ ( β₯ β(πΏβπ)) β π)} β β’ (πΊ β πΆ β (πΊ β πΉ β§ ( β₯ β( β₯ β(πΏβπΊ))) = (πΏβπΊ) β§ ( β₯ β(πΏβπΊ)) β π)) | ||
Theorem | lcfls1N 40406* | Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015.) (New usage is discouraged.) |
β’ πΆ = {π β πΉ β£ (( β₯ β( β₯ β(πΏβπ))) = (πΏβπ) β§ ( β₯ β(πΏβπ)) β π)} & β’ (π β πΊ β πΉ) β β’ (π β (πΊ β πΆ β (( β₯ β( β₯ β(πΏβπΊ))) = (πΏβπΊ) β§ ( β₯ β(πΏβπΊ)) β π))) | ||
Theorem | lcfls1c 40407* | Property of a functional with a closed kernel. (Contributed by NM, 28-Jan-2015.) |
β’ πΆ = {π β πΉ β£ (( β₯ β( β₯ β(πΏβπ))) = (πΏβπ) β§ ( β₯ β(πΏβπ)) β π)} & β’ π· = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} β β’ (πΊ β πΆ β (πΊ β π· β§ ( β₯ β(πΏβπΊ)) β π)) | ||
Theorem | lclkrslem1 40408* | 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 40409* | 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 40410* | 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 40404 proof. Do we achieve overall shortening by breaking them out as subtheorems? Or make lclkr 40404 a special case of this? (Contributed by NM, 29-Jan-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (LSubSpβπ·) & β’ πΆ = {π β πΉ β£ (( β₯ β( β₯ β(πΏβπ))) = (πΏβπ) β§ ( β₯ β(πΏβπ)) β π )} & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β πΆ β π) | ||
Theorem | lclkrs2 40411* | 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 40499. (Contributed by NM, 12-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (LSubSpβπ·) & β’ πΆ = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} & β’ π = {π β πΉ β£ (( β₯ β( β₯ β(πΏβπ))) = (πΏβπ) β§ ( β₯ β(πΏβπ)) β π)} & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β (π β π β§ π β πΆ)) | ||
Theorem | lcfrvalsnN 40412* | 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 40413 | Lemma for lcfr 40456. 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 40414 | Lemma for lcfr 40456. (Contributed by NM, 27-Feb-2015.) |
β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ Γ = (.rβπ) & β’ 0 = (0gβπ) & β’ πΌ = (invrβπ) & β’ πΉ = (LFnlβπ) & β’ π· = (LDualβπ) & β’ Β· = ( Β·π βπ·) & β’ β = (-gβπ·) & β’ (π β π β LVec) & β’ (π β πΈ β πΉ) & β’ (π β πΊ β πΉ) & β’ (π β π β π) & β’ (π β (πΊβπ) β 0 ) & β’ π» = (πΈ β (((πΌβ(πΊβπ)) Γ (πΈβπ)) Β· πΊ)) & β’ πΏ = (LKerβπ) β β’ (π β ((πΏβπΈ) β© (πΏβπΊ)) β (πΏβπ»)) | ||
Theorem | lcfrlem3 40415 | Lemma for lcfr 40456. (Contributed by NM, 27-Feb-2015.) |
β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ Γ = (.rβπ) & β’ 0 = (0gβπ) & β’ πΌ = (invrβπ) & β’ πΉ = (LFnlβπ) & β’ π· = (LDualβπ) & β’ Β· = ( Β·π βπ·) & β’ β = (-gβπ·) & β’ (π β π β LVec) & β’ (π β πΈ β πΉ) & β’ (π β πΊ β πΉ) & β’ (π β π β π) & β’ (π β (πΊβπ) β 0 ) & β’ π» = (πΈ β (((πΌβ(πΊβπ)) Γ (πΈβπ)) Β· πΊ)) & β’ πΏ = (LKerβπ) β β’ (π β π β (πΏβπ»)) | ||
Theorem | lcfrlem4 40416* | Lemma for lcfr 40456. (Contributed by NM, 10-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (LSubSpβπ·) & β’ πΈ = βͺ π β πΊ ( β₯ β(πΏβπ)) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΊ β π) & β’ (π β π β πΈ) β β’ (π β π β π) | ||
Theorem | lcfrlem5 40417* | Lemma for lcfr 40456. 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 40418* | Lemma for lcfr 40456. 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 40419* | Lemma for lcfr 40456. 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 40420* | Lemma for lcf1o 40422 and lcfr 40456. (Contributed by NM, 21-Feb-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (0gβπ·) & β’ πΆ = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} & β’ π½ = (π₯ β (π β { 0 }) β¦ (π£ β π β¦ (β©π β π βπ€ β ( β₯ β{π₯})π£ = (π€ + (π Β· π₯))))) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) β β’ (π β (π½βπ) = (π£ β π β¦ (β©π β π βπ€ β ( β₯ β{π})π£ = (π€ + (π Β· π))))) | ||
Theorem | lcfrlem9 40421* | Lemma for lcf1o 40422. (This part has undesirable $d's on π½ and π that we remove in lcf1o 40422.) 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 40422* | 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 40423* | Lemma for lcfr 40456. (Contributed by NM, 23-Feb-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (0gβπ·) & β’ πΆ = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} & β’ π½ = (π₯ β (π β { 0 }) β¦ (π£ β π β¦ (β©π β π βπ€ β ( β₯ β{π₯})π£ = (π€ + (π Β· π₯))))) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) β β’ (π β (π½βπ) β πΉ) | ||
Theorem | lcfrlem11 40424* | Lemma for lcfr 40456. (Contributed by NM, 23-Feb-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (0gβπ·) & β’ πΆ = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} & β’ π½ = (π₯ β (π β { 0 }) β¦ (π£ β π β¦ (β©π β π βπ€ β ( β₯ β{π₯})π£ = (π€ + (π Β· π₯))))) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) β β’ (π β (πΏβ(π½βπ)) = ( β₯ β{π})) | ||
Theorem | lcfrlem12N 40425* | Lemma for lcfr 40456. (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 40426* | Lemma for lcfr 40456. (Contributed by NM, 8-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (0gβπ·) & β’ πΆ = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} & β’ π½ = (π₯ β (π β { 0 }) β¦ (π£ β π β¦ (β©π β π βπ€ β ( β₯ β{π₯})π£ = (π€ + (π Β· π₯))))) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) β β’ (π β (π½βπ) β (πΆ β {π})) | ||
Theorem | lcfrlem14 40427* | Lemma for lcfr 40456. (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 40428* | Lemma for lcfr 40456. (Contributed by NM, 9-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (0gβπ·) & β’ πΆ = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} & β’ π½ = (π₯ β (π β { 0 }) β¦ (π£ β π β¦ (β©π β π βπ€ β ( β₯ β{π₯})π£ = (π€ + (π Β· π₯))))) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) β β’ (π β π β ( β₯ β(πΏβ(π½βπ)))) | ||
Theorem | lcfrlem16 40429* | Lemma for lcfr 40456. (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 40430 | Lemma for lcfr 40456. 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 40431 | Lemma for lcfr 40456. (Contributed by NM, 24-Feb-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ{π}) β (πβ{π})) β β’ (π β ( β₯ β{π, π}) = (( β₯ β{π}) β© ( β₯ β{π}))) | ||
Theorem | lcfrlem19 40432 | Lemma for lcfr 40456. (Contributed by NM, 11-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ{π}) β (πβ{π})) β β’ (π β (Β¬ π β ( β₯ β{(π + π)}) β¨ Β¬ π β ( β₯ β{(π + π)}))) | ||
Theorem | lcfrlem20 40433 | Lemma for lcfr 40456. (Contributed by NM, 11-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β Β¬ π β ( β₯ β{(π + π)})) β β’ (π β ((πβ{π, π}) β© ( β₯ β{(π + π)})) β π΄) | ||
Theorem | lcfrlem21 40434 | Lemma for lcfr 40456. (Contributed by NM, 11-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ{π}) β (πβ{π})) β β’ (π β ((πβ{π, π}) β© ( β₯ β{(π + π)})) β π΄) | ||
Theorem | lcfrlem22 40435 | Lemma for lcfr 40456. (Contributed by NM, 24-Feb-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ{π}) β (πβ{π})) & β’ π΅ = ((πβ{π, π}) β© ( β₯ β{(π + π)})) β β’ (π β π΅ β π΄) | ||
Theorem | lcfrlem23 40436 | Lemma for lcfr 40456. 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 40437* | Lemma for lcfr 40456. (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 40438* | Lemma for lcfr 40456. Special case of lcfrlem35 40448 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 40439* | Lemma for lcfr 40456. Special case of lcfrlem36 40449 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 40440* | Lemma for lcfr 40456. Special case of lcfrlem37 40450 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 40441* | Lemma for lcfr 40456. 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 40442* | Lemma for lcfr 40456. (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 40443* | Lemma for lcfr 40456. (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 40444* | Lemma for lcfr 40456. (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 40445* | Lemma for lcfr 40456. (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 40446* | Lemma for lcfr 40456. (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 40447* | Lemma for lcfr 40456. (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 40448* | Lemma for lcfr 40456. (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 40449* | Lemma for lcfr 40456. (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 40450* | Lemma for lcfr 40456. (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 40451* | Lemma for lcfr 40456. Combine lcfrlem27 40440 and lcfrlem37 40450. (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 40452* | Lemma for lcfr 40456. 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 40453* | Lemma for lcfr 40456. 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 40454* | Lemma for lcfr 40456. 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 40455* | Lemma for lcfr 40456. Eliminate nonzero condition. (Contributed by NM, 11-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ + = (+gβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (LSubSpβπ·) & β’ πΆ = {π β (LFnlβπ) β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} & β’ πΈ = βͺ π β πΊ ( β₯ β(πΏβπ)) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΊ β π) & β’ (π β πΊ β πΆ) & β’ (π β π β πΈ) & β’ (π β π β πΈ) β β’ (π β (π + π) β πΈ) | ||
Theorem | lcfr 40456* | 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 40457 | Extend class notation with vector space of functionals with closed kernels. |
class LCDual | ||
Definition | df-lcdual 40458* | Dual vector space of functionals with closed kernels. Note: we could also define this directly without mapd by using mapdrn 40520. TODO: see if it makes sense to go back and replace some of the LDual stuff with this. TODO: We could simplify df-mapd 40496 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 40459* | 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 40460* | Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ (π β (πΎ β π β§ π β π»)) β β’ (π β πΆ = (π· βΎs {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)})) | ||
Theorem | lcdval2 40461* | Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ β₯ = ((ocHβπΎ)βπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ (π β (πΎ β π β§ π β π»)) & β’ π΅ = {π β πΉ β£ ( β₯ β( β₯ β(πΏβπ))) = (πΏβπ)} β β’ (π β πΆ = (π· βΎs π΅)) | ||
Theorem | lcdlvec 40462 | 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 40463 | 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 40464* | 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 40465 | 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 40466 | 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 40467 | 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 40468 | Vector addition for the closed kernel vector space dual. (Contributed by NM, 10-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π· = (LDualβπ) & β’ + = (+gβπ·) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = (+gβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β β = + ) | ||
Theorem | lcdvaddval 40469 | 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 40470 | 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 40471 | 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 40472 | 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 40473 | 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 40474 | Scalar product for the closed kernel vector space dual. (Contributed by NM, 28-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π· = (LDualβπ) & β’ Β· = ( Β·π βπ·) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = ( Β·π βπΆ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β β = Β· ) | ||
Theorem | lcdvsval 40475 | 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 40476 | The scalar product operation value is a functional. (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = (BaseβπΆ) & β’ Β· = ( Β·π βπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π ) & β’ (π β πΊ β π) β β’ (π β (π Β· πΊ) β π) | ||
Theorem | lcdlssvscl 40477 | 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 40478 | 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 40479 | 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 40480 | 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 40481 | 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 40482 | 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 40483 | 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 40484 | 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 40485 | 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 40486 | 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 40487 | 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 40488 | 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 40489 | 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 40490* | 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 40491 | 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 40492 | 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 40493 | 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 40494 | 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 40495 | Extend class notation with projectivity from subspaces of vector space H to subspaces of functionals with closed kernels. |
class mapd | ||
Definition | df-mapd 40496* | Extend class notation with a one-to-one onto (mapd1o 40519), order-preserving (mapdord 40509) 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 40497* | 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βπΎ)βπ€))βπ)) β π )}))) | ||
Theorem | mapdfval 40498* | Projectivity from vector space H to dual space. (Contributed by NM, 25-Jan-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((mapdβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β π = (π β π β¦ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π )})) | ||
Theorem | mapdval 40499* | Value of projectivity from vector space H to dual space. (Contributed by NM, 27-Jan-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((mapdβπΎ)βπ) & β’ (π β (πΎ β π β§ π β π»)) & β’ (π β π β π) β β’ (π β (πβπ) = {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π)}) | ||
Theorem | mapdvalc 40500* | Value of projectivity from vector space H to dual space. (Contributed by NM, 27-Jan-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((mapdβπΎ)βπ) & β’ (π β (πΎ β π β§ π β π»)) & β’ (π β π β π) & β’ πΆ = {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} β β’ (π β (πβπ) = {π β πΆ β£ (πβ(πΏβπ)) β π}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |