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 syl6bi ( 𝐴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 )