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	$$⊢\left(A\in \mathscr{H}\wedge A\ne 0_{ℎ}\right)\to 0<A{\cdot }_{\mathrm{ih}}A$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		chba	$$class\mathscr{H}$$
2	0 1	wcel	$$wffA\in \mathscr{H}$$
3		c0v	$$class{0}_{ℎ}$$
4	0 3	wne	$$wffA\ne 0_{ℎ}$$
5	2 4	wa	$$wff\left(A\in \mathscr{H}\wedge A\ne 0_{ℎ}\right)$$
6		cc0	$$class0$$
7		clt	$$class<$$
8		csp	$$class{\cdot }_{\mathrm{ih}}$$
9	0 0 8	co	$$class\left(A{\cdot }_{\mathrm{ih}}A\right)$$
10	6 9 7	wbr	$$wff0<A{\cdot }_{\mathrm{ih}}A$$
11	5 10	wi	$$wff\left(\left(A\in \mathscr{H}\wedge A\ne 0_{ℎ}\right)\to 0<A{\cdot }_{\mathrm{ih}}A\right)$$