Step | Hyp | Ref
| Expression |
1 | | lcfrlem30.c |
. . 3
β’ πΆ = ((π½βπ) β (((πΉβ((π½βπ)βπΌ))(.rβπ)((π½βπ)βπΌ))( Β·π
βπ·)(π½βπ))) |
2 | | lcfrlem33.xi |
. . . . . . . . 9
β’ (π β ((π½βπ)βπΌ) = π) |
3 | 2 | oveq2d 7377 |
. . . . . . . 8
β’ (π β ((πΉβ((π½βπ)βπΌ))(.rβπ)((π½βπ)βπΌ)) = ((πΉβ((π½βπ)βπΌ))(.rβπ)π)) |
4 | | lcfrlem17.h |
. . . . . . . . . . 11
β’ π» = (LHypβπΎ) |
5 | | lcfrlem17.u |
. . . . . . . . . . 11
β’ π = ((DVecHβπΎ)βπ) |
6 | | lcfrlem17.k |
. . . . . . . . . . 11
β’ (π β (πΎ β HL β§ π β π»)) |
7 | 4, 5, 6 | dvhlmod 39623 |
. . . . . . . . . 10
β’ (π β π β LMod) |
8 | | lcfrlem24.s |
. . . . . . . . . . 11
β’ π = (Scalarβπ) |
9 | 8 | lmodring 20373 |
. . . . . . . . . 10
β’ (π β LMod β π β Ring) |
10 | 7, 9 | syl 17 |
. . . . . . . . 9
β’ (π β π β Ring) |
11 | 4, 5, 6 | dvhlvec 39622 |
. . . . . . . . . . 11
β’ (π β π β LVec) |
12 | 8 | lvecdrng 20610 |
. . . . . . . . . . 11
β’ (π β LVec β π β
DivRing) |
13 | 11, 12 | syl 17 |
. . . . . . . . . 10
β’ (π β π β DivRing) |
14 | | lcfrlem17.o |
. . . . . . . . . . . 12
β’ β₯ =
((ocHβπΎ)βπ) |
15 | | lcfrlem17.v |
. . . . . . . . . . . 12
β’ π = (Baseβπ) |
16 | | lcfrlem17.p |
. . . . . . . . . . . 12
β’ + =
(+gβπ) |
17 | | lcfrlem24.t |
. . . . . . . . . . . 12
β’ Β· = (
Β·π βπ) |
18 | | lcfrlem24.r |
. . . . . . . . . . . 12
β’ π
= (Baseβπ) |
19 | | lcfrlem17.z |
. . . . . . . . . . . 12
β’ 0 =
(0gβπ) |
20 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(LFnlβπ) =
(LFnlβπ) |
21 | | lcfrlem24.l |
. . . . . . . . . . . 12
β’ πΏ = (LKerβπ) |
22 | | lcfrlem25.d |
. . . . . . . . . . . 12
β’ π· = (LDualβπ) |
23 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(0gβπ·) = (0gβπ·) |
24 | | eqid 2733 |
. . . . . . . . . . . 12
β’ {π β (LFnlβπ) β£ ( β₯ β( β₯
β(πΏβπ))) = (πΏβπ)} = {π β (LFnlβπ) β£ ( β₯ β( β₯
β(πΏβπ))) = (πΏβπ)} |
25 | | lcfrlem24.j |
. . . . . . . . . . . 12
β’ π½ = (π₯ β (π β { 0 }) β¦ (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π₯})π£ = (π€ + (π Β· π₯))))) |
26 | | lcfrlem17.y |
. . . . . . . . . . . 12
β’ (π β π β (π β { 0 })) |
27 | 4, 14, 5, 15, 16, 17, 8, 18, 19, 20, 21, 22, 23, 24, 25, 6, 26 | lcfrlem10 40065 |
. . . . . . . . . . 11
β’ (π β (π½βπ) β (LFnlβπ)) |
28 | | lcfrlem17.a |
. . . . . . . . . . . . 13
β’ π΄ = (LSAtomsβπ) |
29 | | lcfrlem17.n |
. . . . . . . . . . . . . 14
β’ π = (LSpanβπ) |
30 | | lcfrlem17.x |
. . . . . . . . . . . . . 14
β’ (π β π β (π β { 0 })) |
31 | | lcfrlem17.ne |
. . . . . . . . . . . . . 14
β’ (π β (πβ{π}) β (πβ{π})) |
32 | | lcfrlem22.b |
. . . . . . . . . . . . . 14
β’ π΅ = ((πβ{π, π}) β© ( β₯ β{(π + π)})) |
33 | 4, 14, 5, 15, 16, 19, 29, 28, 6, 30, 26, 31, 32 | lcfrlem22 40077 |
. . . . . . . . . . . . 13
β’ (π β π΅ β π΄) |
34 | 15, 28, 7, 33 | lsatssv 37510 |
. . . . . . . . . . . 12
β’ (π β π΅ β π) |
35 | | lcfrlem24.ib |
. . . . . . . . . . . 12
β’ (π β πΌ β π΅) |
36 | 34, 35 | sseldd 3949 |
. . . . . . . . . . 11
β’ (π β πΌ β π) |
37 | 8, 18, 15, 20 | lflcl 37576 |
. . . . . . . . . . 11
β’ ((π β LMod β§ (π½βπ) β (LFnlβπ) β§ πΌ β π) β ((π½βπ)βπΌ) β π
) |
38 | 7, 27, 36, 37 | syl3anc 1372 |
. . . . . . . . . 10
β’ (π β ((π½βπ)βπΌ) β π
) |
39 | | lcfrlem28.jn |
. . . . . . . . . 10
β’ (π β ((π½βπ)βπΌ) β π) |
40 | | lcfrlem24.q |
. . . . . . . . . . 11
β’ π = (0gβπ) |
41 | | lcfrlem29.i |
. . . . . . . . . . 11
β’ πΉ = (invrβπ) |
42 | 18, 40, 41 | drnginvrcl 20240 |
. . . . . . . . . 10
β’ ((π β DivRing β§ ((π½βπ)βπΌ) β π
β§ ((π½βπ)βπΌ) β π) β (πΉβ((π½βπ)βπΌ)) β π
) |
43 | 13, 38, 39, 42 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (πΉβ((π½βπ)βπΌ)) β π
) |
44 | | eqid 2733 |
. . . . . . . . . 10
β’
(.rβπ) = (.rβπ) |
45 | 18, 44, 40 | ringrz 20020 |
. . . . . . . . 9
β’ ((π β Ring β§ (πΉβ((π½βπ)βπΌ)) β π
) β ((πΉβ((π½βπ)βπΌ))(.rβπ)π) = π) |
46 | 10, 43, 45 | syl2anc 585 |
. . . . . . . 8
β’ (π β ((πΉβ((π½βπ)βπΌ))(.rβπ)π) = π) |
47 | 3, 46 | eqtrd 2773 |
. . . . . . 7
β’ (π β ((πΉβ((π½βπ)βπΌ))(.rβπ)((π½βπ)βπΌ)) = π) |
48 | 47 | oveq1d 7376 |
. . . . . 6
β’ (π β (((πΉβ((π½βπ)βπΌ))(.rβπ)((π½βπ)βπΌ))( Β·π
βπ·)(π½βπ)) = (π( Β·π
βπ·)(π½βπ))) |
49 | | eqid 2733 |
. . . . . . 7
β’ (
Β·π βπ·) = ( Β·π
βπ·) |
50 | 20, 8, 40, 22, 49, 23, 7, 27 | ldual0vs 37672 |
. . . . . 6
β’ (π β (π( Β·π
βπ·)(π½βπ)) = (0gβπ·)) |
51 | 48, 50 | eqtrd 2773 |
. . . . 5
β’ (π β (((πΉβ((π½βπ)βπΌ))(.rβπ)((π½βπ)βπΌ))( Β·π
βπ·)(π½βπ)) = (0gβπ·)) |
52 | 51 | oveq2d 7377 |
. . . 4
β’ (π β ((π½βπ) β (((πΉβ((π½βπ)βπΌ))(.rβπ)((π½βπ)βπΌ))( Β·π
βπ·)(π½βπ))) = ((π½βπ) β
(0gβπ·))) |
53 | 22, 7 | ldualgrp 37658 |
. . . . 5
β’ (π β π· β Grp) |
54 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ·) =
(Baseβπ·) |
55 | 4, 14, 5, 15, 16, 17, 8, 18, 19, 20, 21, 22, 23, 24, 25, 6, 30 | lcfrlem10 40065 |
. . . . . 6
β’ (π β (π½βπ) β (LFnlβπ)) |
56 | 20, 22, 54, 7, 55 | ldualelvbase 37639 |
. . . . 5
β’ (π β (π½βπ) β (Baseβπ·)) |
57 | | lcfrlem30.m |
. . . . . 6
β’ β =
(-gβπ·) |
58 | 54, 23, 57 | grpsubid1 18840 |
. . . . 5
β’ ((π· β Grp β§ (π½βπ) β (Baseβπ·)) β ((π½βπ) β
(0gβπ·)) =
(π½βπ)) |
59 | 53, 56, 58 | syl2anc 585 |
. . . 4
β’ (π β ((π½βπ) β
(0gβπ·)) =
(π½βπ)) |
60 | 52, 59 | eqtrd 2773 |
. . 3
β’ (π β ((π½βπ) β (((πΉβ((π½βπ)βπΌ))(.rβπ)((π½βπ)βπΌ))( Β·π
βπ·)(π½βπ))) = (π½βπ)) |
61 | 1, 60 | eqtrid 2785 |
. 2
β’ (π β πΆ = (π½βπ)) |
62 | 4, 14, 5, 15, 16, 17, 8, 18, 19, 20, 21, 22, 23, 24, 25, 6, 30 | lcfrlem13 40068 |
. . 3
β’ (π β (π½βπ) β ({π β (LFnlβπ) β£ ( β₯ β( β₯
β(πΏβπ))) = (πΏβπ)} β {(0gβπ·)})) |
63 | | eldifsni 4754 |
. . 3
β’ ((π½βπ) β ({π β (LFnlβπ) β£ ( β₯ β( β₯
β(πΏβπ))) = (πΏβπ)} β {(0gβπ·)}) β (π½βπ) β (0gβπ·)) |
64 | 62, 63 | syl 17 |
. 2
β’ (π β (π½βπ) β (0gβπ·)) |
65 | 61, 64 | eqnetrd 3008 |
1
β’ (π β πΆ β (0gβπ·)) |