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 ∧ 𝑊 ∈ 𝐻 ) → 𝑄 = 𝑍 )