Theorem hgmapval

Description: Value of map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. Function sigma of scalar f in part 14 of Baer p. 50 line 4. TODO: variable names are inherited from older version. Maybe make more consistent with hdmap14lem15 . (Contributed by NM, 25-Mar-2015)

	Ref	Expression
Hypotheses	hgmapval.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hgmapfval.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hgmapfval.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	hgmapfval.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
	hgmapfval.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
	hgmapfval.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	hgmapfval.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	hgmapfval.s	⊢ ∙ = ( ·𝑠 ‘ 𝐶 )
	hgmapfval.m	⊢ 𝑀 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
	hgmapfval.i	⊢ 𝐼 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
	hgmapfval.k	⊢ ( 𝜑 → ( 𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻 ) )
	hgmapval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	hgmapval	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑋 ) = ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑋 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		hgmapval.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hgmapfval.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		hgmapfval.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
4		hgmapfval.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
5		hgmapfval.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
6		hgmapfval.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
7		hgmapfval.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
8		hgmapfval.s	⊢ ∙ = ( ·𝑠 ‘ 𝐶 )
9		hgmapfval.m	⊢ 𝑀 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
10		hgmapfval.i	⊢ 𝐼 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
11		hgmapfval.k	⊢ ( 𝜑 → ( 𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻 ) )
12		hgmapval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
13	1 2 3 4 5 6 7 8 9 10 11	hgmapfval	⊢ ( 𝜑 → 𝐼 = ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) ) )
14	13	fveq1d	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑋 ) = ( ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) ) ‘ 𝑋 ) )
15		riotaex	⊢ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑋 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) ∈ V
16		fvoveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑀 ‘ ( 𝑋 · 𝑣 ) ) )
17	16	eqeq1d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ↔ ( 𝑀 ‘ ( 𝑋 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) )
18	17	ralbidv	⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ↔ ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑋 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) )
19	18	riotabidv	⊢ ( 𝑥 = 𝑋 → ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) = ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑋 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) )
20		eqid	⊢ ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) ) = ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) )
21	19 20	fvmptg	⊢ ( ( 𝑋 ∈ 𝐵 ∧ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑋 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) ∈ V ) → ( ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) ) ‘ 𝑋 ) = ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑋 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) )
22	12 15 21	sylancl	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) ) ‘ 𝑋 ) = ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑋 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) )
23	14 22	eqtrd	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑋 ) = ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑋 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) )