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

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