Step | Hyp | Ref
| Expression |
1 | | lcfrlem17.h |
. . . 4
β’ π» = (LHypβπΎ) |
2 | | lcfrlem17.o |
. . . 4
β’ β₯ =
((ocHβπΎ)βπ) |
3 | | lcfrlem17.u |
. . . 4
β’ π = ((DVecHβπΎ)βπ) |
4 | | lcfrlem17.v |
. . . 4
β’ π = (Baseβπ) |
5 | | lcfrlem17.p |
. . . 4
β’ + =
(+gβπ) |
6 | | lcfrlem17.z |
. . . 4
β’ 0 =
(0gβπ) |
7 | | lcfrlem17.n |
. . . 4
β’ π = (LSpanβπ) |
8 | | lcfrlem17.a |
. . . 4
β’ π΄ = (LSAtomsβπ) |
9 | | lcfrlem17.k |
. . . 4
β’ (π β (πΎ β HL β§ π β π»)) |
10 | | lcfrlem17.x |
. . . 4
β’ (π β π β (π β { 0 })) |
11 | | lcfrlem17.y |
. . . 4
β’ (π β π β (π β { 0 })) |
12 | | lcfrlem17.ne |
. . . 4
β’ (π β (πβ{π}) β (πβ{π})) |
13 | | lcfrlem22.b |
. . . 4
β’ π΅ = ((πβ{π, π}) β© ( β₯ β{(π + π)})) |
14 | | eqid 2732 |
. . . 4
β’
(LSSumβπ) =
(LSSumβπ) |
15 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14 | lcfrlem23 40424 |
. . 3
β’ (π β (( β₯ β{π, π})(LSSumβπ)π΅) = ( β₯ β{(π + π)})) |
16 | | lcfrlem24.t |
. . . . . 6
β’ Β· = (
Β·π βπ) |
17 | | lcfrlem24.s |
. . . . . 6
β’ π = (Scalarβπ) |
18 | | lcfrlem24.q |
. . . . . 6
β’ π = (0gβπ) |
19 | | lcfrlem24.r |
. . . . . 6
β’ π
= (Baseβπ) |
20 | | lcfrlem24.j |
. . . . . 6
β’ π½ = (π₯ β (π β { 0 }) β¦ (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π₯})π£ = (π€ + (π Β· π₯))))) |
21 | | lcfrlem24.ib |
. . . . . 6
β’ (π β πΌ β π΅) |
22 | | lcfrlem24.l |
. . . . . 6
β’ πΏ = (LKerβπ) |
23 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 16, 17, 18, 19, 20, 21, 22 | lcfrlem24 40425 |
. . . . 5
β’ (π β ( β₯ β{π, π}) = ((πΏβ(π½βπ)) β© (πΏβ(π½βπ)))) |
24 | | eqid 2732 |
. . . . . 6
β’
(.rβπ) = (.rβπ) |
25 | | lcfrlem29.i |
. . . . . 6
β’ πΉ = (invrβπ) |
26 | | eqid 2732 |
. . . . . 6
β’
(LFnlβπ) =
(LFnlβπ) |
27 | | lcfrlem25.d |
. . . . . 6
β’ π· = (LDualβπ) |
28 | | eqid 2732 |
. . . . . 6
β’ (
Β·π βπ·) = ( Β·π
βπ·) |
29 | | lcfrlem30.m |
. . . . . 6
β’ β =
(-gβπ·) |
30 | 1, 3, 9 | dvhlvec 39968 |
. . . . . 6
β’ (π β π β LVec) |
31 | | eqid 2732 |
. . . . . . 7
β’
(0gβπ·) = (0gβπ·) |
32 | | eqid 2732 |
. . . . . . 7
β’ {π β (LFnlβπ) β£ ( β₯ β( β₯
β(πΏβπ))) = (πΏβπ)} = {π β (LFnlβπ) β£ ( β₯ β( β₯
β(πΏβπ))) = (πΏβπ)} |
33 | 1, 2, 3, 4, 5, 16,
17, 19, 6, 26, 22, 27, 31, 32, 20, 9, 10 | lcfrlem10 40411 |
. . . . . 6
β’ (π β (π½βπ) β (LFnlβπ)) |
34 | 1, 2, 3, 4, 5, 16,
17, 19, 6, 26, 22, 27, 31, 32, 20, 9, 11 | lcfrlem10 40411 |
. . . . . 6
β’ (π β (π½βπ) β (LFnlβπ)) |
35 | | eqid 2732 |
. . . . . . . 8
β’
(LSubSpβπ) =
(LSubSpβπ) |
36 | 1, 3, 9 | dvhlmod 39969 |
. . . . . . . 8
β’ (π β π β LMod) |
37 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13 | lcfrlem22 40423 |
. . . . . . . 8
β’ (π β π΅ β π΄) |
38 | 35, 8, 36, 37 | lsatlssel 37855 |
. . . . . . 7
β’ (π β π΅ β (LSubSpβπ)) |
39 | 4, 35 | lssel 20540 |
. . . . . . 7
β’ ((π΅ β (LSubSpβπ) β§ πΌ β π΅) β πΌ β π) |
40 | 38, 21, 39 | syl2anc 584 |
. . . . . 6
β’ (π β πΌ β π) |
41 | | lcfrlem28.jn |
. . . . . 6
β’ (π β ((π½βπ)βπΌ) β π) |
42 | | lcfrlem30.c |
. . . . . 6
β’ πΆ = ((π½βπ) β (((πΉβ((π½βπ)βπΌ))(.rβπ)((π½βπ)βπΌ))( Β·π
βπ·)(π½βπ))) |
43 | 4, 17, 24, 18, 25, 26, 27, 28, 29, 30, 33, 34, 40, 41, 42, 22 | lcfrlem2 40402 |
. . . . 5
β’ (π β ((πΏβ(π½βπ)) β© (πΏβ(π½βπ))) β (πΏβπΆ)) |
44 | 23, 43 | eqsstrd 4019 |
. . . 4
β’ (π β ( β₯ β{π, π}) β (πΏβπΆ)) |
45 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 16, 17, 18, 19, 20, 21, 22, 27, 41 | lcfrlem28 40429 |
. . . . . 6
β’ (π β πΌ β 0 ) |
46 | 6, 7, 8, 30, 37, 21, 45 | lsatel 37863 |
. . . . 5
β’ (π β π΅ = (πβ{πΌ})) |
47 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 16, 17, 18, 19, 20, 21, 22, 27, 41, 25, 29, 42 | lcfrlem30 40431 |
. . . . . . 7
β’ (π β πΆ β (LFnlβπ)) |
48 | 26, 22, 35 | lkrlss 37953 |
. . . . . . 7
β’ ((π β LMod β§ πΆ β (LFnlβπ)) β (πΏβπΆ) β (LSubSpβπ)) |
49 | 36, 47, 48 | syl2anc 584 |
. . . . . 6
β’ (π β (πΏβπΆ) β (LSubSpβπ)) |
50 | 4, 17, 24, 18, 25, 26, 27, 28, 29, 30, 33, 34, 40, 41, 42, 22 | lcfrlem3 40403 |
. . . . . 6
β’ (π β πΌ β (πΏβπΆ)) |
51 | 35, 7, 36, 49, 50 | lspsnel5a 20599 |
. . . . 5
β’ (π β (πβ{πΌ}) β (πΏβπΆ)) |
52 | 46, 51 | eqsstrd 4019 |
. . . 4
β’ (π β π΅ β (πΏβπΆ)) |
53 | 35 | lsssssubg 20561 |
. . . . . . 7
β’ (π β LMod β
(LSubSpβπ) β
(SubGrpβπ)) |
54 | 36, 53 | syl 17 |
. . . . . 6
β’ (π β (LSubSpβπ) β (SubGrpβπ)) |
55 | 10 | eldifad 3959 |
. . . . . . . 8
β’ (π β π β π) |
56 | 11 | eldifad 3959 |
. . . . . . . 8
β’ (π β π β π) |
57 | | prssi 4823 |
. . . . . . . 8
β’ ((π β π β§ π β π) β {π, π} β π) |
58 | 55, 56, 57 | syl2anc 584 |
. . . . . . 7
β’ (π β {π, π} β π) |
59 | 1, 3, 4, 35, 2 | dochlss 40213 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ {π, π} β π) β ( β₯ β{π, π}) β (LSubSpβπ)) |
60 | 9, 58, 59 | syl2anc 584 |
. . . . . 6
β’ (π β ( β₯ β{π, π}) β (LSubSpβπ)) |
61 | 54, 60 | sseldd 3982 |
. . . . 5
β’ (π β ( β₯ β{π, π}) β (SubGrpβπ)) |
62 | 54, 38 | sseldd 3982 |
. . . . 5
β’ (π β π΅ β (SubGrpβπ)) |
63 | 54, 49 | sseldd 3982 |
. . . . 5
β’ (π β (πΏβπΆ) β (SubGrpβπ)) |
64 | 14 | lsmlub 19526 |
. . . . 5
β’ ((( β₯
β{π, π}) β (SubGrpβπ) β§ π΅ β (SubGrpβπ) β§ (πΏβπΆ) β (SubGrpβπ)) β ((( β₯ β{π, π}) β (πΏβπΆ) β§ π΅ β (πΏβπΆ)) β (( β₯ β{π, π})(LSSumβπ)π΅) β (πΏβπΆ))) |
65 | 61, 62, 63, 64 | syl3anc 1371 |
. . . 4
β’ (π β ((( β₯ β{π, π}) β (πΏβπΆ) β§ π΅ β (πΏβπΆ)) β (( β₯ β{π, π})(LSSumβπ)π΅) β (πΏβπΆ))) |
66 | 44, 52, 65 | mpbi2and 710 |
. . 3
β’ (π β (( β₯ β{π, π})(LSSumβπ)π΅) β (πΏβπΆ)) |
67 | 15, 66 | eqsstrrd 4020 |
. 2
β’ (π β ( β₯ β{(π + π)}) β (πΏβπΆ)) |
68 | | eqid 2732 |
. . 3
β’
(LSHypβπ) =
(LSHypβπ) |
69 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | lcfrlem17 40418 |
. . . 4
β’ (π β (π + π) β (π β { 0 })) |
70 | 1, 2, 3, 4, 6, 68,
9, 69 | dochsnshp 40312 |
. . 3
β’ (π β ( β₯ β{(π + π)}) β (LSHypβπ)) |
71 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 16, 17, 18, 19, 20, 21, 22, 27, 41, 25, 29, 42 | lcfrlem34 40435 |
. . . 4
β’ (π β πΆ β (0gβπ·)) |
72 | 68, 26, 22, 27, 31, 30, 47 | lduallkr3 38020 |
. . . 4
β’ (π β ((πΏβπΆ) β (LSHypβπ) β πΆ β (0gβπ·))) |
73 | 71, 72 | mpbird 256 |
. . 3
β’ (π β (πΏβπΆ) β (LSHypβπ)) |
74 | 68, 30, 70, 73 | lshpcmp 37846 |
. 2
β’ (π β (( β₯ β{(π + π)}) β (πΏβπΆ) β ( β₯ β{(π + π)}) = (πΏβπΆ))) |
75 | 67, 74 | mpbid 231 |
1
β’ (π β ( β₯ β{(π + π)}) = (πΏβπΆ)) |