Step | Hyp | Ref
| Expression |
1 | | hdmap1fval.k |
. 2
⊢ (𝜑 → (𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻)) |
2 | | hdmap1fval.i |
. . . 4
⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) |
3 | | hdmap1val.h |
. . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) |
4 | 3 | hdmap1ffval 39546 |
. . . . 5
⊢ (𝐾 ∈ 𝐴 → (HDMap1‘𝐾) = (𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝐾)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))))})) |
5 | 4 | fveq1d 6719 |
. . . 4
⊢ (𝐾 ∈ 𝐴 → ((HDMap1‘𝐾)‘𝑊) = ((𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝐾)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))))})‘𝑊)) |
6 | 2, 5 | syl5eq 2790 |
. . 3
⊢ (𝐾 ∈ 𝐴 → 𝐼 = ((𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝐾)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))))})‘𝑊)) |
7 | | fveq2 6717 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → ((DVecH‘𝐾)‘𝑤) = ((DVecH‘𝐾)‘𝑊)) |
8 | | fveq2 6717 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → ((LCDual‘𝐾)‘𝑤) = ((LCDual‘𝐾)‘𝑊)) |
9 | | fveq2 6717 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑊 → ((mapd‘𝐾)‘𝑤) = ((mapd‘𝐾)‘𝑊)) |
10 | 9 | sbceq1d 3699 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑊 → ([((mapd‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))) ↔ [((mapd‘𝐾)‘𝑊) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))))) |
11 | 10 | sbcbidv 3753 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑊 → ([(LSpan‘𝑐) / 𝑗][((mapd‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))) ↔ [(LSpan‘𝑐) / 𝑗][((mapd‘𝐾)‘𝑊) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))))) |
12 | 11 | sbcbidv 3753 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → ([(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))) ↔ [(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝐾)‘𝑊) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))))) |
13 | 8, 12 | sbceqbid 3701 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → ([((LCDual‘𝐾)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))) ↔ [((LCDual‘𝐾)‘𝑊) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝐾)‘𝑊) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))))) |
14 | 13 | sbcbidv 3753 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → ([(LSpan‘𝑢) / 𝑛][((LCDual‘𝐾)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))) ↔ [(LSpan‘𝑢) / 𝑛][((LCDual‘𝐾)‘𝑊) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝐾)‘𝑊) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))))) |
15 | 14 | sbcbidv 3753 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → ([(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝐾)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))) ↔ [(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝐾)‘𝑊) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝐾)‘𝑊) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))))) |
16 | 7, 15 | sbceqbid 3701 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ([((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝐾)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))) ↔ [((DVecH‘𝐾)‘𝑊) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝐾)‘𝑊) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝐾)‘𝑊) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))))) |
17 | | fvex 6730 |
. . . . . . 7
⊢
((DVecH‘𝐾)‘𝑊) ∈ V |
18 | | fvex 6730 |
. . . . . . 7
⊢
(Base‘𝑢)
∈ V |
19 | | fvex 6730 |
. . . . . . 7
⊢
(LSpan‘𝑢)
∈ V |
20 | | hdmap1fval.u |
. . . . . . . . . . 11
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
21 | 20 | eqeq2i 2750 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑈 ↔ 𝑢 = ((DVecH‘𝐾)‘𝑊)) |
22 | 21 | biimpri 231 |
. . . . . . . . 9
⊢ (𝑢 = ((DVecH‘𝐾)‘𝑊) → 𝑢 = 𝑈) |
23 | 22 | 3ad2ant1 1135 |
. . . . . . . 8
⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑢 = 𝑈) |
24 | | simp2 1139 |
. . . . . . . . . 10
⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑣 = (Base‘𝑢)) |
25 | 22 | fveq2d 6721 |
. . . . . . . . . . 11
⊢ (𝑢 = ((DVecH‘𝐾)‘𝑊) → (Base‘𝑢) = (Base‘𝑈)) |
26 | 25 | 3ad2ant1 1135 |
. . . . . . . . . 10
⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → (Base‘𝑢) = (Base‘𝑈)) |
27 | 24, 26 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑣 = (Base‘𝑈)) |
28 | | hdmap1fval.v |
. . . . . . . . 9
⊢ 𝑉 = (Base‘𝑈) |
29 | 27, 28 | eqtr4di 2796 |
. . . . . . . 8
⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑣 = 𝑉) |
30 | | simp3 1140 |
. . . . . . . . . 10
⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑛 = (LSpan‘𝑢)) |
31 | 23 | fveq2d 6721 |
. . . . . . . . . 10
⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → (LSpan‘𝑢) = (LSpan‘𝑈)) |
32 | 30, 31 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑛 = (LSpan‘𝑈)) |
33 | | hdmap1fval.n |
. . . . . . . . 9
⊢ 𝑁 = (LSpan‘𝑈) |
34 | 32, 33 | eqtr4di 2796 |
. . . . . . . 8
⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑛 = 𝑁) |
35 | | fvex 6730 |
. . . . . . . . . 10
⊢
((LCDual‘𝐾)‘𝑊) ∈ V |
36 | | fvex 6730 |
. . . . . . . . . 10
⊢
(Base‘𝑐)
∈ V |
37 | | fvex 6730 |
. . . . . . . . . 10
⊢
(LSpan‘𝑐)
∈ V |
38 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑐 = ((LCDual‘𝐾)‘𝑊) → 𝑐 = ((LCDual‘𝐾)‘𝑊)) |
39 | | hdmap1fval.c |
. . . . . . . . . . . . 13
⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) |
40 | 38, 39 | eqtr4di 2796 |
. . . . . . . . . . . 12
⊢ (𝑐 = ((LCDual‘𝐾)‘𝑊) → 𝑐 = 𝐶) |
41 | 40 | 3ad2ant1 1135 |
. . . . . . . . . . 11
⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → 𝑐 = 𝐶) |
42 | | simp2 1139 |
. . . . . . . . . . . 12
⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → 𝑑 = (Base‘𝑐)) |
43 | 41 | fveq2d 6721 |
. . . . . . . . . . . . 13
⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → (Base‘𝑐) = (Base‘𝐶)) |
44 | | hdmap1fval.d |
. . . . . . . . . . . . 13
⊢ 𝐷 = (Base‘𝐶) |
45 | 43, 44 | eqtr4di 2796 |
. . . . . . . . . . . 12
⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → (Base‘𝑐) = 𝐷) |
46 | 42, 45 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → 𝑑 = 𝐷) |
47 | | simp3 1140 |
. . . . . . . . . . . 12
⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → 𝑗 = (LSpan‘𝑐)) |
48 | 41 | fveq2d 6721 |
. . . . . . . . . . . . 13
⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → (LSpan‘𝑐) = (LSpan‘𝐶)) |
49 | | hdmap1fval.j |
. . . . . . . . . . . . 13
⊢ 𝐽 = (LSpan‘𝐶) |
50 | 48, 49 | eqtr4di 2796 |
. . . . . . . . . . . 12
⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → (LSpan‘𝑐) = 𝐽) |
51 | 47, 50 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → 𝑗 = 𝐽) |
52 | | fvex 6730 |
. . . . . . . . . . . . 13
⊢
((mapd‘𝐾)‘𝑊) ∈ V |
53 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = ((mapd‘𝐾)‘𝑊) → 𝑚 = ((mapd‘𝐾)‘𝑊)) |
54 | | hdmap1fval.m |
. . . . . . . . . . . . . . 15
⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) |
55 | 53, 54 | eqtr4di 2796 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = ((mapd‘𝐾)‘𝑊) → 𝑚 = 𝑀) |
56 | | fveq1 6716 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = 𝑀 → (𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑀‘(𝑛‘{(2nd ‘𝑥)}))) |
57 | 56 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 = 𝑀 → ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ↔ (𝑀‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}))) |
58 | | fveq1 6716 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = 𝑀 → (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))}))) |
59 | 58 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 = 𝑀 → ((𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}) ↔ (𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))) |
60 | 57, 59 | anbi12d 634 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 = 𝑀 → (((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)})) ↔ ((𝑀‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))) |
61 | 60 | riotabidv 7172 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = 𝑀 → (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))) = (℩ℎ ∈ 𝑑 ((𝑀‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))) |
62 | 61 | ifeq2d 4459 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = 𝑀 → if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))) = if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑀‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))) |
63 | 62 | mpteq2dv 5151 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑀 → (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))) = (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑀‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))))) |
64 | 63 | eleq2d 2823 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑀 → (𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))) ↔ 𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑀‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))))) |
65 | 55, 64 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑚 = ((mapd‘𝐾)‘𝑊) → (𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))) ↔ 𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑀‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))))) |
66 | 52, 65 | sbcie 3737 |
. . . . . . . . . . . 12
⊢
([((mapd‘𝐾)‘𝑊) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))) ↔ 𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑀‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))))) |
67 | | simp2 1139 |
. . . . . . . . . . . . . . 15
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → 𝑑 = 𝐷) |
68 | | xpeq2 5572 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = 𝐷 → (𝑣 × 𝑑) = (𝑣 × 𝐷)) |
69 | 68 | xpeq1d 5580 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = 𝐷 → ((𝑣 × 𝑑) × 𝑣) = ((𝑣 × 𝐷) × 𝑣)) |
70 | 67, 69 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → ((𝑣 × 𝑑) × 𝑣) = ((𝑣 × 𝐷) × 𝑣)) |
71 | | simp1 1138 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → 𝑐 = 𝐶) |
72 | 71 | fveq2d 6721 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (0g‘𝑐) = (0g‘𝐶)) |
73 | | hdmap1fval.q |
. . . . . . . . . . . . . . . 16
⊢ 𝑄 = (0g‘𝐶) |
74 | 72, 73 | eqtr4di 2796 |
. . . . . . . . . . . . . . 15
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (0g‘𝑐) = 𝑄) |
75 | | simp3 1140 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → 𝑗 = 𝐽) |
76 | 75 | fveq1d 6719 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (𝑗‘{ℎ}) = (𝐽‘{ℎ})) |
77 | 76 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → ((𝑀‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ↔ (𝑀‘(𝑛‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}))) |
78 | 71 | fveq2d 6721 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (-g‘𝑐) = (-g‘𝐶)) |
79 | | hdmap1fval.r |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑅 = (-g‘𝐶) |
80 | 78, 79 | eqtr4di 2796 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (-g‘𝑐) = 𝑅) |
81 | 80 | oveqd 7230 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → ((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ) = ((2nd ‘(1st
‘𝑥))𝑅ℎ)) |
82 | 81 | sneqd 4553 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → {((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)} = {((2nd ‘(1st
‘𝑥))𝑅ℎ)}) |
83 | 75, 82 | fveq12d 6724 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)})) |
84 | 83 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → ((𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}) ↔ (𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}))) |
85 | 77, 84 | anbi12d 634 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (((𝑀‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)})) ↔ ((𝑀‘(𝑛‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)})))) |
86 | 67, 85 | riotaeqbidv 7173 |
. . . . . . . . . . . . . . 15
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (℩ℎ ∈ 𝑑 ((𝑀‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))) = (℩ℎ ∈ 𝐷 ((𝑀‘(𝑛‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)})))) |
87 | 74, 86 | ifeq12d 4460 |
. . . . . . . . . . . . . 14
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑀‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))) = if((2nd ‘𝑥) = (0g‘𝑢), 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑛‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}))))) |
88 | 70, 87 | mpteq12dv 5140 |
. . . . . . . . . . . . 13
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑀‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))) = (𝑥 ∈ ((𝑣 × 𝐷) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑛‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)})))))) |
89 | 88 | eleq2d 2823 |
. . . . . . . . . . . 12
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑀‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))) ↔ 𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝐷) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑛‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}))))))) |
90 | 66, 89 | syl5bb 286 |
. . . . . . . . . . 11
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → ([((mapd‘𝐾)‘𝑊) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))) ↔ 𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝐷) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑛‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}))))))) |
91 | 41, 46, 51, 90 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → ([((mapd‘𝐾)‘𝑊) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))) ↔ 𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝐷) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑛‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}))))))) |
92 | 35, 36, 37, 91 | sbc3ie 3781 |
. . . . . . . . 9
⊢
([((LCDual‘𝐾)‘𝑊) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝐾)‘𝑊) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))) ↔ 𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝐷) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑛‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)})))))) |
93 | | simp2 1139 |
. . . . . . . . . . . . 13
⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → 𝑣 = 𝑉) |
94 | 93 | xpeq1d 5580 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (𝑣 × 𝐷) = (𝑉 × 𝐷)) |
95 | 94, 93 | xpeq12d 5582 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → ((𝑣 × 𝐷) × 𝑣) = ((𝑉 × 𝐷) × 𝑉)) |
96 | | simp1 1138 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → 𝑢 = 𝑈) |
97 | 96 | fveq2d 6721 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (0g‘𝑢) = (0g‘𝑈)) |
98 | | hdmap1fval.o |
. . . . . . . . . . . . . 14
⊢ 0 =
(0g‘𝑈) |
99 | 97, 98 | eqtr4di 2796 |
. . . . . . . . . . . . 13
⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (0g‘𝑢) = 0 ) |
100 | 99 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → ((2nd ‘𝑥) = (0g‘𝑢) ↔ (2nd
‘𝑥) = 0
)) |
101 | | simp3 1140 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → 𝑛 = 𝑁) |
102 | 101 | fveq1d 6719 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (𝑛‘{(2nd ‘𝑥)}) = (𝑁‘{(2nd ‘𝑥)})) |
103 | 102 | fveqeq2d 6725 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → ((𝑀‘(𝑛‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ↔ (𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}))) |
104 | 96 | fveq2d 6721 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (-g‘𝑢) = (-g‘𝑈)) |
105 | | hdmap1fval.s |
. . . . . . . . . . . . . . . . . . 19
⊢ − =
(-g‘𝑈) |
106 | 104, 105 | eqtr4di 2796 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (-g‘𝑢) = − ) |
107 | 106 | oveqd 7230 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → ((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥)) = ((1st ‘(1st
‘𝑥)) −
(2nd ‘𝑥))) |
108 | 107 | sneqd 4553 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → {((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))} = {((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))}) |
109 | 101, 108 | fveq12d 6724 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))}) = (𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) |
110 | 109 | fveqeq2d 6725 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → ((𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}) ↔ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}))) |
111 | 103, 110 | anbi12d 634 |
. . . . . . . . . . . . 13
⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (((𝑀‘(𝑛‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)})) ↔ ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)})))) |
112 | 111 | riotabidv 7172 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (℩ℎ ∈ 𝐷 ((𝑀‘(𝑛‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}))) = (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)})))) |
113 | 100, 112 | ifbieq2d 4465 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → if((2nd ‘𝑥) = (0g‘𝑢), 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑛‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)})))) = if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}))))) |
114 | 95, 113 | mpteq12dv 5140 |
. . . . . . . . . 10
⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (𝑥 ∈ ((𝑣 × 𝐷) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑛‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}))))) = (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)})))))) |
115 | 114 | eleq2d 2823 |
. . . . . . . . 9
⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝐷) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑛‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}))))) ↔ 𝑎 ∈ (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}))))))) |
116 | 92, 115 | syl5bb 286 |
. . . . . . . 8
⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → ([((LCDual‘𝐾)‘𝑊) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝐾)‘𝑊) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))) ↔ 𝑎 ∈ (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}))))))) |
117 | 23, 29, 34, 116 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → ([((LCDual‘𝐾)‘𝑊) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝐾)‘𝑊) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))) ↔ 𝑎 ∈ (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}))))))) |
118 | 17, 18, 19, 117 | sbc3ie 3781 |
. . . . . 6
⊢
([((DVecH‘𝐾)‘𝑊) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝐾)‘𝑊) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝐾)‘𝑊) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))) ↔ 𝑎 ∈ (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)})))))) |
119 | 16, 118 | bitrdi 290 |
. . . . 5
⊢ (𝑤 = 𝑊 → ([((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝐾)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))) ↔ 𝑎 ∈ (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}))))))) |
120 | 119 | abbi1dv 2875 |
. . . 4
⊢ (𝑤 = 𝑊 → {𝑎 ∣ [((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝐾)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))))} = (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)})))))) |
121 | | eqid 2737 |
. . . 4
⊢ (𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝐾)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))))}) = (𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝐾)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))))}) |
122 | 28 | fvexi 6731 |
. . . . . . 7
⊢ 𝑉 ∈ V |
123 | 44 | fvexi 6731 |
. . . . . . 7
⊢ 𝐷 ∈ V |
124 | 122, 123 | xpex 7538 |
. . . . . 6
⊢ (𝑉 × 𝐷) ∈ V |
125 | 124, 122 | xpex 7538 |
. . . . 5
⊢ ((𝑉 × 𝐷) × 𝑉) ∈ V |
126 | 125 | mptex 7039 |
. . . 4
⊢ (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}))))) ∈ V |
127 | 120, 121,
126 | fvmpt 6818 |
. . 3
⊢ (𝑊 ∈ 𝐻 → ((𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝐾)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st
‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd
‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))))})‘𝑊) = (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)})))))) |
128 | 6, 127 | sylan9eq 2798 |
. 2
⊢ ((𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻) → 𝐼 = (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)})))))) |
129 | 1, 128 | syl 17 |
1
⊢ (𝜑 → 𝐼 = (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)})))))) |