df-hdmap1

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

		Ref	Expression
	Assertion	df-hdmap1	⊢ HDMap1 = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chdma1	⊢ HDMap1
1		vk	⊢ 𝑘
2		cvv	⊢ V
3		vw	⊢ 𝑤
4		clh	⊢ LHyp
5	1	cv	⊢ 𝑘
6	5 4	cfv	⊢ ( LHyp ‘ 𝑘 )
7		va	⊢ 𝑎
8		cdvh	⊢ DVecH
9	5 8	cfv	⊢ ( DVecH ‘ 𝑘 )
10	3	cv	⊢ 𝑤
11	10 9	cfv	⊢ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 )
12		vu	⊢ 𝑢
13		cbs	⊢ Base
14	12	cv	⊢ 𝑢
15	14 13	cfv	⊢ ( Base ‘ 𝑢 )
16		vv	⊢ 𝑣
17		clspn	⊢ LSpan
18	14 17	cfv	⊢ ( LSpan ‘ 𝑢 )
19		vn	⊢ 𝑛
20		clcd	⊢ LCDual
21	5 20	cfv	⊢ ( LCDual ‘ 𝑘 )
22	10 21	cfv	⊢ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 )
23		vc	⊢ 𝑐
24	23	cv	⊢ 𝑐
25	24 13	cfv	⊢ ( Base ‘ 𝑐 )
26		vd	⊢ 𝑑
27	24 17	cfv	⊢ ( LSpan ‘ 𝑐 )
28		vj	⊢ 𝑗
29		cmpd	⊢ mapd
30	5 29	cfv	⊢ ( mapd ‘ 𝑘 )
31	10 30	cfv	⊢ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 )
32		vm	⊢ 𝑚
33	7	cv	⊢ 𝑎
34		vx	⊢ 𝑥
35	16	cv	⊢ 𝑣
36	26	cv	⊢ 𝑑
37	35 36	cxp	⊢ ( 𝑣 × 𝑑 )
38	37 35	cxp	⊢ ( ( 𝑣 × 𝑑 ) × 𝑣 )
39		c2nd	⊢ 2^nd
40	34	cv	⊢ 𝑥
41	40 39	cfv	⊢ ( 2^nd ‘ 𝑥 )
42		c0g	⊢ 0_g
43	14 42	cfv	⊢ ( 0_g ‘ 𝑢 )
44	41 43	wceq	⊢ ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 )
45	24 42	cfv	⊢ ( 0_g ‘ 𝑐 )
46		vh	⊢ ℎ
47	32	cv	⊢ 𝑚
48	19	cv	⊢ 𝑛
49	41	csn	⊢ { ( 2^nd ‘ 𝑥 ) }
50	49 48	cfv	⊢ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } )
51	50 47	cfv	⊢ ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) )
52	28	cv	⊢ 𝑗
53	46	cv	⊢ ℎ
54	53	csn	⊢ { ℎ }
55	54 52	cfv	⊢ ( 𝑗 ‘ { ℎ } )
56	51 55	wceq	⊢ ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } )
57		c1st	⊢ 1^st
58	40 57	cfv	⊢ ( 1^st ‘ 𝑥 )
59	58 57	cfv	⊢ ( 1^st ‘ ( 1^st ‘ 𝑥 ) )
60		csg	⊢ -_g
61	14 60	cfv	⊢ ( -_g ‘ 𝑢 )
62	59 41 61	co	⊢ ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) )
63	62	csn	⊢ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) }
64	63 48	cfv	⊢ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } )
65	64 47	cfv	⊢ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) )
66	58 39	cfv	⊢ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) )
67	24 60	cfv	⊢ ( -_g ‘ 𝑐 )
68	66 53 67	co	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ )
69	68	csn	⊢ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) }
70	69 52	cfv	⊢ ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } )
71	65 70	wceq	⊢ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } )
72	56 71	wa	⊢ ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) )
73	72 46 36	crio	⊢ ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) )
74	44 45 73	cif	⊢ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) )
75	34 38 74	cmpt	⊢ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) )
76	33 75	wcel	⊢ 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) )
77	76 32 31	wsbc	⊢ [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) )
78	77 28 27	wsbc	⊢ [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) )
79	78 26 25	wsbc	⊢ [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) )
80	79 23 22	wsbc	⊢ [ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) )
81	80 19 18	wsbc	⊢ [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) )
82	81 16 15	wsbc	⊢ [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) )
83	82 12 11	wsbc	⊢ [ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) )
84	83 7	cab	⊢ { 𝑎 ∣ [ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) }
85	3 6 84	cmpt	⊢ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) } )
86	1 2 85	cmpt	⊢ ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) } ) )
87	0 86	wceq	⊢ HDMap1 = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) } ) )

Metamath Proof Explorer

Definition df-hdmap1

Detailed syntax breakdown