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

Metamath Proof Explorer

Theorem hdmapgln2

Proof