# 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 )`
` |-  ( ( ( 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 ) )`
` |-  ( ( ( 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 ) )`