Metamath Proof Explorer

Axiom ax-his4

Description: Identity law for inner product. Postulate (S4) of Beran p. 95. (Contributed by NM, 29-May-1999) (New usage is discouraged.)

Ref Expression
Assertion ax-his4 
|- ( ( A e. ~H /\ A =/= 0h ) -> 0 < ( A .ih A ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 
 |-  A
1 chba 
 |-  ~H
2 0 1 wcel 
 |-  A e. ~H
3 c0v 
 |-  0h
4 0 3 wne 
 |-  A =/= 0h
5 2 4 wa 
 |-  ( A e. ~H /\ A =/= 0h )
6 cc0 
 |-  0
7 clt 
 |-  <
8 csp 
 |-  .ih
9 0 0 8 co 
 |-  ( A .ih A )
10 6 9 7 wbr 
 |-  0 < ( A .ih A )
11 5 10 wi 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> 0 < ( A .ih A ) )