Theorem hial0

Description: A vector whose inner product is always zero is zero. (Contributed by NM, 24-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	hial0	|- ( A e. ~H -> ( A. x e. ~H ( A .ih x ) = 0 <-> A = 0h ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	|- ( x = A -> ( A .ih x ) = ( A .ih A ) )
2	1	eqeq1d	|- ( x = A -> ( ( A .ih x ) = 0 <-> ( A .ih A ) = 0 ) )
3	2	rspcv	|- ( A e. ~H -> ( A. x e. ~H ( A .ih x ) = 0 -> ( A .ih A ) = 0 ) )
4		his6	|- ( A e. ~H -> ( ( A .ih A ) = 0 <-> A = 0h ) )
5	3 4	sylibd	|- ( A e. ~H -> ( A. x e. ~H ( A .ih x ) = 0 -> A = 0h ) )
6		oveq1	|- ( A = 0h -> ( A .ih x ) = ( 0h .ih x ) )
7		hi01	|- ( x e. ~H -> ( 0h .ih x ) = 0 )
8	6 7	sylan9eq	|- ( ( A = 0h /\ x e. ~H ) -> ( A .ih x ) = 0 )
9	8	ex	|- ( A = 0h -> ( x e. ~H -> ( A .ih x ) = 0 ) )
10	9	a1i	|- ( A e. ~H -> ( A = 0h -> ( x e. ~H -> ( A .ih x ) = 0 ) ) )
11	10	ralrimdv	|- ( A e. ~H -> ( A = 0h -> A. x e. ~H ( A .ih x ) = 0 ) )
12	5 11	impbid	|- ( A e. ~H -> ( A. x e. ~H ( A .ih x ) = 0 <-> A = 0h ) )