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