Theorem axhis42 5049

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

Assertion

Ref	Expression
axhis42	|- ((A e. H~ /\ -. A = 0v) -> 0 < (A .i A))

Proof of Theorem axhis42

Step	Hyp	Ref	Expression
1		ax-his4 5048	. 2 |- ((A e. H~ /\ A =/= 0v) -> 0 < (A .i A))
2		df-ne 1192	. 2 |- (A =/= 0v <-> -. A = 0v)
3	1, 2	sylan2br 348	1 |- ((A e. H~ /\ -. A = 0v) -> 0 < (A .i A))

Syntax hints:  -. wn 1   -> wi 2   /\ wa 196   = wceq 1091   e. wcel 1092   =/= wne 1190   class class class wbr 2054  (class class class)co 3001  0cc0 4028   < clt 4033  H~chil 4958  0vc0v 4961   .i csp 4963

This theorem is referenced by:  hiidge0t 5056  his6 5057  normgt0t 5078  pjthlem2 5226  pjthlem3 5227  pjthlem7 5231

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-his4 5048

This theorem depends on definitions:  df-bi 128  df-an 198  df-ne 1192

metamath.org