Metamath Proof Explorer


Theorem sspm

Description: Vector subtraction on a subspace is a restriction of vector subtraction on the parent space. (Contributed by NM, 28-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses sspm.y 𝑌 = ( BaseSet ‘ 𝑊 )
sspm.m 𝑀 = ( −𝑣𝑈 )
sspm.l 𝐿 = ( −𝑣𝑊 )
sspm.h 𝐻 = ( SubSp ‘ 𝑈 )
Assertion sspm ( ( 𝑈 ∈ NrmCVec ∧ 𝑊𝐻 ) → 𝐿 = ( 𝑀 ↾ ( 𝑌 × 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 sspm.y 𝑌 = ( BaseSet ‘ 𝑊 )
2 sspm.m 𝑀 = ( −𝑣𝑈 )
3 sspm.l 𝐿 = ( −𝑣𝑊 )
4 sspm.h 𝐻 = ( SubSp ‘ 𝑈 )
5 1 2 3 4 sspmval ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊𝐻 ) ∧ ( 𝑥𝑌𝑦𝑌 ) ) → ( 𝑥 𝐿 𝑦 ) = ( 𝑥 𝑀 𝑦 ) )
6 1 3 nvmf ( 𝑊 ∈ NrmCVec → 𝐿 : ( 𝑌 × 𝑌 ) ⟶ 𝑌 )
7 eqid ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 )
8 7 2 nvmf ( 𝑈 ∈ NrmCVec → 𝑀 : ( ( BaseSet ‘ 𝑈 ) × ( BaseSet ‘ 𝑈 ) ) ⟶ ( BaseSet ‘ 𝑈 ) )
9 1 4 5 6 8 sspmlem ( ( 𝑈 ∈ NrmCVec ∧ 𝑊𝐻 ) → 𝐿 = ( 𝑀 ↾ ( 𝑌 × 𝑌 ) ) )