Axiom ax-his4 31687

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

Assertion

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

Detailed syntax breakdown of Axiom ax-his4

Step	Hyp	Ref	Expression
1		cA	. . . 4 class 𝐴
2		chba 31521	. . . 4 class ℋ
3	1, 2	wcel 2145	. . 3 wff 𝐴 ∈ ℋ
4		c0v 31526	. . . 4 class 0ℎ
5	1, 4	wne 2956	. . 3 wff 𝐴 ≠ 0ℎ
6	3, 5	wa 401	. 2 wff (𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
7		cc0 11200	. . 3 class 0
8		csp 31524	. . . 4 class ·ih
9	1, 1, 8	co 7420	. . 3 class (𝐴 ·ih 𝐴)
10		clt 11343	. . 3 class <
11	7, 9, 10	wbr 5103	. 2 wff 0 < (𝐴 ·ih 𝐴)
12	6, 11	wi 4	1 wff ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ) → 0 < (𝐴 ·ih 𝐴))

This axiom is used by:  hiidge0  31700  his6  31701  normgt0  31729  eigrei  32436  eigposi  32438