Axiom ax-his4 10377

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

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 10212	. . . 4 class ~H
3	1, 2	wcel 1138	. . 3 wff A e. ~H
4		c0v 10215	. . . 4 class 0h
5	1, 4	wne 1854	. . 3 wff A =/= 0h
6	3, 5	wa 239	. 2 wff (A e. ~H /\ A =/= 0h)
7		cc0 6182	. . 3 class 0
8		csp 10217	. . . 4 class .ih
9	1, 1, 8	co 4695	. . 3 class (A .ih A)
10		clt 6449	. . 3 class <
11	7, 9, 10	wbr 3158	. 2 wff 0 < (A .ih A)
12	6, 11	wi 3	1 wff ((A e. ~H /\ A =/= 0h) -> 0 < (A .ih A))

This axiom is referenced by:  hiidge0 10389  his6 10390  normgt0OLD 10418  normgt0 10419  pjthlem2 10645  pjthlem3 10646  pjthlem7 10650  eigrei 11189  eigposi 11191

Copyright terms: Public domain