# Metamath Proof Explorer

## Theorem ocin

Description: Intersection of a Hilbert subspace and its complement. Part of Proposition 1 of Kalmbach p. 65. (Contributed by NM, 11-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion ocin
`|- ( A e. SH -> ( A i^i ( _|_ ` A ) ) = 0H )`

### Proof

Step Hyp Ref Expression
1 shocel
` |-  ( A e. SH -> ( x e. ( _|_ ` A ) <-> ( x e. ~H /\ A. y e. A ( x .ih y ) = 0 ) ) )`
2 oveq2
` |-  ( y = x -> ( x .ih y ) = ( x .ih x ) )`
3 2 eqeq1d
` |-  ( y = x -> ( ( x .ih y ) = 0 <-> ( x .ih x ) = 0 ) )`
4 3 rspccv
` |-  ( A. y e. A ( x .ih y ) = 0 -> ( x e. A -> ( x .ih x ) = 0 ) )`
5 his6
` |-  ( x e. ~H -> ( ( x .ih x ) = 0 <-> x = 0h ) )`
6 5 biimpd
` |-  ( x e. ~H -> ( ( x .ih x ) = 0 -> x = 0h ) )`
7 4 6 sylan9r
` |-  ( ( x e. ~H /\ A. y e. A ( x .ih y ) = 0 ) -> ( x e. A -> x = 0h ) )`
8 1 7 syl6bi
` |-  ( A e. SH -> ( x e. ( _|_ ` A ) -> ( x e. A -> x = 0h ) ) )`
9 8 com23
` |-  ( A e. SH -> ( x e. A -> ( x e. ( _|_ ` A ) -> x = 0h ) ) )`
10 9 impd
` |-  ( A e. SH -> ( ( x e. A /\ x e. ( _|_ ` A ) ) -> x = 0h ) )`
11 sh0
` |-  ( A e. SH -> 0h e. A )`
12 oc0
` |-  ( A e. SH -> 0h e. ( _|_ ` A ) )`
13 11 12 jca
` |-  ( A e. SH -> ( 0h e. A /\ 0h e. ( _|_ ` A ) ) )`
14 eleq1
` |-  ( x = 0h -> ( x e. A <-> 0h e. A ) )`
15 eleq1
` |-  ( x = 0h -> ( x e. ( _|_ ` A ) <-> 0h e. ( _|_ ` A ) ) )`
16 14 15 anbi12d
` |-  ( x = 0h -> ( ( x e. A /\ x e. ( _|_ ` A ) ) <-> ( 0h e. A /\ 0h e. ( _|_ ` A ) ) ) )`
17 13 16 syl5ibrcom
` |-  ( A e. SH -> ( x = 0h -> ( x e. A /\ x e. ( _|_ ` A ) ) ) )`
18 10 17 impbid
` |-  ( A e. SH -> ( ( x e. A /\ x e. ( _|_ ` A ) ) <-> x = 0h ) )`
19 elin
` |-  ( x e. ( A i^i ( _|_ ` A ) ) <-> ( x e. A /\ x e. ( _|_ ` A ) ) )`
20 elch0
` |-  ( x e. 0H <-> x = 0h )`
21 18 19 20 3bitr4g
` |-  ( A e. SH -> ( x e. ( A i^i ( _|_ ` A ) ) <-> x e. 0H ) )`
22 21 eqrdv
` |-  ( A e. SH -> ( A i^i ( _|_ ` A ) ) = 0H )`