Metamath Proof Explorer

Definition df-hdmap

Description: Define map from vectors to functionals in the closed kernel dual space. See hdmapfval description for more details. (Contributed by NM, 15-May-2015)

Ref Expression
Assertion df-hdmap HDMap = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑎 ∣ [ ⟨ ( I ↾ ( Base ‘ 𝑘 ) ) , ( I ↾ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ) ⟩ / 𝑒 ] [ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝑘 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 chdma ⊢ HDMap
1 vk ⊢ 𝑘
2 cvv ⊢ V
3 vw ⊢ 𝑤
4 clh ⊢ LHyp
5 1 cv ⊢ 𝑘
6 5 4 cfv ⊢ ( LHyp ‘ 𝑘 )
7 va ⊢ 𝑎
8 cid ⊢ I
9 cbs ⊢ Base
10 5 9 cfv ⊢ ( Base ‘ 𝑘 )
11 8 10 cres ⊢ ( I ↾ ( Base ‘ 𝑘 ) )
12 cltrn ⊢ LTrn
13 5 12 cfv ⊢ ( LTrn ‘ 𝑘 )
14 3 cv ⊢ 𝑤
15 14 13 cfv ⊢ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 )
16 8 15 cres ⊢ ( I ↾ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) )
17 11 16 cop ⊢ ⟨ ( I ↾ ( Base ‘ 𝑘 ) ) , ( I ↾ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ) ⟩
18 ve ⊢ 𝑒
19 cdvh ⊢ DVecH
20 5 19 cfv ⊢ ( DVecH ‘ 𝑘 )
21 14 20 cfv ⊢ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 )
22 vu ⊢ 𝑢
23 22 cv ⊢ 𝑢
24 23 9 cfv ⊢ ( Base ‘ 𝑢 )
25 vv ⊢ 𝑣
26 chdma1 ⊢ HDMap1
27 5 26 cfv ⊢ ( HDMap1 ‘ 𝑘 )
28 14 27 cfv ⊢ ( ( HDMap1 ‘ 𝑘 ) ‘ 𝑤 )
29 vi ⊢ 𝑖
30 7 cv ⊢ 𝑎
31 vt ⊢ 𝑡
32 25 cv ⊢ 𝑣
33 vy ⊢ 𝑦
34 clcd ⊢ LCDual
35 5 34 cfv ⊢ ( LCDual ‘ 𝑘 )
36 14 35 cfv ⊢ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 )
37 36 9 cfv ⊢ ( Base ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) )
38 vz ⊢ 𝑧
39 38 cv ⊢ 𝑧
40 clspn ⊢ LSpan
41 23 40 cfv ⊢ ( LSpan ‘ 𝑢 )
42 18 cv ⊢ 𝑒
43 42 csn ⊢ { 𝑒 }
44 43 41 cfv ⊢ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } )
45 31 cv ⊢ 𝑡
46 45 csn ⊢ { 𝑡 }
47 46 41 cfv ⊢ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } )
48 44 47 cun ⊢ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) )
49 39 48 wcel ⊢ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) )
50 49 wn ⊢ ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) )
51 33 cv ⊢ 𝑦
52 29 cv ⊢ 𝑖
53 chvm ⊢ HVMap
54 5 53 cfv ⊢ ( HVMap ‘ 𝑘 )
55 14 54 cfv ⊢ ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 )
56 42 55 cfv ⊢ ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 )
57 42 56 39 cotp ⊢ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩
58 57 52 cfv ⊢ ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ )
59 39 58 45 cotp ⊢ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩
60 59 52 cfv ⊢ ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ )
61 51 60 wceq ⊢ 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ )
62 50 61 wi ⊢ ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) )
63 62 38 32 wral ⊢ ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) )
64 63 33 37 crio ⊢ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) )
65 31 32 64 cmpt ⊢ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) )
66 30 65 wcel ⊢ 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) )
67 66 29 28 wsbc ⊢ [ ( ( HDMap1 ‘ 𝑘 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) )
68 67 25 24 wsbc ⊢ [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝑘 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) )
69 68 22 21 wsbc ⊢ [ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝑘 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) )
70 69 18 17 wsbc ⊢ [ ⟨ ( I ↾ ( Base ‘ 𝑘 ) ) , ( I ↾ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ) ⟩ / 𝑒 ] [ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝑘 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) )
71 70 7 cab ⊢ { 𝑎 ∣ [ ⟨ ( I ↾ ( Base ‘ 𝑘 ) ) , ( I ↾ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ) ⟩ / 𝑒 ] [ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝑘 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) }
72 3 6 71 cmpt ⊢ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑎 ∣ [ ⟨ ( I ↾ ( Base ‘ 𝑘 ) ) , ( I ↾ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ) ⟩ / 𝑒 ] [ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝑘 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) } )
73 1 2 72 cmpt ⊢ ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑎 ∣ [ ⟨ ( I ↾ ( Base ‘ 𝑘 ) ) , ( I ↾ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ) ⟩ / 𝑒 ] [ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝑘 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) } ) )
74 0 73 wceq ⊢ HDMap = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑎 ∣ [ ⟨ ( I ↾ ( Base ‘ 𝑘 ) ) , ( I ↾ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ) ⟩ / 𝑒 ] [ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝑘 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) } ) )