Metamath Proof Explorer

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 ℋ → x ∈ ⊥ ⁡ 0 ℋ ↔ x ∈ ℋ ∧ ∀ y ∈ 0 ℋ x ⋅ ih y = 0
3 1 2 ax-mp ⊢ x ∈ ⊥ ⁡ 0 ℋ ↔ x ∈ ℋ ∧ ∀ y ∈ 0 ℋ x ⋅ ih y = 0
4 hi02 ⊢ x ∈ ℋ → x ⋅ ih 0 ℎ = 0
5 df-ral ⊢ ∀ y ∈ 0 ℋ x ⋅ ih y = 0 ↔ ∀ y y ∈ 0 ℋ → x ⋅ ih y = 0
6 elch0 ⊢ y ∈ 0 ℋ ↔ y = 0 ℎ
7 6 imbi1i ⊢ y ∈ 0 ℋ → x ⋅ ih y = 0 ↔ y = 0 ℎ → x ⋅ ih y = 0
8 7 albii ⊢ ∀ y y ∈ 0 ℋ → x ⋅ ih y = 0 ↔ ∀ y y = 0 ℎ → x ⋅ ih y = 0
9 ax-hv0cl ⊢ 0 ℎ ∈ ℋ
10 9 elexi ⊢ 0 ℎ ∈ V
11 oveq2 ⊢ y = 0 ℎ → x ⋅ ih y = x ⋅ ih 0 ℎ
12 11 eqeq1d ⊢ y = 0 ℎ → x ⋅ ih y = 0 ↔ x ⋅ ih 0 ℎ = 0
13 10 12 ceqsalv ⊢ ∀ y y = 0 ℎ → x ⋅ ih y = 0 ↔ x ⋅ ih 0 ℎ = 0
14 8 13 bitri ⊢ ∀ y y ∈ 0 ℋ → x ⋅ ih y = 0 ↔ x ⋅ ih 0 ℎ = 0
15 5 14 bitri ⊢ ∀ y ∈ 0 ℋ x ⋅ ih y = 0 ↔ x ⋅ ih 0 ℎ = 0
16 4 15 sylibr ⊢ x ∈ ℋ → ∀ y ∈ 0 ℋ x ⋅ ih y = 0
17 abai ⊢ x ∈ ℋ ∧ ∀ y ∈ 0 ℋ x ⋅ ih y = 0 ↔ x ∈ ℋ ∧ x ∈ ℋ → ∀ y ∈ 0 ℋ x ⋅ ih y = 0
18 16 17 mpbiran2 ⊢ x ∈ ℋ ∧ ∀ y ∈ 0 ℋ x ⋅ ih y = 0 ↔ x ∈ ℋ
19 3 18 bitri ⊢ x ∈ ⊥ ⁡ 0 ℋ ↔ x ∈ ℋ
20 19 eqriv ⊢ ⊥ ⁡ 0 ℋ = ℋ