Step | Hyp | Ref
| Expression |
1 | | lshpkrlem.w |
. . . . 5
β’ (π β π β LVec) |
2 | | lveclmod 20567 |
. . . . 5
β’ (π β LVec β π β LMod) |
3 | 1, 2 | syl 17 |
. . . 4
β’ (π β π β LMod) |
4 | | lshpkrlem.d |
. . . . 5
β’ π· = (Scalarβπ) |
5 | 4 | lmodfgrp 20331 |
. . . 4
β’ (π β LMod β π· β Grp) |
6 | | lshpkrlem.k |
. . . . 5
β’ πΎ = (Baseβπ·) |
7 | | lshpkrlem.o |
. . . . 5
β’ 0 =
(0gβπ·) |
8 | 6, 7 | grpidcl 18778 |
. . . 4
β’ (π· β Grp β 0 β πΎ) |
9 | 3, 5, 8 | 3syl 18 |
. . 3
β’ (π β 0 β πΎ) |
10 | | lshpkrlem.v |
. . . 4
β’ π = (Baseβπ) |
11 | | lshpkrlem.a |
. . . 4
β’ + =
(+gβπ) |
12 | | lshpkrlem.n |
. . . 4
β’ π = (LSpanβπ) |
13 | | lshpkrlem.p |
. . . 4
β’ β =
(LSSumβπ) |
14 | | lshpkrlem.h |
. . . 4
β’ π» = (LSHypβπ) |
15 | | lshpkrlem.u |
. . . 4
β’ (π β π β π») |
16 | | lshpkrlem.z |
. . . 4
β’ (π β π β π) |
17 | | lshpkrlem.x |
. . . 4
β’ (π β π β π) |
18 | | lshpkrlem.e |
. . . 4
β’ (π β (π β (πβ{π})) = π) |
19 | | lshpkrlem.t |
. . . 4
β’ Β· = (
Β·π βπ) |
20 | 10, 11, 12, 13, 14, 1, 15, 16, 17, 18, 4, 6, 19 | lshpsmreu 37571 |
. . 3
β’ (π β β!π β πΎ βπ β π π = (π + (π Β· π))) |
21 | | oveq1 7364 |
. . . . . . 7
β’ (π = 0 β (π Β· π) = ( 0 Β· π)) |
22 | 21 | oveq2d 7373 |
. . . . . 6
β’ (π = 0 β (π + (π Β· π)) = (π + ( 0 Β· π))) |
23 | 22 | eqeq2d 2747 |
. . . . 5
β’ (π = 0 β (π = (π + (π Β· π)) β π = (π + ( 0 Β· π)))) |
24 | 23 | rexbidv 3175 |
. . . 4
β’ (π = 0 β (βπ β π π = (π + (π Β· π)) β βπ β π π = (π + ( 0 Β· π)))) |
25 | 24 | riota2 7339 |
. . 3
β’ (( 0 β πΎ β§ β!π β πΎ βπ β π π = (π + (π Β· π))) β (βπ β π π = (π + ( 0 Β· π)) β (β©π β πΎ βπ β π π = (π + (π Β· π))) = 0 )) |
26 | 9, 20, 25 | syl2anc 584 |
. 2
β’ (π β (βπ β π π = (π + ( 0 Β· π)) β (β©π β πΎ βπ β π π = (π + (π Β· π))) = 0 )) |
27 | | simpr 485 |
. . . . . 6
β’ ((π β§ π β π) β π β π) |
28 | | eqidd 2737 |
. . . . . 6
β’ ((π β§ π β π) β π = π) |
29 | | eqeq2 2748 |
. . . . . . 7
β’ (π = π β (π = π β π = π)) |
30 | 29 | rspcev 3581 |
. . . . . 6
β’ ((π β π β§ π = π) β βπ β π π = π) |
31 | 27, 28, 30 | syl2anc 584 |
. . . . 5
β’ ((π β§ π β π) β βπ β π π = π) |
32 | 31 | ex 413 |
. . . 4
β’ (π β (π β π β βπ β π π = π)) |
33 | | eleq1a 2832 |
. . . . . 6
β’ (π β π β (π = π β π β π)) |
34 | 33 | a1i 11 |
. . . . 5
β’ (π β (π β π β (π = π β π β π))) |
35 | 34 | rexlimdv 3150 |
. . . 4
β’ (π β (βπ β π π = π β π β π)) |
36 | 32, 35 | impbid 211 |
. . 3
β’ (π β (π β π β βπ β π π = π)) |
37 | | eqid 2736 |
. . . . . . . . . . 11
β’
(0gβπ) = (0gβπ) |
38 | 10, 4, 19, 7, 37 | lmod0vs 20355 |
. . . . . . . . . 10
β’ ((π β LMod β§ π β π) β ( 0 Β· π) = (0gβπ)) |
39 | 3, 16, 38 | syl2anc 584 |
. . . . . . . . 9
β’ (π β ( 0 Β· π) = (0gβπ)) |
40 | 39 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π β π) β ( 0 Β· π) = (0gβπ)) |
41 | 40 | oveq2d 7373 |
. . . . . . 7
β’ ((π β§ π β π) β (π + ( 0 Β· π)) = (π + (0gβπ))) |
42 | 1 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β π) β π β LVec) |
43 | 42, 2 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β π) β π β LMod) |
44 | | eqid 2736 |
. . . . . . . . . 10
β’
(LSubSpβπ) =
(LSubSpβπ) |
45 | 44, 14, 3, 15 | lshplss 37443 |
. . . . . . . . 9
β’ (π β π β (LSubSpβπ)) |
46 | 10, 44 | lssel 20398 |
. . . . . . . . 9
β’ ((π β (LSubSpβπ) β§ π β π) β π β π) |
47 | 45, 46 | sylan 580 |
. . . . . . . 8
β’ ((π β§ π β π) β π β π) |
48 | 10, 11, 37 | lmod0vrid 20353 |
. . . . . . . 8
β’ ((π β LMod β§ π β π) β (π + (0gβπ)) = π) |
49 | 43, 47, 48 | syl2anc 584 |
. . . . . . 7
β’ ((π β§ π β π) β (π + (0gβπ)) = π) |
50 | 41, 49 | eqtrd 2776 |
. . . . . 6
β’ ((π β§ π β π) β (π + ( 0 Β· π)) = π) |
51 | 50 | eqeq2d 2747 |
. . . . 5
β’ ((π β§ π β π) β (π = (π + ( 0 Β· π)) β π = π)) |
52 | 51 | bicomd 222 |
. . . 4
β’ ((π β§ π β π) β (π = π β π = (π + ( 0 Β· π)))) |
53 | 52 | rexbidva 3173 |
. . 3
β’ (π β (βπ β π π = π β βπ β π π = (π + ( 0 Β· π)))) |
54 | 36, 53 | bitrd 278 |
. 2
β’ (π β (π β π β βπ β π π = (π + ( 0 Β· π)))) |
55 | | eqeq1 2740 |
. . . . . . . 8
β’ (π₯ = π β (π₯ = (π¦ + (π Β· π)) β π = (π¦ + (π Β· π)))) |
56 | 55 | rexbidv 3175 |
. . . . . . 7
β’ (π₯ = π β (βπ¦ β π π₯ = (π¦ + (π Β· π)) β βπ¦ β π π = (π¦ + (π Β· π)))) |
57 | 56 | riotabidv 7315 |
. . . . . 6
β’ (π₯ = π β (β©π β πΎ βπ¦ β π π₯ = (π¦ + (π Β· π))) = (β©π β πΎ βπ¦ β π π = (π¦ + (π Β· π)))) |
58 | | lshpkrlem.g |
. . . . . 6
β’ πΊ = (π₯ β π β¦ (β©π β πΎ βπ¦ β π π₯ = (π¦ + (π Β· π)))) |
59 | | riotaex 7317 |
. . . . . 6
β’
(β©π
β πΎ βπ¦ β π π = (π¦ + (π Β· π))) β V |
60 | 57, 58, 59 | fvmpt 6948 |
. . . . 5
β’ (π β π β (πΊβπ) = (β©π β πΎ βπ¦ β π π = (π¦ + (π Β· π)))) |
61 | | oveq1 7364 |
. . . . . . . . 9
β’ (π¦ = π β (π¦ + (π Β· π)) = (π + (π Β· π))) |
62 | 61 | eqeq2d 2747 |
. . . . . . . 8
β’ (π¦ = π β (π = (π¦ + (π Β· π)) β π = (π + (π Β· π)))) |
63 | 62 | cbvrexvw 3226 |
. . . . . . 7
β’
(βπ¦ β
π π = (π¦ + (π Β· π)) β βπ β π π = (π + (π Β· π))) |
64 | 63 | a1i 11 |
. . . . . 6
β’ (π β πΎ β (βπ¦ β π π = (π¦ + (π Β· π)) β βπ β π π = (π + (π Β· π)))) |
65 | 64 | riotabiia 7334 |
. . . . 5
β’
(β©π
β πΎ βπ¦ β π π = (π¦ + (π Β· π))) = (β©π β πΎ βπ β π π = (π + (π Β· π))) |
66 | 60, 65 | eqtrdi 2792 |
. . . 4
β’ (π β π β (πΊβπ) = (β©π β πΎ βπ β π π = (π + (π Β· π)))) |
67 | 17, 66 | syl 17 |
. . 3
β’ (π β (πΊβπ) = (β©π β πΎ βπ β π π = (π + (π Β· π)))) |
68 | 67 | eqeq1d 2738 |
. 2
β’ (π β ((πΊβπ) = 0 β
(β©π β
πΎ βπ β π π = (π + (π Β· π))) = 0 )) |
69 | 26, 54, 68 | 3bitr4d 310 |
1
β’ (π β (π β π β (πΊβπ) = 0 )) |