Metamath Proof Explorer

Theorem hdmapglnm2

Description: g-linear property of second (inner product) argument. Line 19 in Holland95 p. 14. (Contributed by NM, 10-Jun-2015)

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

Proof

Step Hyp Ref Expression
1 hdmapglnm2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmapglnm2.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hdmapglnm2.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 hdmapglnm2.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
5 hdmapglnm2.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
6 hdmapglnm2.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
7 hdmapglnm2.m ⊢ × = ( .r ‘ 𝑅 )
8 hdmapglnm2.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
9 hdmapglnm2.g ⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
10 hdmapglnm2.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
11 hdmapglnm2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
12 hdmapglnm2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
13 hdmapglnm2.z ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
14 eqid ⊢ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
15 eqid ⊢ ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
16 1 2 3 4 5 6 14 15 8 9 10 12 13 hgmapvs ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐴 · 𝑌 ) ) = ( ( 𝐺 ‘ 𝐴 ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑆 ‘ 𝑌 ) ) )
17 16 fveq1d ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐴 · 𝑌 ) ) ‘ 𝑋 ) = ( ( ( 𝐺 ‘ 𝐴 ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑆 ‘ 𝑌 ) ) ‘ 𝑋 ) )
18 eqid ⊢ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
19 1 2 5 6 9 10 13 hgmapcl ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐴 ) ∈ 𝐵 )
20 1 2 3 14 18 8 10 12 hdmapcl ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑌 ) ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
21 1 2 3 5 6 7 14 18 15 10 19 20 11 lcdvsval ⊢ ( 𝜑 → ( ( ( 𝐺 ‘ 𝐴 ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑆 ‘ 𝑌 ) ) ‘ 𝑋 ) = ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝑋 ) × ( 𝐺 ‘ 𝐴 ) ) )
22 17 21 eqtrd ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐴 · 𝑌 ) ) ‘ 𝑋 ) = ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝑋 ) × ( 𝐺 ‘ 𝐴 ) ) )