Theorem choc0

Description: The orthocomplement of the zero subspace is the unit subspace. (Contributed by NM, 15-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	choc0	⊢ ( ⊥ ‘ 0ℋ ) = ℋ

Proof

Step	Hyp	Ref	Expression
1		h0elsh	⊢ 0ℋ ∈ Sℋ
2		shocel	⊢ ( 0ℋ ∈ Sℋ → ( 𝑥 ∈ ( ⊥ ‘ 0ℋ ) ↔ ( 𝑥 ∈ ℋ ∧ ∀ 𝑦 ∈ 0ℋ ( 𝑥 ·ih 𝑦 ) = 0 ) ) )
3	1 2	ax-mp	⊢ ( 𝑥 ∈ ( ⊥ ‘ 0ℋ ) ↔ ( 𝑥 ∈ ℋ ∧ ∀ 𝑦 ∈ 0ℋ ( 𝑥 ·ih 𝑦 ) = 0 ) )
4		hi02	⊢ ( 𝑥 ∈ ℋ → ( 𝑥 ·ih 0ℎ ) = 0 )
5		df-ral	⊢ ( ∀ 𝑦 ∈ 0ℋ ( 𝑥 ·ih 𝑦 ) = 0 ↔ ∀ 𝑦 ( 𝑦 ∈ 0ℋ → ( 𝑥 ·ih 𝑦 ) = 0 ) )
6		elch0	⊢ ( 𝑦 ∈ 0ℋ ↔ 𝑦 = 0ℎ )
7	6	imbi1i	⊢ ( ( 𝑦 ∈ 0ℋ → ( 𝑥 ·ih 𝑦 ) = 0 ) ↔ ( 𝑦 = 0ℎ → ( 𝑥 ·ih 𝑦 ) = 0 ) )
8	7	albii	⊢ ( ∀ 𝑦 ( 𝑦 ∈ 0ℋ → ( 𝑥 ·ih 𝑦 ) = 0 ) ↔ ∀ 𝑦 ( 𝑦 = 0ℎ → ( 𝑥 ·ih 𝑦 ) = 0 ) )
9		ax-hv0cl	⊢ 0ℎ ∈ ℋ
10	9	elexi	⊢ 0ℎ ∈ V
11		oveq2	⊢ ( 𝑦 = 0ℎ → ( 𝑥 ·ih 𝑦 ) = ( 𝑥 ·ih 0ℎ ) )
12	11	eqeq1d	⊢ ( 𝑦 = 0ℎ → ( ( 𝑥 ·ih 𝑦 ) = 0 ↔ ( 𝑥 ·ih 0ℎ ) = 0 ) )
13	10 12	ceqsalv	⊢ ( ∀ 𝑦 ( 𝑦 = 0ℎ → ( 𝑥 ·ih 𝑦 ) = 0 ) ↔ ( 𝑥 ·ih 0ℎ ) = 0 )
14	8 13	bitri	⊢ ( ∀ 𝑦 ( 𝑦 ∈ 0ℋ → ( 𝑥 ·ih 𝑦 ) = 0 ) ↔ ( 𝑥 ·ih 0ℎ ) = 0 )
15	5 14	bitri	⊢ ( ∀ 𝑦 ∈ 0ℋ ( 𝑥 ·ih 𝑦 ) = 0 ↔ ( 𝑥 ·ih 0ℎ ) = 0 )
16	4 15	sylibr	⊢ ( 𝑥 ∈ ℋ → ∀ 𝑦 ∈ 0ℋ ( 𝑥 ·ih 𝑦 ) = 0 )
17		abai	⊢ ( ( 𝑥 ∈ ℋ ∧ ∀ 𝑦 ∈ 0ℋ ( 𝑥 ·ih 𝑦 ) = 0 ) ↔ ( 𝑥 ∈ ℋ ∧ ( 𝑥 ∈ ℋ → ∀ 𝑦 ∈ 0ℋ ( 𝑥 ·ih 𝑦 ) = 0 ) ) )
18	16 17	mpbiran2	⊢ ( ( 𝑥 ∈ ℋ ∧ ∀ 𝑦 ∈ 0ℋ ( 𝑥 ·ih 𝑦 ) = 0 ) ↔ 𝑥 ∈ ℋ )
19	3 18	bitri	⊢ ( 𝑥 ∈ ( ⊥ ‘ 0ℋ ) ↔ 𝑥 ∈ ℋ )
20	19	eqriv	⊢ ( ⊥ ‘ 0ℋ ) = ℋ