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 37403 |
. . 3
⊢ (𝜑 → 𝐼 = (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2^{nd} ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ)})))))) |
16 | 15 | fveq1d 6231 |
. 2
⊢ (𝜑 → (𝐼‘𝑇) = ((𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2^{nd} ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ)})))))‘𝑇)) |
17 | | hdmap1val.t |
. . 3
⊢ (𝜑 → 𝑇 ∈ ((𝑉 × 𝐷) × 𝑉)) |
18 | | fvex 6239 |
. . . . 5
⊢
(0_{g}‘𝐶) ∈ V |
19 | 10, 18 | eqeltri 2726 |
. . . 4
⊢ 𝑄 ∈ V |
20 | | riotaex 6655 |
. . . 4
⊢
(℩ℎ
∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑇)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑇)) − (2^{nd}
‘𝑇))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑇))𝑅ℎ)}))) ∈ V |
21 | 19, 20 | ifex 4189 |
. . 3
⊢
if((2^{nd} ‘𝑇) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑇)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑇)) − (2^{nd}
‘𝑇))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑇))𝑅ℎ)})))) ∈ V |
22 | | fveq2 6229 |
. . . . . 6
⊢ (𝑥 = 𝑇 → (2^{nd} ‘𝑥) = (2^{nd} ‘𝑇)) |
23 | 22 | eqeq1d 2653 |
. . . . 5
⊢ (𝑥 = 𝑇 → ((2^{nd} ‘𝑥) = 0 ↔ (2^{nd}
‘𝑇) = 0
)) |
24 | 22 | sneqd 4222 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑇 → {(2^{nd} ‘𝑥)} = {(2^{nd}
‘𝑇)}) |
25 | 24 | fveq2d 6233 |
. . . . . . . . 9
⊢ (𝑥 = 𝑇 → (𝑁‘{(2^{nd} ‘𝑥)}) = (𝑁‘{(2^{nd} ‘𝑇)})) |
26 | 25 | fveq2d 6233 |
. . . . . . . 8
⊢ (𝑥 = 𝑇 → (𝑀‘(𝑁‘{(2^{nd} ‘𝑥)})) = (𝑀‘(𝑁‘{(2^{nd} ‘𝑇)}))) |
27 | 26 | eqeq1d 2653 |
. . . . . . 7
⊢ (𝑥 = 𝑇 → ((𝑀‘(𝑁‘{(2^{nd} ‘𝑥)})) = (𝐽‘{ℎ}) ↔ (𝑀‘(𝑁‘{(2^{nd} ‘𝑇)})) = (𝐽‘{ℎ}))) |
28 | | fveq2 6229 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑇 → (1^{st} ‘𝑥) = (1^{st} ‘𝑇)) |
29 | 28 | fveq2d 6233 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑇 → (1^{st}
‘(1^{st} ‘𝑥)) = (1^{st} ‘(1^{st}
‘𝑇))) |
30 | 29, 22 | oveq12d 6708 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑇 → ((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥)) =
((1^{st} ‘(1^{st} ‘𝑇)) − (2^{nd}
‘𝑇))) |
31 | 30 | sneqd 4222 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑇 → {((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))} =
{((1^{st} ‘(1^{st} ‘𝑇)) − (2^{nd}
‘𝑇))}) |
32 | 31 | fveq2d 6233 |
. . . . . . . . 9
⊢ (𝑥 = 𝑇 → (𝑁‘{((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))}) = (𝑁‘{((1^{st}
‘(1^{st} ‘𝑇)) − (2^{nd}
‘𝑇))})) |
33 | 32 | fveq2d 6233 |
. . . . . . . 8
⊢ (𝑥 = 𝑇 → (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))})) = (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑇)) − (2^{nd}
‘𝑇))}))) |
34 | 28 | fveq2d 6233 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑇 → (2^{nd}
‘(1^{st} ‘𝑥)) = (2^{nd} ‘(1^{st}
‘𝑇))) |
35 | 34 | oveq1d 6705 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑇 → ((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ) = ((2^{nd} ‘(1^{st}
‘𝑇))𝑅ℎ)) |
36 | 35 | sneqd 4222 |
. . . . . . . . 9
⊢ (𝑥 = 𝑇 → {((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ)} = {((2^{nd} ‘(1^{st}
‘𝑇))𝑅ℎ)}) |
37 | 36 | fveq2d 6233 |
. . . . . . . 8
⊢ (𝑥 = 𝑇 → (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ)}) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑇))𝑅ℎ)})) |
38 | 33, 37 | eqeq12d 2666 |
. . . . . . 7
⊢ (𝑥 = 𝑇 → ((𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ)}) ↔ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑇)) − (2^{nd}
‘𝑇))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑇))𝑅ℎ)}))) |
39 | 27, 38 | anbi12d 747 |
. . . . . 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} ‘𝑇))𝑅ℎ)})))) |
40 | 39 | riotabidv 6653 |
. . . . 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} ‘𝑇))𝑅ℎ)})))) |
41 | 23, 40 | ifbieq2d 4144 |
. . . 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} ‘𝑇))𝑅ℎ)}))))) |
42 | | eqid 2651 |
. . . 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} ‘𝑥))𝑅ℎ)}))))) |
43 | 41, 42 | fvmptg 6319 |
. . 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} ‘𝑇))𝑅ℎ)}))))) |
44 | 17, 21, 43 | sylancl 695 |
. 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} ‘𝑇))𝑅ℎ)}))))) |
45 | 16, 44 | eqtrd 2685 |
1
⊢ (𝜑 → (𝐼‘𝑇) = if((2^{nd} ‘𝑇) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑇)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑇)) − (2^{nd}
‘𝑇))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑇))𝑅ℎ)}))))) |