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	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → 0 < ( 𝐴 ·ih 𝐴 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		chba	⊢ ℋ
2	0 1	wcel	⊢ 𝐴 ∈ ℋ
3		c0v	⊢ 0ℎ
4	0 3	wne	⊢ 𝐴 ≠ 0ℎ
5	2 4	wa	⊢ ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ )
6		cc0	⊢ 0
7		clt	⊢ <
8		csp	⊢ ·ih
9	0 0 8	co	⊢ ( 𝐴 ·ih 𝐴 )
10	6 9 7	wbr	⊢ 0 < ( 𝐴 ·ih 𝐴 )
11	5 10	wi	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → 0 < ( 𝐴 ·ih 𝐴 ) )