Metamath Proof Explorer

Theorem hdmapgln2

Description: g-linear property that will be used for inner product. (Contributed by NM, 14-Jun-2015)

Ref Expression
Hypotheses hdmapgln2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hdmapgln2.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmapgln2.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
hdmapgln2.p ⊢ + = ( +g ‘ 𝑈 )
hdmapgln2.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
hdmapgln2.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
hdmapgln2.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
hdmapgln2.q ⊢ ⨣ = ( +g ‘ 𝑅 )
hdmapgln2.m ⊢ × = ( .r ‘ 𝑅 )
hdmapgln2.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hdmapgln2.g ⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
hdmapgln2.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
hdmapgln2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
hdmapgln2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
hdmapgln2.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
hdmapgln2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
Assertion hdmapgln2 ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝐴 · 𝑌 ) + 𝑍 ) ) ‘ 𝑋 ) = ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝑋 ) × ( 𝐺 ‘ 𝐴 ) ) ⨣ ( ( 𝑆 ‘ 𝑍 ) ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 hdmapgln2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmapgln2.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hdmapgln2.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 hdmapgln2.p ⊢ + = ( +g ‘ 𝑈 )
5 hdmapgln2.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
6 hdmapgln2.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
7 hdmapgln2.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
8 hdmapgln2.q ⊢ ⨣ = ( +g ‘ 𝑅 )
9 hdmapgln2.m ⊢ × = ( .r ‘ 𝑅 )
10 hdmapgln2.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
11 hdmapgln2.g ⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
12 hdmapgln2.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13 hdmapgln2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
14 hdmapgln2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
15 hdmapgln2.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
16 hdmapgln2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
17 1 2 12 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
18 3 6 5 7 lmodvscl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝐴 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → ( 𝐴 · 𝑌 ) ∈ 𝑉 )
19 17 16 14 18 syl3anc ⊢ ( 𝜑 → ( 𝐴 · 𝑌 ) ∈ 𝑉 )
20 1 2 3 4 6 8 10 12 13 19 15 hdmaplna2 ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝐴 · 𝑌 ) + 𝑍 ) ) ‘ 𝑋 ) = ( ( ( 𝑆 ‘ ( 𝐴 · 𝑌 ) ) ‘ 𝑋 ) ⨣ ( ( 𝑆 ‘ 𝑍 ) ‘ 𝑋 ) ) )
21 1 2 3 5 6 7 9 10 11 12 13 14 16 hdmapglnm2 ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐴 · 𝑌 ) ) ‘ 𝑋 ) = ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝑋 ) × ( 𝐺 ‘ 𝐴 ) ) )
22 21 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ ( 𝐴 · 𝑌 ) ) ‘ 𝑋 ) ⨣ ( ( 𝑆 ‘ 𝑍 ) ‘ 𝑋 ) ) = ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝑋 ) × ( 𝐺 ‘ 𝐴 ) ) ⨣ ( ( 𝑆 ‘ 𝑍 ) ‘ 𝑋 ) ) )
23 20 22 eqtrd ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝐴 · 𝑌 ) + 𝑍 ) ) ‘ 𝑋 ) = ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝑋 ) × ( 𝐺 ‘ 𝐴 ) ) ⨣ ( ( 𝑆 ‘ 𝑍 ) ‘ 𝑋 ) ) )