Theorem ocorth

Description: Members of a subset and its complement are orthogonal. (Contributed by NM, 9-Aug-2000) (New usage is discouraged.)

	Ref	Expression
Assertion	ocorth	|- ( H C_ ~H -> ( ( A e. H /\ B e. ( _|_ ` H ) ) -> ( A .ih B ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		ocel	|- ( H C_ ~H -> ( B e. ( _|_ ` H ) <-> ( B e. ~H /\ A. x e. H ( B .ih x ) = 0 ) ) )
2	1	simplbda	|- ( ( H C_ ~H /\ B e. ( _|_ ` H ) ) -> A. x e. H ( B .ih x ) = 0 )
3	2	adantl	|- ( ( ( H C_ ~H /\ A e. H ) /\ ( H C_ ~H /\ B e. ( _|_ ` H ) ) ) -> A. x e. H ( B .ih x ) = 0 )
4		oveq2	|- ( x = A -> ( B .ih x ) = ( B .ih A ) )
5	4	eqeq1d	|- ( x = A -> ( ( B .ih x ) = 0 <-> ( B .ih A ) = 0 ) )
6	5	rspcv	|- ( A e. H -> ( A. x e. H ( B .ih x ) = 0 -> ( B .ih A ) = 0 ) )
7	6	ad2antlr	|- ( ( ( H C_ ~H /\ A e. H ) /\ ( H C_ ~H /\ B e. ( _|_ ` H ) ) ) -> ( A. x e. H ( B .ih x ) = 0 -> ( B .ih A ) = 0 ) )
8		ssel2	|- ( ( H C_ ~H /\ A e. H ) -> A e. ~H )
9		ocss	|- ( H C_ ~H -> ( _|_ ` H ) C_ ~H )
10	9	sselda	|- ( ( H C_ ~H /\ B e. ( _|_ ` H ) ) -> B e. ~H )
11		orthcom	|- ( ( A e. ~H /\ B e. ~H ) -> ( ( A .ih B ) = 0 <-> ( B .ih A ) = 0 ) )
12	8 10 11	syl2an	|- ( ( ( H C_ ~H /\ A e. H ) /\ ( H C_ ~H /\ B e. ( _|_ ` H ) ) ) -> ( ( A .ih B ) = 0 <-> ( B .ih A ) = 0 ) )
13	7 12	sylibrd	|- ( ( ( H C_ ~H /\ A e. H ) /\ ( H C_ ~H /\ B e. ( _|_ ` H ) ) ) -> ( A. x e. H ( B .ih x ) = 0 -> ( A .ih B ) = 0 ) )
14	3 13	mpd	|- ( ( ( H C_ ~H /\ A e. H ) /\ ( H C_ ~H /\ B e. ( _|_ ` H ) ) ) -> ( A .ih B ) = 0 )
15	14	anandis	|- ( ( H C_ ~H /\ ( A e. H /\ B e. ( _|_ ` H ) ) ) -> ( A .ih B ) = 0 )
16	15	ex	|- ( H C_ ~H -> ( ( A e. H /\ B e. ( _|_ ` H ) ) -> ( A .ih B ) = 0 ) )