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∈Sℋ→A∩⊥⁡A=0ℋ

Proof

Step Hyp Ref Expression
1 shocel ⊢A∈Sℋ→x∈⊥⁡A↔x∈ℋ∧∀y∈Ax⋅ihy=0
2 oveq2 ⊢y=x→x⋅ihy=x⋅ihx
3 2 eqeq1d ⊢y=x→x⋅ihy=0↔x⋅ihx=0
4 3 rspccv ⊢∀y∈Ax⋅ihy=0→x∈A→x⋅ihx=0
5 his6 ⊢x∈ℋ→x⋅ihx=0↔x=0ℎ
6 5 biimpd ⊢x∈ℋ→x⋅ihx=0→x=0ℎ
7 4 6 sylan9r ⊢x∈ℋ∧∀y∈Ax⋅ihy=0→x∈A→x=0ℎ
8 1 7 syl6bi ⊢A∈Sℋ→x∈⊥⁡A→x∈A→x=0ℎ
9 8 com23 ⊢A∈Sℋ→x∈A→x∈⊥⁡A→x=0ℎ
10 9 impd ⊢A∈Sℋ→x∈A∧x∈⊥⁡A→x=0ℎ
11 sh0 ⊢A∈Sℋ→0ℎ∈A
12 oc0 ⊢A∈Sℋ→0ℎ∈⊥⁡A
13 11 12 jca ⊢A∈Sℋ→0ℎ∈A∧0ℎ∈⊥⁡A
14 eleq1 ⊢x=0ℎ→x∈A↔0ℎ∈A
15 eleq1 ⊢x=0ℎ→x∈⊥⁡A↔0ℎ∈⊥⁡A
16 14 15 anbi12d ⊢x=0ℎ→x∈A∧x∈⊥⁡A↔0ℎ∈A∧0ℎ∈⊥⁡A
17 13 16 syl5ibrcom ⊢A∈Sℋ→x=0ℎ→x∈A∧x∈⊥⁡A
18 10 17 impbid ⊢A∈Sℋ→x∈A∧x∈⊥⁡A↔x=0ℎ
19 elin ⊢x∈A∩⊥⁡A↔x∈A∧x∈⊥⁡A
20 elch0 ⊢x∈0ℋ↔x=0ℎ
21 18 19 20 3bitr4g ⊢A∈Sℋ→x∈A∩⊥⁡A↔x∈0ℋ
22 21 eqrdv ⊢A∈Sℋ→A∩⊥⁡A=0ℋ