| Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > HSE Home > Th. List > ax-his4 | Structured version Visualization version GIF version | ||
| Description: Identity law for inner product. Postulate (S4) of [Beran] p. 95. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
| Ref | Expression |
|---|---|
| ax-his4 | ⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ) → 0 < (𝐴 ·ih 𝐴)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA | . . . 4 class 𝐴 | |
| 2 | chba 30938 | . . . 4 class ℋ | |
| 3 | 1, 2 | wcel 2108 | . . 3 wff 𝐴 ∈ ℋ |
| 4 | c0v 30943 | . . . 4 class 0ℎ | |
| 5 | 1, 4 | wne 2940 | . . 3 wff 𝐴 ≠ 0ℎ |
| 6 | 3, 5 | wa 395 | . 2 wff (𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ) |
| 7 | cc0 11155 | . . 3 class 0 | |
| 8 | csp 30941 | . . . 4 class ·ih | |
| 9 | 1, 1, 8 | co 7431 | . . 3 class (𝐴 ·ih 𝐴) |
| 10 | clt 11295 | . . 3 class < | |
| 11 | 7, 9, 10 | wbr 5143 | . 2 wff 0 < (𝐴 ·ih 𝐴) |
| 12 | 6, 11 | wi 4 | 1 wff ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ) → 0 < (𝐴 ·ih 𝐴)) |
| Colors of variables: wff setvar class |
| This axiom is referenced by: hiidge0 31117 his6 31118 normgt0 31146 eigrei 31853 eigposi 31855 |
| Copyright terms: Public domain | W3C validator |