Definition df-hvmap

Description: Extend class notation with a map from each nonzero vector x to a unique nonzero functional in the closed kernel dual space. (We could extend it to include the zero vector, but that is unnecessary for our purposes.) TODO: This pattern is used several times earlier, e.g., lcf1o , dochfl1 - should we update those to use this definition? (Contributed by NM, 23-Mar-2015)

	Ref	Expression
Assertion	df-hvmap	⊢ HVMap = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ ( ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) } ) ↦ ( 𝑣 ∈ ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ( ℩ 𝑗 ∈ ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ) ∃ 𝑡 ∈ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ { 𝑥 } ) 𝑣 = ( 𝑡 ( +g ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ( 𝑗 ( ·𝑠 ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) 𝑥 ) ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chvm	⊢ HVMap
1		vk	⊢ 𝑘
2		cvv	⊢ V
3		vw	⊢ 𝑤
4		clh	⊢ LHyp
5	1	cv	⊢ 𝑘
6	5 4	cfv	⊢ ( LHyp ‘ 𝑘 )
7		vx	⊢ 𝑥
8		cbs	⊢ Base
9		cdvh	⊢ DVecH
10	5 9	cfv	⊢ ( DVecH ‘ 𝑘 )
11	3	cv	⊢ 𝑤
12	11 10	cfv	⊢ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 )
13	12 8	cfv	⊢ ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) )
14		c0g	⊢ 0g
15	12 14	cfv	⊢ ( 0g ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) )
16	15	csn	⊢ { ( 0g ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) }
17	13 16	cdif	⊢ ( ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) } )
18		vv	⊢ 𝑣
19		vj	⊢ 𝑗
20		csca	⊢ Scalar
21	12 20	cfv	⊢ ( Scalar ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) )
22	21 8	cfv	⊢ ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) )
23		vt	⊢ 𝑡
24		coch	⊢ ocH
25	5 24	cfv	⊢ ( ocH ‘ 𝑘 )
26	11 25	cfv	⊢ ( ( ocH ‘ 𝑘 ) ‘ 𝑤 )
27	7	cv	⊢ 𝑥
28	27	csn	⊢ { 𝑥 }
29	28 26	cfv	⊢ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ { 𝑥 } )
30	18	cv	⊢ 𝑣
31	23	cv	⊢ 𝑡
32		cplusg	⊢ +g
33	12 32	cfv	⊢ ( +g ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) )
34	19	cv	⊢ 𝑗
35		cvsca	⊢ ·𝑠
36	12 35	cfv	⊢ ( ·𝑠 ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) )
37	34 27 36	co	⊢ ( 𝑗 ( ·𝑠 ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) 𝑥 )
38	31 37 33	co	⊢ ( 𝑡 ( +g ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ( 𝑗 ( ·𝑠 ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) 𝑥 ) )
39	30 38	wceq	⊢ 𝑣 = ( 𝑡 ( +g ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ( 𝑗 ( ·𝑠 ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) 𝑥 ) )
40	39 23 29	wrex	⊢ ∃ 𝑡 ∈ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ { 𝑥 } ) 𝑣 = ( 𝑡 ( +g ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ( 𝑗 ( ·𝑠 ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) 𝑥 ) )
41	40 19 22	crio	⊢ ( ℩ 𝑗 ∈ ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ) ∃ 𝑡 ∈ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ { 𝑥 } ) 𝑣 = ( 𝑡 ( +g ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ( 𝑗 ( ·𝑠 ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) 𝑥 ) ) )
42	18 13 41	cmpt	⊢ ( 𝑣 ∈ ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ( ℩ 𝑗 ∈ ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ) ∃ 𝑡 ∈ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ { 𝑥 } ) 𝑣 = ( 𝑡 ( +g ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ( 𝑗 ( ·𝑠 ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) 𝑥 ) ) ) )
43	7 17 42	cmpt	⊢ ( 𝑥 ∈ ( ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) } ) ↦ ( 𝑣 ∈ ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ( ℩ 𝑗 ∈ ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ) ∃ 𝑡 ∈ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ { 𝑥 } ) 𝑣 = ( 𝑡 ( +g ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ( 𝑗 ( ·𝑠 ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) 𝑥 ) ) ) ) )
44	3 6 43	cmpt	⊢ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ ( ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) } ) ↦ ( 𝑣 ∈ ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ( ℩ 𝑗 ∈ ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ) ∃ 𝑡 ∈ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ { 𝑥 } ) 𝑣 = ( 𝑡 ( +g ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ( 𝑗 ( ·𝑠 ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) 𝑥 ) ) ) ) ) )
45	1 2 44	cmpt	⊢ ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ ( ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) } ) ↦ ( 𝑣 ∈ ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ( ℩ 𝑗 ∈ ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ) ∃ 𝑡 ∈ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ { 𝑥 } ) 𝑣 = ( 𝑡 ( +g ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ( 𝑗 ( ·𝑠 ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) 𝑥 ) ) ) ) ) ) )
46	0 45	wceq	⊢ HVMap = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ ( ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) } ) ↦ ( 𝑣 ∈ ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ( ℩ 𝑗 ∈ ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ) ∃ 𝑡 ∈ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ { 𝑥 } ) 𝑣 = ( 𝑡 ( +g ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ( 𝑗 ( ·𝑠 ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) 𝑥 ) ) ) ) ) ) )