Theorem hial02

Description: A vector whose inner product is always zero is zero. (Contributed by NM, 28-Jan-2006) (New usage is discouraged.)

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

Proof

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