Step | Hyp | Ref
| Expression |
1 | | isfld 20230 |
. . . . 5
β’ (πΉ β Field β (πΉ β DivRing β§ πΉ β CRing)) |
2 | 1 | simplbi 499 |
. . . 4
β’ (πΉ β Field β πΉ β
DivRing) |
3 | | eqid 2733 |
. . . . . 6
β’
(BaseβπΉ) =
(BaseβπΉ) |
4 | 3 | ressid 17133 |
. . . . 5
β’ (πΉ β Field β (πΉ βΎs
(BaseβπΉ)) = πΉ) |
5 | 4, 2 | eqeltrd 2834 |
. . . 4
β’ (πΉ β Field β (πΉ βΎs
(BaseβπΉ)) β
DivRing) |
6 | | drngring 20226 |
. . . . 5
β’ (πΉ β DivRing β πΉ β Ring) |
7 | 3 | subrgid 20266 |
. . . . 5
β’ (πΉ β Ring β
(BaseβπΉ) β
(SubRingβπΉ)) |
8 | 2, 6, 7 | 3syl 18 |
. . . 4
β’ (πΉ β Field β
(BaseβπΉ) β
(SubRingβπΉ)) |
9 | | rgmoddim.1 |
. . . . . 6
β’ π = (ringLModβπΉ) |
10 | | rlmval 20705 |
. . . . . 6
β’
(ringLModβπΉ) =
((subringAlg βπΉ)β(BaseβπΉ)) |
11 | 9, 10 | eqtri 2761 |
. . . . 5
β’ π = ((subringAlg βπΉ)β(BaseβπΉ)) |
12 | | eqid 2733 |
. . . . 5
β’ (πΉ βΎs
(BaseβπΉ)) = (πΉ βΎs
(BaseβπΉ)) |
13 | 11, 12 | sralvec 32351 |
. . . 4
β’ ((πΉ β DivRing β§ (πΉ βΎs
(BaseβπΉ)) β
DivRing β§ (BaseβπΉ) β (SubRingβπΉ)) β π β LVec) |
14 | 2, 5, 8, 13 | syl3anc 1372 |
. . 3
β’ (πΉ β Field β π β LVec) |
15 | 2, 6 | syl 17 |
. . . . . . 7
β’ (πΉ β Field β πΉ β Ring) |
16 | | ssidd 3971 |
. . . . . . 7
β’ (πΉ β Field β
(BaseβπΉ) β
(BaseβπΉ)) |
17 | 11, 3 | sraring 32348 |
. . . . . . 7
β’ ((πΉ β Ring β§
(BaseβπΉ) β
(BaseβπΉ)) β
π β
Ring) |
18 | 15, 16, 17 | syl2anc 585 |
. . . . . 6
β’ (πΉ β Field β π β Ring) |
19 | | eqid 2733 |
. . . . . . 7
β’
(Baseβπ) =
(Baseβπ) |
20 | | eqid 2733 |
. . . . . . 7
β’
(1rβπ) = (1rβπ) |
21 | 19, 20 | ringidcl 19997 |
. . . . . 6
β’ (π β Ring β
(1rβπ)
β (Baseβπ)) |
22 | 18, 21 | syl 17 |
. . . . 5
β’ (πΉ β Field β
(1rβπ)
β (Baseβπ)) |
23 | 11, 3 | sradrng 32349 |
. . . . . . 7
β’ ((πΉ β DivRing β§
(BaseβπΉ) β
(BaseβπΉ)) β
π β
DivRing) |
24 | 2, 16, 23 | syl2anc 585 |
. . . . . 6
β’ (πΉ β Field β π β
DivRing) |
25 | | eqid 2733 |
. . . . . . 7
β’
(0gβπ) = (0gβπ) |
26 | 25, 20 | drngunz 20237 |
. . . . . 6
β’ (π β DivRing β
(1rβπ)
β (0gβπ)) |
27 | 24, 26 | syl 17 |
. . . . 5
β’ (πΉ β Field β
(1rβπ)
β (0gβπ)) |
28 | 19, 25 | lindssn 32220 |
. . . . 5
β’ ((π β LVec β§
(1rβπ)
β (Baseβπ) β§
(1rβπ)
β (0gβπ)) β {(1rβπ)} β (LIndSβπ)) |
29 | 14, 22, 27, 28 | syl3anc 1372 |
. . . 4
β’ (πΉ β Field β
{(1rβπ)}
β (LIndSβπ)) |
30 | | rspval 20707 |
. . . . . . . . 9
β’
(RSpanβπΉ) =
(LSpanβ(ringLModβπΉ)) |
31 | 9 | fveq2i 6849 |
. . . . . . . . 9
β’
(LSpanβπ) =
(LSpanβ(ringLModβπΉ)) |
32 | 30, 31 | eqtr4i 2764 |
. . . . . . . 8
β’
(RSpanβπΉ) =
(LSpanβπ) |
33 | 32 | fveq1i 6847 |
. . . . . . 7
β’
((RSpanβπΉ)β{(1rβπΉ)}) = ((LSpanβπ)β{(1rβπΉ)}) |
34 | | eqid 2733 |
. . . . . . . 8
β’
(RSpanβπΉ) =
(RSpanβπΉ) |
35 | | eqid 2733 |
. . . . . . . 8
β’
(1rβπΉ) = (1rβπΉ) |
36 | 34, 3, 35 | rsp1 20739 |
. . . . . . 7
β’ (πΉ β Ring β
((RSpanβπΉ)β{(1rβπΉ)}) = (BaseβπΉ)) |
37 | 33, 36 | eqtr3id 2787 |
. . . . . 6
β’ (πΉ β Ring β
((LSpanβπ)β{(1rβπΉ)}) = (BaseβπΉ)) |
38 | 2, 6, 37 | 3syl 18 |
. . . . 5
β’ (πΉ β Field β
((LSpanβπ)β{(1rβπΉ)}) = (BaseβπΉ)) |
39 | 11 | a1i 11 |
. . . . . . . 8
β’ (πΉ β Field β π = ((subringAlg βπΉ)β(BaseβπΉ))) |
40 | | eqidd 2734 |
. . . . . . . 8
β’ (πΉ β Field β
(1rβπΉ) =
(1rβπΉ)) |
41 | 39, 40, 16 | sra1r 32347 |
. . . . . . 7
β’ (πΉ β Field β
(1rβπΉ) =
(1rβπ)) |
42 | 41 | sneqd 4602 |
. . . . . 6
β’ (πΉ β Field β
{(1rβπΉ)} =
{(1rβπ)}) |
43 | 42 | fveq2d 6850 |
. . . . 5
β’ (πΉ β Field β
((LSpanβπ)β{(1rβπΉ)}) = ((LSpanβπ)β{(1rβπ)})) |
44 | 39, 16 | srabase 20685 |
. . . . 5
β’ (πΉ β Field β
(BaseβπΉ) =
(Baseβπ)) |
45 | 38, 43, 44 | 3eqtr3d 2781 |
. . . 4
β’ (πΉ β Field β
((LSpanβπ)β{(1rβπ)}) = (Baseβπ)) |
46 | | eqid 2733 |
. . . . 5
β’
(LBasisβπ) =
(LBasisβπ) |
47 | | eqid 2733 |
. . . . 5
β’
(LSpanβπ) =
(LSpanβπ) |
48 | 19, 46, 47 | islbs4 21261 |
. . . 4
β’
({(1rβπ)} β (LBasisβπ) β ({(1rβπ)} β (LIndSβπ) β§ ((LSpanβπ)β{(1rβπ)}) = (Baseβπ))) |
49 | 29, 45, 48 | sylanbrc 584 |
. . 3
β’ (πΉ β Field β
{(1rβπ)}
β (LBasisβπ)) |
50 | 46 | dimval 32362 |
. . 3
β’ ((π β LVec β§
{(1rβπ)}
β (LBasisβπ))
β (dimβπ) =
(β―β{(1rβπ)})) |
51 | 14, 49, 50 | syl2anc 585 |
. 2
β’ (πΉ β Field β
(dimβπ) =
(β―β{(1rβπ)})) |
52 | | fvex 6859 |
. . 3
β’
(1rβπ) β V |
53 | | hashsng 14278 |
. . 3
β’
((1rβπ) β V β
(β―β{(1rβπ)}) = 1) |
54 | 52, 53 | ax-mp 5 |
. 2
β’
(β―β{(1rβπ)}) = 1 |
55 | 51, 54 | eqtrdi 2789 |
1
β’ (πΉ β Field β
(dimβπ) =
1) |