![]() |
Metamath
Proof Explorer Theorem List (p. 247 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 | clmmcl 24601 | Closure of ring multiplication for a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βMod β§ π β πΎ β§ π β πΎ) β (π Β· π) β πΎ) | ||
Theorem | clmsubcl 24602 | Closure of ring subtraction for a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βMod β§ π β πΎ β§ π β πΎ) β (π β π) β πΎ) | ||
Theorem | lmhmclm 24603 | The domain of a linear operator is a subcomplex module iff the range is. (Contributed by Mario Carneiro, 21-Oct-2015.) |
β’ (πΉ β (π LMHom π) β (π β βMod β π β βMod)) | ||
Theorem | clmvscl 24604 | Closure of scalar product for a subcomplex module. Analogue of lmodvscl 20489. (Contributed by NM, 3-Nov-2006.) (Revised by AV, 28-Sep-2021.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βMod β§ π β πΎ β§ π β π) β (π Β· π) β π) | ||
Theorem | clmvsass 24605 | Associative law for scalar product. Analogue of lmodvsass 20497. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βMod β§ (π β πΎ β§ π β πΎ β§ π β π)) β ((π Β· π ) Β· π) = (π Β· (π Β· π))) | ||
Theorem | clmvscom 24606 | Commutative law for the scalar product. (Contributed by NM, 14-Feb-2008.) (Revised by AV, 7-Oct-2021.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βMod β§ (π β πΎ β§ π β πΎ β§ π β π)) β (π Β· (π Β· π)) = (π Β· (π Β· π))) | ||
Theorem | clmvsdir 24607 | Distributive law for scalar product (right-distributivity). (lmodvsdir 20496 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) & β’ + = (+gβπ) β β’ ((π β βMod β§ (π β πΎ β§ π β πΎ β§ π β π)) β ((π + π ) Β· π) = ((π Β· π) + (π Β· π))) | ||
Theorem | clmvsdi 24608 | Distributive law for scalar product (left-distributivity). (lmodvsdi 20495 analog.) (Contributed by NM, 3-Nov-2006.) (Revised by AV, 28-Sep-2021.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) & β’ + = (+gβπ) β β’ ((π β βMod β§ (π΄ β πΎ β§ π β π β§ π β π)) β (π΄ Β· (π + π)) = ((π΄ Β· π) + (π΄ Β· π))) | ||
Theorem | clmvs1 24609 | Scalar product with ring unity. (lmodvs1 20500 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) β β’ ((π β βMod β§ π β π) β (1 Β· π) = π) | ||
Theorem | clmvs2 24610 | A vector plus itself is two times the vector. (Contributed by NM, 1-Feb-2007.) (Revised by AV, 21-Sep-2021.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ + = (+gβπ) β β’ ((π β βMod β§ π΄ β π) β (π΄ + π΄) = (2 Β· π΄)) | ||
Theorem | clm0vs 24611 | Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (lmod0vs 20505 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπ) β β’ ((π β βMod β§ π β π) β (0 Β· π) = 0 ) | ||
Theorem | clmopfne 24612 | The (functionalized) operations of addition and multiplication by a scalar of a subcomplex module cannot be identical. (Contributed by NM, 31-May-2008.) (Revised by AV, 3-Oct-2021.) |
β’ Β· = ( Β·sf βπ) & β’ + = (+πβπ) β β’ (π β βMod β + β Β· ) | ||
Theorem | isclmp 24613* | The predicate "is a subcomplex module". (Contributed by NM, 31-May-2008.) (Revised by AV, 4-Oct-2021.) |
β’ Β· = ( Β·π βπ) & β’ + = (+gβπ) & β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ) β β’ (π β βMod β ((π β Grp β§ π = (βfld βΎs πΎ) β§ πΎ β (SubRingββfld)) β§ βπ₯ β π ((1 Β· π₯) = π₯ β§ βπ¦ β πΎ ((π¦ Β· π₯) β π β§ βπ§ β π (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§)) β§ βπ§ β πΎ (((π§ + π¦) Β· π₯) = ((π§ Β· π₯) + (π¦ Β· π₯)) β§ ((π§ Β· π¦) Β· π₯) = (π§ Β· (π¦ Β· π₯))))))) | ||
Theorem | isclmi0 24614* | Properties that determine a subcomplex module. (Contributed by NM, 5-Nov-2006.) (Revised by AV, 4-Oct-2021.) |
β’ Β· = ( Β·π βπ) & β’ + = (+gβπ) & β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ) & β’ π = (βfld βΎs πΎ) & β’ π β Grp & β’ πΎ β (SubRingββfld) & β’ (π₯ β π β (1 Β· π₯) = π₯) & β’ ((π¦ β πΎ β§ π₯ β π) β (π¦ Β· π₯) β π) & β’ ((π¦ β πΎ β§ π₯ β π β§ π§ β π) β (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§))) & β’ ((π¦ β πΎ β§ π§ β πΎ β§ π₯ β π) β ((π§ + π¦) Β· π₯) = ((π§ Β· π₯) + (π¦ Β· π₯))) & β’ ((π¦ β πΎ β§ π§ β πΎ β§ π₯ β π) β ((π§ Β· π¦) Β· π₯) = (π§ Β· (π¦ Β· π₯))) β β’ π β βMod | ||
Theorem | clmvneg1 24615 | Minus 1 times a vector is the negative of the vector. Equation 2 of [Kreyszig] p. 51. (lmodvneg1 20515 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ π = (Baseβπ) & β’ π = (invgβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) β β’ ((π β βMod β§ π β π) β (-1 Β· π) = (πβπ)) | ||
Theorem | clmvsneg 24616 | Multiplication of a vector by a negated scalar. (lmodvsneg 20516 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ π΅ = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ π = (invgβπ) & β’ πΎ = (BaseβπΉ) & β’ (π β π β βMod) & β’ (π β π β π΅) & β’ (π β π β πΎ) β β’ (π β (πβ(π Β· π)) = (-π Β· π)) | ||
Theorem | clmmulg 24617 | The group multiple function matches the scalar multiplication function. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ π = (Baseβπ) & β’ β = (.gβπ) & β’ Β· = ( Β·π βπ) β β’ ((π β βMod β§ π΄ β β€ β§ π΅ β π) β (π΄ β π΅) = (π΄ Β· π΅)) | ||
Theorem | clmsubdir 24618 | Scalar multiplication distributive law for subtraction. (lmodsubdir 20530 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ β = (-gβπ) & β’ (π β π β βMod) & β’ (π β π΄ β πΎ) & β’ (π β π΅ β πΎ) & β’ (π β π β π) β β’ (π β ((π΄ β π΅) Β· π) = ((π΄ Β· π) β (π΅ Β· π))) | ||
Theorem | clmpm1dir 24619 | Subtractive distributive law for the scalar product of a subcomplex module. (Contributed by NM, 31-Jul-2007.) (Revised by AV, 21-Sep-2021.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ + = (+gβπ) & β’ πΎ = (Baseβ(Scalarβπ)) β β’ ((π β βMod β§ (π΄ β πΎ β§ π΅ β πΎ β§ πΆ β π)) β ((π΄ β π΅) Β· πΆ) = ((π΄ Β· πΆ) + (-1 Β· (π΅ Β· πΆ)))) | ||
Theorem | clmnegneg 24620 | Double negative of a vector. (Contributed by NM, 6-Aug-2007.) (Revised by AV, 21-Sep-2021.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ + = (+gβπ) β β’ ((π β βMod β§ π΄ β π) β (-1 Β· (-1 Β· π΄)) = π΄) | ||
Theorem | clmnegsubdi2 24621 | Distribution of negative over vector subtraction. (Contributed by NM, 6-Aug-2007.) (Revised by AV, 29-Sep-2021.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ + = (+gβπ) β β’ ((π β βMod β§ π΄ β π β§ π΅ β π) β (-1 Β· (π΄ + (-1 Β· π΅))) = (π΅ + (-1 Β· π΄))) | ||
Theorem | clmsub4 24622 | Rearrangement of 4 terms in a mixed vector addition and subtraction. (Contributed by NM, 5-Aug-2007.) (Revised by AV, 29-Sep-2021.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ + = (+gβπ) β β’ ((π β βMod β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β ((π΄ + π΅) + (-1 Β· (πΆ + π·))) = ((π΄ + (-1 Β· πΆ)) + (π΅ + (-1 Β· π·)))) | ||
Theorem | clmvsrinv 24623 | A vector minus itself. (Contributed by NM, 4-Dec-2006.) (Revised by AV, 28-Sep-2021.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) β β’ ((π β βMod β§ π΄ β π) β (π΄ + (-1 Β· π΄)) = 0 ) | ||
Theorem | clmvslinv 24624 | Minus a vector plus itself. (Contributed by NM, 4-Dec-2006.) (Revised by AV, 28-Sep-2021.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) β β’ ((π β βMod β§ π΄ β π) β ((-1 Β· π΄) + π΄) = 0 ) | ||
Theorem | clmvsubval 24625 | Value of vector subtraction in terms of addition in a subcomplex module. Analogue of lmodvsubval2 20527. (Contributed by NM, 31-Mar-2014.) (Revised by AV, 7-Oct-2021.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) β β’ ((π β βMod β§ π΄ β π β§ π΅ β π) β (π΄ β π΅) = (π΄ + (-1 Β· π΅))) | ||
Theorem | clmvsubval2 24626 | Value of vector subtraction on a subcomplex module. (Contributed by Mario Carneiro, 19-Nov-2013.) (Revised by AV, 7-Oct-2021.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) β β’ ((π β βMod β§ π΄ β π β§ π΅ β π) β (π΄ β π΅) = ((-1 Β· π΅) + π΄)) | ||
Theorem | clmvz 24627 | Two ways to express the negative of a vector. (Contributed by NM, 29-Feb-2008.) (Revised by AV, 7-Oct-2021.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπ) β β’ ((π β βMod β§ π΄ β π) β ( 0 β π΄) = (-1 Β· π΄)) | ||
Theorem | zlmclm 24628 | The β€-module operation turns an arbitrary abelian group into a subcomplex module. (Contributed by Mario Carneiro, 30-Oct-2015.) |
β’ π = (β€ModβπΊ) β β’ (πΊ β Abel β π β βMod) | ||
Theorem | clmzlmvsca 24629 | The scalar product of a subcomplex module matches the scalar product of the derived β€-module, which implies, together with zlmbas 21068 and zlmplusg 21070, that any module over β€ is structure-equivalent to the canonical β€-module β€ModβπΊ. (Contributed by Mario Carneiro, 30-Oct-2015.) |
β’ π = (β€ModβπΊ) & β’ π = (BaseβπΊ) β β’ ((πΊ β βMod β§ (π΄ β β€ β§ π΅ β π)) β (π΄( Β·π βπΊ)π΅) = (π΄( Β·π βπ)π΅)) | ||
Theorem | nmoleub2lem 24630* | Lemma for nmoleub2a 24633 and similar theorems. (Contributed by Mario Carneiro, 19-Oct-2015.) |
β’ π = (π normOp π) & β’ π = (Baseβπ) & β’ πΏ = (normβπ) & β’ π = (normβπ) & β’ πΊ = (Scalarβπ) & β’ πΎ = (BaseβπΊ) & β’ (π β π β (NrmMod β© βMod)) & β’ (π β π β (NrmMod β© βMod)) & β’ (π β πΉ β (π LMHom π)) & β’ (π β π΄ β β*) & β’ (π β π β β+) & β’ ((π β§ βπ₯ β π (π β ((πβ(πΉβπ₯)) / π ) β€ π΄)) β 0 β€ π΄) & β’ ((((π β§ βπ₯ β π (π β ((πβ(πΉβπ₯)) / π ) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (πβ(πΉβπ¦)) β€ (π΄ Β· (πΏβπ¦))) & β’ ((π β§ π₯ β π) β (π β (πΏβπ₯) β€ π )) β β’ (π β ((πβπΉ) β€ π΄ β βπ₯ β π (π β ((πβ(πΉβπ₯)) / π ) β€ π΄))) | ||
Theorem | nmoleub2lem3 24631* | Lemma for nmoleub2a 24633 and similar theorems. (Contributed by Mario Carneiro, 19-Oct-2015.) (Proof shortened by AV, 29-Sep-2021.) |
β’ π = (π normOp π) & β’ π = (Baseβπ) & β’ πΏ = (normβπ) & β’ π = (normβπ) & β’ πΊ = (Scalarβπ) & β’ πΎ = (BaseβπΊ) & β’ (π β π β (NrmMod β© βMod)) & β’ (π β π β (NrmMod β© βMod)) & β’ (π β πΉ β (π LMHom π)) & β’ (π β π΄ β β*) & β’ (π β π β β+) & β’ (π β β β πΎ) & β’ Β· = ( Β·π βπ) & β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) & β’ (π β π΅ β π) & β’ (π β π΅ β (0gβπ)) & β’ (π β ((π Β· π΅) β π β ((πΏβ(π Β· π΅)) < π β ((πβ(πΉβ(π Β· π΅))) / π ) β€ π΄))) & β’ (π β Β¬ (πβ(πΉβπ΅)) β€ (π΄ Β· (πΏβπ΅))) β β’ Β¬ π | ||
Theorem | nmoleub2lem2 24632* | Lemma for nmoleub2a 24633 and similar theorems. (Contributed by Mario Carneiro, 19-Oct-2015.) |
β’ π = (π normOp π) & β’ π = (Baseβπ) & β’ πΏ = (normβπ) & β’ π = (normβπ) & β’ πΊ = (Scalarβπ) & β’ πΎ = (BaseβπΊ) & β’ (π β π β (NrmMod β© βMod)) & β’ (π β π β (NrmMod β© βMod)) & β’ (π β πΉ β (π LMHom π)) & β’ (π β π΄ β β*) & β’ (π β π β β+) & β’ (π β β β πΎ) & β’ (((πΏβπ₯) β β β§ π β β) β ((πΏβπ₯)ππ β (πΏβπ₯) β€ π )) & β’ (((πΏβπ₯) β β β§ π β β) β ((πΏβπ₯) < π β (πΏβπ₯)ππ )) β β’ (π β ((πβπΉ) β€ π΄ β βπ₯ β π ((πΏβπ₯)ππ β ((πβ(πΉβπ₯)) / π ) β€ π΄))) | ||
Theorem | nmoleub2a 24633* | The operator norm is the supremum of the value of a linear operator in the closed unit ball. (Contributed by Mario Carneiro, 19-Oct-2015.) |
β’ π = (π normOp π) & β’ π = (Baseβπ) & β’ πΏ = (normβπ) & β’ π = (normβπ) & β’ πΊ = (Scalarβπ) & β’ πΎ = (BaseβπΊ) & β’ (π β π β (NrmMod β© βMod)) & β’ (π β π β (NrmMod β© βMod)) & β’ (π β πΉ β (π LMHom π)) & β’ (π β π΄ β β*) & β’ (π β π β β+) & β’ (π β β β πΎ) β β’ (π β ((πβπΉ) β€ π΄ β βπ₯ β π ((πΏβπ₯) β€ π β ((πβ(πΉβπ₯)) / π ) β€ π΄))) | ||
Theorem | nmoleub2b 24634* | The operator norm is the supremum of the value of a linear operator in the open unit ball. (Contributed by Mario Carneiro, 19-Oct-2015.) |
β’ π = (π normOp π) & β’ π = (Baseβπ) & β’ πΏ = (normβπ) & β’ π = (normβπ) & β’ πΊ = (Scalarβπ) & β’ πΎ = (BaseβπΊ) & β’ (π β π β (NrmMod β© βMod)) & β’ (π β π β (NrmMod β© βMod)) & β’ (π β πΉ β (π LMHom π)) & β’ (π β π΄ β β*) & β’ (π β π β β+) & β’ (π β β β πΎ) β β’ (π β ((πβπΉ) β€ π΄ β βπ₯ β π ((πΏβπ₯) < π β ((πβ(πΉβπ₯)) / π ) β€ π΄))) | ||
Theorem | nmoleub3 24635* | The operator norm is the supremum of the value of a linear operator on the unit sphere. (Contributed by Mario Carneiro, 19-Oct-2015.) (Proof shortened by AV, 29-Sep-2021.) |
β’ π = (π normOp π) & β’ π = (Baseβπ) & β’ πΏ = (normβπ) & β’ π = (normβπ) & β’ πΊ = (Scalarβπ) & β’ πΎ = (BaseβπΊ) & β’ (π β π β (NrmMod β© βMod)) & β’ (π β π β (NrmMod β© βMod)) & β’ (π β πΉ β (π LMHom π)) & β’ (π β π΄ β β*) & β’ (π β π β β+) & β’ (π β 0 β€ π΄) & β’ (π β β β πΎ) β β’ (π β ((πβπΉ) β€ π΄ β βπ₯ β π ((πΏβπ₯) = π β ((πβ(πΉβπ₯)) / π ) β€ π΄))) | ||
Theorem | nmhmcn 24636 | A linear operator over a normed subcomplex module is bounded iff it is continuous. (Contributed by Mario Carneiro, 22-Oct-2015.) |
β’ π½ = (TopOpenβπ) & β’ πΎ = (TopOpenβπ) & β’ πΊ = (Scalarβπ) & β’ π΅ = (BaseβπΊ) β β’ ((π β (NrmMod β© βMod) β§ π β (NrmMod β© βMod) β§ β β π΅) β (πΉ β (π NMHom π) β (πΉ β (π LMHom π) β§ πΉ β (π½ Cn πΎ)))) | ||
Theorem | cmodscexp 24637 | The powers of i belong to the scalar subring of a subcomplex module if i belongs to the scalar subring . (Contributed by AV, 18-Oct-2021.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (((π β βMod β§ i β πΎ) β§ π β β) β (iβπ) β πΎ) | ||
Theorem | cmodscmulexp 24638 | The scalar product of a vector with powers of i belongs to the base set of a subcomplex module if the scalar subring of th subcomplex module contains i. (Contributed by AV, 18-Oct-2021.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) β β’ ((π β βMod β§ (i β πΎ β§ π΅ β π β§ π β β)) β ((iβπ) Β· π΅) β π) | ||
Usually, "complex vector spaces" are vector spaces over the field of the complex numbers, see for example the definition in [Roman] p. 36. In the setting of set.mm, it is convenient to consider collectively vector spaces on subfields of the field of complex numbers. We call these, "subcomplex vector spaces" and collect them in the class βVec defined in df-cvs 24640 and characterized in iscvs 24643. These include rational vector spaces (qcvs 24664), real vector spaces (recvs 24662) and complex vector spaces (cncvs 24661). This definition is analogous to the definition of subcomplex modules (and their class βMod), which are modules over subrings of the field of complex numbers. Note that ZZ-modules (that are roughly the same thing as Abelian groups, see zlmclm 24628) are subcomplex modules but are not subcomplex vector spaces (see zclmncvs 24665), because the ring ZZ is not a division ring (see zringndrg 21038). Since the field of complex numbers is commutative, so are its subrings, so there is no need to explicitly state "left module" or "left vector space" for subcomplex modules or vector spaces. | ||
Syntax | ccvs 24639 | Syntax for the class of subcomplex vector spaces. |
class βVec | ||
Definition | df-cvs 24640 | Define the class of subcomplex vector spaces, which are the subcomplex modules which are also vector spaces. (Contributed by Thierry Arnoux, 22-May-2019.) |
β’ βVec = (βMod β© LVec) | ||
Theorem | cvslvec 24641 | A subcomplex vector space is a (left) vector space. (Contributed by Thierry Arnoux, 22-May-2019.) |
β’ (π β π β βVec) β β’ (π β π β LVec) | ||
Theorem | cvsclm 24642 | A subcomplex vector space is a subcomplex module. (Contributed by Thierry Arnoux, 22-May-2019.) |
β’ (π β π β βVec) β β’ (π β π β βMod) | ||
Theorem | iscvs 24643 | A subcomplex vector space is a subcomplex module over a division ring. For example, the subcomplex modules over the rational or real or complex numbers are subcomplex vector spaces. (Contributed by AV, 4-Oct-2021.) |
β’ (π β βVec β (π β βMod β§ (Scalarβπ) β DivRing)) | ||
Theorem | iscvsp 24644* | The predicate "is a subcomplex vector space". (Contributed by NM, 31-May-2008.) (Revised by AV, 4-Oct-2021.) |
β’ Β· = ( Β·π βπ) & β’ + = (+gβπ) & β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ) β β’ (π β βVec β ((π β Grp β§ (π β DivRing β§ π = (βfld βΎs πΎ)) β§ πΎ β (SubRingββfld)) β§ βπ₯ β π ((1 Β· π₯) = π₯ β§ βπ¦ β πΎ ((π¦ Β· π₯) β π β§ βπ§ β π (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§)) β§ βπ§ β πΎ (((π§ + π¦) Β· π₯) = ((π§ Β· π₯) + (π¦ Β· π₯)) β§ ((π§ Β· π¦) Β· π₯) = (π§ Β· (π¦ Β· π₯))))))) | ||
Theorem | iscvsi 24645* | Properties that determine a subcomplex vector space. (Contributed by NM, 5-Nov-2006.) (Revised by AV, 4-Oct-2021.) |
β’ Β· = ( Β·π βπ) & β’ + = (+gβπ) & β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ) & β’ π β Grp & β’ π = (βfld βΎs πΎ) & β’ π β DivRing & β’ πΎ β (SubRingββfld) & β’ (π₯ β π β (1 Β· π₯) = π₯) & β’ ((π¦ β πΎ β§ π₯ β π) β (π¦ Β· π₯) β π) & β’ ((π¦ β πΎ β§ π₯ β π β§ π§ β π) β (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§))) & β’ ((π¦ β πΎ β§ π§ β πΎ β§ π₯ β π) β ((π§ + π¦) Β· π₯) = ((π§ Β· π₯) + (π¦ Β· π₯))) & β’ ((π¦ β πΎ β§ π§ β πΎ β§ π₯ β π) β ((π§ Β· π¦) Β· π₯) = (π§ Β· (π¦ Β· π₯))) β β’ π β βVec | ||
Theorem | cvsi 24646* | The properties of a subcomplex vector space, which is an Abelian group (i.e. the vectors, with the operation of vector addition) accompanied by a scalar multiplication operation on the field of complex numbers. (Contributed by NM, 3-Nov-2006.) (Revised by AV, 21-Sep-2021.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ π = (Baseβ(Scalarβπ)) & β’ β = ( Β·sf βπ) & β’ Β· = ( Β·π βπ) β β’ (π β βVec β (π β Abel β§ (π β β β§ β :(π Γ π)βΆπ) β§ βπ₯ β π ((1 Β· π₯) = π₯ β§ βπ¦ β π (βπ§ β π (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§)) β§ βπ§ β π (((π¦ + π§) Β· π₯) = ((π¦ Β· π₯) + (π§ Β· π₯)) β§ ((π¦ Β· π§) Β· π₯) = (π¦ Β· (π§ Β· π₯))))))) | ||
Theorem | cvsunit 24647 | Unit group of the scalar ring of a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (π β βVec β (πΎ β {0}) = (UnitβπΉ)) | ||
Theorem | cvsdiv 24648 | Division of the scalar ring of a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βVec β§ (π΄ β πΎ β§ π΅ β πΎ β§ π΅ β 0)) β (π΄ / π΅) = (π΄(/rβπΉ)π΅)) | ||
Theorem | cvsdivcl 24649 | The scalar field of a subcomplex vector space is closed under division. (Contributed by Thierry Arnoux, 22-May-2019.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βVec β§ (π΄ β πΎ β§ π΅ β πΎ β§ π΅ β 0)) β (π΄ / π΅) β πΎ) | ||
Theorem | cvsmuleqdivd 24650 | An equality involving ratios in a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ (π β π β βVec) & β’ (π β π΄ β πΎ) & β’ (π β π΅ β πΎ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π΄ β 0) & β’ (π β (π΄ Β· π) = (π΅ Β· π)) β β’ (π β π = ((π΅ / π΄) Β· π)) | ||
Theorem | cvsdiveqd 24651 | An equality involving ratios in a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ (π β π β βVec) & β’ (π β π΄ β πΎ) & β’ (π β π΅ β πΎ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π΄ β 0) & β’ (π β π΅ β 0) & β’ (π β π = ((π΄ / π΅) Β· π)) β β’ (π β ((π΅ / π΄) Β· π) = π) | ||
Theorem | cnlmodlem1 24652 | Lemma 1 for cnlmod 24656. (Contributed by AV, 20-Sep-2021.) |
β’ π = ({β¨(Baseβndx), ββ©, β¨(+gβndx), + β©} βͺ {β¨(Scalarβndx), βfldβ©, β¨( Β·π βndx), Β· β©}) β β’ (Baseβπ) = β | ||
Theorem | cnlmodlem2 24653 | Lemma 2 for cnlmod 24656. (Contributed by AV, 20-Sep-2021.) |
β’ π = ({β¨(Baseβndx), ββ©, β¨(+gβndx), + β©} βͺ {β¨(Scalarβndx), βfldβ©, β¨( Β·π βndx), Β· β©}) β β’ (+gβπ) = + | ||
Theorem | cnlmodlem3 24654 | Lemma 3 for cnlmod 24656. (Contributed by AV, 20-Sep-2021.) |
β’ π = ({β¨(Baseβndx), ββ©, β¨(+gβndx), + β©} βͺ {β¨(Scalarβndx), βfldβ©, β¨( Β·π βndx), Β· β©}) β β’ (Scalarβπ) = βfld | ||
Theorem | cnlmod4 24655 | Lemma 4 for cnlmod 24656. (Contributed by AV, 20-Sep-2021.) |
β’ π = ({β¨(Baseβndx), ββ©, β¨(+gβndx), + β©} βͺ {β¨(Scalarβndx), βfldβ©, β¨( Β·π βndx), Β· β©}) β β’ ( Β·π βπ) = Β· | ||
Theorem | cnlmod 24656 | The set of complex numbers is a left module over itself. The vector operation is +, and the scalar product is Β·. (Contributed by AV, 20-Sep-2021.) |
β’ π = ({β¨(Baseβndx), ββ©, β¨(+gβndx), + β©} βͺ {β¨(Scalarβndx), βfldβ©, β¨( Β·π βndx), Β· β©}) β β’ π β LMod | ||
Theorem | cnstrcvs 24657 | The set of complex numbers is a subcomplex vector space. The vector operation is +, and the scalar product is Β·. (Contributed by NM, 5-Nov-2006.) (Revised by AV, 20-Sep-2021.) |
β’ π = ({β¨(Baseβndx), ββ©, β¨(+gβndx), + β©} βͺ {β¨(Scalarβndx), βfldβ©, β¨( Β·π βndx), Β· β©}) β β’ π β βVec | ||
Theorem | cnrbas 24658 | The set of complex numbers is the base set of the complex left module of complex numbers. (Contributed by AV, 21-Sep-2021.) |
β’ πΆ = (ringLModββfld) β β’ (BaseβπΆ) = β | ||
Theorem | cnrlmod 24659 | The complex left module of complex numbers is a left module. The vector operation is +, and the scalar product is Β·. (Contributed by AV, 21-Sep-2021.) |
β’ πΆ = (ringLModββfld) β β’ πΆ β LMod | ||
Theorem | cnrlvec 24660 | The complex left module of complex numbers is a left vector space. The vector operation is +, and the scalar product is Β·. (Contributed by AV, 21-Sep-2021.) |
β’ πΆ = (ringLModββfld) β β’ πΆ β LVec | ||
Theorem | cncvs 24661 | The complex left module of complex numbers is a subcomplex vector space. The vector operation is +, and the scalar product is Β·. (Contributed by NM, 5-Nov-2006.) (Revised by AV, 21-Sep-2021.) |
β’ πΆ = (ringLModββfld) β β’ πΆ β βVec | ||
Theorem | recvs 24662 | The field of the real numbers as left module over itself is a subcomplex vector space. The vector operation is +, and the scalar product is Β·. (Contributed by AV, 22-Oct-2021.) (Proof shortened by SN, 23-Nov-2024.) |
β’ π = (ringLModββfld) β β’ π β βVec | ||
Theorem | recvsOLD 24663 | Obsolete version of recvs 24662 as of 23-Nov-2024. (Contributed by AV, 22-Oct-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π = (ringLModββfld) β β’ π β βVec | ||
Theorem | qcvs 24664 | The field of rational numbers as left module over itself is a subcomplex vector space. The vector operation is +, and the scalar product is Β·. (Contributed by AV, 22-Oct-2021.) |
β’ π = (ringLModβ(βfld βΎs β)) β β’ π β βVec | ||
Theorem | zclmncvs 24665 | The ring of integers as left module over itself is a subcomplex module, but not a subcomplex vector space. The vector operation is +, and the scalar product is Β·. (Contributed by AV, 22-Oct-2021.) |
β’ π = (ringLModββ€ring) β β’ (π β βMod β§ π β βVec) | ||
This section characterizes normed subcomplex vector spaces as subcomplex vector spaces which are also normed vector spaces (that is, normed groups with a positively homogeneous norm). For the moment, there is no need of a special token to represent their class, so we only use the characterization isncvsngp 24666. Most theorems for normed subcomplex vector spaces have a label containing "ncvs". The idiom π β (NrmVec β© βVec) is used in the following to say that π is a normed subcomplex vector space, i.e., a subcomplex vector space which is also a normed vector space. | ||
Theorem | isncvsngp 24666* | A normed subcomplex vector space is a subcomplex vector space which is a normed group with a positively homogeneous norm. (Contributed by NM, 5-Jun-2008.) (Revised by AV, 7-Oct-2021.) |
β’ π = (Baseβπ) & β’ π = (normβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (π β (NrmVec β© βVec) β (π β βVec β§ π β NrmGrp β§ βπ₯ β π βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯)))) | ||
Theorem | isncvsngpd 24667* | Properties that determine a normed subcomplex vector space. (Contributed by NM, 15-Apr-2007.) (Revised by AV, 7-Oct-2021.) |
β’ π = (Baseβπ) & β’ π = (normβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ (π β π β βVec) & β’ (π β π β NrmGrp) & β’ ((π β§ (π₯ β π β§ π β πΎ)) β (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯))) β β’ (π β π β (NrmVec β© βVec)) | ||
Theorem | ncvsi 24668* | The properties of a normed subcomplex vector space, which is a vector space accompanied by a norm. (Contributed by NM, 11-Nov-2006.) (Revised by AV, 7-Oct-2021.) |
β’ π = (Baseβπ) & β’ π = (normβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) β β’ (π β (NrmVec β© βVec) β (π β βVec β§ π:πβΆβ β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦)) β§ βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯))))) | ||
Theorem | ncvsprp 24669 | Proportionality property of the norm of a scalar product in a normed subcomplex vector space. (Contributed by NM, 11-Nov-2006.) (Revised by AV, 8-Oct-2021.) |
β’ π = (Baseβπ) & β’ π = (normβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β (NrmVec β© βVec) β§ π΄ β πΎ β§ π΅ β π) β (πβ(π΄ Β· π΅)) = ((absβπ΄) Β· (πβπ΅))) | ||
Theorem | ncvsge0 24670 | The norm of a scalar product with a nonnegative real. (Contributed by NM, 1-Jan-2008.) (Revised by AV, 8-Oct-2021.) |
β’ π = (Baseβπ) & β’ π = (normβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β (NrmVec β© βVec) β§ (π΄ β (πΎ β© β) β§ 0 β€ π΄) β§ π΅ β π) β (πβ(π΄ Β· π΅)) = (π΄ Β· (πβπ΅))) | ||
Theorem | ncvsm1 24671 | The norm of the opposite of a vector. (Contributed by NM, 28-Nov-2006.) (Revised by AV, 8-Oct-2021.) |
β’ π = (Baseβπ) & β’ π = (normβπ) & β’ Β· = ( Β·π βπ) β β’ ((π β (NrmVec β© βVec) β§ π΄ β π) β (πβ(-1 Β· π΄)) = (πβπ΄)) | ||
Theorem | ncvsdif 24672 | The norm of the difference between two vectors. (Contributed by NM, 1-Dec-2006.) (Revised by AV, 8-Oct-2021.) |
β’ π = (Baseβπ) & β’ π = (normβπ) & β’ Β· = ( Β·π βπ) & β’ + = (+gβπ) β β’ ((π β (NrmVec β© βVec) β§ π΄ β π β§ π΅ β π) β (πβ(π΄ + (-1 Β· π΅))) = (πβ(π΅ + (-1 Β· π΄)))) | ||
Theorem | ncvspi 24673 | The norm of a vector plus the imaginary scalar product of another. (Contributed by NM, 2-Feb-2007.) (Revised by AV, 8-Oct-2021.) |
β’ π = (Baseβπ) & β’ π = (normβπ) & β’ Β· = ( Β·π βπ) & β’ + = (+gβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β (NrmVec β© βVec) β§ (π΄ β π β§ π΅ β π) β§ i β πΎ) β (πβ(π΄ + (i Β· π΅))) = (πβ(π΅ + (-i Β· π΄)))) | ||
Theorem | ncvs1 24674 | From any nonzero vector of a normed subcomplex vector space, construct a collinear vector whose norm is one. (Contributed by NM, 6-Dec-2007.) (Revised by AV, 8-Oct-2021.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) & β’ 0 = (0gβπΊ) & β’ Β· = ( Β·π βπΊ) & β’ πΉ = (ScalarβπΊ) & β’ πΎ = (BaseβπΉ) β β’ ((πΊ β (NrmVec β© βVec) β§ (π΄ β π β§ π΄ β 0 ) β§ (1 / (πβπ΄)) β πΎ) β (πβ((1 / (πβπ΄)) Β· π΄)) = 1) | ||
Theorem | cnrnvc 24675 | The module of complex numbers (as a module over itself) is a normed vector space over itself. The vector operation is +, and the scalar product is Β·, and the norm function is abs. (Contributed by AV, 9-Oct-2021.) |
β’ πΆ = (ringLModββfld) β β’ πΆ β NrmVec | ||
Theorem | cnncvs 24676 | The module of complex numbers (as a module over itself) is a normed subcomplex vector space. The vector operation is +, the scalar product is Β·, and the norm is abs (see cnnm 24677) . (Contributed by Steve Rodriguez, 3-Dec-2006.) (Revised by AV, 9-Oct-2021.) |
β’ πΆ = (ringLModββfld) β β’ πΆ β (NrmVec β© βVec) | ||
Theorem | cnnm 24677 | The norm of the normed subcomplex vector space of complex numbers is the absolute value. (Contributed by NM, 12-Jan-2008.) (Revised by AV, 9-Oct-2021.) |
β’ πΆ = (ringLModββfld) β β’ (normβπΆ) = abs | ||
Theorem | ncvspds 24678 | Value of the distance function in terms of the norm of a normed subcomplex vector space. Equation 1 of [Kreyszig] p. 59. (Contributed by NM, 28-Nov-2006.) (Revised by AV, 13-Oct-2021.) |
β’ π = (normβπΊ) & β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ π· = (distβπΊ) & β’ Β· = ( Β·π βπΊ) β β’ ((πΊ β (NrmVec β© βVec) β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) = (πβ(π΄ + (-1 Β· π΅)))) | ||
Theorem | cnindmet 24679 | The metric induced on the complex numbers. cnmet 24288 proves that it is a metric. The induced metric is identical with the original metric on the complex numbers, see cnfldds 20954 and also cnmet 24288. (Contributed by Steve Rodriguez, 5-Dec-2006.) (Revised by AV, 17-Oct-2021.) |
β’ π = (βfld toNrmGrp abs) β β’ (distβπ) = (abs β β ) | ||
Theorem | cnncvsaddassdemo 24680 | Derive the associative law for complex number addition addass 11197 to demonstrate the use of the properties of a normed subcomplex vector space for the complex numbers. (Contributed by NM, 12-Jan-2008.) (Revised by AV, 9-Oct-2021.) (Proof modification is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + π΅) + πΆ) = (π΄ + (π΅ + πΆ))) | ||
Theorem | cnncvsmulassdemo 24681 | Derive the associative law for complex number multiplication mulass 11198 interpreted as scalar multiplication to demonstrate the use of the properties of a normed subcomplex vector space for the complex numbers. (Contributed by AV, 9-Oct-2021.) (Proof modification is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ Β· π΅) Β· πΆ) = (π΄ Β· (π΅ Β· πΆ))) | ||
Theorem | cnncvsabsnegdemo 24682 | Derive the absolute value of a negative complex number absneg 15224 to demonstrate the use of the properties of a normed subcomplex vector space for the complex numbers. (Contributed by AV, 9-Oct-2021.) (Proof modification is discouraged.) |
β’ (π΄ β β β (absβ-π΄) = (absβπ΄)) | ||
Syntax | ccph 24683 | Extend class notation with the class of subcomplex pre-Hilbert spaces. |
class βPreHil | ||
Syntax | ctcph 24684 | Function to put a norm on a pre-Hilbert space. |
class toβPreHil | ||
Definition | df-cph 24685* | Define the class of subcomplex pre-Hilbert spaces. By restricting the scalar field to a subfield of βfld closed under square roots of nonnegative reals, we have enough structure to define a norm, with the associated connection to a metric and topology. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ βPreHil = {π€ β (PreHil β© NrmMod) β£ [(Scalarβπ€) / π][(Baseβπ) / π](π = (βfld βΎs π) β§ (β β (π β© (0[,)+β))) β π β§ (normβπ€) = (π₯ β (Baseβπ€) β¦ (ββ(π₯(Β·πβπ€)π₯))))} | ||
Definition | df-tcph 24686* | Define a function to augment a pre-Hilbert space with a norm. No extra parameters are needed, but some conditions must be satisfied to ensure that this in fact creates a normed subcomplex pre-Hilbert space (see tcphcph 24754). (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ toβPreHil = (π€ β V β¦ (π€ toNrmGrp (π₯ β (Baseβπ€) β¦ (ββ(π₯(Β·πβπ€)π₯))))) | ||
Theorem | iscph 24687* | A subcomplex pre-Hilbert space is exactly a pre-Hilbert space over a subfield of the field of complex numbers closed under square roots of nonnegative reals equipped with a norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) & β’ π = (normβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (π β βPreHil β ((π β PreHil β§ π β NrmMod β§ πΉ = (βfld βΎs πΎ)) β§ (β β (πΎ β© (0[,)+β))) β πΎ β§ π = (π₯ β π β¦ (ββ(π₯ , π₯))))) | ||
Theorem | cphphl 24688 | A subcomplex pre-Hilbert space is a pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ (π β βPreHil β π β PreHil) | ||
Theorem | cphnlm 24689 | A subcomplex pre-Hilbert space is a normed module. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ (π β βPreHil β π β NrmMod) | ||
Theorem | cphngp 24690 | A subcomplex pre-Hilbert space is a normed group. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ (π β βPreHil β π β NrmGrp) | ||
Theorem | cphlmod 24691 | A subcomplex pre-Hilbert space is a left module. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ (π β βPreHil β π β LMod) | ||
Theorem | cphlvec 24692 | A subcomplex pre-Hilbert space is a left vector space. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ (π β βPreHil β π β LVec) | ||
Theorem | cphnvc 24693 | A subcomplex pre-Hilbert space is a normed vector space. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ (π β βPreHil β π β NrmVec) | ||
Theorem | cphsubrglem 24694 | Lemma for cphsubrg 24697. (Contributed by Mario Carneiro, 9-Oct-2015.) |
β’ πΎ = (BaseβπΉ) & β’ (π β πΉ = (βfld βΎs π΄)) & β’ (π β πΉ β DivRing) β β’ (π β (πΉ = (βfld βΎs πΎ) β§ πΎ = (π΄ β© β) β§ πΎ β (SubRingββfld))) | ||
Theorem | cphreccllem 24695 | Lemma for cphreccl 24698. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΎ = (BaseβπΉ) & β’ (π β πΉ = (βfld βΎs π΄)) & β’ (π β πΉ β DivRing) β β’ ((π β§ π β πΎ β§ π β 0) β (1 / π) β πΎ) | ||
Theorem | cphsca 24696 | A subcomplex pre-Hilbert space is a vector space over a subfield of βfld. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (π β βPreHil β πΉ = (βfld βΎs πΎ)) | ||
Theorem | cphsubrg 24697 | The scalar field of a subcomplex pre-Hilbert space is a subring of βfld. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (π β βPreHil β πΎ β (SubRingββfld)) | ||
Theorem | cphreccl 24698 | The scalar field of a subcomplex pre-Hilbert space is closed under reciprocal. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βPreHil β§ π΄ β πΎ β§ π΄ β 0) β (1 / π΄) β πΎ) | ||
Theorem | cphdivcl 24699 | The scalar field of a subcomplex pre-Hilbert space is closed under reciprocal. (Contributed by Mario Carneiro, 11-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βPreHil β§ (π΄ β πΎ β§ π΅ β πΎ β§ π΅ β 0)) β (π΄ / π΅) β πΎ) | ||
Theorem | cphcjcl 24700 | The scalar field of a subcomplex pre-Hilbert space is closed under conjugation. (Contributed by Mario Carneiro, 11-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βPreHil β§ π΄ β πΎ) β (ββπ΄) β πΎ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |