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 40309 |
. . 3
β’ (π β πΌ = (π₯ β ((π Γ π·) Γ π) β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st
β(1st βπ₯)) β (2nd
βπ₯))})) = (π½β{((2nd
β(1st βπ₯))π
β)})))))) |
16 | 15 | fveq1d 6848 |
. 2
β’ (π β (πΌβπ) = ((π₯ β ((π Γ π·) Γ π) β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st
β(1st βπ₯)) β (2nd
βπ₯))})) = (π½β{((2nd
β(1st βπ₯))π
β)})))))βπ)) |
17 | | hdmap1val.t |
. . 3
β’ (π β π β ((π Γ π·) Γ π)) |
18 | 10 | fvexi 6860 |
. . . 4
β’ π β V |
19 | | riotaex 7321 |
. . . 4
β’
(β©β
β π· ((πβ(πβ{(2nd βπ)})) = (π½β{β}) β§ (πβ(πβ{((1st
β(1st βπ)) β (2nd
βπ))})) = (π½β{((2nd
β(1st βπ))π
β)}))) β V |
20 | 18, 19 | ifex 4540 |
. . 3
β’
if((2nd βπ) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ)})) = (π½β{β}) β§ (πβ(πβ{((1st
β(1st βπ)) β (2nd
βπ))})) = (π½β{((2nd
β(1st βπ))π
β)})))) β V |
21 | | fveqeq2 6855 |
. . . . 5
β’ (π₯ = π β ((2nd βπ₯) = 0 β (2nd
βπ) = 0
)) |
22 | | fveq2 6846 |
. . . . . . . . . 10
β’ (π₯ = π β (2nd βπ₯) = (2nd βπ)) |
23 | 22 | sneqd 4602 |
. . . . . . . . 9
β’ (π₯ = π β {(2nd βπ₯)} = {(2nd
βπ)}) |
24 | 23 | fveq2d 6850 |
. . . . . . . 8
β’ (π₯ = π β (πβ{(2nd βπ₯)}) = (πβ{(2nd βπ)})) |
25 | 24 | fveqeq2d 6854 |
. . . . . . 7
β’ (π₯ = π β ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β (πβ(πβ{(2nd βπ)})) = (π½β{β}))) |
26 | | 2fveq3 6851 |
. . . . . . . . . . . 12
β’ (π₯ = π β (1st
β(1st βπ₯)) = (1st β(1st
βπ))) |
27 | 26, 22 | oveq12d 7379 |
. . . . . . . . . . 11
β’ (π₯ = π β ((1st
β(1st βπ₯)) β (2nd
βπ₯)) =
((1st β(1st βπ)) β (2nd
βπ))) |
28 | 27 | sneqd 4602 |
. . . . . . . . . 10
β’ (π₯ = π β {((1st
β(1st βπ₯)) β (2nd
βπ₯))} =
{((1st β(1st βπ)) β (2nd
βπ))}) |
29 | 28 | fveq2d 6850 |
. . . . . . . . 9
β’ (π₯ = π β (πβ{((1st
β(1st βπ₯)) β (2nd
βπ₯))}) = (πβ{((1st
β(1st βπ)) β (2nd
βπ))})) |
30 | 29 | fveq2d 6850 |
. . . . . . . 8
β’ (π₯ = π β (πβ(πβ{((1st
β(1st βπ₯)) β (2nd
βπ₯))})) = (πβ(πβ{((1st
β(1st βπ)) β (2nd
βπ))}))) |
31 | | 2fveq3 6851 |
. . . . . . . . . . 11
β’ (π₯ = π β (2nd
β(1st βπ₯)) = (2nd β(1st
βπ))) |
32 | 31 | oveq1d 7376 |
. . . . . . . . . 10
β’ (π₯ = π β ((2nd
β(1st βπ₯))π
β) = ((2nd β(1st
βπ))π
β)) |
33 | 32 | sneqd 4602 |
. . . . . . . . 9
β’ (π₯ = π β {((2nd
β(1st βπ₯))π
β)} = {((2nd β(1st
βπ))π
β)}) |
34 | 33 | fveq2d 6850 |
. . . . . . . 8
β’ (π₯ = π β (π½β{((2nd
β(1st βπ₯))π
β)}) = (π½β{((2nd
β(1st βπ))π
β)})) |
35 | 30, 34 | eqeq12d 2749 |
. . . . . . 7
β’ (π₯ = π β ((πβ(πβ{((1st
β(1st βπ₯)) β (2nd
βπ₯))})) = (π½β{((2nd
β(1st βπ₯))π
β)}) β (πβ(πβ{((1st
β(1st βπ)) β (2nd
βπ))})) = (π½β{((2nd
β(1st βπ))π
β)}))) |
36 | 25, 35 | anbi12d 632 |
. . . . . 6
β’ (π₯ = π β (((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st
β(1st βπ₯)) β (2nd
βπ₯))})) = (π½β{((2nd
β(1st βπ₯))π
β)})) β ((πβ(πβ{(2nd βπ)})) = (π½β{β}) β§ (πβ(πβ{((1st
β(1st βπ)) β (2nd
βπ))})) = (π½β{((2nd
β(1st βπ))π
β)})))) |
37 | 36 | riotabidv 7319 |
. . . . 5
β’ (π₯ = π β (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st
β(1st βπ₯)) β (2nd
βπ₯))})) = (π½β{((2nd
β(1st βπ₯))π
β)}))) = (β©β β π· ((πβ(πβ{(2nd βπ)})) = (π½β{β}) β§ (πβ(πβ{((1st
β(1st βπ)) β (2nd
βπ))})) = (π½β{((2nd
β(1st βπ))π
β)})))) |
38 | 21, 37 | ifbieq2d 4516 |
. . . 4
β’ (π₯ = π β if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st
β(1st βπ₯)) β (2nd
βπ₯))})) = (π½β{((2nd
β(1st βπ₯))π
β)})))) = if((2nd βπ) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ)})) = (π½β{β}) β§ (πβ(πβ{((1st
β(1st βπ)) β (2nd
βπ))})) = (π½β{((2nd
β(1st βπ))π
β)}))))) |
39 | | eqid 2733 |
. . . 4
β’ (π₯ β ((π Γ π·) Γ π) β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st
β(1st βπ₯)) β (2nd
βπ₯))})) = (π½β{((2nd
β(1st βπ₯))π
β)}))))) = (π₯ β ((π Γ π·) Γ π) β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st
β(1st βπ₯)) β (2nd
βπ₯))})) = (π½β{((2nd
β(1st βπ₯))π
β)}))))) |
40 | 38, 39 | fvmptg 6950 |
. . 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 587 |
. 2
β’ (π β ((π₯ β ((π Γ π·) Γ π) β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st
β(1st βπ₯)) β (2nd
βπ₯))})) = (π½β{((2nd
β(1st βπ₯))π
β)})))))βπ) = if((2nd βπ) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ)})) = (π½β{β}) β§ (πβ(πβ{((1st
β(1st βπ)) β (2nd
βπ))})) = (π½β{((2nd
β(1st βπ))π
β)}))))) |
42 | 16, 41 | eqtrd 2773 |
1
β’ (π β (πΌβπ) = if((2nd βπ) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ)})) = (π½β{β}) β§ (πβ(πβ{((1st
β(1st βπ)) β (2nd
βπ))})) = (π½β{((2nd
β(1st βπ))π
β)}))))) |