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 e. NrmCVec /\ W e. 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 e. NrmCVec /\ W e. H ) -> W e. NrmCVec )
5 eqid 
 |-  ( BaseSet ` W ) = ( BaseSet ` W )
6 5 2 nvzcl 
 |-  ( W e. NrmCVec -> Q e. ( BaseSet ` W ) )
7 6 6 jca 
 |-  ( W e. NrmCVec -> ( Q e. ( BaseSet ` W ) /\ Q e. ( BaseSet ` W ) ) )
8 4 7 syl 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( Q e. ( BaseSet ` W ) /\ Q e. ( BaseSet ` W ) ) )
9 eqid 
 |-  ( -v ` U ) = ( -v ` U )
10 eqid 
 |-  ( -v ` W ) = ( -v ` W )
11 5 9 10 3 sspmval 
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( Q e. ( BaseSet ` W ) /\ Q e. ( BaseSet ` W ) ) ) -> ( Q ( -v ` W ) Q ) = ( Q ( -v ` U ) Q ) )
12 8 11 mpdan 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( Q ( -v ` W ) Q ) = ( Q ( -v ` U ) Q ) )
13 5 10 2 nvmid 
 |-  ( ( W e. NrmCVec /\ Q e. ( BaseSet ` W ) ) -> ( Q ( -v ` W ) Q ) = Q )
14 4 6 13 syl2anc2 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( Q ( -v ` W ) Q ) = Q )
15 eqid 
 |-  ( BaseSet ` U ) = ( BaseSet ` U )
16 15 5 3 sspba 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( BaseSet ` W ) C_ ( BaseSet ` U ) )
17 4 6 syl 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> Q e. ( BaseSet ` W ) )
18 16 17 sseldd 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> Q e. ( BaseSet ` U ) )
19 15 9 1 nvmid 
 |-  ( ( U e. NrmCVec /\ Q e. ( BaseSet ` U ) ) -> ( Q ( -v ` U ) Q ) = Z )
20 18 19 syldan 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( Q ( -v ` U ) Q ) = Z )
21 12 14 20 3eqtr3d 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> Q = Z )