This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in ℋ \land A \neq 0_{ℎ}) \to 0 < A \cdot_{ih} A$

Step	Hyp	Ref	Expression
0		cA	$class A$
1		chba	$class ℋ$
2	0 1	wcel	$wff A \in ℋ$
3		c0v	$class 0_{ℎ}$
4	0 3	wne	$wff A \neq 0_{ℎ}$
5	2 4	wa	$wff (A \in ℋ \land A \neq 0_{ℎ})$
6		cc0	$class 0$
7		clt	$class <$
8		csp	$class \cdot_{ih}$
9	0 0 8	co	$class (A \cdot_{ih} A)$
10	6 9 7	wbr	$wff 0 < A \cdot_{ih} A$
11	5 10	wi	$wff ((A \in ℋ \land A \neq 0_{ℎ}) \to 0 < A \cdot_{ih} A)$