Step |
Hyp |
Ref |
Expression |
1 |
|
hdmapval.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
2 |
|
elex |
⊢ ( 𝐾 ∈ 𝑋 → 𝐾 ∈ V ) |
3 |
|
fveq2 |
⊢ ( 𝑘 = 𝐾 → ( LHyp ‘ 𝑘 ) = ( LHyp ‘ 𝐾 ) ) |
4 |
3 1
|
eqtr4di |
⊢ ( 𝑘 = 𝐾 → ( LHyp ‘ 𝑘 ) = 𝐻 ) |
5 |
|
fveq2 |
⊢ ( 𝑘 = 𝐾 → ( Base ‘ 𝑘 ) = ( Base ‘ 𝐾 ) ) |
6 |
5
|
reseq2d |
⊢ ( 𝑘 = 𝐾 → ( I ↾ ( Base ‘ 𝑘 ) ) = ( I ↾ ( Base ‘ 𝐾 ) ) ) |
7 |
|
fveq2 |
⊢ ( 𝑘 = 𝐾 → ( LTrn ‘ 𝑘 ) = ( LTrn ‘ 𝐾 ) ) |
8 |
7
|
fveq1d |
⊢ ( 𝑘 = 𝐾 → ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ) |
9 |
8
|
reseq2d |
⊢ ( 𝑘 = 𝐾 → ( I ↾ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ) = ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ) ) |
10 |
6 9
|
opeq12d |
⊢ ( 𝑘 = 𝐾 → 〈 ( I ↾ ( Base ‘ 𝑘 ) ) , ( I ↾ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ) 〉 = 〈 ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ) 〉 ) |
11 |
|
fveq2 |
⊢ ( 𝑘 = 𝐾 → ( DVecH ‘ 𝑘 ) = ( DVecH ‘ 𝐾 ) ) |
12 |
11
|
fveq1d |
⊢ ( 𝑘 = 𝐾 → ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) |
13 |
|
fveq2 |
⊢ ( 𝑘 = 𝐾 → ( HDMap1 ‘ 𝑘 ) = ( HDMap1 ‘ 𝐾 ) ) |
14 |
13
|
fveq1d |
⊢ ( 𝑘 = 𝐾 → ( ( HDMap1 ‘ 𝑘 ) ‘ 𝑤 ) = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑤 ) ) |
15 |
|
fveq2 |
⊢ ( 𝑘 = 𝐾 → ( LCDual ‘ 𝑘 ) = ( LCDual ‘ 𝐾 ) ) |
16 |
15
|
fveq1d |
⊢ ( 𝑘 = 𝐾 → ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) = ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) |
17 |
16
|
fveq2d |
⊢ ( 𝑘 = 𝐾 → ( Base ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) = ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ) |
18 |
|
fveq2 |
⊢ ( 𝑘 = 𝐾 → ( HVMap ‘ 𝑘 ) = ( HVMap ‘ 𝐾 ) ) |
19 |
18
|
fveq1d |
⊢ ( 𝑘 = 𝐾 → ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) = ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ) |
20 |
19
|
fveq1d |
⊢ ( 𝑘 = 𝐾 → ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) = ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) ) |
21 |
20
|
oteq2d |
⊢ ( 𝑘 = 𝐾 → 〈 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 = 〈 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) |
22 |
21
|
fveq2d |
⊢ ( 𝑘 = 𝐾 → ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) = ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) ) |
23 |
22
|
oteq2d |
⊢ ( 𝑘 = 𝐾 → 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 = 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) |
24 |
23
|
fveq2d |
⊢ ( 𝑘 = 𝐾 → ( 𝑖 ‘ 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) = ( 𝑖 ‘ 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) ) |
25 |
24
|
eqeq2d |
⊢ ( 𝑘 = 𝐾 → ( 𝑦 = ( 𝑖 ‘ 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) ↔ 𝑦 = ( 𝑖 ‘ 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) ) ) |
26 |
25
|
imbi2d |
⊢ ( 𝑘 = 𝐾 → ( ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) ) ↔ ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) ) ) ) |
27 |
26
|
ralbidv |
⊢ ( 𝑘 = 𝐾 → ( ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) ) ↔ ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) ) ) ) |
28 |
17 27
|
riotaeqbidv |
⊢ ( 𝑘 = 𝐾 → ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) ) ) = ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) ) ) ) |
29 |
28
|
mpteq2dv |
⊢ ( 𝑘 = 𝐾 → ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) ) ) ) = ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) ) ) ) ) |
30 |
29
|
eleq2d |
⊢ ( 𝑘 = 𝐾 → ( 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) ) ) ) ↔ 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) ) ) ) ) ) |
31 |
14 30
|
sbceqbid |
⊢ ( 𝑘 = 𝐾 → ( [ ( ( HDMap1 ‘ 𝑘 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) ) ) ) ↔ [ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) ) ) ) ) ) |
32 |
31
|
sbcbidv |
⊢ ( 𝑘 = 𝐾 → ( [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝑘 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) ) ) ) ↔ [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) ) ) ) ) ) |
33 |
12 32
|
sbceqbid |
⊢ ( 𝑘 = 𝐾 → ( [ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝑘 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) ) ) ) ↔ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) ) ) ) ) ) |
34 |
10 33
|
sbceqbid |
⊢ ( 𝑘 = 𝐾 → ( [ 〈 ( I ↾ ( Base ‘ 𝑘 ) ) , ( I ↾ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ) 〉 / 𝑒 ] [ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝑘 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) ) ) ) ↔ [ 〈 ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ) 〉 / 𝑒 ] [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) ) ) ) ) ) |
35 |
34
|
abbidv |
⊢ ( 𝑘 = 𝐾 → { 𝑎 ∣ [ 〈 ( I ↾ ( Base ‘ 𝑘 ) ) , ( I ↾ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ) 〉 / 𝑒 ] [ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝑘 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) ) ) ) } = { 𝑎 ∣ [ 〈 ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ) 〉 / 𝑒 ] [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) ) ) ) } ) |
36 |
4 35
|
mpteq12dv |
⊢ ( 𝑘 = 𝐾 → ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑎 ∣ [ 〈 ( I ↾ ( Base ‘ 𝑘 ) ) , ( I ↾ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ) 〉 / 𝑒 ] [ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝑘 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) ) ) ) } ) = ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ 〈 ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ) 〉 / 𝑒 ] [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) ) ) ) } ) ) |
37 |
|
df-hdmap |
⊢ HDMap = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑎 ∣ [ 〈 ( I ↾ ( Base ‘ 𝑘 ) ) , ( I ↾ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ) 〉 / 𝑒 ] [ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝑘 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) ) ) ) } ) ) |
38 |
36 37 1
|
mptfvmpt |
⊢ ( 𝐾 ∈ V → ( HDMap ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ 〈 ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ) 〉 / 𝑒 ] [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) ) ) ) } ) ) |
39 |
2 38
|
syl |
⊢ ( 𝐾 ∈ 𝑋 → ( HDMap ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ 〈 ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ) 〉 / 𝑒 ] [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ 〈 𝑧 , ( 𝑖 ‘ 〈 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 〉 ) , 𝑡 〉 ) ) ) ) } ) ) |