This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )