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 ∈ 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 ⊢ ∀ y ∈ A x ⋅ ih y = 0 → x ∈ A → x ⋅ ih x = 0
5 his6 ⊢ x ∈ ℋ → x ⋅ ih x = 0 ↔ x = 0 ℎ
6 5 biimpd ⊢ x ∈ ℋ → x ⋅ ih x = 0 → x = 0 ℎ
7 4 6 sylan9r ⊢ x ∈ ℋ ∧ ∀ y ∈ A x ⋅ ih y = 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 ℋ