Theorem hgmapvs

Description: Part 15 of Baer p. 50 line 6. Also line 15 in Holland95 p. 14. (Contributed by NM, 6-Jun-2015)

	Ref	Expression
Hypotheses	hgmapvs.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hgmapvs.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hgmapvs.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	hgmapvs.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
	hgmapvs.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
	hgmapvs.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	hgmapvs.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	hgmapvs.e	⊢ ∙ = ( ·𝑠 ‘ 𝐶 )
	hgmapvs.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
	hgmapvs.g	⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
	hgmapvs.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	hgmapvs.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	hgmapvs.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
Assertion	hgmapvs	⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( ( 𝐺 ‘ 𝐹 ) ∙ ( 𝑆 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		hgmapvs.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hgmapvs.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		hgmapvs.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
4		hgmapvs.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
5		hgmapvs.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
6		hgmapvs.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
7		hgmapvs.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
8		hgmapvs.e	⊢ ∙ = ( ·𝑠 ‘ 𝐶 )
9		hgmapvs.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
10		hgmapvs.g	⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
11		hgmapvs.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12		hgmapvs.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
13		hgmapvs.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
14	1 2 3 4 5 6 7 8 9 10 11 13	hgmapval	⊢ ( 𝜑 → ( 𝐺 ‘ 𝐹 ) = ( ℩ 𝑔 ∈ 𝐵 ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑥 ) ) ) )
15	14	eqcomd	⊢ ( 𝜑 → ( ℩ 𝑔 ∈ 𝐵 ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑥 ) ) ) = ( 𝐺 ‘ 𝐹 ) )
16	1 2 5 6 10 11 13	hgmapcl	⊢ ( 𝜑 → ( 𝐺 ‘ 𝐹 ) ∈ 𝐵 )
17	1 2 3 4 5 6 7 8 9 11 13	hdmap14lem15	⊢ ( 𝜑 → ∃! 𝑔 ∈ 𝐵 ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑥 ) ) )
18		oveq1	⊢ ( 𝑔 = ( 𝐺 ‘ 𝐹 ) → ( 𝑔 ∙ ( 𝑆 ‘ 𝑥 ) ) = ( ( 𝐺 ‘ 𝐹 ) ∙ ( 𝑆 ‘ 𝑥 ) ) )
19	18	eqeq2d	⊢ ( 𝑔 = ( 𝐺 ‘ 𝐹 ) → ( ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑥 ) ) ↔ ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( ( 𝐺 ‘ 𝐹 ) ∙ ( 𝑆 ‘ 𝑥 ) ) ) )
20	19	ralbidv	⊢ ( 𝑔 = ( 𝐺 ‘ 𝐹 ) → ( ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( ( 𝐺 ‘ 𝐹 ) ∙ ( 𝑆 ‘ 𝑥 ) ) ) )
21	20	riota2	⊢ ( ( ( 𝐺 ‘ 𝐹 ) ∈ 𝐵 ∧ ∃! 𝑔 ∈ 𝐵 ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑥 ) ) ) → ( ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( ( 𝐺 ‘ 𝐹 ) ∙ ( 𝑆 ‘ 𝑥 ) ) ↔ ( ℩ 𝑔 ∈ 𝐵 ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑥 ) ) ) = ( 𝐺 ‘ 𝐹 ) ) )
22	16 17 21	syl2anc	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( ( 𝐺 ‘ 𝐹 ) ∙ ( 𝑆 ‘ 𝑥 ) ) ↔ ( ℩ 𝑔 ∈ 𝐵 ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑥 ) ) ) = ( 𝐺 ‘ 𝐹 ) ) )
23	15 22	mpbird	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( ( 𝐺 ‘ 𝐹 ) ∙ ( 𝑆 ‘ 𝑥 ) ) )
24		oveq2	⊢ ( 𝑥 = 𝑋 → ( 𝐹 · 𝑥 ) = ( 𝐹 · 𝑋 ) )
25	24	fveq2d	⊢ ( 𝑥 = 𝑋 → ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) )
26		fveq2	⊢ ( 𝑥 = 𝑋 → ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑋 ) )
27	26	oveq2d	⊢ ( 𝑥 = 𝑋 → ( ( 𝐺 ‘ 𝐹 ) ∙ ( 𝑆 ‘ 𝑥 ) ) = ( ( 𝐺 ‘ 𝐹 ) ∙ ( 𝑆 ‘ 𝑋 ) ) )
28	25 27	eqeq12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( ( 𝐺 ‘ 𝐹 ) ∙ ( 𝑆 ‘ 𝑥 ) ) ↔ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( ( 𝐺 ‘ 𝐹 ) ∙ ( 𝑆 ‘ 𝑋 ) ) ) )
29	28	rspcva	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( ( 𝐺 ‘ 𝐹 ) ∙ ( 𝑆 ‘ 𝑥 ) ) ) → ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( ( 𝐺 ‘ 𝐹 ) ∙ ( 𝑆 ‘ 𝑋 ) ) )
30	12 23 29	syl2anc	⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( ( 𝐺 ‘ 𝐹 ) ∙ ( 𝑆 ‘ 𝑋 ) ) )