Step | Hyp | Ref
| Expression |
1 | | lcfrlem1.s |
. . . . . 6
β’ π = (Scalarβπ) |
2 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
3 | | lcfrlem1.f |
. . . . . 6
β’ πΉ = (LFnlβπ) |
4 | | lcfrlem2.l |
. . . . . 6
β’ πΏ = (LKerβπ) |
5 | | lcfrlem1.d |
. . . . . 6
β’ π· = (LDualβπ) |
6 | | lcfrlem1.t |
. . . . . 6
β’ Β· = (
Β·π βπ·) |
7 | | lcfrlem1.u |
. . . . . 6
β’ (π β π β LVec) |
8 | | lcfrlem1.g |
. . . . . 6
β’ (π β πΊ β πΉ) |
9 | | lveclmod 20611 |
. . . . . . . . 9
β’ (π β LVec β π β LMod) |
10 | 7, 9 | syl 17 |
. . . . . . . 8
β’ (π β π β LMod) |
11 | 1 | lmodring 20373 |
. . . . . . . 8
β’ (π β LMod β π β Ring) |
12 | 10, 11 | syl 17 |
. . . . . . 7
β’ (π β π β Ring) |
13 | 1 | lvecdrng 20610 |
. . . . . . . . 9
β’ (π β LVec β π β
DivRing) |
14 | 7, 13 | syl 17 |
. . . . . . . 8
β’ (π β π β DivRing) |
15 | | lcfrlem1.x |
. . . . . . . . 9
β’ (π β π β π) |
16 | | lcfrlem1.v |
. . . . . . . . . 10
β’ π = (Baseβπ) |
17 | 1, 2, 16, 3 | lflcl 37576 |
. . . . . . . . 9
β’ ((π β LVec β§ πΊ β πΉ β§ π β π) β (πΊβπ) β (Baseβπ)) |
18 | 7, 8, 15, 17 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (πΊβπ) β (Baseβπ)) |
19 | | lcfrlem1.n |
. . . . . . . 8
β’ (π β (πΊβπ) β 0 ) |
20 | | lcfrlem1.z |
. . . . . . . . 9
β’ 0 =
(0gβπ) |
21 | | lcfrlem1.i |
. . . . . . . . 9
β’ πΌ = (invrβπ) |
22 | 2, 20, 21 | drnginvrcl 20240 |
. . . . . . . 8
β’ ((π β DivRing β§ (πΊβπ) β (Baseβπ) β§ (πΊβπ) β 0 ) β (πΌβ(πΊβπ)) β (Baseβπ)) |
23 | 14, 18, 19, 22 | syl3anc 1372 |
. . . . . . 7
β’ (π β (πΌβ(πΊβπ)) β (Baseβπ)) |
24 | | lcfrlem1.e |
. . . . . . . 8
β’ (π β πΈ β πΉ) |
25 | 1, 2, 16, 3 | lflcl 37576 |
. . . . . . . 8
β’ ((π β LVec β§ πΈ β πΉ β§ π β π) β (πΈβπ) β (Baseβπ)) |
26 | 7, 24, 15, 25 | syl3anc 1372 |
. . . . . . 7
β’ (π β (πΈβπ) β (Baseβπ)) |
27 | | lcfrlem1.q |
. . . . . . . 8
β’ Γ =
(.rβπ) |
28 | 2, 27 | ringcl 19989 |
. . . . . . 7
β’ ((π β Ring β§ (πΌβ(πΊβπ)) β (Baseβπ) β§ (πΈβπ) β (Baseβπ)) β ((πΌβ(πΊβπ)) Γ (πΈβπ)) β (Baseβπ)) |
29 | 12, 23, 26, 28 | syl3anc 1372 |
. . . . . 6
β’ (π β ((πΌβ(πΊβπ)) Γ (πΈβπ)) β (Baseβπ)) |
30 | 1, 2, 3, 4, 5, 6, 7, 8, 29 | lkrss 37680 |
. . . . 5
β’ (π β (πΏβπΊ) β (πΏβ(((πΌβ(πΊβπ)) Γ (πΈβπ)) Β· πΊ))) |
31 | 3, 1, 2, 5, 6, 10,
29, 8 | ldualvscl 37651 |
. . . . . 6
β’ (π β (((πΌβ(πΊβπ)) Γ (πΈβπ)) Β· πΊ) β πΉ) |
32 | | ringgrp 19977 |
. . . . . . . 8
β’ (π β Ring β π β Grp) |
33 | 12, 32 | syl 17 |
. . . . . . 7
β’ (π β π β Grp) |
34 | | eqid 2733 |
. . . . . . . . 9
β’
(1rβπ) = (1rβπ) |
35 | 2, 34 | ringidcl 19997 |
. . . . . . . 8
β’ (π β Ring β
(1rβπ)
β (Baseβπ)) |
36 | 12, 35 | syl 17 |
. . . . . . 7
β’ (π β (1rβπ) β (Baseβπ)) |
37 | | eqid 2733 |
. . . . . . . 8
β’
(invgβπ) = (invgβπ) |
38 | 2, 37 | grpinvcl 18806 |
. . . . . . 7
β’ ((π β Grp β§
(1rβπ)
β (Baseβπ))
β ((invgβπ)β(1rβπ)) β (Baseβπ)) |
39 | 33, 36, 38 | syl2anc 585 |
. . . . . 6
β’ (π β
((invgβπ)β(1rβπ)) β (Baseβπ)) |
40 | 1, 2, 3, 4, 5, 6, 7, 31, 39 | lkrss 37680 |
. . . . 5
β’ (π β (πΏβ(((πΌβ(πΊβπ)) Γ (πΈβπ)) Β· πΊ)) β (πΏβ(((invgβπ)β(1rβπ)) Β· (((πΌβ(πΊβπ)) Γ (πΈβπ)) Β· πΊ)))) |
41 | 30, 40 | sstrd 3958 |
. . . 4
β’ (π β (πΏβπΊ) β (πΏβ(((invgβπ)β(1rβπ)) Β· (((πΌβ(πΊβπ)) Γ (πΈβπ)) Β· πΊ)))) |
42 | | sslin 4198 |
. . . 4
β’ ((πΏβπΊ) β (πΏβ(((invgβπ)β(1rβπ)) Β· (((πΌβ(πΊβπ)) Γ (πΈβπ)) Β· πΊ))) β ((πΏβπΈ) β© (πΏβπΊ)) β ((πΏβπΈ) β© (πΏβ(((invgβπ)β(1rβπ)) Β· (((πΌβ(πΊβπ)) Γ (πΈβπ)) Β· πΊ))))) |
43 | 41, 42 | syl 17 |
. . 3
β’ (π β ((πΏβπΈ) β© (πΏβπΊ)) β ((πΏβπΈ) β© (πΏβ(((invgβπ)β(1rβπ)) Β· (((πΌβ(πΊβπ)) Γ (πΈβπ)) Β· πΊ))))) |
44 | | eqid 2733 |
. . . 4
β’
(+gβπ·) = (+gβπ·) |
45 | 3, 1, 2, 5, 6, 10,
39, 31 | ldualvscl 37651 |
. . . 4
β’ (π β
(((invgβπ)β(1rβπ)) Β· (((πΌβ(πΊβπ)) Γ (πΈβπ)) Β· πΊ)) β πΉ) |
46 | 3, 4, 5, 44, 10, 24, 45 | lkrin 37676 |
. . 3
β’ (π β ((πΏβπΈ) β© (πΏβ(((invgβπ)β(1rβπ)) Β· (((πΌβ(πΊβπ)) Γ (πΈβπ)) Β· πΊ)))) β (πΏβ(πΈ(+gβπ·)(((invgβπ)β(1rβπ)) Β· (((πΌβ(πΊβπ)) Γ (πΈβπ)) Β· πΊ))))) |
47 | 43, 46 | sstrd 3958 |
. 2
β’ (π β ((πΏβπΈ) β© (πΏβπΊ)) β (πΏβ(πΈ(+gβπ·)(((invgβπ)β(1rβπ)) Β· (((πΌβ(πΊβπ)) Γ (πΈβπ)) Β· πΊ))))) |
48 | | lcfrlem1.h |
. . . 4
β’ π» = (πΈ β (((πΌβ(πΊβπ)) Γ (πΈβπ)) Β· πΊ)) |
49 | 48 | fveq2i 6849 |
. . 3
β’ (πΏβπ») = (πΏβ(πΈ β (((πΌβ(πΊβπ)) Γ (πΈβπ)) Β· πΊ))) |
50 | | lcfrlem1.m |
. . . . 5
β’ β =
(-gβπ·) |
51 | 1, 37, 34, 3, 5, 44, 6, 50, 10, 24, 31 | ldualvsub 37667 |
. . . 4
β’ (π β (πΈ β (((πΌβ(πΊβπ)) Γ (πΈβπ)) Β· πΊ)) = (πΈ(+gβπ·)(((invgβπ)β(1rβπ)) Β· (((πΌβ(πΊβπ)) Γ (πΈβπ)) Β· πΊ)))) |
52 | 51 | fveq2d 6850 |
. . 3
β’ (π β (πΏβ(πΈ β (((πΌβ(πΊβπ)) Γ (πΈβπ)) Β· πΊ))) = (πΏβ(πΈ(+gβπ·)(((invgβπ)β(1rβπ)) Β· (((πΌβ(πΊβπ)) Γ (πΈβπ)) Β· πΊ))))) |
53 | 49, 52 | eqtr2id 2786 |
. 2
β’ (π β (πΏβ(πΈ(+gβπ·)(((invgβπ)β(1rβπ)) Β· (((πΌβ(πΊβπ)) Γ (πΈβπ)) Β· πΊ)))) = (πΏβπ»)) |
54 | 47, 53 | sseqtrd 3988 |
1
β’ (π β ((πΏβπΈ) β© (πΏβπΊ)) β (πΏβπ»)) |