Step | Hyp | Ref
| Expression |
1 | | hdmap14lem1.h |
. . . . . . . . 9
β’ π» = (LHypβπΎ) |
2 | | hdmap14lem1.u |
. . . . . . . . 9
β’ π = ((DVecHβπΎ)βπ) |
3 | | hdmap14lem1.v |
. . . . . . . . 9
β’ π = (Baseβπ) |
4 | | hdmap14lem3.o |
. . . . . . . . 9
β’ 0 =
(0gβπ) |
5 | | hdmap14lem1.c |
. . . . . . . . 9
β’ πΆ = ((LCDualβπΎ)βπ) |
6 | | eqid 2737 |
. . . . . . . . 9
β’
(0gβπΆ) = (0gβπΆ) |
7 | | eqid 2737 |
. . . . . . . . 9
β’
(BaseβπΆ) =
(BaseβπΆ) |
8 | | hdmap14lem1.s |
. . . . . . . . 9
β’ π = ((HDMapβπΎ)βπ) |
9 | | hdmap14lem1.k |
. . . . . . . . 9
β’ (π β (πΎ β HL β§ π β π»)) |
10 | 1, 2, 9 | dvhlmod 39576 |
. . . . . . . . . . 11
β’ (π β π β LMod) |
11 | | hdmap14lem1.f |
. . . . . . . . . . . 12
β’ (π β πΉ β (π΅ β {π})) |
12 | 11 | eldifad 3923 |
. . . . . . . . . . 11
β’ (π β πΉ β π΅) |
13 | | hdmap14lem3.x |
. . . . . . . . . . . 12
β’ (π β π β (π β { 0 })) |
14 | 13 | eldifad 3923 |
. . . . . . . . . . 11
β’ (π β π β π) |
15 | | hdmap14lem1.r |
. . . . . . . . . . . 12
β’ π
= (Scalarβπ) |
16 | | hdmap14lem1.t |
. . . . . . . . . . . 12
β’ Β· = (
Β·π βπ) |
17 | | hdmap14lem1.b |
. . . . . . . . . . . 12
β’ π΅ = (Baseβπ
) |
18 | 3, 15, 16, 17 | lmodvscl 20342 |
. . . . . . . . . . 11
β’ ((π β LMod β§ πΉ β π΅ β§ π β π) β (πΉ Β· π) β π) |
19 | 10, 12, 14, 18 | syl3anc 1372 |
. . . . . . . . . 10
β’ (π β (πΉ Β· π) β π) |
20 | | eldifsni 4751 |
. . . . . . . . . . . 12
β’ (πΉ β (π΅ β {π}) β πΉ β π) |
21 | 11, 20 | syl 17 |
. . . . . . . . . . 11
β’ (π β πΉ β π) |
22 | | eldifsni 4751 |
. . . . . . . . . . . 12
β’ (π β (π β { 0 }) β π β 0 ) |
23 | 13, 22 | syl 17 |
. . . . . . . . . . 11
β’ (π β π β 0 ) |
24 | | hdmap14lem1.z |
. . . . . . . . . . . 12
β’ π = (0gβπ
) |
25 | 1, 2, 9 | dvhlvec 39575 |
. . . . . . . . . . . 12
β’ (π β π β LVec) |
26 | 3, 16, 15, 17, 24, 4, 25, 12, 14 | lvecvsn0 20573 |
. . . . . . . . . . 11
β’ (π β ((πΉ Β· π) β 0 β (πΉ β π β§ π β 0 ))) |
27 | 21, 23, 26 | mpbir2and 712 |
. . . . . . . . . 10
β’ (π β (πΉ Β· π) β 0 ) |
28 | | eldifsn 4748 |
. . . . . . . . . 10
β’ ((πΉ Β· π) β (π β { 0 }) β ((πΉ Β· π) β π β§ (πΉ Β· π) β 0 )) |
29 | 19, 27, 28 | sylanbrc 584 |
. . . . . . . . 9
β’ (π β (πΉ Β· π) β (π β { 0 })) |
30 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 29 | hdmapnzcl 40311 |
. . . . . . . 8
β’ (π β (πβ(πΉ Β· π)) β ((BaseβπΆ) β {(0gβπΆ)})) |
31 | | eldifsni 4751 |
. . . . . . . 8
β’ ((πβ(πΉ Β· π)) β ((BaseβπΆ) β {(0gβπΆ)}) β (πβ(πΉ Β· π)) β (0gβπΆ)) |
32 | 30, 31 | syl 17 |
. . . . . . 7
β’ (π β (πβ(πΉ Β· π)) β (0gβπΆ)) |
33 | 32 | adantr 482 |
. . . . . 6
β’ ((π β§ π β {π}) β (πβ(πΉ Β· π)) β (0gβπΆ)) |
34 | | elsni 4604 |
. . . . . . . 8
β’ (π β {π} β π = π) |
35 | 34 | oveq1d 7373 |
. . . . . . 7
β’ (π β {π} β (π β (πβπ)) = (π β (πβπ))) |
36 | 1, 5, 9 | lcdlmod 40058 |
. . . . . . . 8
β’ (π β πΆ β LMod) |
37 | 1, 2, 3, 5, 7, 8, 9, 14 | hdmapcl 40296 |
. . . . . . . 8
β’ (π β (πβπ) β (BaseβπΆ)) |
38 | | hdmap14lem2.p |
. . . . . . . . 9
β’ π = (ScalarβπΆ) |
39 | | hdmap14lem2.e |
. . . . . . . . 9
β’ β = (
Β·π βπΆ) |
40 | | hdmap14lem2.q |
. . . . . . . . 9
β’ π = (0gβπ) |
41 | 7, 38, 39, 40, 6 | lmod0vs 20358 |
. . . . . . . 8
β’ ((πΆ β LMod β§ (πβπ) β (BaseβπΆ)) β (π β (πβπ)) = (0gβπΆ)) |
42 | 36, 37, 41 | syl2anc 585 |
. . . . . . 7
β’ (π β (π β (πβπ)) = (0gβπΆ)) |
43 | 35, 42 | sylan9eqr 2799 |
. . . . . 6
β’ ((π β§ π β {π}) β (π β (πβπ)) = (0gβπΆ)) |
44 | 33, 43 | neeqtrrd 3019 |
. . . . 5
β’ ((π β§ π β {π}) β (πβ(πΉ Β· π)) β (π β (πβπ))) |
45 | 44 | neneqd 2949 |
. . . 4
β’ ((π β§ π β {π}) β Β¬ (πβ(πΉ Β· π)) = (π β (πβπ))) |
46 | 45 | nrexdv 3147 |
. . 3
β’ (π β Β¬ βπ β {π} (πβ(πΉ Β· π)) = (π β (πβπ))) |
47 | | reuun2 4275 |
. . 3
β’ (Β¬
βπ β {π} (πβ(πΉ Β· π)) = (π β (πβπ)) β (β!π β ((π΄ β {π}) βͺ {π})(πβ(πΉ Β· π)) = (π β (πβπ)) β β!π β (π΄ β {π})(πβ(πΉ Β· π)) = (π β (πβπ)))) |
48 | 46, 47 | syl 17 |
. 2
β’ (π β (β!π β ((π΄ β {π}) βͺ {π})(πβ(πΉ Β· π)) = (π β (πβπ)) β β!π β (π΄ β {π})(πβ(πΉ Β· π)) = (π β (πβπ)))) |
49 | | hdmap14lem2.a |
. . . 4
β’ π΄ = (Baseβπ) |
50 | 38, 49, 40 | lmod0cl 20351 |
. . 3
β’ (πΆ β LMod β π β π΄) |
51 | | difsnid 4771 |
. . 3
β’ (π β π΄ β ((π΄ β {π}) βͺ {π}) = π΄) |
52 | | reueq1 3393 |
. . 3
β’ (((π΄ β {π}) βͺ {π}) = π΄ β (β!π β ((π΄ β {π}) βͺ {π})(πβ(πΉ Β· π)) = (π β (πβπ)) β β!π β π΄ (πβ(πΉ Β· π)) = (π β (πβπ)))) |
53 | 36, 50, 51, 52 | 4syl 19 |
. 2
β’ (π β (β!π β ((π΄ β {π}) βͺ {π})(πβ(πΉ Β· π)) = (π β (πβπ)) β β!π β π΄ (πβ(πΉ Β· π)) = (π β (πβπ)))) |
54 | 48, 53 | bitr3d 281 |
1
β’ (π β (β!π β (π΄ β {π})(πβ(πΉ Β· π)) = (π β (πβπ)) β β!π β π΄ (πβ(πΉ Β· π)) = (π β (πβπ)))) |