Step | Hyp | Ref
| Expression |
1 | | hdmap11.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
2 | | hdmap11.u |
. . . . . 6
β’ π = ((DVecHβπΎ)βπ) |
3 | | hdmap11.v |
. . . . . 6
β’ π = (Baseβπ) |
4 | | hdmap11.n |
. . . . . 6
β’ π = (LSpanβπ) |
5 | | hdmap11.k |
. . . . . 6
β’ (π β (πΎ β HL β§ π β π»)) |
6 | | hdmap11.x |
. . . . . 6
β’ (π β π β π) |
7 | | hdmap11.y |
. . . . . 6
β’ (π β π β π) |
8 | 1, 2, 3, 4, 5, 6, 7 | dvh3dim 39955 |
. . . . 5
β’ (π β βπ§ β π Β¬ π§ β (πβ{π, π})) |
9 | 8 | adantr 482 |
. . . 4
β’ ((π β§ πΈ β (πβ{π, π})) β βπ§ β π Β¬ π§ β (πβ{π, π})) |
10 | | eqid 2733 |
. . . . . . . 8
β’
(LSubSpβπ) =
(LSubSpβπ) |
11 | 1, 2, 5 | dvhlmod 39619 |
. . . . . . . . 9
β’ (π β π β LMod) |
12 | 11 | adantr 482 |
. . . . . . . 8
β’ ((π β§ πΈ β (πβ{π, π})) β π β LMod) |
13 | 3, 10, 4, 11, 6, 7 | lspprcl 20454 |
. . . . . . . . 9
β’ (π β (πβ{π, π}) β (LSubSpβπ)) |
14 | 13 | adantr 482 |
. . . . . . . 8
β’ ((π β§ πΈ β (πβ{π, π})) β (πβ{π, π}) β (LSubSpβπ)) |
15 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ πΈ β (πβ{π, π})) β πΈ β (πβ{π, π})) |
16 | 10, 4, 12, 14, 15 | lspsnel5a 20472 |
. . . . . . 7
β’ ((π β§ πΈ β (πβ{π, π})) β (πβ{πΈ}) β (πβ{π, π})) |
17 | 16 | ssneld 3947 |
. . . . . 6
β’ ((π β§ πΈ β (πβ{π, π})) β (Β¬ π§ β (πβ{π, π}) β Β¬ π§ β (πβ{πΈ}))) |
18 | 17 | ancld 552 |
. . . . 5
β’ ((π β§ πΈ β (πβ{π, π})) β (Β¬ π§ β (πβ{π, π}) β (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{πΈ})))) |
19 | 18 | reximdv 3164 |
. . . 4
β’ ((π β§ πΈ β (πβ{π, π})) β (βπ§ β π Β¬ π§ β (πβ{π, π}) β βπ§ β π (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{πΈ})))) |
20 | 9, 19 | mpd 15 |
. . 3
β’ ((π β§ πΈ β (πβ{π, π})) β βπ§ β π (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{πΈ}))) |
21 | | eqid 2733 |
. . . . . . . . . 10
β’
(BaseβπΎ) =
(BaseβπΎ) |
22 | | eqid 2733 |
. . . . . . . . . 10
β’
((LTrnβπΎ)βπ) = ((LTrnβπΎ)βπ) |
23 | | hdmap11.o |
. . . . . . . . . 10
β’ 0 =
(0gβπ) |
24 | | hdmap11.e |
. . . . . . . . . 10
β’ πΈ = β¨( I βΎ
(BaseβπΎ)), ( I
βΎ ((LTrnβπΎ)βπ))β© |
25 | 1, 21, 22, 2, 3, 23, 24, 5 | dvheveccl 39621 |
. . . . . . . . 9
β’ (π β πΈ β (π β { 0 })) |
26 | 25 | eldifad 3923 |
. . . . . . . 8
β’ (π β πΈ β π) |
27 | 1, 2, 3, 4, 5, 26,
7 | dvh3dim 39955 |
. . . . . . 7
β’ (π β βπ§ β π Β¬ π§ β (πβ{πΈ, π})) |
28 | 27 | adantr 482 |
. . . . . 6
β’ ((π β§ π = 0 ) β βπ§ β π Β¬ π§ β (πβ{πΈ, π})) |
29 | | preq1 4695 |
. . . . . . . . . . . . 13
β’ (π = 0 β {π, π} = { 0 , π}) |
30 | | prcom 4694 |
. . . . . . . . . . . . 13
β’ { 0 , π} = {π, 0 } |
31 | 29, 30 | eqtrdi 2789 |
. . . . . . . . . . . 12
β’ (π = 0 β {π, π} = {π, 0 }) |
32 | 31 | fveq2d 6847 |
. . . . . . . . . . 11
β’ (π = 0 β (πβ{π, π}) = (πβ{π, 0 })) |
33 | 3, 23, 4, 11, 7 | lsppr0 20568 |
. . . . . . . . . . 11
β’ (π β (πβ{π, 0 }) = (πβ{π})) |
34 | 32, 33 | sylan9eqr 2795 |
. . . . . . . . . 10
β’ ((π β§ π = 0 ) β (πβ{π, π}) = (πβ{π})) |
35 | 3, 10, 4, 11, 26, 7 | lspprcl 20454 |
. . . . . . . . . . . 12
β’ (π β (πβ{πΈ, π}) β (LSubSpβπ)) |
36 | 3, 4, 11, 26, 7 | lspprid2 20474 |
. . . . . . . . . . . 12
β’ (π β π β (πβ{πΈ, π})) |
37 | 10, 4, 11, 35, 36 | lspsnel5a 20472 |
. . . . . . . . . . 11
β’ (π β (πβ{π}) β (πβ{πΈ, π})) |
38 | 37 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π = 0 ) β (πβ{π}) β (πβ{πΈ, π})) |
39 | 34, 38 | eqsstrd 3983 |
. . . . . . . . 9
β’ ((π β§ π = 0 ) β (πβ{π, π}) β (πβ{πΈ, π})) |
40 | 39 | ssneld 3947 |
. . . . . . . 8
β’ ((π β§ π = 0 ) β (Β¬ π§ β (πβ{πΈ, π}) β Β¬ π§ β (πβ{π, π}))) |
41 | 3, 4, 11, 26, 7 | lspprid1 20473 |
. . . . . . . . . . 11
β’ (π β πΈ β (πβ{πΈ, π})) |
42 | 10, 4, 11, 35, 41 | lspsnel5a 20472 |
. . . . . . . . . 10
β’ (π β (πβ{πΈ}) β (πβ{πΈ, π})) |
43 | 42 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π = 0 ) β (πβ{πΈ}) β (πβ{πΈ, π})) |
44 | 43 | ssneld 3947 |
. . . . . . . 8
β’ ((π β§ π = 0 ) β (Β¬ π§ β (πβ{πΈ, π}) β Β¬ π§ β (πβ{πΈ}))) |
45 | 40, 44 | jcad 514 |
. . . . . . 7
β’ ((π β§ π = 0 ) β (Β¬ π§ β (πβ{πΈ, π}) β (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{πΈ})))) |
46 | 45 | reximdv 3164 |
. . . . . 6
β’ ((π β§ π = 0 ) β (βπ§ β π Β¬ π§ β (πβ{πΈ, π}) β βπ§ β π (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{πΈ})))) |
47 | 28, 46 | mpd 15 |
. . . . 5
β’ ((π β§ π = 0 ) β βπ§ β π (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{πΈ}))) |
48 | 47 | adantlr 714 |
. . . 4
β’ (((π β§ Β¬ πΈ β (πβ{π, π})) β§ π = 0 ) β βπ§ β π (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{πΈ}))) |
49 | | hdmap11.p |
. . . . . . . 8
β’ + =
(+gβπ) |
50 | 3, 49 | lmodvacl 20351 |
. . . . . . 7
β’ ((π β LMod β§ πΈ β π β§ π β π) β (πΈ + π) β π) |
51 | 11, 26, 6, 50 | syl3anc 1372 |
. . . . . 6
β’ (π β (πΈ + π) β π) |
52 | 51 | ad2antrr 725 |
. . . . 5
β’ (((π β§ Β¬ πΈ β (πβ{π, π})) β§ π β 0 ) β (πΈ + π) β π) |
53 | 11 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ Β¬ πΈ β (πβ{π, π})) β§ π β 0 ) β π β LMod) |
54 | 13 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ Β¬ πΈ β (πβ{π, π})) β§ π β 0 ) β (πβ{π, π}) β (LSubSpβπ)) |
55 | 3, 4, 11, 6, 7 | lspprid1 20473 |
. . . . . . 7
β’ (π β π β (πβ{π, π})) |
56 | 55 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ Β¬ πΈ β (πβ{π, π})) β§ π β 0 ) β π β (πβ{π, π})) |
57 | 26 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ Β¬ πΈ β (πβ{π, π})) β§ π β 0 ) β πΈ β π) |
58 | | simplr 768 |
. . . . . 6
β’ (((π β§ Β¬ πΈ β (πβ{π, π})) β§ π β 0 ) β Β¬ πΈ β (πβ{π, π})) |
59 | 3, 49, 10, 53, 54, 56, 57, 58 | lssvancl2 20421 |
. . . . 5
β’ (((π β§ Β¬ πΈ β (πβ{π, π})) β§ π β 0 ) β Β¬ (πΈ + π) β (πβ{π, π})) |
60 | 3, 10, 4 | lspsncl 20453 |
. . . . . . . 8
β’ ((π β LMod β§ πΈ β π) β (πβ{πΈ}) β (LSubSpβπ)) |
61 | 11, 26, 60 | syl2anc 585 |
. . . . . . 7
β’ (π β (πβ{πΈ}) β (LSubSpβπ)) |
62 | 61 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ Β¬ πΈ β (πβ{π, π})) β§ π β 0 ) β (πβ{πΈ}) β (LSubSpβπ)) |
63 | 3, 4 | lspsnid 20469 |
. . . . . . . 8
β’ ((π β LMod β§ πΈ β π) β πΈ β (πβ{πΈ})) |
64 | 11, 26, 63 | syl2anc 585 |
. . . . . . 7
β’ (π β πΈ β (πβ{πΈ})) |
65 | 64 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ Β¬ πΈ β (πβ{π, π})) β§ π β 0 ) β πΈ β (πβ{πΈ})) |
66 | 6 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ Β¬ πΈ β (πβ{π, π})) β§ π β 0 ) β π β π) |
67 | 1, 2, 5 | dvhlvec 39618 |
. . . . . . . 8
β’ (π β π β LVec) |
68 | 67 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ Β¬ πΈ β (πβ{π, π})) β§ π β 0 ) β π β LVec) |
69 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ Β¬ πΈ β (πβ{π, π})) β§ π β 0 ) β π β 0 ) |
70 | | eldifsn 4748 |
. . . . . . . 8
β’ (π β (π β { 0 }) β (π β π β§ π β 0 )) |
71 | 66, 69, 70 | sylanbrc 584 |
. . . . . . 7
β’ (((π β§ Β¬ πΈ β (πβ{π, π})) β§ π β 0 ) β π β (π β { 0 })) |
72 | 10, 4, 11, 13, 55 | lspsnel5a 20472 |
. . . . . . . . . 10
β’ (π β (πβ{π}) β (πβ{π, π})) |
73 | 72 | sseld 3944 |
. . . . . . . . 9
β’ (π β (πΈ β (πβ{π}) β πΈ β (πβ{π, π}))) |
74 | 73 | con3dimp 410 |
. . . . . . . 8
β’ ((π β§ Β¬ πΈ β (πβ{π, π})) β Β¬ πΈ β (πβ{π})) |
75 | 74 | adantr 482 |
. . . . . . 7
β’ (((π β§ Β¬ πΈ β (πβ{π, π})) β§ π β 0 ) β Β¬ πΈ β (πβ{π})) |
76 | 3, 23, 4, 68, 57, 71, 75 | lspsnnecom 20596 |
. . . . . 6
β’ (((π β§ Β¬ πΈ β (πβ{π, π})) β§ π β 0 ) β Β¬ π β (πβ{πΈ})) |
77 | 3, 49, 10, 53, 62, 65, 66, 76 | lssvancl1 20420 |
. . . . 5
β’ (((π β§ Β¬ πΈ β (πβ{π, π})) β§ π β 0 ) β Β¬ (πΈ + π) β (πβ{πΈ})) |
78 | | eleq1 2822 |
. . . . . . . 8
β’ (π§ = (πΈ + π) β (π§ β (πβ{π, π}) β (πΈ + π) β (πβ{π, π}))) |
79 | 78 | notbid 318 |
. . . . . . 7
β’ (π§ = (πΈ + π) β (Β¬ π§ β (πβ{π, π}) β Β¬ (πΈ + π) β (πβ{π, π}))) |
80 | | eleq1 2822 |
. . . . . . . 8
β’ (π§ = (πΈ + π) β (π§ β (πβ{πΈ}) β (πΈ + π) β (πβ{πΈ}))) |
81 | 80 | notbid 318 |
. . . . . . 7
β’ (π§ = (πΈ + π) β (Β¬ π§ β (πβ{πΈ}) β Β¬ (πΈ + π) β (πβ{πΈ}))) |
82 | 79, 81 | anbi12d 632 |
. . . . . 6
β’ (π§ = (πΈ + π) β ((Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{πΈ})) β (Β¬ (πΈ + π) β (πβ{π, π}) β§ Β¬ (πΈ + π) β (πβ{πΈ})))) |
83 | 82 | rspcev 3580 |
. . . . 5
β’ (((πΈ + π) β π β§ (Β¬ (πΈ + π) β (πβ{π, π}) β§ Β¬ (πΈ + π) β (πβ{πΈ}))) β βπ§ β π (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{πΈ}))) |
84 | 52, 59, 77, 83 | syl12anc 836 |
. . . 4
β’ (((π β§ Β¬ πΈ β (πβ{π, π})) β§ π β 0 ) β βπ§ β π (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{πΈ}))) |
85 | 48, 84 | pm2.61dane 3029 |
. . 3
β’ ((π β§ Β¬ πΈ β (πβ{π, π})) β βπ§ β π (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{πΈ}))) |
86 | 20, 85 | pm2.61dan 812 |
. 2
β’ (π β βπ§ β π (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{πΈ}))) |
87 | | hdmap11.c |
. . . 4
β’ πΆ = ((LCDualβπΎ)βπ) |
88 | | hdmap11.a |
. . . 4
β’ β =
(+gβπΆ) |
89 | | hdmap11.s |
. . . 4
β’ π = ((HDMapβπΎ)βπ) |
90 | 5 | 3ad2ant1 1134 |
. . . 4
β’ ((π β§ π§ β π β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{πΈ}))) β (πΎ β HL β§ π β π»)) |
91 | 6 | 3ad2ant1 1134 |
. . . 4
β’ ((π β§ π§ β π β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{πΈ}))) β π β π) |
92 | 7 | 3ad2ant1 1134 |
. . . 4
β’ ((π β§ π§ β π β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{πΈ}))) β π β π) |
93 | | hdmap11.d |
. . . 4
β’ π· = (BaseβπΆ) |
94 | | hdmap11.l |
. . . 4
β’ πΏ = (LSpanβπΆ) |
95 | | hdmap11.m |
. . . 4
β’ π = ((mapdβπΎ)βπ) |
96 | | hdmap11.j |
. . . 4
β’ π½ = ((HVMapβπΎ)βπ) |
97 | | hdmap11.i |
. . . 4
β’ πΌ = ((HDMap1βπΎ)βπ) |
98 | | simp2 1138 |
. . . 4
β’ ((π β§ π§ β π β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{πΈ}))) β π§ β π) |
99 | | simp3l 1202 |
. . . 4
β’ ((π β§ π§ β π β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{πΈ}))) β Β¬ π§ β (πβ{π, π})) |
100 | 11 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ π§ β π β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{πΈ}))) β π β LMod) |
101 | 26 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ π§ β π β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{πΈ}))) β πΈ β π) |
102 | | simp3r 1203 |
. . . . 5
β’ ((π β§ π§ β π β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{πΈ}))) β Β¬ π§ β (πβ{πΈ})) |
103 | 3, 4, 100, 98, 101, 102 | lspsnne2 20595 |
. . . 4
β’ ((π β§ π§ β π β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{πΈ}))) β (πβ{π§}) β (πβ{πΈ})) |
104 | 1, 2, 3, 49, 87, 88, 89, 90, 91, 92, 24, 23, 4, 93, 94, 95, 96, 97, 98, 99, 103 | hdmap11lem1 40350 |
. . 3
β’ ((π β§ π§ β π β§ (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{πΈ}))) β (πβ(π + π)) = ((πβπ) β (πβπ))) |
105 | 104 | rexlimdv3a 3153 |
. 2
β’ (π β (βπ§ β π (Β¬ π§ β (πβ{π, π}) β§ Β¬ π§ β (πβ{πΈ})) β (πβ(π + π)) = ((πβπ) β (πβπ)))) |
106 | 86, 105 | mpd 15 |
1
β’ (π β (πβ(π + π)) = ((πβπ) β (πβπ))) |