Step | Hyp | Ref
| Expression |
1 | | sspss 4060 |
. . 3
β’ ((πΎβπΊ) β (πΎβπ») β ((πΎβπΊ) β (πΎβπ») β¨ (πΎβπΊ) = (πΎβπ»))) |
2 | | lkrss2.f |
. . . . . . 7
β’ πΉ = (LFnlβπ) |
3 | | lkrss2.k |
. . . . . . 7
β’ πΎ = (LKerβπ) |
4 | | lkrss2.d |
. . . . . . 7
β’ π· = (LDualβπ) |
5 | | eqid 2737 |
. . . . . . 7
β’
(0gβπ·) = (0gβπ·) |
6 | | lkrss2.w |
. . . . . . 7
β’ (π β π β LVec) |
7 | | lkrss2.g |
. . . . . . 7
β’ (π β πΊ β πΉ) |
8 | | lkrss2.h |
. . . . . . 7
β’ (π β π» β πΉ) |
9 | 2, 3, 4, 5, 6, 7, 8 | lkrpssN 37628 |
. . . . . 6
β’ (π β ((πΎβπΊ) β (πΎβπ») β (πΊ β (0gβπ·) β§ π» = (0gβπ·)))) |
10 | | lveclmod 20570 |
. . . . . . . . . . . 12
β’ (π β LVec β π β LMod) |
11 | 6, 10 | syl 17 |
. . . . . . . . . . 11
β’ (π β π β LMod) |
12 | | lkrss2.s |
. . . . . . . . . . . 12
β’ π = (Scalarβπ) |
13 | | lkrss2.r |
. . . . . . . . . . . 12
β’ π
= (Baseβπ) |
14 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(0gβπ) = (0gβπ) |
15 | 12, 13, 14 | lmod0cl 20351 |
. . . . . . . . . . 11
β’ (π β LMod β
(0gβπ)
β π
) |
16 | 11, 15 | syl 17 |
. . . . . . . . . 10
β’ (π β (0gβπ) β π
) |
17 | 16 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π» = (0gβπ·)) β (0gβπ) β π
) |
18 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π» = (0gβπ·)) β π» = (0gβπ·)) |
19 | | lkrss2.t |
. . . . . . . . . . . 12
β’ Β· = (
Β·π βπ·) |
20 | 2, 12, 14, 4, 19, 5, 11, 7 | ldual0vs 37625 |
. . . . . . . . . . 11
β’ (π β
((0gβπ)
Β·
πΊ) =
(0gβπ·)) |
21 | 20 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π» = (0gβπ·)) β ((0gβπ) Β· πΊ) = (0gβπ·)) |
22 | 18, 21 | eqtr4d 2780 |
. . . . . . . . 9
β’ ((π β§ π» = (0gβπ·)) β π» = ((0gβπ) Β· πΊ)) |
23 | | oveq1 7365 |
. . . . . . . . . 10
β’ (π = (0gβπ) β (π Β· πΊ) = ((0gβπ) Β· πΊ)) |
24 | 23 | rspceeqv 3596 |
. . . . . . . . 9
β’
(((0gβπ) β π
β§ π» = ((0gβπ) Β· πΊ)) β βπ β π
π» = (π Β· πΊ)) |
25 | 17, 22, 24 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π» = (0gβπ·)) β βπ β π
π» = (π Β· πΊ)) |
26 | 25 | ex 414 |
. . . . . . 7
β’ (π β (π» = (0gβπ·) β βπ β π
π» = (π Β· πΊ))) |
27 | 26 | adantld 492 |
. . . . . 6
β’ (π β ((πΊ β (0gβπ·) β§ π» = (0gβπ·)) β βπ β π
π» = (π Β· πΊ))) |
28 | 9, 27 | sylbid 239 |
. . . . 5
β’ (π β ((πΎβπΊ) β (πΎβπ») β βπ β π
π» = (π Β· πΊ))) |
29 | 28 | imp 408 |
. . . 4
β’ ((π β§ (πΎβπΊ) β (πΎβπ»)) β βπ β π
π» = (π Β· πΊ)) |
30 | 6 | adantr 482 |
. . . . 5
β’ ((π β§ (πΎβπΊ) = (πΎβπ»)) β π β LVec) |
31 | 7 | adantr 482 |
. . . . 5
β’ ((π β§ (πΎβπΊ) = (πΎβπ»)) β πΊ β πΉ) |
32 | 8 | adantr 482 |
. . . . 5
β’ ((π β§ (πΎβπΊ) = (πΎβπ»)) β π» β πΉ) |
33 | | simpr 486 |
. . . . 5
β’ ((π β§ (πΎβπΊ) = (πΎβπ»)) β (πΎβπΊ) = (πΎβπ»)) |
34 | 12, 13, 2, 3, 4, 19,
30, 31, 32, 33 | eqlkr4 37630 |
. . . 4
β’ ((π β§ (πΎβπΊ) = (πΎβπ»)) β βπ β π
π» = (π Β· πΊ)) |
35 | 29, 34 | jaodan 957 |
. . 3
β’ ((π β§ ((πΎβπΊ) β (πΎβπ») β¨ (πΎβπΊ) = (πΎβπ»))) β βπ β π
π» = (π Β· πΊ)) |
36 | 1, 35 | sylan2b 595 |
. 2
β’ ((π β§ (πΎβπΊ) β (πΎβπ»)) β βπ β π
π» = (π Β· πΊ)) |
37 | 6 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β π
) β π β LVec) |
38 | 7 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β π
) β πΊ β πΉ) |
39 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π β π
) β π β π
) |
40 | 12, 13, 2, 3, 4, 19,
37, 38, 39 | lkrss 37633 |
. . . . . 6
β’ ((π β§ π β π
) β (πΎβπΊ) β (πΎβ(π Β· πΊ))) |
41 | 40 | ex 414 |
. . . . 5
β’ (π β (π β π
β (πΎβπΊ) β (πΎβ(π Β· πΊ)))) |
42 | | fveq2 6843 |
. . . . . . 7
β’ (π» = (π Β· πΊ) β (πΎβπ») = (πΎβ(π Β· πΊ))) |
43 | 42 | sseq2d 3977 |
. . . . . 6
β’ (π» = (π Β· πΊ) β ((πΎβπΊ) β (πΎβπ») β (πΎβπΊ) β (πΎβ(π Β· πΊ)))) |
44 | 43 | biimprcd 250 |
. . . . 5
β’ ((πΎβπΊ) β (πΎβ(π Β· πΊ)) β (π» = (π Β· πΊ) β (πΎβπΊ) β (πΎβπ»))) |
45 | 41, 44 | syl6 35 |
. . . 4
β’ (π β (π β π
β (π» = (π Β· πΊ) β (πΎβπΊ) β (πΎβπ»)))) |
46 | 45 | rexlimdv 3151 |
. . 3
β’ (π β (βπ β π
π» = (π Β· πΊ) β (πΎβπΊ) β (πΎβπ»))) |
47 | 46 | imp 408 |
. 2
β’ ((π β§ βπ β π
π» = (π Β· πΊ)) β (πΎβπΊ) β (πΎβπ»)) |
48 | 36, 47 | impbida 800 |
1
β’ (π β ((πΎβπΊ) β (πΎβπ») β βπ β π
π» = (π Β· πΊ))) |