This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Axiom ax-his4

Description: Identity law for inner product. Postulate (S4) of Beran p. 95. (Contributed by NM, 29-May-1999) (New usage is discouraged.)

Ref Expression
Assertion ax-his4 ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → 0 < ( 𝐴 ·ih 𝐴 ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA ⊢ 𝐴
1 chba ⊢ ℋ
2 0 1 wcel ⊢ 𝐴 ∈ ℋ
3 c0v ⊢ 0ℎ
4 0 3 wne ⊢ 𝐴 ≠ 0ℎ
5 2 4 wa ⊢ ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ )
6 cc0 ⊢ 0
7 clt ⊢ <
8 csp ⊢ ·ih
9 0 0 8 co ⊢ ( 𝐴 ·ih 𝐴 )
10 6 9 7 wbr ⊢ 0 < ( 𝐴 ·ih 𝐴 )
11 5 10 wi ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → 0 < ( 𝐴 ·ih 𝐴 ) )