Theorem axhis42 5049

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

Assertion

Ref	Expression
axhis42	⊢ ((A ∈ ℋ ∧ ¬ A = 0v) → 0 < (A ·i A))

Proof of Theorem axhis42

Step	Hyp	Ref	Expression
1		ax-his4 5048	. 2 ⊢ ((A ∈ ℋ ∧ A ≠ 0v) → 0 < (A ·i A))
2		df-ne 1192	. 2 ⊢ (A ≠ 0v ↔ ¬ A = 0v)
3	1, 2	sylan2br 348	1 ⊢ ((A ∈ ℋ ∧ ¬ A = 0v) → 0 < (A ·i A))

Syntax hints:  ¬ wn 1   → wi 2   ∧ wa 196   = wceq 1091   ∈ wcel 1092   ≠ wne 1190   class class class wbr 2054  (class class class)co 3001  0cc0 4028   < clt 4033   ℋ chil 4958  0_vc0v 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