Home | Metamath
Proof Explorer Theorem List (p. 240 of 470) | < 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: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nmsub 23901 | The norm of the difference between two elements. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π β§ π΅ β π) β (πβ(π΄ β π΅)) = (πβ(π΅ β π΄))) | ||
Theorem | nmrtri 23902 | Reverse triangle inequality for the norm of a subtraction. Problem 3 of [Kreyszig] p. 64. (Contributed by NM, 4-Dec-2006.) (Revised by Mario Carneiro, 4-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π β§ π΅ β π) β (absβ((πβπ΄) β (πβπ΅))) β€ (πβ(π΄ β π΅))) | ||
Theorem | nm2dif 23903 | Inequality for the difference of norms. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π β§ π΅ β π) β ((πβπ΄) β (πβπ΅)) β€ (πβ(π΄ β π΅))) | ||
Theorem | nmtri 23904 | The triangle inequality for the norm of a sum. (Contributed by NM, 11-Nov-2006.) (Revised by Mario Carneiro, 4-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π β§ π΅ β π) β (πβ(π΄ + π΅)) β€ ((πβπ΄) + (πβπ΅))) | ||
Theorem | nmtri2 23905 | Triangle inequality for the norm of two subtractions. (Contributed by NM, 24-Feb-2008.) (Revised by AV, 8-Oct-2021.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β NrmGrp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (πβ(π΄ β πΆ)) β€ ((πβ(π΄ β π΅)) + (πβ(π΅ β πΆ)))) | ||
Theorem | ngpi 23906* | The properties of a normed group, which is a group accompanied by a norm. (Contributed by AV, 7-Oct-2021.) |
β’ π = (Baseβπ) & β’ π = (normβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) β β’ (π β NrmGrp β (π β Grp β§ π:πβΆβ β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))))) | ||
Theorem | nm0 23907 | Norm of the identity element. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (normβπΊ) & β’ 0 = (0gβπΊ) β β’ (πΊ β NrmGrp β (πβ 0 ) = 0) | ||
Theorem | nmgt0 23908 | The norm of a nonzero element is a positive real. (Contributed by NM, 20-Nov-2007.) (Revised by AV, 8-Oct-2021.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π) β (π΄ β 0 β 0 < (πβπ΄))) | ||
Theorem | sgrim 23909 | The induced metric on a subgroup is the induced metric on the parent group equipped with a norm. (Contributed by NM, 1-Feb-2008.) (Revised by AV, 19-Oct-2021.) |
β’ π = (π βΎs π) & β’ π· = (distβπ) & β’ πΈ = (distβπ) β β’ (π β π β πΈ = π·) | ||
Theorem | sgrimval 23910 | The induced metric on a subgroup in terms of the induced metric on the parent normed group. (Contributed by NM, 1-Feb-2008.) (Revised by AV, 19-Oct-2021.) |
β’ π = (π βΎs π) & β’ π· = (distβπ) & β’ πΈ = (distβπ) & β’ π = (πΊ toNrmGrp π) & β’ π = (normβπΊ) & β’ π = (SubGrpβπ) β β’ (((πΊ β NrmGrp β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (π΄πΈπ΅) = (π΄π·π΅)) | ||
Theorem | subgnm 23911 | The norm in a subgroup. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π» = (πΊ βΎs π΄) & β’ π = (normβπΊ) & β’ π = (normβπ») β β’ (π΄ β (SubGrpβπΊ) β π = (π βΎ π΄)) | ||
Theorem | subgnm2 23912 | A substructure assigns the same values to the norms of elements of a subgroup. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π» = (πΊ βΎs π΄) & β’ π = (normβπΊ) & β’ π = (normβπ») β β’ ((π΄ β (SubGrpβπΊ) β§ π β π΄) β (πβπ) = (πβπ)) | ||
Theorem | subgngp 23913 | A normed group restricted to a subgroup is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π» = (πΊ βΎs π΄) β β’ ((πΊ β NrmGrp β§ π΄ β (SubGrpβπΊ)) β π» β NrmGrp) | ||
Theorem | ngptgp 23914 | A normed abelian group is a topological group (with the topology induced by the metric induced by the norm). (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ ((πΊ β NrmGrp β§ πΊ β Abel) β πΊ β TopGrp) | ||
Theorem | ngppropd 23915* | Property deduction for a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) & β’ (π β ((distβπΎ) βΎ (π΅ Γ π΅)) = ((distβπΏ) βΎ (π΅ Γ π΅))) & β’ (π β (TopOpenβπΎ) = (TopOpenβπΏ)) β β’ (π β (πΎ β NrmGrp β πΏ β NrmGrp)) | ||
Theorem | reldmtng 23916 | The function toNrmGrp is a two-argument function. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ Rel dom toNrmGrp | ||
Theorem | tngval 23917 | Value of the function which augments a given structure πΊ with a norm π. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (πΊ toNrmGrp π) & β’ β = (-gβπΊ) & β’ π· = (π β β ) & β’ π½ = (MetOpenβπ·) β β’ ((πΊ β π β§ π β π) β π = ((πΊ sSet β¨(distβndx), π·β©) sSet β¨(TopSetβndx), π½β©)) | ||
Theorem | tnglem 23918 | Lemma for tngbas 23920 and similar theorems. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.) |
β’ π = (πΊ toNrmGrp π) & β’ πΈ = Slot (πΈβndx) & β’ (πΈβndx) β (TopSetβndx) & β’ (πΈβndx) β (distβndx) β β’ (π β π β (πΈβπΊ) = (πΈβπ)) | ||
Theorem | tnglemOLD 23919 | Obsolete version of tnglem 23918 as of 31-Oct-2024. Lemma for tngbas 23920 and similar theorems. (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (πΊ toNrmGrp π) & β’ πΈ = Slot πΎ & β’ πΎ β β & β’ πΎ < 9 β β’ (π β π β (πΈβπΊ) = (πΈβπ)) | ||
Theorem | tngbas 23920 | The base set of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.) |
β’ π = (πΊ toNrmGrp π) & β’ π΅ = (BaseβπΊ) β β’ (π β π β π΅ = (Baseβπ)) | ||
Theorem | tngbasOLD 23921 | Obsolete proof of tngbas 23920 as of 31-Oct-2024. The base set of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (πΊ toNrmGrp π) & β’ π΅ = (BaseβπΊ) β β’ (π β π β π΅ = (Baseβπ)) | ||
Theorem | tngplusg 23922 | The group addition of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.) |
β’ π = (πΊ toNrmGrp π) & β’ + = (+gβπΊ) β β’ (π β π β + = (+gβπ)) | ||
Theorem | tngplusgOLD 23923 | Obsolete proof of tngplusg 23922 as of 31-Oct-2024. The group addition of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (πΊ toNrmGrp π) & β’ + = (+gβπΊ) β β’ (π β π β + = (+gβπ)) | ||
Theorem | tng0 23924 | The group identity of a structure augmented with a norm. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by AV, 31-Oct-2024.) |
β’ π = (πΊ toNrmGrp π) & β’ 0 = (0gβπΊ) β β’ (π β π β 0 = (0gβπ)) | ||
Theorem | tngmulr 23925 | The ring multiplication of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.) |
β’ π = (πΊ toNrmGrp π) & β’ Β· = (.rβπΊ) β β’ (π β π β Β· = (.rβπ)) | ||
Theorem | tngmulrOLD 23926 | Obsolete proof of tngmulr 23925 as of 31-Oct-2024. The ring multiplication of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (πΊ toNrmGrp π) & β’ Β· = (.rβπΊ) β β’ (π β π β Β· = (.rβπ)) | ||
Theorem | tngsca 23927 | The scalar ring of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.) |
β’ π = (πΊ toNrmGrp π) & β’ πΉ = (ScalarβπΊ) β β’ (π β π β πΉ = (Scalarβπ)) | ||
Theorem | tngscaOLD 23928 | Obsolete proof of tngsca 23927 as of 31-Oct-2024. The scalar ring of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (πΊ toNrmGrp π) & β’ πΉ = (ScalarβπΊ) β β’ (π β π β πΉ = (Scalarβπ)) | ||
Theorem | tngvsca 23929 | The scalar multiplication of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.) |
β’ π = (πΊ toNrmGrp π) & β’ Β· = ( Β·π βπΊ) β β’ (π β π β Β· = ( Β·π βπ)) | ||
Theorem | tngvscaOLD 23930 | Obsolete proof of tngvsca 23929 as of 31-Oct-2024. The scalar multiplication of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (πΊ toNrmGrp π) & β’ Β· = ( Β·π βπΊ) β β’ (π β π β Β· = ( Β·π βπ)) | ||
Theorem | tngip 23931 | The inner product operation of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.) |
β’ π = (πΊ toNrmGrp π) & β’ , = (Β·πβπΊ) β β’ (π β π β , = (Β·πβπ)) | ||
Theorem | tngipOLD 23932 | Obsolete proof of tngip 23931 as of 31-Oct-2024. The inner product operation of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (πΊ toNrmGrp π) & β’ , = (Β·πβπΊ) β β’ (π β π β , = (Β·πβπ)) | ||
Theorem | tngds 23933 | The metric function of a structure augmented with a norm. (Contributed by Mario Carneiro, 3-Oct-2015.) (Proof shortened by AV, 29-Oct-2024.) |
β’ π = (πΊ toNrmGrp π) & β’ β = (-gβπΊ) β β’ (π β π β (π β β ) = (distβπ)) | ||
Theorem | tngdsOLD 23934 | Obsolete proof of tngds 23933 as of 29-Oct-2024. The metric function of a structure augmented with a norm. (Contributed by Mario Carneiro, 3-Oct-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π = (πΊ toNrmGrp π) & β’ β = (-gβπΊ) β β’ (π β π β (π β β ) = (distβπ)) | ||
Theorem | tngtset 23935 | The topology generated by a normed structure. (Contributed by Mario Carneiro, 3-Oct-2015.) |
β’ π = (πΊ toNrmGrp π) & β’ π· = (distβπ) & β’ π½ = (MetOpenβπ·) β β’ ((πΊ β π β§ π β π) β π½ = (TopSetβπ)) | ||
Theorem | tngtopn 23936 | The topology generated by a normed structure. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (πΊ toNrmGrp π) & β’ π· = (distβπ) & β’ π½ = (MetOpenβπ·) β β’ ((πΊ β π β§ π β π) β π½ = (TopOpenβπ)) | ||
Theorem | tngnm 23937 | The topology generated by a normed structure. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (πΊ toNrmGrp π) & β’ π = (BaseβπΊ) & β’ π΄ β V β β’ ((πΊ β Grp β§ π:πβΆπ΄) β π = (normβπ)) | ||
Theorem | tngngp2 23938 | A norm turns a group into a normed group iff the generated metric is in fact a metric. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (πΊ toNrmGrp π) & β’ π = (BaseβπΊ) & β’ π· = (distβπ) β β’ (π:πβΆβ β (π β NrmGrp β (πΊ β Grp β§ π· β (Metβπ)))) | ||
Theorem | tngngpd 23939* | Derive the axioms for a normed group from the axioms for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (πΊ toNrmGrp π) & β’ π = (BaseβπΊ) & β’ β = (-gβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β Grp) & β’ (π β π:πβΆβ) & β’ ((π β§ π₯ β π) β ((πβπ₯) = 0 β π₯ = 0 )) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) β β’ (π β π β NrmGrp) | ||
Theorem | tngngp 23940* | Derive the axioms for a normed group from the axioms for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (πΊ toNrmGrp π) & β’ π = (BaseβπΊ) & β’ β = (-gβπΊ) & β’ 0 = (0gβπΊ) β β’ (π:πβΆβ β (π β NrmGrp β (πΊ β Grp β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦)))))) | ||
Theorem | tnggrpr 23941 | If a structure equipped with a norm is a normed group, the structure itself must be a group. (Contributed by AV, 15-Oct-2021.) |
β’ π = (πΊ toNrmGrp π) β β’ ((π β π β§ π β NrmGrp) β πΊ β Grp) | ||
Theorem | tngngp3 23942* | Alternate definition of a normed group (i.e., a group equipped with a norm) without using the properties of a metric space. This corresponds to the definition in N. H. Bingham, A. J. Ostaszewski: "Normed versus topological groups: dichotomy and duality", 2010, Dissertationes Mathematicae 472, pp. 1-138 and E. Deza, M.M. Deza: "Dictionary of Distances", Elsevier, 2006. (Contributed by AV, 16-Oct-2021.) |
β’ π = (πΊ toNrmGrp π) & β’ π = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ + = (+gβπΊ) & β’ πΌ = (invgβπΊ) β β’ (π:πβΆβ β (π β NrmGrp β (πΊ β Grp β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ (πβ(πΌβπ₯)) = (πβπ₯) β§ βπ¦ β π (πβ(π₯ + π¦)) β€ ((πβπ₯) + (πβπ¦)))))) | ||
Theorem | nrmtngdist 23943 | The augmentation of a normed group by its own norm has the same distance function as the normed group (restricted to the base set). (Contributed by AV, 15-Oct-2021.) |
β’ π = (πΊ toNrmGrp (normβπΊ)) & β’ π = (BaseβπΊ) β β’ (πΊ β NrmGrp β (distβπ) = ((distβπΊ) βΎ (π Γ π))) | ||
Theorem | nrmtngnrm 23944 | The augmentation of a normed group by its own norm is a normed group with the same norm. (Contributed by AV, 15-Oct-2021.) |
β’ π = (πΊ toNrmGrp (normβπΊ)) β β’ (πΊ β NrmGrp β (π β NrmGrp β§ (normβπ) = (normβπΊ))) | ||
Theorem | tngngpim 23945 | The induced metric of a normed group is a function. (Contributed by AV, 19-Oct-2021.) |
β’ π = (πΊ toNrmGrp π) & β’ π = (normβπΊ) & β’ π = (BaseβπΊ) & β’ π· = (distβπ) β β’ (πΊ β NrmGrp β π·:(π Γ π)βΆβ) | ||
Theorem | isnrg 23946 | A normed ring is a ring with a norm that makes it into a normed group, and such that the norm is an absolute value on the ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (normβπ ) & β’ π΄ = (AbsValβπ ) β β’ (π β NrmRing β (π β NrmGrp β§ π β π΄)) | ||
Theorem | nrgabv 23947 | The norm of a normed ring is an absolute value. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (normβπ ) & β’ π΄ = (AbsValβπ ) β β’ (π β NrmRing β π β π΄) | ||
Theorem | nrgngp 23948 | A normed ring is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β NrmRing β π β NrmGrp) | ||
Theorem | nrgring 23949 | A normed ring is a ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β NrmRing β π β Ring) | ||
Theorem | nmmul 23950 | The norm of a product in a normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π = (Baseβπ ) & β’ π = (normβπ ) & β’ Β· = (.rβπ ) β β’ ((π β NrmRing β§ π΄ β π β§ π΅ β π) β (πβ(π΄ Β· π΅)) = ((πβπ΄) Β· (πβπ΅))) | ||
Theorem | nrgdsdi 23951 | Distribute a distance calculation. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π = (Baseβπ ) & β’ π = (normβπ ) & β’ Β· = (.rβπ ) & β’ π· = (distβπ ) β β’ ((π β NrmRing β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((πβπ΄) Β· (π΅π·πΆ)) = ((π΄ Β· π΅)π·(π΄ Β· πΆ))) | ||
Theorem | nrgdsdir 23952 | Distribute a distance calculation. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π = (Baseβπ ) & β’ π = (normβπ ) & β’ Β· = (.rβπ ) & β’ π· = (distβπ ) β β’ ((π β NrmRing β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄π·π΅) Β· (πβπΆ)) = ((π΄ Β· πΆ)π·(π΅ Β· πΆ))) | ||
Theorem | nm1 23953 | The norm of one in a nonzero normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π = (normβπ ) & β’ 1 = (1rβπ ) β β’ ((π β NrmRing β§ π β NzRing) β (πβ 1 ) = 1) | ||
Theorem | unitnmn0 23954 | The norm of a unit is nonzero in a nonzero normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π = (normβπ ) & β’ π = (Unitβπ ) β β’ ((π β NrmRing β§ π β NzRing β§ π΄ β π) β (πβπ΄) β 0) | ||
Theorem | nminvr 23955 | The norm of an inverse in a nonzero normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π = (normβπ ) & β’ π = (Unitβπ ) & β’ πΌ = (invrβπ ) β β’ ((π β NrmRing β§ π β NzRing β§ π΄ β π) β (πβ(πΌβπ΄)) = (1 / (πβπ΄))) | ||
Theorem | nmdvr 23956 | The norm of a division in a nonzero normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π = (Baseβπ ) & β’ π = (normβπ ) & β’ π = (Unitβπ ) & β’ / = (/rβπ ) β β’ (((π β NrmRing β§ π β NzRing) β§ (π΄ β π β§ π΅ β π)) β (πβ(π΄ / π΅)) = ((πβπ΄) / (πβπ΅))) | ||
Theorem | nrgdomn 23957 | A nonzero normed ring is a domain. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β NrmRing β (π β Domn β π β NzRing)) | ||
Theorem | nrgtgp 23958 | A normed ring is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β NrmRing β π β TopGrp) | ||
Theorem | subrgnrg 23959 | A normed ring restricted to a subring is a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π» = (πΊ βΎs π΄) β β’ ((πΊ β NrmRing β§ π΄ β (SubRingβπΊ)) β π» β NrmRing) | ||
Theorem | tngnrg 23960 | Given any absolute value over a ring, augmenting the ring with the absolute value produces a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (π toNrmGrp πΉ) & β’ π΄ = (AbsValβπ ) β β’ (πΉ β π΄ β π β NrmRing) | ||
Theorem | isnlm 23961* | A normed (left) module is a module which is also a normed group over a normed ring, such that the norm distributes over scalar multiplication. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (Baseβπ) & β’ π = (normβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π΄ = (normβπΉ) β β’ (π β NrmMod β ((π β NrmGrp β§ π β LMod β§ πΉ β NrmRing) β§ βπ₯ β πΎ βπ¦ β π (πβ(π₯ Β· π¦)) = ((π΄βπ₯) Β· (πβπ¦)))) | ||
Theorem | nmvs 23962 | Defining property of a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (Baseβπ) & β’ π = (normβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π΄ = (normβπΉ) β β’ ((π β NrmMod β§ π β πΎ β§ π β π) β (πβ(π Β· π)) = ((π΄βπ) Β· (πβπ))) | ||
Theorem | nlmngp 23963 | A normed module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β NrmMod β π β NrmGrp) | ||
Theorem | nlmlmod 23964 | A normed module is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β NrmMod β π β LMod) | ||
Theorem | nlmnrg 23965 | The scalar component of a left module is a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β NrmMod β πΉ β NrmRing) | ||
Theorem | nlmngp2 23966 | The scalar component of a left module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β NrmMod β πΉ β NrmGrp) | ||
Theorem | nlmdsdi 23967 | Distribute a distance calculation. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π· = (distβπ) & β’ π΄ = (normβπΉ) β β’ ((π β NrmMod β§ (π β πΎ β§ π β π β§ π β π)) β ((π΄βπ) Β· (ππ·π)) = ((π Β· π)π·(π Β· π))) | ||
Theorem | nlmdsdir 23968 | Distribute a distance calculation. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π· = (distβπ) & β’ π = (normβπ) & β’ πΈ = (distβπΉ) β β’ ((π β NrmMod β§ (π β πΎ β§ π β πΎ β§ π β π)) β ((ππΈπ) Β· (πβπ)) = ((π Β· π)π·(π Β· π))) | ||
Theorem | nlmmul0or 23969 | If a scalar product is zero, one of its factors must be zero. (Contributed by NM, 6-Dec-2007.) (Revised by Mario Carneiro, 4-Oct-2015.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π = (0gβπΉ) β β’ ((π β NrmMod β§ π΄ β πΎ β§ π΅ β π) β ((π΄ Β· π΅) = 0 β (π΄ = π β¨ π΅ = 0 ))) | ||
Theorem | sranlm 23970 | The subring algebra over a normed ring is a normed left module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π΄ = ((subringAlg βπ)βπ) β β’ ((π β NrmRing β§ π β (SubRingβπ)) β π΄ β NrmMod) | ||
Theorem | nlmvscnlem2 23971 | Lemma for nlmvscn 23973. Compare this proof with the similar elementary proof mulcn2 15413 for continuity of multiplication on β. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ π = (Baseβπ) & β’ πΎ = (BaseβπΉ) & β’ π· = (distβπ) & β’ πΈ = (distβπΉ) & β’ π = (normβπ) & β’ π΄ = (normβπΉ) & β’ Β· = ( Β·π βπ) & β’ π = ((π / 2) / ((π΄βπ΅) + 1)) & β’ π = ((π / 2) / ((πβπ) + π)) & β’ (π β π β NrmMod) & β’ (π β π β β+) & β’ (π β π΅ β πΎ) & β’ (π β π β π) & β’ (π β πΆ β πΎ) & β’ (π β π β π) & β’ (π β (π΅πΈπΆ) < π) & β’ (π β (ππ·π) < π) β β’ (π β ((π΅ Β· π)π·(πΆ Β· π)) < π ) | ||
Theorem | nlmvscnlem1 23972* | Lemma for nlmvscn 23973. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ π = (Baseβπ) & β’ πΎ = (BaseβπΉ) & β’ π· = (distβπ) & β’ πΈ = (distβπΉ) & β’ π = (normβπ) & β’ π΄ = (normβπΉ) & β’ Β· = ( Β·π βπ) & β’ π = ((π / 2) / ((π΄βπ΅) + 1)) & β’ π = ((π / 2) / ((πβπ) + π)) & β’ (π β π β NrmMod) & β’ (π β π β β+) & β’ (π β π΅ β πΎ) & β’ (π β π β π) β β’ (π β βπ β β+ βπ₯ β πΎ βπ¦ β π (((π΅πΈπ₯) < π β§ (ππ·π¦) < π) β ((π΅ Β· π)π·(π₯ Β· π¦)) < π )) | ||
Theorem | nlmvscn 23973 | The scalar multiplication of a normed module is continuous. Lemma for nrgtrg 23976 and nlmtlm 23980. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·sf βπ) & β’ π½ = (TopOpenβπ) & β’ πΎ = (TopOpenβπΉ) β β’ (π β NrmMod β Β· β ((πΎ Γt π½) Cn π½)) | ||
Theorem | rlmnlm 23974 | The ring module over a normed ring is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β NrmRing β (ringLModβπ ) β NrmMod) | ||
Theorem | rlmnm 23975 | The norm function in the ring module. (Contributed by AV, 9-Oct-2021.) |
β’ (normβπ ) = (normβ(ringLModβπ )) | ||
Theorem | nrgtrg 23976 | A normed ring is a topological ring. (Contributed by Mario Carneiro, 4-Oct-2015.) (Proof shortened by AV, 31-Oct-2024.) |
β’ (π β NrmRing β π β TopRing) | ||
Theorem | nrginvrcnlem 23977* | Lemma for nrginvrcn 23978. Compare this proof with reccn2 15414, the elementary proof of continuity of division. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ π = (Baseβπ ) & β’ π = (Unitβπ ) & β’ πΌ = (invrβπ ) & β’ π = (normβπ ) & β’ π· = (distβπ ) & β’ (π β π β NrmRing) & β’ (π β π β NzRing) & β’ (π β π΄ β π) & β’ (π β π΅ β β+) & β’ π = (if(1 β€ ((πβπ΄) Β· π΅), 1, ((πβπ΄) Β· π΅)) Β· ((πβπ΄) / 2)) β β’ (π β βπ₯ β β+ βπ¦ β π ((π΄π·π¦) < π₯ β ((πΌβπ΄)π·(πΌβπ¦)) < π΅)) | ||
Theorem | nrginvrcn 23978 | The ring inverse function is continuous in a normed ring. (Note that this is true even in rings which are not division rings.) (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ π = (Baseβπ ) & β’ π = (Unitβπ ) & β’ πΌ = (invrβπ ) & β’ π½ = (TopOpenβπ ) β β’ (π β NrmRing β πΌ β ((π½ βΎt π) Cn (π½ βΎt π))) | ||
Theorem | nrgtdrg 23979 | A normed division ring is a topological division ring. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ ((π β NrmRing β§ π β DivRing) β π β TopDRing) | ||
Theorem | nlmtlm 23980 | A normed module is a topological module. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ (π β NrmMod β π β TopMod) | ||
Theorem | isnvc 23981 | A normed vector space is just a normed module which is algebraically a vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β NrmVec β (π β NrmMod β§ π β LVec)) | ||
Theorem | nvcnlm 23982 | A normed vector space is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β NrmVec β π β NrmMod) | ||
Theorem | nvclvec 23983 | A normed vector space is a left vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β NrmVec β π β LVec) | ||
Theorem | nvclmod 23984 | A normed vector space is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β NrmVec β π β LMod) | ||
Theorem | isnvc2 23985 | A normed vector space is just a normed module whose scalar ring is a division ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β NrmVec β (π β NrmMod β§ πΉ β DivRing)) | ||
Theorem | nvctvc 23986 | A normed vector space is a topological vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β NrmVec β π β TopVec) | ||
Theorem | lssnlm 23987 | A subspace of a normed module is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (π βΎs π) & β’ π = (LSubSpβπ) β β’ ((π β NrmMod β§ π β π) β π β NrmMod) | ||
Theorem | lssnvc 23988 | A subspace of a normed vector space is a normed vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (π βΎs π) & β’ π = (LSubSpβπ) β β’ ((π β NrmVec β§ π β π) β π β NrmVec) | ||
Theorem | rlmnvc 23989 | The ring module over a normed division ring is a normed vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ ((π β NrmRing β§ π β DivRing) β (ringLModβπ ) β NrmVec) | ||
Theorem | ngpocelbl 23990 | Membership of an off-center vector in a ball in a normed module. (Contributed by NM, 27-Dec-2007.) (Revised by AV, 14-Oct-2021.) |
β’ π = (normβπΊ) & β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ π· = ((distβπΊ) βΎ (π Γ π)) β β’ ((πΊ β NrmMod β§ π β β* β§ (π β π β§ π΄ β π)) β ((π + π΄) β (π(ballβπ·)π ) β (πβπ΄) < π )) | ||
Syntax | cnmo 23991 | The operator norm function. |
class normOp | ||
Syntax | cnghm 23992 | The class of normed group homomorphisms. |
class NGHom | ||
Syntax | cnmhm 23993 | The class of normed module homomorphisms. |
class NMHom | ||
Definition | df-nmo 23994* | Define the norm of an operator between two normed groups (usually vector spaces). This definition produces an operator norm function for each pair of groups β¨π , π‘β©. Equivalent to the definition of linear operator norm in [AkhiezerGlazman] p. 39. (Contributed by Mario Carneiro, 18-Oct-2015.) (Revised by AV, 25-Sep-2020.) |
β’ normOp = (π β NrmGrp, π‘ β NrmGrp β¦ (π β (π GrpHom π‘) β¦ inf({π β (0[,)+β) β£ βπ₯ β (Baseβπ )((normβπ‘)β(πβπ₯)) β€ (π Β· ((normβπ )βπ₯))}, β*, < ))) | ||
Definition | df-nghm 23995* | Define the set of normed group homomorphisms between two normed groups. A normed group homomorphism is a group homomorphism which additionally bounds the increase of norm by a fixed real operator. In vector spaces these are also known as bounded linear operators. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ NGHom = (π β NrmGrp, π‘ β NrmGrp β¦ (β‘(π normOp π‘) β β)) | ||
Definition | df-nmhm 23996* | Define a normed module homomorphism, also known as a bounded linear operator. This is a module homomorphism (a linear function) such that the operator norm is finite, or equivalently there is a constant π such that... (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ NMHom = (π β NrmMod, π‘ β NrmMod β¦ ((π LMHom π‘) β© (π NGHom π‘))) | ||
Theorem | nmoffn 23997 | The function producing operator norm functions is a function on normed groups. (Contributed by Mario Carneiro, 18-Oct-2015.) (Proof shortened by AV, 26-Sep-2020.) |
β’ normOp Fn (NrmGrp Γ NrmGrp) | ||
Theorem | reldmnghm 23998 | Lemma for normed group homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ Rel dom NGHom | ||
Theorem | reldmnmhm 23999 | Lemma for module homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ Rel dom NMHom | ||
Theorem | nmofval 24000* | Value of the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) (Revised by AV, 26-Sep-2020.) |
β’ π = (π normOp π) & β’ π = (Baseβπ) & β’ πΏ = (normβπ) & β’ π = (normβπ) β β’ ((π β NrmGrp β§ π β NrmGrp) β π = (π β (π GrpHom π) β¦ inf({π β (0[,)+β) β£ βπ₯ β π (πβ(πβπ₯)) β€ (π Β· (πΏβπ₯))}, β*, < ))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |