Unitization.norm_splitMul_snd_sq

theorem Unitization.norm_splitMul_snd_sq : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : DenselyNormedField 𝕜] [inst_1 : NonUnitalNormedRing E] [inst_2 : StarRing E] [inst_3 : CstarRing E] [inst_4 : NormedSpace 𝕜 E] [inst_5 : IsScalarTower 𝕜 E E] [inst_6 : SMulCommClass 𝕜 E E] [inst_7 : StarRing 𝕜] [inst_8 : StarModule 𝕜 E] (x : Unitization 𝕜 E), ‖((Unitization.splitMul 𝕜 E) x).2‖ ^ 2 ≤ ‖((Unitization.splitMul 𝕜 E) (star x * x)).2‖

This theorem, named `Unitization.norm_splitMul_snd_sq`, is central to establishing that the norm on the unitization of a non-unital `𝕜`-algebra `E` satisfies the C*-property (a key property in C*-algebras). In particular, for any element `x` of the unitization of `𝕜` and `E`, the norm of the second component of the split multiplication of `x` squared is less than or equal to the norm of the second component of the split multiplication of the starred `x` multiplied by `x`. This theorem assumes that `𝕜` is a densely normed field, `E` is a non-unital normed ring, a star ring, and a C*-ring, and that `E` is also a normed space over `𝕜`, a scalar tower of `𝕜` over `E`, a star ring over `𝕜`, and that `E` is a star module over `𝕜`.

More concisely: For any element `x` in the unitization of a densely normed field `𝕜` and a C*-ring `E`, the square of the second component of the split multiplication of `x` is norm-dominanted by the second component of the starred multiplication of `x` with itself.