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 ( 𝐴 ∈ Sℋ → ( 𝐴 ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ )

Proof

Step Hyp Ref Expression
1 shocel ⊢ ( 𝐴 ∈ Sℋ → ( 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ↔ ( 𝑥 ∈ ℋ ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ·ih 𝑦 ) = 0 ) ) )
2 oveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝑥 ·ih 𝑦 ) = ( 𝑥 ·ih 𝑥 ) )
3 2 eqeq1d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 ·ih 𝑦 ) = 0 ↔ ( 𝑥 ·ih 𝑥 ) = 0 ) )
4 3 rspccv ⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 ·ih 𝑦 ) = 0 → ( 𝑥 ∈ 𝐴 → ( 𝑥 ·ih 𝑥 ) = 0 ) )
5 his6 ⊢ ( 𝑥 ∈ ℋ → ( ( 𝑥 ·ih 𝑥 ) = 0 ↔ 𝑥 = 0ℎ ) )
6 5 biimpd ⊢ ( 𝑥 ∈ ℋ → ( ( 𝑥 ·ih 𝑥 ) = 0 → 𝑥 = 0ℎ ) )
7 4 6 sylan9r ⊢ ( ( 𝑥 ∈ ℋ ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ·ih 𝑦 ) = 0 ) → ( 𝑥 ∈ 𝐴 → 𝑥 = 0ℎ ) )
8 1 7 biimtrdi ⊢ ( 𝐴 ∈ Sℋ → ( 𝑥 ∈ ( ⊥ ‘ 𝐴 ) → ( 𝑥 ∈ 𝐴 → 𝑥 = 0ℎ ) ) )
9 8 com23 ⊢ ( 𝐴 ∈ Sℋ → ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ ( ⊥ ‘ 𝐴 ) → 𝑥 = 0ℎ ) ) )
10 9 impd ⊢ ( 𝐴 ∈ Sℋ → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ) → 𝑥 = 0ℎ ) )
11 sh0 ⊢ ( 𝐴 ∈ Sℋ → 0ℎ ∈ 𝐴 )
12 oc0 ⊢ ( 𝐴 ∈ Sℋ → 0ℎ ∈ ( ⊥ ‘ 𝐴 ) )
13 11 12 jca ⊢ ( 𝐴 ∈ Sℋ → ( 0ℎ ∈ 𝐴 ∧ 0ℎ ∈ ( ⊥ ‘ 𝐴 ) ) )
14 eleq1 ⊢ ( 𝑥 = 0ℎ → ( 𝑥 ∈ 𝐴 ↔ 0ℎ ∈ 𝐴 ) )
15 eleq1 ⊢ ( 𝑥 = 0ℎ → ( 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ↔ 0ℎ ∈ ( ⊥ ‘ 𝐴 ) ) )
16 14 15 anbi12d ⊢ ( 𝑥 = 0ℎ → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ) ↔ ( 0ℎ ∈ 𝐴 ∧ 0ℎ ∈ ( ⊥ ‘ 𝐴 ) ) ) )
17 13 16 syl5ibrcom ⊢ ( 𝐴 ∈ Sℋ → ( 𝑥 = 0ℎ → ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ) ) )
18 10 17 impbid ⊢ ( 𝐴 ∈ Sℋ → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ) ↔ 𝑥 = 0ℎ ) )
19 elin ⊢ ( 𝑥 ∈ ( 𝐴 ∩ ( ⊥ ‘ 𝐴 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ) )
20 elch0 ⊢ ( 𝑥 ∈ 0ℋ ↔ 𝑥 = 0ℎ )
21 18 19 20 3bitr4g ⊢ ( 𝐴 ∈ Sℋ → ( 𝑥 ∈ ( 𝐴 ∩ ( ⊥ ‘ 𝐴 ) ) ↔ 𝑥 ∈ 0ℋ ) )
22 21 eqrdv ⊢ ( 𝐴 ∈ Sℋ → ( 𝐴 ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ )