Theorem h1dei

Description: Membership in 1-dimensional subspace. (Contributed by NM, 7-Jul-2001) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

	Ref	Expression
Hypothesis	h1deot.1	|- B e. ~H
Assertion	h1dei	|- ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> ( A e. ~H /\ A. x e. ~H ( ( B .ih x ) = 0 -> ( A .ih x ) = 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		h1deot.1	|- B e. ~H
2		snssi	|- ( B e. ~H -> { B } C_ ~H )
3		occl	|- ( { B } C_ ~H -> ( _|_ ` { B } ) e. CH )
4	1 2 3	mp2b	|- ( _|_ ` { B } ) e. CH
5	4	chssii	|- ( _|_ ` { B } ) C_ ~H
6		ocel	|- ( ( _|_ ` { B } ) C_ ~H -> ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> ( A e. ~H /\ A. x e. ( _|_ ` { B } ) ( A .ih x ) = 0 ) ) )
7	5 6	ax-mp	|- ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> ( A e. ~H /\ A. x e. ( _|_ ` { B } ) ( A .ih x ) = 0 ) )
8	1	h1deoi	|- ( x e. ( _|_ ` { B } ) <-> ( x e. ~H /\ ( x .ih B ) = 0 ) )
9		orthcom	|- ( ( x e. ~H /\ B e. ~H ) -> ( ( x .ih B ) = 0 <-> ( B .ih x ) = 0 ) )
10	1 9	mpan2	|- ( x e. ~H -> ( ( x .ih B ) = 0 <-> ( B .ih x ) = 0 ) )
11	10	pm5.32i	|- ( ( x e. ~H /\ ( x .ih B ) = 0 ) <-> ( x e. ~H /\ ( B .ih x ) = 0 ) )
12	8 11	bitri	|- ( x e. ( _|_ ` { B } ) <-> ( x e. ~H /\ ( B .ih x ) = 0 ) )
13	12	imbi1i	|- ( ( x e. ( _|_ ` { B } ) -> ( A .ih x ) = 0 ) <-> ( ( x e. ~H /\ ( B .ih x ) = 0 ) -> ( A .ih x ) = 0 ) )
14		impexp	|- ( ( ( x e. ~H /\ ( B .ih x ) = 0 ) -> ( A .ih x ) = 0 ) <-> ( x e. ~H -> ( ( B .ih x ) = 0 -> ( A .ih x ) = 0 ) ) )
15	13 14	bitri	|- ( ( x e. ( _|_ ` { B } ) -> ( A .ih x ) = 0 ) <-> ( x e. ~H -> ( ( B .ih x ) = 0 -> ( A .ih x ) = 0 ) ) )
16	15	ralbii2	|- ( A. x e. ( _|_ ` { B } ) ( A .ih x ) = 0 <-> A. x e. ~H ( ( B .ih x ) = 0 -> ( A .ih x ) = 0 ) )
17	16	anbi2i	|- ( ( A e. ~H /\ A. x e. ( _|_ ` { B } ) ( A .ih x ) = 0 ) <-> ( A e. ~H /\ A. x e. ~H ( ( B .ih x ) = 0 -> ( A .ih x ) = 0 ) ) )
18	7 17	bitri	|- ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> ( A e. ~H /\ A. x e. ~H ( ( B .ih x ) = 0 -> ( A .ih x ) = 0 ) ) )