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 =
(0_{g}‘𝑈) |
6 | | hdmap1fval.n |
. . . 4
⊢ 𝑁 = (LSpan‘𝑈) |
7 | | hdmap1fval.c |
. . . 4
⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) |
8 | | hdmap1fval.d |
. . . 4
⊢ 𝐷 = (Base‘𝐶) |
9 | | hdmap1fval.r |
. . . 4
⊢ 𝑅 = (-_{g}‘𝐶) |
10 | | hdmap1fval.q |
. . . 4
⊢ 𝑄 = (0_{g}‘𝐶) |
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 38919 |
. . 3
⊢ (𝜑 → 𝐼 = (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2^{nd} ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ)})))))) |
16 | 15 | fveq1d 6665 |
. 2
⊢ (𝜑 → (𝐼‘𝑇) = ((𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2^{nd} ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ)})))))‘𝑇)) |
17 | | hdmap1val.t |
. . 3
⊢ (𝜑 → 𝑇 ∈ ((𝑉 × 𝐷) × 𝑉)) |
18 | 10 | fvexi 6677 |
. . . 4
⊢ 𝑄 ∈ V |
19 | | riotaex 7110 |
. . . 4
⊢
(℩ℎ
∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑇)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑇)) − (2^{nd}
‘𝑇))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑇))𝑅ℎ)}))) ∈ V |
20 | 18, 19 | ifex 4513 |
. . 3
⊢
if((2^{nd} ‘𝑇) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑇)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑇)) − (2^{nd}
‘𝑇))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑇))𝑅ℎ)})))) ∈ V |
21 | | fveqeq2 6672 |
. . . . 5
⊢ (𝑥 = 𝑇 → ((2^{nd} ‘𝑥) = 0 ↔ (2^{nd}
‘𝑇) = 0
)) |
22 | | fveq2 6663 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑇 → (2^{nd} ‘𝑥) = (2^{nd} ‘𝑇)) |
23 | 22 | sneqd 4571 |
. . . . . . . . 9
⊢ (𝑥 = 𝑇 → {(2^{nd} ‘𝑥)} = {(2^{nd}
‘𝑇)}) |
24 | 23 | fveq2d 6667 |
. . . . . . . 8
⊢ (𝑥 = 𝑇 → (𝑁‘{(2^{nd} ‘𝑥)}) = (𝑁‘{(2^{nd} ‘𝑇)})) |
25 | 24 | fveqeq2d 6671 |
. . . . . . 7
⊢ (𝑥 = 𝑇 → ((𝑀‘(𝑁‘{(2^{nd} ‘𝑥)})) = (𝐽‘{ℎ}) ↔ (𝑀‘(𝑁‘{(2^{nd} ‘𝑇)})) = (𝐽‘{ℎ}))) |
26 | | 2fveq3 6668 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑇 → (1^{st}
‘(1^{st} ‘𝑥)) = (1^{st} ‘(1^{st}
‘𝑇))) |
27 | 26, 22 | oveq12d 7166 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑇 → ((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥)) =
((1^{st} ‘(1^{st} ‘𝑇)) − (2^{nd}
‘𝑇))) |
28 | 27 | sneqd 4571 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑇 → {((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))} =
{((1^{st} ‘(1^{st} ‘𝑇)) − (2^{nd}
‘𝑇))}) |
29 | 28 | fveq2d 6667 |
. . . . . . . . 9
⊢ (𝑥 = 𝑇 → (𝑁‘{((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))}) = (𝑁‘{((1^{st}
‘(1^{st} ‘𝑇)) − (2^{nd}
‘𝑇))})) |
30 | 29 | fveq2d 6667 |
. . . . . . . 8
⊢ (𝑥 = 𝑇 → (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))})) = (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑇)) − (2^{nd}
‘𝑇))}))) |
31 | | 2fveq3 6668 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑇 → (2^{nd}
‘(1^{st} ‘𝑥)) = (2^{nd} ‘(1^{st}
‘𝑇))) |
32 | 31 | oveq1d 7163 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑇 → ((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ) = ((2^{nd} ‘(1^{st}
‘𝑇))𝑅ℎ)) |
33 | 32 | sneqd 4571 |
. . . . . . . . 9
⊢ (𝑥 = 𝑇 → {((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ)} = {((2^{nd} ‘(1^{st}
‘𝑇))𝑅ℎ)}) |
34 | 33 | fveq2d 6667 |
. . . . . . . 8
⊢ (𝑥 = 𝑇 → (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ)}) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑇))𝑅ℎ)})) |
35 | 30, 34 | eqeq12d 2835 |
. . . . . . 7
⊢ (𝑥 = 𝑇 → ((𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ)}) ↔ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑇)) − (2^{nd}
‘𝑇))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑇))𝑅ℎ)}))) |
36 | 25, 35 | anbi12d 632 |
. . . . . 6
⊢ (𝑥 = 𝑇 → (((𝑀‘(𝑁‘{(2^{nd} ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ)})) ↔ ((𝑀‘(𝑁‘{(2^{nd} ‘𝑇)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑇)) − (2^{nd}
‘𝑇))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑇))𝑅ℎ)})))) |
37 | 36 | riotabidv 7108 |
. . . . 5
⊢ (𝑥 = 𝑇 → (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ)}))) = (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑇)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑇)) − (2^{nd}
‘𝑇))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑇))𝑅ℎ)})))) |
38 | 21, 37 | ifbieq2d 4490 |
. . . 4
⊢ (𝑥 = 𝑇 → if((2^{nd} ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ)})))) = if((2^{nd} ‘𝑇) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑇)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑇)) − (2^{nd}
‘𝑇))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑇))𝑅ℎ)}))))) |
39 | | eqid 2819 |
. . . 4
⊢ (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2^{nd} ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ)}))))) = (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2^{nd} ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ)}))))) |
40 | 38, 39 | fvmptg 6759 |
. . 3
⊢ ((𝑇 ∈ ((𝑉 × 𝐷) × 𝑉) ∧ if((2^{nd} ‘𝑇) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑇)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑇)) − (2^{nd}
‘𝑇))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑇))𝑅ℎ)})))) ∈ V) → ((𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2^{nd} ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ)})))))‘𝑇) = if((2^{nd} ‘𝑇) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑇)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑇)) − (2^{nd}
‘𝑇))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑇))𝑅ℎ)}))))) |
41 | 17, 20, 40 | sylancl 588 |
. 2
⊢ (𝜑 → ((𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2^{nd} ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ)})))))‘𝑇) = if((2^{nd} ‘𝑇) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑇)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑇)) − (2^{nd}
‘𝑇))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑇))𝑅ℎ)}))))) |
42 | 16, 41 | eqtrd 2854 |
1
⊢ (𝜑 → (𝐼‘𝑇) = if((2^{nd} ‘𝑇) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑇)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑇)) − (2^{nd}
‘𝑇))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑇))𝑅ℎ)}))))) |