![]() |
Metamath
Proof Explorer Theorem List (p. 250 of 481) | < 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-30640) |
![]() (30641-32163) |
![]() (32164-48040) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pi1inv 24901* | An inverse in the fundamental group. (Contributed by Mario Carneiro, 12-Feb-2015.) (Revised by Mario Carneiro, 10-Aug-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ π = (invgβπΊ) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ (π β πΉ β (II Cn π½)) & β’ (π β (πΉβ0) = π) & β’ (π β (πΉβ1) = π) & β’ πΌ = (π₯ β (0[,]1) β¦ (πΉβ(1 β π₯))) β β’ (π β (πβ[πΉ]( βphβπ½)) = [πΌ]( βphβπ½)) | ||
Theorem | pi1xfrf 24902* | Functionality of the loop transfer function on the equivalence class of a path. (Contributed by Mario Carneiro, 23-Dec-2016.) |
β’ π = (π½ Ο1 (πΉβ0)) & β’ π = (π½ Ο1 (πΉβ1)) & β’ π΅ = (Baseβπ) & β’ πΊ = ran (π β βͺ π΅ β¦ β¨[π]( βphβπ½), [(πΌ(*πβπ½)(π(*πβπ½)πΉ))]( βphβπ½)β©) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (II Cn π½)) & β’ (π β πΌ β (II Cn π½)) & β’ (π β (πΉβ1) = (πΌβ0)) & β’ (π β (πΌβ1) = (πΉβ0)) β β’ (π β πΊ:π΅βΆ(Baseβπ)) | ||
Theorem | pi1xfrval 24903* | The value of the loop transfer function on the equivalence class of a path. (Contributed by Mario Carneiro, 12-Feb-2015.) (Revised by Mario Carneiro, 23-Dec-2016.) |
β’ π = (π½ Ο1 (πΉβ0)) & β’ π = (π½ Ο1 (πΉβ1)) & β’ π΅ = (Baseβπ) & β’ πΊ = ran (π β βͺ π΅ β¦ β¨[π]( βphβπ½), [(πΌ(*πβπ½)(π(*πβπ½)πΉ))]( βphβπ½)β©) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (II Cn π½)) & β’ (π β πΌ β (II Cn π½)) & β’ (π β (πΉβ1) = (πΌβ0)) & β’ (π β (πΌβ1) = (πΉβ0)) & β’ (π β π΄ β βͺ π΅) β β’ (π β (πΊβ[π΄]( βphβπ½)) = [(πΌ(*πβπ½)(π΄(*πβπ½)πΉ))]( βphβπ½)) | ||
Theorem | pi1xfr 24904* | Given a path πΉ and its inverse πΌ between two basepoints, there is an induced group homomorphism on the fundamental groups. (Contributed by Mario Carneiro, 12-Feb-2015.) |
β’ π = (π½ Ο1 (πΉβ0)) & β’ π = (π½ Ο1 (πΉβ1)) & β’ π΅ = (Baseβπ) & β’ πΊ = ran (π β βͺ π΅ β¦ β¨[π]( βphβπ½), [(πΌ(*πβπ½)(π(*πβπ½)πΉ))]( βphβπ½)β©) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (II Cn π½)) & β’ πΌ = (π₯ β (0[,]1) β¦ (πΉβ(1 β π₯))) β β’ (π β πΊ β (π GrpHom π)) | ||
Theorem | pi1xfrcnvlem 24905* | Given a path πΉ between two basepoints, there is an induced group homomorphism on the fundamental groups. (Contributed by Mario Carneiro, 12-Feb-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.) |
β’ π = (π½ Ο1 (πΉβ0)) & β’ π = (π½ Ο1 (πΉβ1)) & β’ π΅ = (Baseβπ) & β’ πΊ = ran (π β βͺ π΅ β¦ β¨[π]( βphβπ½), [(πΌ(*πβπ½)(π(*πβπ½)πΉ))]( βphβπ½)β©) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (II Cn π½)) & β’ πΌ = (π₯ β (0[,]1) β¦ (πΉβ(1 β π₯))) & β’ π» = ran (β β βͺ (Baseβπ) β¦ β¨[β]( βphβπ½), [(πΉ(*πβπ½)(β(*πβπ½)πΌ))]( βphβπ½)β©) β β’ (π β β‘πΊ β π») | ||
Theorem | pi1xfrcnv 24906* | Given a path πΉ between two basepoints, there is an induced group homomorphism on the fundamental groups. (Contributed by Mario Carneiro, 12-Feb-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.) |
β’ π = (π½ Ο1 (πΉβ0)) & β’ π = (π½ Ο1 (πΉβ1)) & β’ π΅ = (Baseβπ) & β’ πΊ = ran (π β βͺ π΅ β¦ β¨[π]( βphβπ½), [(πΌ(*πβπ½)(π(*πβπ½)πΉ))]( βphβπ½)β©) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (II Cn π½)) & β’ πΌ = (π₯ β (0[,]1) β¦ (πΉβ(1 β π₯))) & β’ π» = ran (β β βͺ (Baseβπ) β¦ β¨[β]( βphβπ½), [(πΉ(*πβπ½)(β(*πβπ½)πΌ))]( βphβπ½)β©) β β’ (π β (β‘πΊ = π» β§ β‘πΊ β (π GrpHom π))) | ||
Theorem | pi1xfrgim 24907* | The mapping πΊ between fundamental groups is an isomorphism. (Contributed by Mario Carneiro, 12-Feb-2015.) |
β’ π = (π½ Ο1 (πΉβ0)) & β’ π = (π½ Ο1 (πΉβ1)) & β’ π΅ = (Baseβπ) & β’ πΊ = ran (π β βͺ π΅ β¦ β¨[π]( βphβπ½), [(πΌ(*πβπ½)(π(*πβπ½)πΉ))]( βphβπ½)β©) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (II Cn π½)) & β’ πΌ = (π₯ β (0[,]1) β¦ (πΉβ(1 β π₯))) β β’ (π β πΊ β (π GrpIso π)) | ||
Theorem | pi1cof 24908* | Functionality of the loop transfer function on the equivalence class of a path. (Contributed by Mario Carneiro, 23-Dec-2016.) |
β’ π = (π½ Ο1 π΄) & β’ π = (πΎ Ο1 π΅) & β’ π = (Baseβπ) & β’ πΊ = ran (π β βͺ π β¦ β¨[π]( βphβπ½), [(πΉ β π)]( βphβπΎ)β©) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β π΄ β π) & β’ (π β (πΉβπ΄) = π΅) β β’ (π β πΊ:πβΆ(Baseβπ)) | ||
Theorem | pi1coval 24909* | The value of the loop transfer function on the equivalence class of a path. (Contributed by Mario Carneiro, 10-Aug-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.) |
β’ π = (π½ Ο1 π΄) & β’ π = (πΎ Ο1 π΅) & β’ π = (Baseβπ) & β’ πΊ = ran (π β βͺ π β¦ β¨[π]( βphβπ½), [(πΉ β π)]( βphβπΎ)β©) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β π΄ β π) & β’ (π β (πΉβπ΄) = π΅) β β’ ((π β§ π β βͺ π) β (πΊβ[π]( βphβπ½)) = [(πΉ β π)]( βphβπΎ)) | ||
Theorem | pi1coghm 24910* | The mapping πΊ between fundamental groups is a group homomorphism. (Contributed by Mario Carneiro, 10-Aug-2015.) (Revised by Mario Carneiro, 23-Dec-2016.) |
β’ π = (π½ Ο1 π΄) & β’ π = (πΎ Ο1 π΅) & β’ π = (Baseβπ) & β’ πΊ = ran (π β βͺ π β¦ β¨[π]( βphβπ½), [(πΉ β π)]( βphβπΎ)β©) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β π΄ β π) & β’ (π β (πΉβπ΄) = π΅) β β’ (π β πΊ β (π GrpHom π)) | ||
Syntax | cclm 24911 | Syntax for the class of subcomplex modules. |
class βMod | ||
Definition | df-clm 24912* | Define the class of subcomplex modules, which are left modules over a subring of the field of complex numbers βfld, which allows to use the complex addition, multiplication, etc. in theorems about subcomplex modules. Since the field of complex numbers is commutative and so are its subrings (see subrgcrng 20467), left modules over such subrings are the same as right modules, see rmodislmod 20766. Therefore, we drop the word "left" from "subcomplex left module". (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ βMod = {π€ β LMod β£ [(Scalarβπ€) / π][(Baseβπ) / π](π = (βfld βΎs π) β§ π β (SubRingββfld))} | ||
Theorem | isclm 24913 | A subcomplex module is a left module over a subring of the field of complex numbers. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (π β βMod β (π β LMod β§ πΉ = (βfld βΎs πΎ) β§ πΎ β (SubRingββfld))) | ||
Theorem | clmsca 24914 | The ring of scalars πΉ of a subcomplex module is the restriction of the field of complex numbers to the base set of πΉ. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (π β βMod β πΉ = (βfld βΎs πΎ)) | ||
Theorem | clmsubrg 24915 | The base set of the ring of scalars of a subcomplex module is the base set of a subring of the field of complex numbers. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (π β βMod β πΎ β (SubRingββfld)) | ||
Theorem | clmlmod 24916 | A subcomplex module is a left module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ (π β βMod β π β LMod) | ||
Theorem | clmgrp 24917 | A subcomplex module is an additive group. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ (π β βMod β π β Grp) | ||
Theorem | clmabl 24918 | A subcomplex module is an abelian group. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ (π β βMod β π β Abel) | ||
Theorem | clmring 24919 | The scalar ring of a subcomplex module is a ring. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β βMod β πΉ β Ring) | ||
Theorem | clmfgrp 24920 | The scalar ring of a subcomplex module is a group. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β βMod β πΉ β Grp) | ||
Theorem | clm0 24921 | The zero of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β βMod β 0 = (0gβπΉ)) | ||
Theorem | clm1 24922 | The identity of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β βMod β 1 = (1rβπΉ)) | ||
Theorem | clmadd 24923 | The addition of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β βMod β + = (+gβπΉ)) | ||
Theorem | clmmul 24924 | The multiplication of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β βMod β Β· = (.rβπΉ)) | ||
Theorem | clmcj 24925 | The conjugation of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β βMod β β = (*πβπΉ)) | ||
Theorem | isclmi 24926 | Reverse direction of isclm 24913. (Contributed by Mario Carneiro, 30-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ ((π β LMod β§ πΉ = (βfld βΎs πΎ) β§ πΎ β (SubRingββfld)) β π β βMod) | ||
Theorem | clmzss 24927 | The scalar ring of a subcomplex module contains the integers. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (π β βMod β β€ β πΎ) | ||
Theorem | clmsscn 24928 | The scalar ring of a subcomplex module is a subset of the complex numbers. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (π β βMod β πΎ β β) | ||
Theorem | clmsub 24929 | Subtraction in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βMod β§ π΄ β πΎ β§ π΅ β πΎ) β (π΄ β π΅) = (π΄(-gβπΉ)π΅)) | ||
Theorem | clmneg 24930 | Negation in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βMod β§ π΄ β πΎ) β -π΄ = ((invgβπΉ)βπ΄)) | ||
Theorem | clmneg1 24931 | Minus one is in the scalar ring of a subcomplex module. (Contributed by AV, 28-Sep-2021.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (π β βMod β -1 β πΎ) | ||
Theorem | clmabs 24932 | Norm in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βMod β§ π΄ β πΎ) β (absβπ΄) = ((normβπΉ)βπ΄)) | ||
Theorem | clmacl 24933 | Closure of ring addition for a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βMod β§ π β πΎ β§ π β πΎ) β (π + π) β πΎ) | ||
Theorem | clmmcl 24934 | Closure of ring multiplication for a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βMod β§ π β πΎ β§ π β πΎ) β (π Β· π) β πΎ) | ||
Theorem | clmsubcl 24935 | Closure of ring subtraction for a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βMod β§ π β πΎ β§ π β πΎ) β (π β π) β πΎ) | ||
Theorem | lmhmclm 24936 | 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 24937 | Closure of scalar product for a subcomplex module. Analogue of lmodvscl 20714. (Contributed by NM, 3-Nov-2006.) (Revised by AV, 28-Sep-2021.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βMod β§ π β πΎ β§ π β π) β (π Β· π) β π) | ||
Theorem | clmvsass 24938 | Associative law for scalar product. Analogue of lmodvsass 20723. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βMod β§ (π β πΎ β§ π β πΎ β§ π β π)) β ((π Β· π ) Β· π) = (π Β· (π Β· π))) | ||
Theorem | clmvscom 24939 | Commutative law for the scalar product. (Contributed by NM, 14-Feb-2008.) (Revised by AV, 7-Oct-2021.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βMod β§ (π β πΎ β§ π β πΎ β§ π β π)) β (π Β· (π Β· π)) = (π Β· (π Β· π))) | ||
Theorem | clmvsdir 24940 | Distributive law for scalar product (right-distributivity). (lmodvsdir 20722 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) & β’ + = (+gβπ) β β’ ((π β βMod β§ (π β πΎ β§ π β πΎ β§ π β π)) β ((π + π ) Β· π) = ((π Β· π) + (π Β· π))) | ||
Theorem | clmvsdi 24941 | Distributive law for scalar product (left-distributivity). (lmodvsdi 20721 analog.) (Contributed by NM, 3-Nov-2006.) (Revised by AV, 28-Sep-2021.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) & β’ + = (+gβπ) β β’ ((π β βMod β§ (π΄ β πΎ β§ π β π β§ π β π)) β (π΄ Β· (π + π)) = ((π΄ Β· π) + (π΄ Β· π))) | ||
Theorem | clmvs1 24942 | Scalar product with ring unity. (lmodvs1 20726 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) β β’ ((π β βMod β§ π β π) β (1 Β· π) = π) | ||
Theorem | clmvs2 24943 | 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 24944 | Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (lmod0vs 20731 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπ) β β’ ((π β βMod β§ π β π) β (0 Β· π) = 0 ) | ||
Theorem | clmopfne 24945 | 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 24946* | 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 24947* | 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 24948 | Minus 1 times a vector is the negative of the vector. Equation 2 of [Kreyszig] p. 51. (lmodvneg1 20741 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ π = (Baseβπ) & β’ π = (invgβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) β β’ ((π β βMod β§ π β π) β (-1 Β· π) = (πβπ)) | ||
Theorem | clmvsneg 24949 | Multiplication of a vector by a negated scalar. (lmodvsneg 20742 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ π΅ = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ π = (invgβπ) & β’ πΎ = (BaseβπΉ) & β’ (π β π β βMod) & β’ (π β π β π΅) & β’ (π β π β πΎ) β β’ (π β (πβ(π Β· π)) = (-π Β· π)) | ||
Theorem | clmmulg 24950 | The group multiple function matches the scalar multiplication function. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ π = (Baseβπ) & β’ β = (.gβπ) & β’ Β· = ( Β·π βπ) β β’ ((π β βMod β§ π΄ β β€ β§ π΅ β π) β (π΄ β π΅) = (π΄ Β· π΅)) | ||
Theorem | clmsubdir 24951 | Scalar multiplication distributive law for subtraction. (lmodsubdir 20756 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ β = (-gβπ) & β’ (π β π β βMod) & β’ (π β π΄ β πΎ) & β’ (π β π΅ β πΎ) & β’ (π β π β π) β β’ (π β ((π΄ β π΅) Β· π) = ((π΄ Β· π) β (π΅ Β· π))) | ||
Theorem | clmpm1dir 24952 | 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 24953 | Double negative of a vector. (Contributed by NM, 6-Aug-2007.) (Revised by AV, 21-Sep-2021.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ + = (+gβπ) β β’ ((π β βMod β§ π΄ β π) β (-1 Β· (-1 Β· π΄)) = π΄) | ||
Theorem | clmnegsubdi2 24954 | 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 24955 | 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 24956 | 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 24957 | 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 24958 | Value of vector subtraction in terms of addition in a subcomplex module. Analogue of lmodvsubval2 20753. (Contributed by NM, 31-Mar-2014.) (Revised by AV, 7-Oct-2021.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) β β’ ((π β βMod β§ π΄ β π β§ π΅ β π) β (π΄ β π΅) = (π΄ + (-1 Β· π΅))) | ||
Theorem | clmvsubval2 24959 | 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 24960 | 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 24961 | The β€-module operation turns an arbitrary abelian group into a subcomplex module. (Contributed by Mario Carneiro, 30-Oct-2015.) |
β’ π = (β€ModβπΊ) β β’ (πΊ β Abel β π β βMod) | ||
Theorem | clmzlmvsca 24962 | The scalar product of a subcomplex module matches the scalar product of the derived β€-module, which implies, together with zlmbas 21373 and zlmplusg 21375, that any module over β€ is structure-equivalent to the canonical β€-module β€ModβπΊ. (Contributed by Mario Carneiro, 30-Oct-2015.) |
β’ π = (β€ModβπΊ) & β’ π = (BaseβπΊ) β β’ ((πΊ β βMod β§ (π΄ β β€ β§ π΅ β π)) β (π΄( Β·π βπΊ)π΅) = (π΄( Β·π βπ)π΅)) | ||
Theorem | nmoleub2lem 24963* | Lemma for nmoleub2a 24966 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 24964* | Lemma for nmoleub2a 24966 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 24965* | Lemma for nmoleub2a 24966 and similar theorems. (Contributed by Mario Carneiro, 19-Oct-2015.) |
β’ π = (π normOp π) & β’ π = (Baseβπ) & β’ πΏ = (normβπ) & β’ π = (normβπ) & β’ πΊ = (Scalarβπ) & β’ πΎ = (BaseβπΊ) & β’ (π β π β (NrmMod β© βMod)) & β’ (π β π β (NrmMod β© βMod)) & β’ (π β πΉ β (π LMHom π)) & β’ (π β π΄ β β*) & β’ (π β π β β+) & β’ (π β β β πΎ) & β’ (((πΏβπ₯) β β β§ π β β) β ((πΏβπ₯)ππ β (πΏβπ₯) β€ π )) & β’ (((πΏβπ₯) β β β§ π β β) β ((πΏβπ₯) < π β (πΏβπ₯)ππ )) β β’ (π β ((πβπΉ) β€ π΄ β βπ₯ β π ((πΏβπ₯)ππ β ((πβ(πΉβπ₯)) / π ) β€ π΄))) | ||
Theorem | nmoleub2a 24966* | 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 24967* | 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 24968* | 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 24969 | 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 24970 | 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 24971 | 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 24973 and characterized in iscvs 24976. These include rational vector spaces (qcvs 24997), real vector spaces (recvs 24995) and complex vector spaces (cncvs 24994). 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 24961) are subcomplex modules but are not subcomplex vector spaces (see zclmncvs 24998), because the ring ZZ is not a division ring (see zringndrg 21323). 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 24972 | Syntax for the class of subcomplex vector spaces. |
class βVec | ||
Definition | df-cvs 24973 | 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 24974 | A subcomplex vector space is a (left) vector space. (Contributed by Thierry Arnoux, 22-May-2019.) |
β’ (π β π β βVec) β β’ (π β π β LVec) | ||
Theorem | cvsclm 24975 | A subcomplex vector space is a subcomplex module. (Contributed by Thierry Arnoux, 22-May-2019.) |
β’ (π β π β βVec) β β’ (π β π β βMod) | ||
Theorem | iscvs 24976 | 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 24977* | 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 24978* | 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 24979* | 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 24980 | 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 24981 | Division of the scalar ring of a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βVec β§ (π΄ β πΎ β§ π΅ β πΎ β§ π΅ β 0)) β (π΄ / π΅) = (π΄(/rβπΉ)π΅)) | ||
Theorem | cvsdivcl 24982 | 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 24983 | An equality involving ratios in a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ (π β π β βVec) & β’ (π β π΄ β πΎ) & β’ (π β π΅ β πΎ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π΄ β 0) & β’ (π β (π΄ Β· π) = (π΅ Β· π)) β β’ (π β π = ((π΅ / π΄) Β· π)) | ||
Theorem | cvsdiveqd 24984 | An equality involving ratios in a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ (π β π β βVec) & β’ (π β π΄ β πΎ) & β’ (π β π΅ β πΎ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π΄ β 0) & β’ (π β π΅ β 0) & β’ (π β π = ((π΄ / π΅) Β· π)) β β’ (π β ((π΅ / π΄) Β· π) = π) | ||
Theorem | cnlmodlem1 24985 | Lemma 1 for cnlmod 24989. (Contributed by AV, 20-Sep-2021.) |
β’ π = ({β¨(Baseβndx), ββ©, β¨(+gβndx), + β©} βͺ {β¨(Scalarβndx), βfldβ©, β¨( Β·π βndx), Β· β©}) β β’ (Baseβπ) = β | ||
Theorem | cnlmodlem2 24986 | Lemma 2 for cnlmod 24989. (Contributed by AV, 20-Sep-2021.) |
β’ π = ({β¨(Baseβndx), ββ©, β¨(+gβndx), + β©} βͺ {β¨(Scalarβndx), βfldβ©, β¨( Β·π βndx), Β· β©}) β β’ (+gβπ) = + | ||
Theorem | cnlmodlem3 24987 | Lemma 3 for cnlmod 24989. (Contributed by AV, 20-Sep-2021.) |
β’ π = ({β¨(Baseβndx), ββ©, β¨(+gβndx), + β©} βͺ {β¨(Scalarβndx), βfldβ©, β¨( Β·π βndx), Β· β©}) β β’ (Scalarβπ) = βfld | ||
Theorem | cnlmod4 24988 | Lemma 4 for cnlmod 24989. (Contributed by AV, 20-Sep-2021.) |
β’ π = ({β¨(Baseβndx), ββ©, β¨(+gβndx), + β©} βͺ {β¨(Scalarβndx), βfldβ©, β¨( Β·π βndx), Β· β©}) β β’ ( Β·π βπ) = Β· | ||
Theorem | cnlmod 24989 | 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 24990 | 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 24991 | 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 24992 | 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 24993 | 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 24994 | 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 24995 | 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 24996 | Obsolete version of recvs 24995 as of 23-Nov-2024. (Contributed by AV, 22-Oct-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π = (ringLModββfld) β β’ π β βVec | ||
Theorem | qcvs 24997 | 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 24998 | 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 24999. 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 24999* | 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 25000* | 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)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |