Metamath Proof Explorer

Theorem sspz

Description: The zero vector of a subspace is the same as the parent's. (Contributed by NM, 28-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses sspz.z ⊢ Z = 0 vec ⁡ U
sspz.q ⊢ Q = 0 vec ⁡ W
sspz.h ⊢ H = SubSp ⁡ U
Assertion sspz ⊢ U ∈ NrmCVec ∧ W ∈ H → Q = Z

Proof

Step Hyp Ref Expression
1 sspz.z ⊢ Z = 0 vec ⁡ U
2 sspz.q ⊢ Q = 0 vec ⁡ W
3 sspz.h ⊢ H = SubSp ⁡ U
4 3 sspnv ⊢ U ∈ NrmCVec ∧ W ∈ H → W ∈ NrmCVec
5 eqid ⊢ BaseSet ⁡ W = BaseSet ⁡ W
6 5 2 nvzcl ⊢ W ∈ NrmCVec → Q ∈ BaseSet ⁡ W
7 6 6 jca ⊢ W ∈ NrmCVec → Q ∈ BaseSet ⁡ W ∧ Q ∈ BaseSet ⁡ W
8 4 7 syl ⊢ U ∈ NrmCVec ∧ W ∈ H → Q ∈ BaseSet ⁡ W ∧ Q ∈ BaseSet ⁡ W
9 eqid ⊢ - v ⁡ U = - v ⁡ U
10 eqid ⊢ - v ⁡ W = - v ⁡ W
11 5 9 10 3 sspmval ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ Q ∈ BaseSet ⁡ W ∧ Q ∈ BaseSet ⁡ W → Q - v ⁡ W Q = Q - v ⁡ U Q
12 8 11 mpdan ⊢ U ∈ NrmCVec ∧ W ∈ H → Q - v ⁡ W Q = Q - v ⁡ U Q
13 5 10 2 nvmid ⊢ W ∈ NrmCVec ∧ Q ∈ BaseSet ⁡ W → Q - v ⁡ W Q = Q
14 4 6 13 syl2anc2 ⊢ U ∈ NrmCVec ∧ W ∈ H → Q - v ⁡ W Q = Q
15 eqid ⊢ BaseSet ⁡ U = BaseSet ⁡ U
16 15 5 3 sspba ⊢ U ∈ NrmCVec ∧ W ∈ H → BaseSet ⁡ W ⊆ BaseSet ⁡ U
17 4 6 syl ⊢ U ∈ NrmCVec ∧ W ∈ H → Q ∈ BaseSet ⁡ W
18 16 17 sseldd ⊢ U ∈ NrmCVec ∧ W ∈ H → Q ∈ BaseSet ⁡ U
19 15 9 1 nvmid ⊢ U ∈ NrmCVec ∧ Q ∈ BaseSet ⁡ U → Q - v ⁡ U Q = Z
20 18 19 syldan ⊢ U ∈ NrmCVec ∧ W ∈ H → Q - v ⁡ U Q = Z
21 12 14 20 3eqtr3d ⊢ U ∈ NrmCVec ∧ W ∈ H → Q = Z