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=0vec⁡U
sspz.q ⊢Q=0vec⁡W
sspz.h ⊢H=SubSp⁡U
Assertion sspz ⊢U∈NrmCVec∧W∈H→Q=Z

Proof

Step Hyp Ref Expression
1 sspz.z ⊢Z=0vec⁡U
2 sspz.q ⊢Q=0vec⁡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⁡WQ=Q-v⁡UQ
12 8 11 mpdan ⊢U∈NrmCVec∧W∈H→Q-v⁡WQ=Q-v⁡UQ
13 5 10 2 nvmid ⊢W∈NrmCVec∧Q∈BaseSet⁡W→Q-v⁡WQ=Q
14 4 6 13 syl2anc2 ⊢U∈NrmCVec∧W∈H→Q-v⁡WQ=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⁡UQ=Z
20 18 19 syldan ⊢U∈NrmCVec∧W∈H→Q-v⁡UQ=Z
21 12 14 20 3eqtr3d ⊢U∈NrmCVec∧W∈H→Q=Z