Metamath Proof Explorer

Theorem hdmaplna1

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

Ref Expression
Hypotheses hdmaplna1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hdmaplna1.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmaplna1.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
hdmaplna1.p ⊢ + = ( +g ‘ 𝑈 )
hdmaplna1.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
hdmaplna1.q ⊢ ⨣ = ( +g ‘ 𝑅 )
hdmaplna1.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hdmaplna1.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
hdmaplna1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
hdmaplna1.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
hdmaplna1.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
Assertion hdmaplna1 ( 𝜑 → ( ( 𝑆 ‘ 𝑍 ) ‘ ( 𝑋 + 𝑌 ) ) = ( ( ( 𝑆 ‘ 𝑍 ) ‘ 𝑋 ) ⨣ ( ( 𝑆 ‘ 𝑍 ) ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 hdmaplna1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmaplna1.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hdmaplna1.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 hdmaplna1.p ⊢ + = ( +g ‘ 𝑈 )
5 hdmaplna1.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
6 hdmaplna1.q ⊢ ⨣ = ( +g ‘ 𝑅 )
7 hdmaplna1.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
8 hdmaplna1.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 hdmaplna1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
10 hdmaplna1.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
11 hdmaplna1.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 lfladd ⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝑆 ‘ 𝑍 ) ∈ ( LFnl ‘ 𝑈 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝑆 ‘ 𝑍 ) ‘ ( 𝑋 + 𝑌 ) ) = ( ( ( 𝑆 ‘ 𝑍 ) ‘ 𝑋 ) ⨣ ( ( 𝑆 ‘ 𝑍 ) ‘ 𝑌 ) ) )
19 12 17 9 10 18 syl112anc ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑍 ) ‘ ( 𝑋 + 𝑌 ) ) = ( ( ( 𝑆 ‘ 𝑍 ) ‘ 𝑋 ) ⨣ ( ( 𝑆 ‘ 𝑍 ) ‘ 𝑌 ) ) )