Axiom ax-his4 27942

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	|- ( ( A e. ~H /\ A =/= 0h ) -> 0 < ( A .ih A ) )

Detailed syntax breakdown of Axiom ax-his4

Step	Hyp	Ref	Expression
1		cA	. . . 4 class A
2		chil 27776	. . . 4 class ~H
3	1, 2	wcel 1990	. . 3 wff A e. ~H
4		c0v 27781	. . . 4 class 0h
5	1, 4	wne 2794	. . 3 wff A =/= 0h
6	3, 5	wa 384	. 2 wff ( A e. ~H /\ A =/= 0h )
7		cc0 9936	. . 3 class 0
8		csp 27779	. . . 4 class .ih
9	1, 1, 8	co 6650	. . 3 class ( A .ih A )
10		clt 10074	. . 3 class <
11	7, 9, 10	wbr 4653	. 2 wff 0 < ( A .ih A )
12	6, 11	wi 4	1 wff ( ( A e. ~H /\ A =/= 0h ) -> 0 < ( A .ih A ) )

This axiom is referenced by:  hiidge0  27955  his6  27956  normgt0  27984  eigrei  28693  eigposi  28695