Step | Hyp | Ref
| Expression |
1 | | lclkrlem2o.k |
. . 3
β’ (π β (πΎ β HL β§ π β π»)) |
2 | | lclkrlem2o.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
3 | | lclkrlem2o.u |
. . . . . 6
β’ π = ((DVecHβπΎ)βπ) |
4 | 2, 3, 1 | dvhlmod 39623 |
. . . . 5
β’ (π β π β LMod) |
5 | | lclkrlem2m.y |
. . . . 5
β’ (π β π β π) |
6 | | lclkrlem2m.v |
. . . . . 6
β’ π = (Baseβπ) |
7 | | eqid 2733 |
. . . . . 6
β’
(LSubSpβπ) =
(LSubSpβπ) |
8 | | lclkrlem2n.n |
. . . . . 6
β’ π = (LSpanβπ) |
9 | 6, 7, 8 | lspsncl 20482 |
. . . . 5
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
10 | 4, 5, 9 | syl2anc 585 |
. . . 4
β’ (π β (πβ{π}) β (LSubSpβπ)) |
11 | 6, 7 | lssss 20441 |
. . . 4
β’ ((πβ{π}) β (LSubSpβπ) β (πβ{π}) β π) |
12 | 10, 11 | syl 17 |
. . 3
β’ (π β (πβ{π}) β π) |
13 | | lclkrlem2o.b |
. . . . . . . 8
β’ π΅ = (π β ((((πΈ + πΊ)βπ) Γ (πΌβ((πΈ + πΊ)βπ))) Β· π)) |
14 | | lclkrlem2p.bn |
. . . . . . . 8
β’ (π β π΅ = (0gβπ)) |
15 | 13, 14 | eqtr3id 2787 |
. . . . . . 7
β’ (π β (π β ((((πΈ + πΊ)βπ) Γ (πΌβ((πΈ + πΊ)βπ))) Β· π)) = (0gβπ)) |
16 | | lclkrlem2m.x |
. . . . . . . 8
β’ (π β π β π) |
17 | | lclkrlem2m.s |
. . . . . . . . . . . 12
β’ π = (Scalarβπ) |
18 | 17 | lmodring 20373 |
. . . . . . . . . . 11
β’ (π β LMod β π β Ring) |
19 | 4, 18 | syl 17 |
. . . . . . . . . 10
β’ (π β π β Ring) |
20 | | lclkrlem2m.f |
. . . . . . . . . . . 12
β’ πΉ = (LFnlβπ) |
21 | | lclkrlem2m.d |
. . . . . . . . . . . 12
β’ π· = (LDualβπ) |
22 | | lclkrlem2m.p |
. . . . . . . . . . . 12
β’ + =
(+gβπ·) |
23 | | lclkrlem2m.e |
. . . . . . . . . . . 12
β’ (π β πΈ β πΉ) |
24 | | lclkrlem2m.g |
. . . . . . . . . . . 12
β’ (π β πΊ β πΉ) |
25 | 20, 21, 22, 4, 23, 24 | ldualvaddcl 37642 |
. . . . . . . . . . 11
β’ (π β (πΈ + πΊ) β πΉ) |
26 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(Baseβπ) =
(Baseβπ) |
27 | 17, 26, 6, 20 | lflcl 37576 |
. . . . . . . . . . 11
β’ ((π β LMod β§ (πΈ + πΊ) β πΉ β§ π β π) β ((πΈ + πΊ)βπ) β (Baseβπ)) |
28 | 4, 25, 16, 27 | syl3anc 1372 |
. . . . . . . . . 10
β’ (π β ((πΈ + πΊ)βπ) β (Baseβπ)) |
29 | 2, 3, 1 | dvhlvec 39622 |
. . . . . . . . . . . 12
β’ (π β π β LVec) |
30 | 17 | lvecdrng 20610 |
. . . . . . . . . . . 12
β’ (π β LVec β π β
DivRing) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . 11
β’ (π β π β DivRing) |
32 | 17, 26, 6, 20 | lflcl 37576 |
. . . . . . . . . . . 12
β’ ((π β LMod β§ (πΈ + πΊ) β πΉ β§ π β π) β ((πΈ + πΊ)βπ) β (Baseβπ)) |
33 | 4, 25, 5, 32 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (π β ((πΈ + πΊ)βπ) β (Baseβπ)) |
34 | | lclkrlem2o.n |
. . . . . . . . . . 11
β’ (π β ((πΈ + πΊ)βπ) β 0 ) |
35 | | lclkrlem2m.z |
. . . . . . . . . . . 12
β’ 0 =
(0gβπ) |
36 | | lclkrlem2m.i |
. . . . . . . . . . . 12
β’ πΌ = (invrβπ) |
37 | 26, 35, 36 | drnginvrcl 20240 |
. . . . . . . . . . 11
β’ ((π β DivRing β§ ((πΈ + πΊ)βπ) β (Baseβπ) β§ ((πΈ + πΊ)βπ) β 0 ) β (πΌβ((πΈ + πΊ)βπ)) β (Baseβπ)) |
38 | 31, 33, 34, 37 | syl3anc 1372 |
. . . . . . . . . 10
β’ (π β (πΌβ((πΈ + πΊ)βπ)) β (Baseβπ)) |
39 | | lclkrlem2m.q |
. . . . . . . . . . 11
β’ Γ =
(.rβπ) |
40 | 26, 39 | ringcl 19989 |
. . . . . . . . . 10
β’ ((π β Ring β§ ((πΈ + πΊ)βπ) β (Baseβπ) β§ (πΌβ((πΈ + πΊ)βπ)) β (Baseβπ)) β (((πΈ + πΊ)βπ) Γ (πΌβ((πΈ + πΊ)βπ))) β (Baseβπ)) |
41 | 19, 28, 38, 40 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (((πΈ + πΊ)βπ) Γ (πΌβ((πΈ + πΊ)βπ))) β (Baseβπ)) |
42 | | lclkrlem2m.t |
. . . . . . . . . 10
β’ Β· = (
Β·π βπ) |
43 | 6, 17, 42, 26 | lmodvscl 20383 |
. . . . . . . . 9
β’ ((π β LMod β§ (((πΈ + πΊ)βπ) Γ (πΌβ((πΈ + πΊ)βπ))) β (Baseβπ) β§ π β π) β ((((πΈ + πΊ)βπ) Γ (πΌβ((πΈ + πΊ)βπ))) Β· π) β π) |
44 | 4, 41, 5, 43 | syl3anc 1372 |
. . . . . . . 8
β’ (π β ((((πΈ + πΊ)βπ) Γ (πΌβ((πΈ + πΊ)βπ))) Β· π) β π) |
45 | | eqid 2733 |
. . . . . . . . 9
β’
(0gβπ) = (0gβπ) |
46 | | lclkrlem2m.m |
. . . . . . . . 9
β’ β =
(-gβπ) |
47 | 6, 45, 46 | lmodsubeq0 20425 |
. . . . . . . 8
β’ ((π β LMod β§ π β π β§ ((((πΈ + πΊ)βπ) Γ (πΌβ((πΈ + πΊ)βπ))) Β· π) β π) β ((π β ((((πΈ + πΊ)βπ) Γ (πΌβ((πΈ + πΊ)βπ))) Β· π)) = (0gβπ) β π = ((((πΈ + πΊ)βπ) Γ (πΌβ((πΈ + πΊ)βπ))) Β· π))) |
48 | 4, 16, 44, 47 | syl3anc 1372 |
. . . . . . 7
β’ (π β ((π β ((((πΈ + πΊ)βπ) Γ (πΌβ((πΈ + πΊ)βπ))) Β· π)) = (0gβπ) β π = ((((πΈ + πΊ)βπ) Γ (πΌβ((πΈ + πΊ)βπ))) Β· π))) |
49 | 15, 48 | mpbid 231 |
. . . . . 6
β’ (π β π = ((((πΈ + πΊ)βπ) Γ (πΌβ((πΈ + πΊ)βπ))) Β· π)) |
50 | 49 | sneqd 4602 |
. . . . 5
β’ (π β {π} = {((((πΈ + πΊ)βπ) Γ (πΌβ((πΈ + πΊ)βπ))) Β· π)}) |
51 | 50 | fveq2d 6850 |
. . . 4
β’ (π β (πβ{π}) = (πβ{((((πΈ + πΊ)βπ) Γ (πΌβ((πΈ + πΊ)βπ))) Β· π)})) |
52 | 17, 26, 6, 42, 8 | lspsnvsi 20509 |
. . . . 5
β’ ((π β LMod β§ (((πΈ + πΊ)βπ) Γ (πΌβ((πΈ + πΊ)βπ))) β (Baseβπ) β§ π β π) β (πβ{((((πΈ + πΊ)βπ) Γ (πΌβ((πΈ + πΊ)βπ))) Β· π)}) β (πβ{π})) |
53 | 4, 41, 5, 52 | syl3anc 1372 |
. . . 4
β’ (π β (πβ{((((πΈ + πΊ)βπ) Γ (πΌβ((πΈ + πΊ)βπ))) Β· π)}) β (πβ{π})) |
54 | 51, 53 | eqsstrd 3986 |
. . 3
β’ (π β (πβ{π}) β (πβ{π})) |
55 | | lclkrlem2o.o |
. . . 4
β’ β₯ =
((ocHβπΎ)βπ) |
56 | 2, 3, 6, 55 | dochss 39878 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πβ{π}) β π β§ (πβ{π}) β (πβ{π})) β ( β₯ β(πβ{π})) β ( β₯ β(πβ{π}))) |
57 | 1, 12, 54, 56 | syl3anc 1372 |
. 2
β’ (π β ( β₯ β(πβ{π})) β ( β₯ β(πβ{π}))) |
58 | 5 | snssd 4773 |
. . 3
β’ (π β {π} β π) |
59 | 2, 3, 55, 6, 8, 1,
58 | dochocsp 39892 |
. 2
β’ (π β ( β₯ β(πβ{π})) = ( β₯ β{π})) |
60 | 16 | snssd 4773 |
. . 3
β’ (π β {π} β π) |
61 | 2, 3, 55, 6, 8, 1,
60 | dochocsp 39892 |
. 2
β’ (π β ( β₯ β(πβ{π})) = ( β₯ β{π})) |
62 | 57, 59, 61 | 3sstr3d 3994 |
1
β’ (π β ( β₯ β{π}) β ( β₯ β{π})) |