Metamath Proof Explorer

Theorem hdmaplns1

Description: Subtraction property of first (inner product) argument. (Contributed by NM, 12-Jun-2015)

Ref Expression
Hypotheses hdmaplns1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hdmaplns1.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmaplns1.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
hdmaplns1.m ⊢ − = ( -g ‘ 𝑈 )
hdmaplns1.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
hdmaplns1.n ⊢ 𝑁 = ( -g ‘ 𝑅 )
hdmaplns1.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hdmaplns1.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
hdmaplns1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
hdmaplns1.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
hdmaplns1.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
Assertion hdmaplns1 ( 𝜑 → ( ( 𝑆 ‘ 𝑍 ) ‘ ( 𝑋 − 𝑌 ) ) = ( ( ( 𝑆 ‘ 𝑍 ) ‘ 𝑋 ) 𝑁 ( ( 𝑆 ‘ 𝑍 ) ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 hdmaplns1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmaplns1.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hdmaplns1.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 hdmaplns1.m ⊢ − = ( -g ‘ 𝑈 )
5 hdmaplns1.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
6 hdmaplns1.n ⊢ 𝑁 = ( -g ‘ 𝑅 )
7 hdmaplns1.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
8 hdmaplns1.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 hdmaplns1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
10 hdmaplns1.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
11 hdmaplns1.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
12 1 2 8 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
13 eqid ⊢ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
14 eqid ⊢ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
15 eqid ⊢ ( LFnl ‘ 𝑈 ) = ( LFnl ‘ 𝑈 )
16 1 2 3 13 14 7 8 11 hdmapcl ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑍 ) ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
17 1 13 14 2 15 8 16 lcdvbaselfl ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑍 ) ∈ ( LFnl ‘ 𝑈 ) )
18 5 6 3 4 15 lflsub ⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝑆 ‘ 𝑍 ) ∈ ( LFnl ‘ 𝑈 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝑆 ‘ 𝑍 ) ‘ ( 𝑋 − 𝑌 ) ) = ( ( ( 𝑆 ‘ 𝑍 ) ‘ 𝑋 ) 𝑁 ( ( 𝑆 ‘ 𝑍 ) ‘ 𝑌 ) ) )
19 12 17 9 10 18 syl112anc ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑍 ) ‘ ( 𝑋 − 𝑌 ) ) = ( ( ( 𝑆 ‘ 𝑍 ) ‘ 𝑋 ) 𝑁 ( ( 𝑆 ‘ 𝑍 ) ‘ 𝑌 ) ) )