Step |
Hyp |
Ref |
Expression |
1 |
|
nmsq.v |
β’ π = ( Base β π ) |
2 |
|
nmsq.h |
β’ , = ( Β·π β π ) |
3 |
|
nmsq.n |
β’ π = ( norm β π ) |
4 |
|
eqid |
β’ ( Scalar β π ) = ( Scalar β π ) |
5 |
|
eqid |
β’ ( Base β ( Scalar β π ) ) = ( Base β ( Scalar β π ) ) |
6 |
1 2 3 4 5
|
iscph |
β’ ( π β βPreHil β ( ( π β PreHil β§ π β NrmMod β§ ( Scalar β π ) = ( βfld βΎs ( Base β ( Scalar β π ) ) ) ) β§ ( β β ( ( Base β ( Scalar β π ) ) β© ( 0 [,) +β ) ) ) β ( Base β ( Scalar β π ) ) β§ π = ( π₯ β π β¦ ( β β ( π₯ , π₯ ) ) ) ) ) |
7 |
6
|
simp3bi |
β’ ( π β βPreHil β π = ( π₯ β π β¦ ( β β ( π₯ , π₯ ) ) ) ) |