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 𝑍 = ( 0vec𝑈 )
sspz.q 𝑄 = ( 0vec𝑊 )
sspz.h 𝐻 = ( SubSp ‘ 𝑈 )
Assertion sspz ( ( 𝑈 ∈ NrmCVec ∧ 𝑊𝐻 ) → 𝑄 = 𝑍 )

Proof

Step Hyp Ref Expression
1 sspz.z 𝑍 = ( 0vec𝑈 )
2 sspz.q 𝑄 = ( 0vec𝑊 )
3 sspz.h 𝐻 = ( SubSp ‘ 𝑈 )
4 3 sspnv ( ( 𝑈 ∈ NrmCVec ∧ 𝑊𝐻 ) → 𝑊 ∈ NrmCVec )
5 eqid ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 )
6 5 2 nvzcl ( 𝑊 ∈ NrmCVec → 𝑄 ∈ ( BaseSet ‘ 𝑊 ) )
7 6 6 jca ( 𝑊 ∈ NrmCVec → ( 𝑄 ∈ ( BaseSet ‘ 𝑊 ) ∧ 𝑄 ∈ ( BaseSet ‘ 𝑊 ) ) )
8 4 7 syl ( ( 𝑈 ∈ NrmCVec ∧ 𝑊𝐻 ) → ( 𝑄 ∈ ( BaseSet ‘ 𝑊 ) ∧ 𝑄 ∈ ( BaseSet ‘ 𝑊 ) ) )
9 eqid ( −𝑣𝑈 ) = ( −𝑣𝑈 )
10 eqid ( −𝑣𝑊 ) = ( −𝑣𝑊 )
11 5 9 10 3 sspmval ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊𝐻 ) ∧ ( 𝑄 ∈ ( BaseSet ‘ 𝑊 ) ∧ 𝑄 ∈ ( BaseSet ‘ 𝑊 ) ) ) → ( 𝑄 ( −𝑣𝑊 ) 𝑄 ) = ( 𝑄 ( −𝑣𝑈 ) 𝑄 ) )
12 8 11 mpdan ( ( 𝑈 ∈ NrmCVec ∧ 𝑊𝐻 ) → ( 𝑄 ( −𝑣𝑊 ) 𝑄 ) = ( 𝑄 ( −𝑣𝑈 ) 𝑄 ) )
13 5 10 2 nvmid ( ( 𝑊 ∈ NrmCVec ∧ 𝑄 ∈ ( BaseSet ‘ 𝑊 ) ) → ( 𝑄 ( −𝑣𝑊 ) 𝑄 ) = 𝑄 )
14 4 6 13 syl2anc2 ( ( 𝑈 ∈ NrmCVec ∧ 𝑊𝐻 ) → ( 𝑄 ( −𝑣𝑊 ) 𝑄 ) = 𝑄 )
15 eqid ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 )
16 15 5 3 sspba ( ( 𝑈 ∈ NrmCVec ∧ 𝑊𝐻 ) → ( BaseSet ‘ 𝑊 ) ⊆ ( BaseSet ‘ 𝑈 ) )
17 4 6 syl ( ( 𝑈 ∈ NrmCVec ∧ 𝑊𝐻 ) → 𝑄 ∈ ( BaseSet ‘ 𝑊 ) )
18 16 17 sseldd ( ( 𝑈 ∈ NrmCVec ∧ 𝑊𝐻 ) → 𝑄 ∈ ( BaseSet ‘ 𝑈 ) )
19 15 9 1 nvmid ( ( 𝑈 ∈ NrmCVec ∧ 𝑄 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑄 ( −𝑣𝑈 ) 𝑄 ) = 𝑍 )
20 18 19 syldan ( ( 𝑈 ∈ NrmCVec ∧ 𝑊𝐻 ) → ( 𝑄 ( −𝑣𝑈 ) 𝑄 ) = 𝑍 )
21 12 14 20 3eqtr3d ( ( 𝑈 ∈ NrmCVec ∧ 𝑊𝐻 ) → 𝑄 = 𝑍 )