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 )