Theorem hgmapfval

Description: Map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. (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	⊢ ( 𝜑 → ( 𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻 ) )
Assertion	hgmapfval	⊢ ( 𝜑 → 𝐼 = ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) ) )

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	1	hgmapffval	⊢ ( 𝐾 ∈ 𝑌 → ( HGMap ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ ( ( HDMap ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) } ) )
13	12	fveq1d	⊢ ( 𝐾 ∈ 𝑌 → ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) = ( ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ ( ( HDMap ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) } ) ‘ 𝑊 ) )
14	10 13	eqtrid	⊢ ( 𝐾 ∈ 𝑌 → 𝐼 = ( ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ ( ( HDMap ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) } ) ‘ 𝑊 ) )
15		fveq2	⊢ ( 𝑤 = 𝑊 → ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
16	15 2	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) = 𝑈 )
17		fveq2	⊢ ( 𝑤 = 𝑊 → ( ( HDMap ‘ 𝐾 ) ‘ 𝑤 ) = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) )
18	17 9	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( ( HDMap ‘ 𝐾 ) ‘ 𝑤 ) = 𝑀 )
19		2fveq3	⊢ ( 𝑤 = 𝑊 → ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) = ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
20	19	oveqd	⊢ ( 𝑤 = 𝑊 → ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) )
21	20	eqeq2d	⊢ ( 𝑤 = 𝑊 → ( ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ↔ ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ) )
22	21	ralbidv	⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ↔ ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ) )
23	22	riotabidv	⊢ ( 𝑤 = 𝑊 → ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) = ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ) )
24	23	mpteq2dv	⊢ ( 𝑤 = 𝑊 → ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) = ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) )
25	24	eleq2d	⊢ ( 𝑤 = 𝑊 → ( 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) ↔ 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) ) )
26	18 25	sbceqbid	⊢ ( 𝑤 = 𝑊 → ( [ ( ( HDMap ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) ↔ [ 𝑀 / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) ) )
27	26	sbcbidv	⊢ ( 𝑤 = 𝑊 → ( [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ ( ( HDMap ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) ↔ [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ 𝑀 / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) ) )
28	16 27	sbceqbid	⊢ ( 𝑤 = 𝑊 → ( [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ ( ( HDMap ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) ↔ [ 𝑈 / 𝑢 ] [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ 𝑀 / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) ) )
29	2	fvexi	⊢ 𝑈 ∈ V
30		fvex	⊢ ( Base ‘ ( Scalar ‘ 𝑢 ) ) ∈ V
31	9	fvexi	⊢ 𝑀 ∈ V
32		simp2	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = ( Base ‘ ( Scalar ‘ 𝑢 ) ) ∧ 𝑚 = 𝑀 ) → 𝑏 = ( Base ‘ ( Scalar ‘ 𝑢 ) ) )
33		simp1	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = ( Base ‘ ( Scalar ‘ 𝑢 ) ) ∧ 𝑚 = 𝑀 ) → 𝑢 = 𝑈 )
34	33	fveq2d	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = ( Base ‘ ( Scalar ‘ 𝑢 ) ) ∧ 𝑚 = 𝑀 ) → ( Scalar ‘ 𝑢 ) = ( Scalar ‘ 𝑈 ) )
35	34 5	eqtr4di	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = ( Base ‘ ( Scalar ‘ 𝑢 ) ) ∧ 𝑚 = 𝑀 ) → ( Scalar ‘ 𝑢 ) = 𝑅 )
36	35	fveq2d	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = ( Base ‘ ( Scalar ‘ 𝑢 ) ) ∧ 𝑚 = 𝑀 ) → ( Base ‘ ( Scalar ‘ 𝑢 ) ) = ( Base ‘ 𝑅 ) )
37	32 36	eqtrd	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = ( Base ‘ ( Scalar ‘ 𝑢 ) ) ∧ 𝑚 = 𝑀 ) → 𝑏 = ( Base ‘ 𝑅 ) )
38	37 6	eqtr4di	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = ( Base ‘ ( Scalar ‘ 𝑢 ) ) ∧ 𝑚 = 𝑀 ) → 𝑏 = 𝐵 )
39		simp2	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → 𝑏 = 𝐵 )
40		simp1	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → 𝑢 = 𝑈 )
41	40	fveq2d	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( Base ‘ 𝑢 ) = ( Base ‘ 𝑈 ) )
42	41 3	eqtr4di	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( Base ‘ 𝑢 ) = 𝑉 )
43		simp3	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → 𝑚 = 𝑀 )
44	40	fveq2d	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( ·𝑠 ‘ 𝑢 ) = ( ·𝑠 ‘ 𝑈 ) )
45	44 4	eqtr4di	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( ·𝑠 ‘ 𝑢 ) = · )
46	45	oveqd	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) = ( 𝑥 · 𝑣 ) )
47	43 46	fveq12d	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) )
48		eqidd	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
49	48 7	eqtr4di	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) = 𝐶 )
50	49	fveq2d	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ·𝑠 ‘ 𝐶 ) )
51	50 8	eqtr4di	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ∙ )
52		eqidd	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → 𝑦 = 𝑦 )
53	43	fveq1d	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( 𝑚 ‘ 𝑣 ) = ( 𝑀 ‘ 𝑣 ) )
54	51 52 53	oveq123d	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) )
55	47 54	eqeq12d	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ↔ ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) )
56	42 55	raleqbidv	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ↔ ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) )
57	39 56	riotaeqbidv	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ) = ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) )
58	39 57	mpteq12dv	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) = ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) ) )
59	58	eleq2d	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) ↔ 𝑎 ∈ ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) ) ) )
60	38 59	syld3an2	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = ( Base ‘ ( Scalar ‘ 𝑢 ) ) ∧ 𝑚 = 𝑀 ) → ( 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) ↔ 𝑎 ∈ ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) ) ) )
61	29 30 31 60	sbc3ie	⊢ ( [ 𝑈 / 𝑢 ] [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ 𝑀 / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) ↔ 𝑎 ∈ ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) ) )
62	28 61	bitrdi	⊢ ( 𝑤 = 𝑊 → ( [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ ( ( HDMap ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) ↔ 𝑎 ∈ ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) ) ) )
63	62	eqabcdv	⊢ ( 𝑤 = 𝑊 → { 𝑎 ∣ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ ( ( HDMap ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) } = ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) ) )
64		eqid	⊢ ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ ( ( HDMap ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) } ) = ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ ( ( HDMap ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) } )
65	63 64 6	mptfvmpt	⊢ ( 𝑊 ∈ 𝐻 → ( ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ ( ( HDMap ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) } ) ‘ 𝑊 ) = ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) ) )
66	14 65	sylan9eq	⊢ ( ( 𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻 ) → 𝐼 = ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) ) )
67	11 66	syl	⊢ ( 𝜑 → 𝐼 = ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) ) )