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ℋ )