Step | Hyp | Ref
| Expression |
1 | | hdmap1val.h |
. . . 4
⊢ 𝐻 = (LHyp‘𝐾) |
2 | | hdmap1fval.u |
. . . 4
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
3 | | hdmap1fval.v |
. . . 4
⊢ 𝑉 = (Base‘𝑈) |
4 | | hdmap1fval.s |
. . . 4
⊢ − =
(-g‘𝑈) |
5 | | hdmap1fval.o |
. . . 4
⊢ 0 =
(0g‘𝑈) |
6 | | hdmap1fval.n |
. . . 4
⊢ 𝑁 = (LSpan‘𝑈) |
7 | | hdmap1fval.c |
. . . 4
⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) |
8 | | hdmap1fval.d |
. . . 4
⊢ 𝐷 = (Base‘𝐶) |
9 | | hdmap1fval.r |
. . . 4
⊢ 𝑅 = (-g‘𝐶) |
10 | | hdmap1fval.q |
. . . 4
⊢ 𝑄 = (0g‘𝐶) |
11 | | hdmap1fval.j |
. . . 4
⊢ 𝐽 = (LSpan‘𝐶) |
12 | | hdmap1fval.m |
. . . 4
⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) |
13 | | hdmap1fval.i |
. . . 4
⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) |
14 | | hdmap1fval.k |
. . . 4
⊢ (𝜑 → (𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻)) |
15 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14 | hdmap1fval 39810 |
. . 3
⊢ (𝜑 → 𝐼 = (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)})))))) |
16 | 15 | fveq1d 6776 |
. 2
⊢ (𝜑 → (𝐼‘𝑇) = ((𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)})))))‘𝑇)) |
17 | | hdmap1val.t |
. . 3
⊢ (𝜑 → 𝑇 ∈ ((𝑉 × 𝐷) × 𝑉)) |
18 | 10 | fvexi 6788 |
. . . 4
⊢ 𝑄 ∈ V |
19 | | riotaex 7236 |
. . . 4
⊢
(℩ℎ
∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑇)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑇)) − (2nd
‘𝑇))})) = (𝐽‘{((2nd
‘(1st ‘𝑇))𝑅ℎ)}))) ∈ V |
20 | 18, 19 | ifex 4509 |
. . 3
⊢
if((2nd ‘𝑇) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑇)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑇)) − (2nd
‘𝑇))})) = (𝐽‘{((2nd
‘(1st ‘𝑇))𝑅ℎ)})))) ∈ V |
21 | | fveqeq2 6783 |
. . . . 5
⊢ (𝑥 = 𝑇 → ((2nd ‘𝑥) = 0 ↔ (2nd
‘𝑇) = 0
)) |
22 | | fveq2 6774 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑇 → (2nd ‘𝑥) = (2nd ‘𝑇)) |
23 | 22 | sneqd 4573 |
. . . . . . . . 9
⊢ (𝑥 = 𝑇 → {(2nd ‘𝑥)} = {(2nd
‘𝑇)}) |
24 | 23 | fveq2d 6778 |
. . . . . . . 8
⊢ (𝑥 = 𝑇 → (𝑁‘{(2nd ‘𝑥)}) = (𝑁‘{(2nd ‘𝑇)})) |
25 | 24 | fveqeq2d 6782 |
. . . . . . 7
⊢ (𝑥 = 𝑇 → ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ↔ (𝑀‘(𝑁‘{(2nd ‘𝑇)})) = (𝐽‘{ℎ}))) |
26 | | 2fveq3 6779 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑇 → (1st
‘(1st ‘𝑥)) = (1st ‘(1st
‘𝑇))) |
27 | 26, 22 | oveq12d 7293 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑇 → ((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥)) =
((1st ‘(1st ‘𝑇)) − (2nd
‘𝑇))) |
28 | 27 | sneqd 4573 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑇 → {((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))} =
{((1st ‘(1st ‘𝑇)) − (2nd
‘𝑇))}) |
29 | 28 | fveq2d 6778 |
. . . . . . . . 9
⊢ (𝑥 = 𝑇 → (𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))}) = (𝑁‘{((1st
‘(1st ‘𝑇)) − (2nd
‘𝑇))})) |
30 | 29 | fveq2d 6778 |
. . . . . . . 8
⊢ (𝑥 = 𝑇 → (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑇)) − (2nd
‘𝑇))}))) |
31 | | 2fveq3 6779 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑇 → (2nd
‘(1st ‘𝑥)) = (2nd ‘(1st
‘𝑇))) |
32 | 31 | oveq1d 7290 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑇 → ((2nd
‘(1st ‘𝑥))𝑅ℎ) = ((2nd ‘(1st
‘𝑇))𝑅ℎ)) |
33 | 32 | sneqd 4573 |
. . . . . . . . 9
⊢ (𝑥 = 𝑇 → {((2nd
‘(1st ‘𝑥))𝑅ℎ)} = {((2nd ‘(1st
‘𝑇))𝑅ℎ)}) |
34 | 33 | fveq2d 6778 |
. . . . . . . 8
⊢ (𝑥 = 𝑇 → (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}) = (𝐽‘{((2nd
‘(1st ‘𝑇))𝑅ℎ)})) |
35 | 30, 34 | eqeq12d 2754 |
. . . . . . 7
⊢ (𝑥 = 𝑇 → ((𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}) ↔ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑇)) − (2nd
‘𝑇))})) = (𝐽‘{((2nd
‘(1st ‘𝑇))𝑅ℎ)}))) |
36 | 25, 35 | anbi12d 631 |
. . . . . 6
⊢ (𝑥 = 𝑇 → (((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)})) ↔ ((𝑀‘(𝑁‘{(2nd ‘𝑇)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑇)) − (2nd
‘𝑇))})) = (𝐽‘{((2nd
‘(1st ‘𝑇))𝑅ℎ)})))) |
37 | 36 | riotabidv 7234 |
. . . . 5
⊢ (𝑥 = 𝑇 → (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}))) = (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑇)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑇)) − (2nd
‘𝑇))})) = (𝐽‘{((2nd
‘(1st ‘𝑇))𝑅ℎ)})))) |
38 | 21, 37 | ifbieq2d 4485 |
. . . 4
⊢ (𝑥 = 𝑇 → if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)})))) = if((2nd ‘𝑇) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑇)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑇)) − (2nd
‘𝑇))})) = (𝐽‘{((2nd
‘(1st ‘𝑇))𝑅ℎ)}))))) |
39 | | eqid 2738 |
. . . 4
⊢ (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}))))) = (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}))))) |
40 | 38, 39 | fvmptg 6873 |
. . 3
⊢ ((𝑇 ∈ ((𝑉 × 𝐷) × 𝑉) ∧ if((2nd ‘𝑇) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑇)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑇)) − (2nd
‘𝑇))})) = (𝐽‘{((2nd
‘(1st ‘𝑇))𝑅ℎ)})))) ∈ V) → ((𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)})))))‘𝑇) = if((2nd ‘𝑇) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑇)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑇)) − (2nd
‘𝑇))})) = (𝐽‘{((2nd
‘(1st ‘𝑇))𝑅ℎ)}))))) |
41 | 17, 20, 40 | sylancl 586 |
. 2
⊢ (𝜑 → ((𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)})))))‘𝑇) = if((2nd ‘𝑇) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑇)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑇)) − (2nd
‘𝑇))})) = (𝐽‘{((2nd
‘(1st ‘𝑇))𝑅ℎ)}))))) |
42 | 16, 41 | eqtrd 2778 |
1
⊢ (𝜑 → (𝐼‘𝑇) = if((2nd ‘𝑇) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑇)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑇)) − (2nd
‘𝑇))})) = (𝐽‘{((2nd
‘(1st ‘𝑇))𝑅ℎ)}))))) |