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	⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐴 · 𝑌 ) ) ‘ 𝑋 ) = ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝑋 ) × ( 𝐺 ‘ 𝐴 ) ) )

Metamath Proof Explorer

Theorem hdmapglnm2

Proof