Metamath Proof Explorer


Theorem sspgval

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

Ref Expression
Hypotheses sspg.y 𝑌 = ( BaseSet ‘ 𝑊 )
sspg.g 𝐺 = ( +𝑣𝑈 )
sspg.f 𝐹 = ( +𝑣𝑊 )
sspg.h 𝐻 = ( SubSp ‘ 𝑈 )
Assertion sspgval ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊𝐻 ) ∧ ( 𝐴𝑌𝐵𝑌 ) ) → ( 𝐴 𝐹 𝐵 ) = ( 𝐴 𝐺 𝐵 ) )

Proof

Step Hyp Ref Expression
1 sspg.y 𝑌 = ( BaseSet ‘ 𝑊 )
2 sspg.g 𝐺 = ( +𝑣𝑈 )
3 sspg.f 𝐹 = ( +𝑣𝑊 )
4 sspg.h 𝐻 = ( SubSp ‘ 𝑈 )
5 1 2 3 4 sspg ( ( 𝑈 ∈ NrmCVec ∧ 𝑊𝐻 ) → 𝐹 = ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) )
6 5 oveqd ( ( 𝑈 ∈ NrmCVec ∧ 𝑊𝐻 ) → ( 𝐴 𝐹 𝐵 ) = ( 𝐴 ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) 𝐵 ) )
7 ovres ( ( 𝐴𝑌𝐵𝑌 ) → ( 𝐴 ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) 𝐵 ) = ( 𝐴 𝐺 𝐵 ) )
8 6 7 sylan9eq ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊𝐻 ) ∧ ( 𝐴𝑌𝐵𝑌 ) ) → ( 𝐴 𝐹 𝐵 ) = ( 𝐴 𝐺 𝐵 ) )