Metamath Proof Explorer

Theorem dochoc1

Description: The unit subspace (all vectors) is closed. (Contributed by NM, 16-Feb-2015)

Ref Expression
Hypotheses dochoc1.h ⊢ H = LHyp ⁡ K
dochoc1.u ⊢ U = DVecH ⁡ K ⁡ W
dochoc1.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
dochoc1.v ⊢ V = Base U
dochoc1.k ⊢ φ → K ∈ HL ∧ W ∈ H
Assertion dochoc1 ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ V = V

Proof

Step Hyp Ref Expression
1 dochoc1.h ⊢ H = LHyp ⁡ K
2 dochoc1.u ⊢ U = DVecH ⁡ K ⁡ W
3 dochoc1.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
4 dochoc1.v ⊢ V = Base U
5 dochoc1.k ⊢ φ → K ∈ HL ∧ W ∈ H
6 eqid ⊢ 0 U = 0 U
7 1 2 3 4 6 doch1 ⊢ K ∈ HL ∧ W ∈ H → ⊥ ˙ ⁡ V = 0 U
8 7 fveq2d ⊢ K ∈ HL ∧ W ∈ H → ⊥ ˙ ⁡ ⊥ ˙ ⁡ V = ⊥ ˙ ⁡ 0 U
9 1 2 3 4 6 doch0 ⊢ K ∈ HL ∧ W ∈ H → ⊥ ˙ ⁡ 0 U = V
10 8 9 eqtrd ⊢ K ∈ HL ∧ W ∈ H → ⊥ ˙ ⁡ ⊥ ˙ ⁡ V = V
11 5 10 syl ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ V = V