Axiom ax-his4 5048

Description: Identity law for inner product. Postulate (S4) of [Beran] p. 95.

Assertion

Ref	Expression
ax-his4	⊢ ((A ∈ ℋ ∧ A ≠ 0v) → 0 < (A ·i A))

Detailed syntax breakdown of Axiom ax-his4

Step	Hyp	Ref	Expression
1		cA	. . . 4 class A
2		chil 4958	. . . 4 class ℋ
3	1, 2	wcel 1092	. . 3 wff A ∈ ℋ
4		c0v 4961	. . . 4 class 0v
5	1, 4	wne 1190	. . 3 wff A ≠ 0v
6	3, 5	wa 196	. 2 wff (A ∈ ℋ ∧ A ≠ 0v)
7		cc0 4028	. . 3 class 0
8		csp 4963	. . . 4 class ·i
9	1, 1, 8	co 3001	. . 3 class (A ·i A)
10		clt 4033	. . 3 class <
11	7, 9, 10	wbr 2054	. 2 wff 0 < (A ·i A)
12	6, 11	wi 2	1 wff ((A ∈ ℋ ∧ A ≠ 0v) → 0 < (A ·i A))

This axiom is referenced by:  axhis42 5049

metamath.org