Step | Hyp | Ref
| Expression |
1 | | hdmap14lem1.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
2 | | hdmap14lem1.c |
. . . . . 6
β’ πΆ = ((LCDualβπΎ)βπ) |
3 | | hdmap14lem1.k |
. . . . . 6
β’ (π β (πΎ β HL β§ π β π»)) |
4 | 1, 2, 3 | lcdlmod 40058 |
. . . . 5
β’ (π β πΆ β LMod) |
5 | | hdmap14lem2.p |
. . . . . 6
β’ π = (ScalarβπΆ) |
6 | | hdmap14lem2.a |
. . . . . 6
β’ π΄ = (Baseβπ) |
7 | | hdmap14lem2.q |
. . . . . 6
β’ π = (0gβπ) |
8 | 5, 6, 7 | lmod0cl 20351 |
. . . . 5
β’ (πΆ β LMod β π β π΄) |
9 | 4, 8 | syl 17 |
. . . 4
β’ (π β π β π΄) |
10 | | hdmap14lem1.u |
. . . . . . 7
β’ π = ((DVecHβπΎ)βπ) |
11 | | hdmap14lem1.v |
. . . . . . 7
β’ π = (Baseβπ) |
12 | | eqid 2737 |
. . . . . . 7
β’
(BaseβπΆ) =
(BaseβπΆ) |
13 | | hdmap14lem1.s |
. . . . . . 7
β’ π = ((HDMapβπΎ)βπ) |
14 | | hdmap14lem3.x |
. . . . . . . 8
β’ (π β π β (π β { 0 })) |
15 | 14 | eldifad 3923 |
. . . . . . 7
β’ (π β π β π) |
16 | 1, 10, 11, 2, 12, 13, 3, 15 | hdmapcl 40296 |
. . . . . 6
β’ (π β (πβπ) β (BaseβπΆ)) |
17 | | hdmap14lem2.e |
. . . . . . 7
β’ β = (
Β·π βπΆ) |
18 | | eqid 2737 |
. . . . . . 7
β’
(0gβπΆ) = (0gβπΆ) |
19 | 12, 5, 17, 7, 18 | lmod0vs 20358 |
. . . . . 6
β’ ((πΆ β LMod β§ (πβπ) β (BaseβπΆ)) β (π β (πβπ)) = (0gβπΆ)) |
20 | 4, 16, 19 | syl2anc 585 |
. . . . 5
β’ (π β (π β (πβπ)) = (0gβπΆ)) |
21 | 20 | eqcomd 2743 |
. . . 4
β’ (π β (0gβπΆ) = (π β (πβπ))) |
22 | | oveq1 7365 |
. . . . 5
β’ (π = π β (π β (πβπ)) = (π β (πβπ))) |
23 | 22 | rspceeqv 3596 |
. . . 4
β’ ((π β π΄ β§ (0gβπΆ) = (π β (πβπ))) β βπ β π΄ (0gβπΆ) = (π β (πβπ))) |
24 | 9, 21, 23 | syl2anc 585 |
. . 3
β’ (π β βπ β π΄ (0gβπΆ) = (π β (πβπ))) |
25 | | hdmap14lem3.o |
. . . . . . . . . . 11
β’ 0 =
(0gβπ) |
26 | 1, 10, 11, 25, 2, 18, 12, 13, 3, 14 | hdmapnzcl 40311 |
. . . . . . . . . 10
β’ (π β (πβπ) β ((BaseβπΆ) β {(0gβπΆ)})) |
27 | | eldifsni 4751 |
. . . . . . . . . 10
β’ ((πβπ) β ((BaseβπΆ) β {(0gβπΆ)}) β (πβπ) β (0gβπΆ)) |
28 | 26, 27 | syl 17 |
. . . . . . . . 9
β’ (π β (πβπ) β (0gβπΆ)) |
29 | 28 | neneqd 2949 |
. . . . . . . 8
β’ (π β Β¬ (πβπ) = (0gβπΆ)) |
30 | 29 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π β§ (π β π΄ β§ β β π΄) β§ ((0gβπΆ) = (π β (πβπ)) β§ (0gβπΆ) = (β β (πβπ)))) β Β¬ (πβπ) = (0gβπΆ)) |
31 | | simp3l 1202 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΄ β§ β β π΄) β§ ((0gβπΆ) = (π β (πβπ)) β§ (0gβπΆ) = (β β (πβπ)))) β (0gβπΆ) = (π β (πβπ))) |
32 | 31 | eqcomd 2743 |
. . . . . . . . . 10
β’ ((π β§ (π β π΄ β§ β β π΄) β§ ((0gβπΆ) = (π β (πβπ)) β§ (0gβπΆ) = (β β (πβπ)))) β (π β (πβπ)) = (0gβπΆ)) |
33 | 1, 2, 3 | lcdlvec 40057 |
. . . . . . . . . . . 12
β’ (π β πΆ β LVec) |
34 | 33 | 3ad2ant1 1134 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΄ β§ β β π΄) β§ ((0gβπΆ) = (π β (πβπ)) β§ (0gβπΆ) = (β β (πβπ)))) β πΆ β LVec) |
35 | | simp2l 1200 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΄ β§ β β π΄) β§ ((0gβπΆ) = (π β (πβπ)) β§ (0gβπΆ) = (β β (πβπ)))) β π β π΄) |
36 | 16 | 3ad2ant1 1134 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΄ β§ β β π΄) β§ ((0gβπΆ) = (π β (πβπ)) β§ (0gβπΆ) = (β β (πβπ)))) β (πβπ) β (BaseβπΆ)) |
37 | 12, 17, 5, 6, 7, 18,
34, 35, 36 | lvecvs0or 20572 |
. . . . . . . . . 10
β’ ((π β§ (π β π΄ β§ β β π΄) β§ ((0gβπΆ) = (π β (πβπ)) β§ (0gβπΆ) = (β β (πβπ)))) β ((π β (πβπ)) = (0gβπΆ) β (π = π β¨ (πβπ) = (0gβπΆ)))) |
38 | 32, 37 | mpbid 231 |
. . . . . . . . 9
β’ ((π β§ (π β π΄ β§ β β π΄) β§ ((0gβπΆ) = (π β (πβπ)) β§ (0gβπΆ) = (β β (πβπ)))) β (π = π β¨ (πβπ) = (0gβπΆ))) |
39 | 38 | orcomd 870 |
. . . . . . . 8
β’ ((π β§ (π β π΄ β§ β β π΄) β§ ((0gβπΆ) = (π β (πβπ)) β§ (0gβπΆ) = (β β (πβπ)))) β ((πβπ) = (0gβπΆ) β¨ π = π)) |
40 | 39 | ord 863 |
. . . . . . 7
β’ ((π β§ (π β π΄ β§ β β π΄) β§ ((0gβπΆ) = (π β (πβπ)) β§ (0gβπΆ) = (β β (πβπ)))) β (Β¬ (πβπ) = (0gβπΆ) β π = π)) |
41 | 30, 40 | mpd 15 |
. . . . . 6
β’ ((π β§ (π β π΄ β§ β β π΄) β§ ((0gβπΆ) = (π β (πβπ)) β§ (0gβπΆ) = (β β (πβπ)))) β π = π) |
42 | | simp3r 1203 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΄ β§ β β π΄) β§ ((0gβπΆ) = (π β (πβπ)) β§ (0gβπΆ) = (β β (πβπ)))) β (0gβπΆ) = (β β (πβπ))) |
43 | 42 | eqcomd 2743 |
. . . . . . . . . 10
β’ ((π β§ (π β π΄ β§ β β π΄) β§ ((0gβπΆ) = (π β (πβπ)) β§ (0gβπΆ) = (β β (πβπ)))) β (β β (πβπ)) = (0gβπΆ)) |
44 | | simp2r 1201 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΄ β§ β β π΄) β§ ((0gβπΆ) = (π β (πβπ)) β§ (0gβπΆ) = (β β (πβπ)))) β β β π΄) |
45 | 12, 17, 5, 6, 7, 18,
34, 44, 36 | lvecvs0or 20572 |
. . . . . . . . . 10
β’ ((π β§ (π β π΄ β§ β β π΄) β§ ((0gβπΆ) = (π β (πβπ)) β§ (0gβπΆ) = (β β (πβπ)))) β ((β β (πβπ)) = (0gβπΆ) β (β = π β¨ (πβπ) = (0gβπΆ)))) |
46 | 43, 45 | mpbid 231 |
. . . . . . . . 9
β’ ((π β§ (π β π΄ β§ β β π΄) β§ ((0gβπΆ) = (π β (πβπ)) β§ (0gβπΆ) = (β β (πβπ)))) β (β = π β¨ (πβπ) = (0gβπΆ))) |
47 | 46 | orcomd 870 |
. . . . . . . 8
β’ ((π β§ (π β π΄ β§ β β π΄) β§ ((0gβπΆ) = (π β (πβπ)) β§ (0gβπΆ) = (β β (πβπ)))) β ((πβπ) = (0gβπΆ) β¨ β = π)) |
48 | 47 | ord 863 |
. . . . . . 7
β’ ((π β§ (π β π΄ β§ β β π΄) β§ ((0gβπΆ) = (π β (πβπ)) β§ (0gβπΆ) = (β β (πβπ)))) β (Β¬ (πβπ) = (0gβπΆ) β β = π)) |
49 | 30, 48 | mpd 15 |
. . . . . 6
β’ ((π β§ (π β π΄ β§ β β π΄) β§ ((0gβπΆ) = (π β (πβπ)) β§ (0gβπΆ) = (β β (πβπ)))) β β = π) |
50 | 41, 49 | eqtr4d 2780 |
. . . . 5
β’ ((π β§ (π β π΄ β§ β β π΄) β§ ((0gβπΆ) = (π β (πβπ)) β§ (0gβπΆ) = (β β (πβπ)))) β π = β) |
51 | 50 | 3exp 1120 |
. . . 4
β’ (π β ((π β π΄ β§ β β π΄) β (((0gβπΆ) = (π β (πβπ)) β§ (0gβπΆ) = (β β (πβπ))) β π = β))) |
52 | 51 | ralrimivv 3196 |
. . 3
β’ (π β βπ β π΄ ββ β π΄ (((0gβπΆ) = (π β (πβπ)) β§ (0gβπΆ) = (β β (πβπ))) β π = β)) |
53 | | oveq1 7365 |
. . . . 5
β’ (π = β β (π β (πβπ)) = (β β (πβπ))) |
54 | 53 | eqeq2d 2748 |
. . . 4
β’ (π = β β ((0gβπΆ) = (π β (πβπ)) β (0gβπΆ) = (β β (πβπ)))) |
55 | 54 | reu4 3690 |
. . 3
β’
(β!π β
π΄
(0gβπΆ) =
(π β (πβπ)) β (βπ β π΄ (0gβπΆ) = (π β (πβπ)) β§ βπ β π΄ ββ β π΄ (((0gβπΆ) = (π β (πβπ)) β§ (0gβπΆ) = (β β (πβπ))) β π = β))) |
56 | 24, 52, 55 | sylanbrc 584 |
. 2
β’ (π β β!π β π΄ (0gβπΆ) = (π β (πβπ))) |
57 | | hdmap14lem6.f |
. . . . . . . 8
β’ (π β πΉ = π) |
58 | 57 | oveq1d 7373 |
. . . . . . 7
β’ (π β (πΉ Β· π) = (π Β· π)) |
59 | 1, 10, 3 | dvhlmod 39576 |
. . . . . . . 8
β’ (π β π β LMod) |
60 | | hdmap14lem1.r |
. . . . . . . . 9
β’ π
= (Scalarβπ) |
61 | | hdmap14lem1.t |
. . . . . . . . 9
β’ Β· = (
Β·π βπ) |
62 | | hdmap14lem1.z |
. . . . . . . . 9
β’ π = (0gβπ
) |
63 | 11, 60, 61, 62, 25 | lmod0vs 20358 |
. . . . . . . 8
β’ ((π β LMod β§ π β π) β (π Β· π) = 0 ) |
64 | 59, 15, 63 | syl2anc 585 |
. . . . . . 7
β’ (π β (π Β· π) = 0 ) |
65 | 58, 64 | eqtrd 2777 |
. . . . . 6
β’ (π β (πΉ Β· π) = 0 ) |
66 | 65 | fveq2d 6847 |
. . . . 5
β’ (π β (πβ(πΉ Β· π)) = (πβ 0 )) |
67 | 1, 10, 25, 2, 18, 13, 3 | hdmapval0 40299 |
. . . . 5
β’ (π β (πβ 0 ) =
(0gβπΆ)) |
68 | 66, 67 | eqtrd 2777 |
. . . 4
β’ (π β (πβ(πΉ Β· π)) = (0gβπΆ)) |
69 | 68 | eqeq1d 2739 |
. . 3
β’ (π β ((πβ(πΉ Β· π)) = (π β (πβπ)) β (0gβπΆ) = (π β (πβπ)))) |
70 | 69 | reubidv 3372 |
. 2
β’ (π β (β!π β π΄ (πβ(πΉ Β· π)) = (π β (πβπ)) β β!π β π΄ (0gβπΆ) = (π β (πβπ)))) |
71 | 56, 70 | mpbird 257 |
1
β’ (π β β!π β π΄ (πβ(πΉ Β· π)) = (π β (πβπ))) |