Step | Hyp | Ref
| Expression |
1 | | mapdh8a.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
2 | | mapdh8a.u |
. . . . . 6
β’ π = ((DVecHβπΎ)βπ) |
3 | | mapdh8a.v |
. . . . . 6
β’ π = (Baseβπ) |
4 | | mapdh8a.s |
. . . . . 6
β’ β =
(-gβπ) |
5 | | mapdh8a.o |
. . . . . 6
β’ 0 =
(0gβπ) |
6 | | mapdh8a.n |
. . . . . 6
β’ π = (LSpanβπ) |
7 | | mapdh8a.c |
. . . . . 6
β’ πΆ = ((LCDualβπΎ)βπ) |
8 | | mapdh8a.d |
. . . . . 6
β’ π· = (BaseβπΆ) |
9 | | mapdh8a.r |
. . . . . 6
β’ π
= (-gβπΆ) |
10 | | mapdh8a.q |
. . . . . 6
β’ π = (0gβπΆ) |
11 | | mapdh8a.j |
. . . . . 6
β’ π½ = (LSpanβπΆ) |
12 | | mapdh8a.m |
. . . . . 6
β’ π = ((mapdβπΎ)βπ) |
13 | | mapdh8a.i |
. . . . . 6
β’ πΌ = (π₯ β V β¦ if((2nd
βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st
β(1st βπ₯)) β (2nd
βπ₯))})) = (π½β{((2nd
β(1st βπ₯))π
β)}))))) |
14 | | mapdh8a.k |
. . . . . . 7
β’ (π β (πΎ β HL β§ π β π»)) |
15 | 14 | 3ad2ant1 1134 |
. . . . . 6
β’ ((π β§ (π§ β π β§ π€ β π) β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π}))) β (πΎ β HL β§ π β π»)) |
16 | | mapdh8h.f |
. . . . . . 7
β’ (π β πΉ β π·) |
17 | 16 | 3ad2ant1 1134 |
. . . . . 6
β’ ((π β§ (π§ β π β§ π€ β π) β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π}))) β πΉ β π·) |
18 | | mapdh8h.mn |
. . . . . . 7
β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) |
19 | 18 | 3ad2ant1 1134 |
. . . . . 6
β’ ((π β§ (π§ β π β§ π€ β π) β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π}))) β (πβ(πβ{π})) = (π½β{πΉ})) |
20 | | mapdh9a.x |
. . . . . . 7
β’ (π β π β (π β { 0 })) |
21 | 20 | 3ad2ant1 1134 |
. . . . . 6
β’ ((π β§ (π§ β π β§ π€ β π) β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π}))) β π β (π β { 0 })) |
22 | | eqid 2733 |
. . . . . . 7
β’
(LSubSpβπ) =
(LSubSpβπ) |
23 | 1, 2, 14 | dvhlmod 39623 |
. . . . . . . 8
β’ (π β π β LMod) |
24 | 23 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π β§ (π§ β π β§ π€ β π) β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π}))) β π β LMod) |
25 | 20 | eldifad 3926 |
. . . . . . . . 9
β’ (π β π β π) |
26 | | mapdh9a.t |
. . . . . . . . 9
β’ (π β π β π) |
27 | 3, 22, 6, 23, 25, 26 | lspprcl 20483 |
. . . . . . . 8
β’ (π β (πβ{π, π}) β (LSubSpβπ)) |
28 | 27 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π β§ (π§ β π β§ π€ β π) β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π}))) β (πβ{π, π}) β (LSubSpβπ)) |
29 | | simp2l 1200 |
. . . . . . 7
β’ ((π β§ (π§ β π β§ π€ β π) β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π}))) β π§ β π) |
30 | | simp3l 1202 |
. . . . . . 7
β’ ((π β§ (π§ β π β§ π€ β π) β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π}))) β Β¬ π§ β (πβ{π, π})) |
31 | 5, 22, 24, 28, 29, 30 | lssneln0 20457 |
. . . . . 6
β’ ((π β§ (π§ β π β§ π€ β π) β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π}))) β π§ β (π β { 0 })) |
32 | | simp2r 1201 |
. . . . . . 7
β’ ((π β§ (π§ β π β§ π€ β π) β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π}))) β π€ β π) |
33 | | simp3r 1203 |
. . . . . . 7
β’ ((π β§ (π§ β π β§ π€ β π) β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π}))) β Β¬ π€ β (πβ{π, π})) |
34 | 5, 22, 24, 28, 32, 33 | lssneln0 20457 |
. . . . . 6
β’ ((π β§ (π§ β π β§ π€ β π) β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π}))) β π€ β (π β { 0 })) |
35 | 1, 2, 14 | dvhlvec 39622 |
. . . . . . . . . 10
β’ (π β π β LVec) |
36 | 35 | 3ad2ant1 1134 |
. . . . . . . . 9
β’ ((π β§ (π§ β π β§ π€ β π) β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π}))) β π β LVec) |
37 | 25 | 3ad2ant1 1134 |
. . . . . . . . 9
β’ ((π β§ (π§ β π β§ π€ β π) β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π}))) β π β π) |
38 | 26 | 3ad2ant1 1134 |
. . . . . . . . 9
β’ ((π β§ (π§ β π β§ π€ β π) β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π}))) β π β π) |
39 | 3, 6, 36, 29, 37, 38, 30 | lspindpi 20638 |
. . . . . . . 8
β’ ((π β§ (π§ β π β§ π€ β π) β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π}))) β ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) |
40 | 39 | simpld 496 |
. . . . . . 7
β’ ((π β§ (π§ β π β§ π€ β π) β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π}))) β (πβ{π§}) β (πβ{π})) |
41 | 40 | necomd 2996 |
. . . . . 6
β’ ((π β§ (π§ β π β§ π€ β π) β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π}))) β (πβ{π}) β (πβ{π§})) |
42 | 3, 6, 36, 32, 37, 38, 33 | lspindpi 20638 |
. . . . . . . 8
β’ ((π β§ (π§ β π β§ π€ β π) β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π}))) β ((πβ{π€}) β (πβ{π}) β§ (πβ{π€}) β (πβ{π}))) |
43 | 42 | simpld 496 |
. . . . . . 7
β’ ((π β§ (π§ β π β§ π€ β π) β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π}))) β (πβ{π€}) β (πβ{π})) |
44 | 43 | necomd 2996 |
. . . . . 6
β’ ((π β§ (π§ β π β§ π€ β π) β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π}))) β (πβ{π}) β (πβ{π€})) |
45 | 39 | simprd 497 |
. . . . . 6
β’ ((π β§ (π§ β π β§ π€ β π) β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π}))) β (πβ{π§}) β (πβ{π})) |
46 | 42 | simprd 497 |
. . . . . 6
β’ ((π β§ (π§ β π β§ π€ β π) β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π}))) β (πβ{π€}) β (πβ{π})) |
47 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 15, 17, 19, 21, 31, 34, 41, 44, 45, 46, 38 | mapdh8 40301 |
. . . . 5
β’ ((π β§ (π§ β π β§ π€ β π) β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π}))) β (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©) = (πΌββ¨π€, (πΌββ¨π, πΉ, π€β©), πβ©)) |
48 | 47 | 3exp 1120 |
. . . 4
β’ (π β ((π§ β π β§ π€ β π) β ((Β¬ π§ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π})) β (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©) = (πΌββ¨π€, (πΌββ¨π, πΉ, π€β©), πβ©)))) |
49 | 48 | ralrimivv 3192 |
. . 3
β’ (π β βπ§ β π βπ€ β π ((Β¬ π§ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π})) β (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©) = (πΌββ¨π€, (πΌββ¨π, πΉ, π€β©), πβ©))) |
50 | 1, 2, 3, 6, 14, 25, 26 | dvh3dim 39959 |
. . . . 5
β’ (π β βπ§ β π Β¬ π§ β (πβ{π, π})) |
51 | 14 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β (πΎ β HL β§ π β π»)) |
52 | 16 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β πΉ β π·) |
53 | 18 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β (πβ(πβ{π})) = (π½β{πΉ})) |
54 | 20 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β π β (π β { 0 })) |
55 | | simplr 768 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β π§ β π) |
56 | 35 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β π β LVec) |
57 | 25 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β π β π) |
58 | 26 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β π β π) |
59 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β Β¬ π§ β (πβ{π, π})) |
60 | 3, 6, 56, 55, 57, 58, 59 | lspindpi 20638 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) |
61 | 60 | simpld 496 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β (πβ{π§}) β (πβ{π})) |
62 | 61 | necomd 2996 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β (πβ{π}) β (πβ{π§})) |
63 | 10, 13, 1, 12, 2, 3,
4, 5, 6, 7,
8, 9, 11, 51, 52, 53, 54, 55, 62 | mapdhcl 40240 |
. . . . . . . . 9
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β (πΌββ¨π, πΉ, π§β©) β π·) |
64 | | eqidd 2734 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β (πΌββ¨π, πΉ, π§β©) = (πΌββ¨π, πΉ, π§β©)) |
65 | 23 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β π β LMod) |
66 | 27 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β (πβ{π, π}) β (LSubSpβπ)) |
67 | 5, 22, 65, 66, 55, 59 | lssneln0 20457 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β π§ β (π β { 0 })) |
68 | 10, 13, 1, 12, 2, 3,
4, 5, 6, 7,
8, 9, 11, 51, 52, 53, 54, 67, 63, 62 | mapdheq 40241 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β ((πΌββ¨π, πΉ, π§β©) = (πΌββ¨π, πΉ, π§β©) β ((πβ(πβ{π§})) = (π½β{(πΌββ¨π, πΉ, π§β©)}) β§ (πβ(πβ{(π β π§)})) = (π½β{(πΉπ
(πΌββ¨π, πΉ, π§β©))})))) |
69 | 64, 68 | mpbid 231 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β ((πβ(πβ{π§})) = (π½β{(πΌββ¨π, πΉ, π§β©)}) β§ (πβ(πβ{(π β π§)})) = (π½β{(πΉπ
(πΌββ¨π, πΉ, π§β©))}))) |
70 | 69 | simpld 496 |
. . . . . . . . 9
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β (πβ(πβ{π§})) = (π½β{(πΌββ¨π, πΉ, π§β©)})) |
71 | 60 | simprd 497 |
. . . . . . . . 9
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β (πβ{π§}) β (πβ{π})) |
72 | 10, 13, 1, 12, 2, 3,
4, 5, 6, 7,
8, 9, 11, 51, 63, 70, 67, 58, 71 | mapdhcl 40240 |
. . . . . . . 8
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©) β π·) |
73 | 72 | ex 414 |
. . . . . . 7
β’ ((π β§ π§ β π) β (Β¬ π§ β (πβ{π, π}) β (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©) β π·)) |
74 | 73 | ancld 552 |
. . . . . 6
β’ ((π β§ π§ β π) β (Β¬ π§ β (πβ{π, π}) β (Β¬ π§ β (πβ{π, π}) β§ (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©) β π·))) |
75 | 74 | reximdva 3162 |
. . . . 5
β’ (π β (βπ§ β π Β¬ π§ β (πβ{π, π}) β βπ§ β π (Β¬ π§ β (πβ{π, π}) β§ (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©) β π·))) |
76 | 50, 75 | mpd 15 |
. . . 4
β’ (π β βπ§ β π (Β¬ π§ β (πβ{π, π}) β§ (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©) β π·)) |
77 | | eleq1w 2817 |
. . . . . 6
β’ (π§ = π€ β (π§ β (πβ{π, π}) β π€ β (πβ{π, π}))) |
78 | 77 | notbid 318 |
. . . . 5
β’ (π§ = π€ β (Β¬ π§ β (πβ{π, π}) β Β¬ π€ β (πβ{π, π}))) |
79 | | oteq1 4843 |
. . . . . . 7
β’ (π§ = π€ β β¨π§, (πΌββ¨π, πΉ, π§β©), πβ© = β¨π€, (πΌββ¨π, πΉ, π§β©), πβ©) |
80 | | oteq3 4845 |
. . . . . . . . 9
β’ (π§ = π€ β β¨π, πΉ, π§β© = β¨π, πΉ, π€β©) |
81 | 80 | fveq2d 6850 |
. . . . . . . 8
β’ (π§ = π€ β (πΌββ¨π, πΉ, π§β©) = (πΌββ¨π, πΉ, π€β©)) |
82 | 81 | oteq2d 4847 |
. . . . . . 7
β’ (π§ = π€ β β¨π€, (πΌββ¨π, πΉ, π§β©), πβ© = β¨π€, (πΌββ¨π, πΉ, π€β©), πβ©) |
83 | 79, 82 | eqtrd 2773 |
. . . . . 6
β’ (π§ = π€ β β¨π§, (πΌββ¨π, πΉ, π§β©), πβ© = β¨π€, (πΌββ¨π, πΉ, π€β©), πβ©) |
84 | 83 | fveq2d 6850 |
. . . . 5
β’ (π§ = π€ β (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©) = (πΌββ¨π€, (πΌββ¨π, πΉ, π€β©), πβ©)) |
85 | 78, 84 | reusv3 5364 |
. . . 4
β’
(βπ§ β
π (Β¬ π§ β (πβ{π, π}) β§ (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©) β π·) β (βπ§ β π βπ€ β π ((Β¬ π§ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π})) β (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©) = (πΌββ¨π€, (πΌββ¨π, πΉ, π€β©), πβ©)) β βπ¦ β π· βπ§ β π (Β¬ π§ β (πβ{π, π}) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©)))) |
86 | 76, 85 | syl 17 |
. . 3
β’ (π β (βπ§ β π βπ€ β π ((Β¬ π§ β (πβ{π, π}) β§ Β¬ π€ β (πβ{π, π})) β (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©) = (πΌββ¨π€, (πΌββ¨π, πΉ, π€β©), πβ©)) β βπ¦ β π· βπ§ β π (Β¬ π§ β (πβ{π, π}) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©)))) |
87 | 49, 86 | mpbid 231 |
. 2
β’ (π β βπ¦ β π· βπ§ β π (Β¬ π§ β (πβ{π, π}) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©))) |
88 | | reusv1 5356 |
. . 3
β’
(βπ§ β
π Β¬ π§ β (πβ{π, π}) β (β!π¦ β π· βπ§ β π (Β¬ π§ β (πβ{π, π}) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©)) β βπ¦ β π· βπ§ β π (Β¬ π§ β (πβ{π, π}) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©)))) |
89 | 50, 88 | syl 17 |
. 2
β’ (π β (β!π¦ β π· βπ§ β π (Β¬ π§ β (πβ{π, π}) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©)) β βπ¦ β π· βπ§ β π (Β¬ π§ β (πβ{π, π}) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©)))) |
90 | 87, 89 | mpbird 257 |
1
β’ (π β β!π¦ β π· βπ§ β π (Β¬ π§ β (πβ{π, π}) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©))) |