Step | Hyp | Ref
| Expression |
1 | | ccfldextrr 32377 |
. . 3
β’
βfld/FldExtβfld |
2 | | extdgval 32383 |
. . 3
β’
(βfld/FldExtβfld β
(βfld[:]βfld) = (dimβ((subringAlg
ββfld)β(Baseββfld)))) |
3 | 1, 2 | ax-mp 5 |
. 2
β’
(βfld[:]βfld) =
(dimβ((subringAlg
ββfld)β(Baseββfld))) |
4 | | rebase 21026 |
. . . 4
β’ β =
(Baseββfld) |
5 | 4 | fveq2i 6850 |
. . 3
β’
((subringAlg ββfld)ββ) = ((subringAlg
ββfld)β(Baseββfld)) |
6 | 5 | fveq2i 6850 |
. 2
β’
(dimβ((subringAlg ββfld)ββ)) =
(dimβ((subringAlg
ββfld)β(Baseββfld))) |
7 | | ccfldsrarelvec 32395 |
. . . 4
β’
((subringAlg ββfld)ββ) β
LVec |
8 | | df-pr 4594 |
. . . . . 6
β’ {1, i} =
({1} βͺ {i}) |
9 | | eqid 2737 |
. . . . . . . 8
β’
(LSpanβ((subringAlg ββfld)ββ))
= (LSpanβ((subringAlg
ββfld)ββ)) |
10 | | eqidd 2738 |
. . . . . . . . . 10
β’ (β€
β ((subringAlg ββfld)ββ) = ((subringAlg
ββfld)ββ)) |
11 | | cnfld0 20837 |
. . . . . . . . . . 11
β’ 0 =
(0gββfld) |
12 | 11 | a1i 11 |
. . . . . . . . . 10
β’ (β€
β 0 = (0gββfld)) |
13 | | ax-resscn 11115 |
. . . . . . . . . . . 12
β’ β
β β |
14 | | cnfldbas 20816 |
. . . . . . . . . . . 12
β’ β =
(Baseββfld) |
15 | 13, 14 | sseqtri 3985 |
. . . . . . . . . . 11
β’ β
β (Baseββfld) |
16 | 15 | a1i 11 |
. . . . . . . . . 10
β’ (β€
β β β (Baseββfld)) |
17 | 10, 12, 16 | sralmod0 20673 |
. . . . . . . . 9
β’ (β€
β 0 = (0gβ((subringAlg
ββfld)ββ))) |
18 | 17 | mptru 1549 |
. . . . . . . 8
β’ 0 =
(0gβ((subringAlg
ββfld)ββ)) |
19 | 7 | a1i 11 |
. . . . . . . 8
β’ (β€
β ((subringAlg ββfld)ββ) β
LVec) |
20 | | ax-1cn 11116 |
. . . . . . . . . 10
β’ 1 β
β |
21 | | ax-1ne0 11127 |
. . . . . . . . . 10
β’ 1 β
0 |
22 | 10, 16 | srabase 20656 |
. . . . . . . . . . . . 13
β’ (β€
β (Baseββfld) = (Baseβ((subringAlg
ββfld)ββ))) |
23 | 22 | mptru 1549 |
. . . . . . . . . . . 12
β’
(Baseββfld) = (Baseβ((subringAlg
ββfld)ββ)) |
24 | 14, 23 | eqtri 2765 |
. . . . . . . . . . 11
β’ β =
(Baseβ((subringAlg
ββfld)ββ)) |
25 | 24, 18 | lindssn 32206 |
. . . . . . . . . 10
β’
((((subringAlg ββfld)ββ) β LVec
β§ 1 β β β§ 1 β 0) β {1} β
(LIndSβ((subringAlg
ββfld)ββ))) |
26 | 7, 20, 21, 25 | mp3an 1462 |
. . . . . . . . 9
β’ {1}
β (LIndSβ((subringAlg
ββfld)ββ)) |
27 | 26 | a1i 11 |
. . . . . . . 8
β’ (β€
β {1} β (LIndSβ((subringAlg
ββfld)ββ))) |
28 | | ax-icn 11117 |
. . . . . . . . . 10
β’ i β
β |
29 | | ine0 11597 |
. . . . . . . . . 10
β’ i β
0 |
30 | 24, 18 | lindssn 32206 |
. . . . . . . . . 10
β’
((((subringAlg ββfld)ββ) β LVec
β§ i β β β§ i β 0) β {i} β
(LIndSβ((subringAlg
ββfld)ββ))) |
31 | 7, 28, 29, 30 | mp3an 1462 |
. . . . . . . . 9
β’ {i}
β (LIndSβ((subringAlg
ββfld)ββ)) |
32 | 31 | a1i 11 |
. . . . . . . 8
β’ (β€
β {i} β (LIndSβ((subringAlg
ββfld)ββ))) |
33 | | lveclmod 20583 |
. . . . . . . . . . . . . . 15
β’
(((subringAlg ββfld)ββ) β LVec
β ((subringAlg ββfld)ββ) β
LMod) |
34 | 7, 33 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’
((subringAlg ββfld)ββ) β
LMod |
35 | | df-refld 21025 |
. . . . . . . . . . . . . . . 16
β’
βfld = (βfld βΎs
β) |
36 | 10, 16 | srasca 20662 |
. . . . . . . . . . . . . . . . 17
β’ (β€
β (βfld βΎs β) =
(Scalarβ((subringAlg
ββfld)ββ))) |
37 | 36 | mptru 1549 |
. . . . . . . . . . . . . . . 16
β’
(βfld βΎs β) =
(Scalarβ((subringAlg
ββfld)ββ)) |
38 | 35, 37 | eqtri 2765 |
. . . . . . . . . . . . . . 15
β’
βfld = (Scalarβ((subringAlg
ββfld)ββ)) |
39 | | cnfldmul 20818 |
. . . . . . . . . . . . . . . 16
β’ Β·
= (.rββfld) |
40 | 10, 16 | sravsca 20664 |
. . . . . . . . . . . . . . . . 17
β’ (β€
β (.rββfld) = (
Β·π β((subringAlg
ββfld)ββ))) |
41 | 40 | mptru 1549 |
. . . . . . . . . . . . . . . 16
β’
(.rββfld) = (
Β·π β((subringAlg
ββfld)ββ)) |
42 | 39, 41 | eqtri 2765 |
. . . . . . . . . . . . . . 15
β’ Β·
= ( Β·π β((subringAlg
ββfld)ββ)) |
43 | 38, 4, 24, 42, 9 | lspsnel 20480 |
. . . . . . . . . . . . . 14
β’
((((subringAlg ββfld)ββ) β LMod
β§ 1 β β) β (π§ β ((LSpanβ((subringAlg
ββfld)ββ))β{1}) β βπ₯ β β π§ = (π₯ Β· 1))) |
44 | 34, 20, 43 | mp2an 691 |
. . . . . . . . . . . . 13
β’ (π§ β
((LSpanβ((subringAlg
ββfld)ββ))β{1}) β βπ₯ β β π§ = (π₯ Β· 1)) |
45 | 38, 4, 24, 42, 9 | lspsnel 20480 |
. . . . . . . . . . . . . 14
β’
((((subringAlg ββfld)ββ) β LMod
β§ i β β) β (π§ β ((LSpanβ((subringAlg
ββfld)ββ))β{i}) β βπ¦ β β π§ = (π¦ Β· i))) |
46 | 34, 28, 45 | mp2an 691 |
. . . . . . . . . . . . 13
β’ (π§ β
((LSpanβ((subringAlg
ββfld)ββ))β{i}) β βπ¦ β β π§ = (π¦ Β· i)) |
47 | 44, 46 | anbi12i 628 |
. . . . . . . . . . . 12
β’ ((π§ β
((LSpanβ((subringAlg
ββfld)ββ))β{1}) β§ π§ β
((LSpanβ((subringAlg
ββfld)ββ))β{i})) β (βπ₯ β β π§ = (π₯ Β· 1) β§ βπ¦ β β π§ = (π¦ Β· i))) |
48 | | reeanv 3220 |
. . . . . . . . . . . 12
β’
(βπ₯ β
β βπ¦ β
β (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i)) β (βπ₯ β β π§ = (π₯ Β· 1) β§ βπ¦ β β π§ = (π¦ Β· i))) |
49 | | simprl 770 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β β β§ π¦ β β) β§ (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i))) β π§ = (π₯ Β· 1)) |
50 | | simpll 766 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π₯ β β β§ π¦ β β) β§ (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i))) β π₯ β β) |
51 | 50 | recnd 11190 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ β β β§ π¦ β β) β§ (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i))) β π₯ β β) |
52 | 51 | mulid1d 11179 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β β β§ π¦ β β) β§ (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i))) β (π₯ Β· 1) = π₯) |
53 | 49, 52 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β β β§ π¦ β β) β§ (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i))) β π§ = π₯) |
54 | 53 | negeqd 11402 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π₯ β β β§ π¦ β β) β§ (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i))) β -π§ = -π₯) |
55 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π₯ β β β§ π¦ β β) β§ (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i))) β π§ = (π¦ Β· i)) |
56 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π₯ β β β§ π¦ β β) β§ (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i))) β π¦ β β) |
57 | 56 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π₯ β β β§ π¦ β β) β§ (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i))) β π¦ β β) |
58 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π₯ β β β§ π¦ β β) β§ (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i))) β i β
β) |
59 | 57, 58 | mulcomd 11183 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π₯ β β β§ π¦ β β) β§ (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i))) β (π¦ Β· i) = (i Β· π¦)) |
60 | 55, 59 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π₯ β β β§ π¦ β β) β§ (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i))) β π§ = (i Β· π¦)) |
61 | 54, 60 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π₯ β β β§ π¦ β β) β§ (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i))) β (-π§ + π§) = (-π₯ + (i Β· π¦))) |
62 | 53, 51 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π₯ β β β§ π¦ β β) β§ (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i))) β π§ β β) |
63 | 62 | subidd 11507 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π₯ β β β§ π¦ β β) β§ (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i))) β (π§ β π§) = 0) |
64 | 63 | negeqd 11402 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π₯ β β β§ π¦ β β) β§ (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i))) β -(π§ β π§) = -0) |
65 | 62, 62 | negsubdid 11534 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π₯ β β β§ π¦ β β) β§ (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i))) β -(π§ β π§) = (-π§ + π§)) |
66 | | neg0 11454 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ -0 =
0 |
67 | 66 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π₯ β β β§ π¦ β β) β§ (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i))) β -0 =
0) |
68 | 64, 65, 67 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π₯ β β β§ π¦ β β) β§ (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i))) β (-π§ + π§) = 0) |
69 | 61, 68 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π₯ β β β§ π¦ β β) β§ (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i))) β (-π₯ + (i Β· π¦)) = 0) |
70 | 50 | renegcld 11589 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π₯ β β β§ π¦ β β) β§ (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i))) β -π₯ β β) |
71 | | creq0 31694 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((-π₯ β β β§ π¦ β β) β ((-π₯ = 0 β§ π¦ = 0) β (-π₯ + (i Β· π¦)) = 0)) |
72 | 70, 56, 71 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π₯ β β β§ π¦ β β) β§ (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i))) β ((-π₯ = 0 β§ π¦ = 0) β (-π₯ + (i Β· π¦)) = 0)) |
73 | 69, 72 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ β β β§ π¦ β β) β§ (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i))) β (-π₯ = 0 β§ π¦ = 0)) |
74 | 73 | simpld 496 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β β β§ π¦ β β) β§ (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i))) β -π₯ = 0) |
75 | 51, 74 | negcon1ad 11514 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β β β§ π¦ β β) β§ (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i))) β -0 = π₯) |
76 | 53, 75, 67 | 3eqtr2d 2783 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β β§ π¦ β β) β§ (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i))) β π§ = 0) |
77 | 76 | ex 414 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β β§ π¦ β β) β ((π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i)) β π§ = 0)) |
78 | 77 | rexlimivv 3197 |
. . . . . . . . . . . . 13
β’
(βπ₯ β
β βπ¦ β
β (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i)) β π§ = 0) |
79 | | 0red 11165 |
. . . . . . . . . . . . . 14
β’ (π§ = 0 β 0 β
β) |
80 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ ((π§ = 0 β§ π₯ = 0) β π₯ = 0) |
81 | 80 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
β’ ((π§ = 0 β§ π₯ = 0) β (π₯ Β· 1) = (0 Β·
1)) |
82 | 81 | eqeq2d 2748 |
. . . . . . . . . . . . . . . 16
β’ ((π§ = 0 β§ π₯ = 0) β (π§ = (π₯ Β· 1) β π§ = (0 Β· 1))) |
83 | 82 | anbi1d 631 |
. . . . . . . . . . . . . . 15
β’ ((π§ = 0 β§ π₯ = 0) β ((π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i)) β (π§ = (0 Β· 1) β§ π§ = (π¦ Β· i)))) |
84 | 83 | rexbidv 3176 |
. . . . . . . . . . . . . 14
β’ ((π§ = 0 β§ π₯ = 0) β (βπ¦ β β (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i)) β βπ¦ β β (π§ = (0 Β· 1) β§ π§ = (π¦ Β· i)))) |
85 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ ((π§ = 0 β§ π¦ = 0) β π¦ = 0) |
86 | 85 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
β’ ((π§ = 0 β§ π¦ = 0) β (π¦ Β· i) = (0 Β·
i)) |
87 | 86 | eqeq2d 2748 |
. . . . . . . . . . . . . . . 16
β’ ((π§ = 0 β§ π¦ = 0) β (π§ = (π¦ Β· i) β π§ = (0 Β· i))) |
88 | 87 | anbi2d 630 |
. . . . . . . . . . . . . . 15
β’ ((π§ = 0 β§ π¦ = 0) β ((π§ = (0 Β· 1) β§ π§ = (π¦ Β· i)) β (π§ = (0 Β· 1) β§ π§ = (0 Β· i)))) |
89 | 20 | mul02i 11351 |
. . . . . . . . . . . . . . . . . 18
β’ (0
Β· 1) = 0 |
90 | 89 | eqeq2i 2750 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = (0 Β· 1) β π§ = 0) |
91 | 90 | biimpri 227 |
. . . . . . . . . . . . . . . 16
β’ (π§ = 0 β π§ = (0 Β· 1)) |
92 | 28 | mul02i 11351 |
. . . . . . . . . . . . . . . . . 18
β’ (0
Β· i) = 0 |
93 | 92 | eqeq2i 2750 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = (0 Β· i) β π§ = 0) |
94 | 93 | biimpri 227 |
. . . . . . . . . . . . . . . 16
β’ (π§ = 0 β π§ = (0 Β· i)) |
95 | 91, 94 | jca 513 |
. . . . . . . . . . . . . . 15
β’ (π§ = 0 β (π§ = (0 Β· 1) β§ π§ = (0 Β· i))) |
96 | 79, 88, 95 | rspcedvd 3586 |
. . . . . . . . . . . . . 14
β’ (π§ = 0 β βπ¦ β β (π§ = (0 Β· 1) β§ π§ = (π¦ Β· i))) |
97 | 79, 84, 96 | rspcedvd 3586 |
. . . . . . . . . . . . 13
β’ (π§ = 0 β βπ₯ β β βπ¦ β β (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i))) |
98 | 78, 97 | impbii 208 |
. . . . . . . . . . . 12
β’
(βπ₯ β
β βπ¦ β
β (π§ = (π₯ Β· 1) β§ π§ = (π¦ Β· i)) β π§ = 0) |
99 | 47, 48, 98 | 3bitr2i 299 |
. . . . . . . . . . 11
β’ ((π§ β
((LSpanβ((subringAlg
ββfld)ββ))β{1}) β§ π§ β
((LSpanβ((subringAlg
ββfld)ββ))β{i})) β π§ = 0) |
100 | | elin 3931 |
. . . . . . . . . . 11
β’ (π§ β
(((LSpanβ((subringAlg
ββfld)ββ))β{1}) β©
((LSpanβ((subringAlg
ββfld)ββ))β{i})) β (π§ β
((LSpanβ((subringAlg
ββfld)ββ))β{1}) β§ π§ β
((LSpanβ((subringAlg
ββfld)ββ))β{i}))) |
101 | | velsn 4607 |
. . . . . . . . . . 11
β’ (π§ β {0} β π§ = 0) |
102 | 99, 100, 101 | 3bitr4i 303 |
. . . . . . . . . 10
β’ (π§ β
(((LSpanβ((subringAlg
ββfld)ββ))β{1}) β©
((LSpanβ((subringAlg
ββfld)ββ))β{i})) β π§ β {0}) |
103 | 102 | eqriv 2734 |
. . . . . . . . 9
β’
(((LSpanβ((subringAlg
ββfld)ββ))β{1}) β©
((LSpanβ((subringAlg
ββfld)ββ))β{i})) =
{0} |
104 | 103 | a1i 11 |
. . . . . . . 8
β’ (β€
β (((LSpanβ((subringAlg
ββfld)ββ))β{1}) β©
((LSpanβ((subringAlg
ββfld)ββ))β{i})) =
{0}) |
105 | 9, 18, 19, 27, 32, 104 | lindsun 32360 |
. . . . . . 7
β’ (β€
β ({1} βͺ {i}) β (LIndSβ((subringAlg
ββfld)ββ))) |
106 | 105 | mptru 1549 |
. . . . . 6
β’ ({1}
βͺ {i}) β (LIndSβ((subringAlg
ββfld)ββ)) |
107 | 8, 106 | eqeltri 2834 |
. . . . 5
β’ {1, i}
β (LIndSβ((subringAlg
ββfld)ββ)) |
108 | | cnfldadd 20817 |
. . . . . . . . . 10
β’ + =
(+gββfld) |
109 | 10, 16 | sraaddg 20658 |
. . . . . . . . . . 11
β’ (β€
β (+gββfld) =
(+gβ((subringAlg
ββfld)ββ))) |
110 | 109 | mptru 1549 |
. . . . . . . . . 10
β’
(+gββfld) =
(+gβ((subringAlg
ββfld)ββ)) |
111 | 108, 110 | eqtri 2765 |
. . . . . . . . 9
β’ + =
(+gβ((subringAlg
ββfld)ββ)) |
112 | 34 | a1i 11 |
. . . . . . . . 9
β’ (β€
β ((subringAlg ββfld)ββ) β
LMod) |
113 | | 1cnd 11157 |
. . . . . . . . 9
β’ (β€
β 1 β β) |
114 | 28 | a1i 11 |
. . . . . . . . 9
β’ (β€
β i β β) |
115 | 24, 111, 38, 4, 42, 9, 112, 113, 114 | lspprel 20571 |
. . . . . . . 8
β’ (β€
β (π§ β
((LSpanβ((subringAlg
ββfld)ββ))β{1, i}) β βπ₯ β β βπ¦ β β π§ = ((π₯ Β· 1) + (π¦ Β· i)))) |
116 | 115 | mptru 1549 |
. . . . . . 7
β’ (π§ β
((LSpanβ((subringAlg
ββfld)ββ))β{1, i}) β βπ₯ β β βπ¦ β β π§ = ((π₯ Β· 1) + (π¦ Β· i))) |
117 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((π₯ β β β§ π¦ β β) β π₯ β
β) |
118 | 117 | recnd 11190 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ π¦ β β) β π₯ β
β) |
119 | | 1cnd 11157 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ π¦ β β) β 1 β
β) |
120 | 118, 119 | mulcld 11182 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ π¦ β β) β (π₯ Β· 1) β
β) |
121 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π₯ β β β§ π¦ β β) β π¦ β
β) |
122 | 121 | recnd 11190 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ π¦ β β) β π¦ β
β) |
123 | 28 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ π¦ β β) β i β
β) |
124 | 122, 123 | mulcld 11182 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ π¦ β β) β (π¦ Β· i) β
β) |
125 | 120, 124 | addcld 11181 |
. . . . . . . . . 10
β’ ((π₯ β β β§ π¦ β β) β ((π₯ Β· 1) + (π¦ Β· i)) β
β) |
126 | | eleq1 2826 |
. . . . . . . . . 10
β’ (π§ = ((π₯ Β· 1) + (π¦ Β· i)) β (π§ β β β ((π₯ Β· 1) + (π¦ Β· i)) β
β)) |
127 | 125, 126 | syl5ibrcom 247 |
. . . . . . . . 9
β’ ((π₯ β β β§ π¦ β β) β (π§ = ((π₯ Β· 1) + (π¦ Β· i)) β π§ β β)) |
128 | 127 | rexlimivv 3197 |
. . . . . . . 8
β’
(βπ₯ β
β βπ¦ β
β π§ = ((π₯ Β· 1) + (π¦ Β· i)) β π§ β
β) |
129 | | recl 15002 |
. . . . . . . . 9
β’ (π§ β β β
(ββπ§) β
β) |
130 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π§ β β β§ π₯ = (ββπ§)) β π₯ = (ββπ§)) |
131 | 130 | oveq1d 7377 |
. . . . . . . . . . . 12
β’ ((π§ β β β§ π₯ = (ββπ§)) β (π₯ Β· 1) = ((ββπ§) Β· 1)) |
132 | 131 | oveq1d 7377 |
. . . . . . . . . . 11
β’ ((π§ β β β§ π₯ = (ββπ§)) β ((π₯ Β· 1) + (π¦ Β· i)) = (((ββπ§) Β· 1) + (π¦ Β· i))) |
133 | 132 | eqeq2d 2748 |
. . . . . . . . . 10
β’ ((π§ β β β§ π₯ = (ββπ§)) β (π§ = ((π₯ Β· 1) + (π¦ Β· i)) β π§ = (((ββπ§) Β· 1) + (π¦ Β· i)))) |
134 | 133 | rexbidv 3176 |
. . . . . . . . 9
β’ ((π§ β β β§ π₯ = (ββπ§)) β (βπ¦ β β π§ = ((π₯ Β· 1) + (π¦ Β· i)) β βπ¦ β β π§ = (((ββπ§) Β· 1) + (π¦ Β· i)))) |
135 | | imcl 15003 |
. . . . . . . . . 10
β’ (π§ β β β
(ββπ§) β
β) |
136 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π§ β β β§ π¦ = (ββπ§)) β π¦ = (ββπ§)) |
137 | 136 | oveq1d 7377 |
. . . . . . . . . . . 12
β’ ((π§ β β β§ π¦ = (ββπ§)) β (π¦ Β· i) = ((ββπ§) Β· i)) |
138 | 137 | oveq2d 7378 |
. . . . . . . . . . 11
β’ ((π§ β β β§ π¦ = (ββπ§)) β (((ββπ§) Β· 1) + (π¦ Β· i)) =
(((ββπ§) Β·
1) + ((ββπ§)
Β· i))) |
139 | 138 | eqeq2d 2748 |
. . . . . . . . . 10
β’ ((π§ β β β§ π¦ = (ββπ§)) β (π§ = (((ββπ§) Β· 1) + (π¦ Β· i)) β π§ = (((ββπ§) Β· 1) + ((ββπ§) Β·
i)))) |
140 | | replim 15008 |
. . . . . . . . . . 11
β’ (π§ β β β π§ = ((ββπ§) + (i Β·
(ββπ§)))) |
141 | 129 | recnd 11190 |
. . . . . . . . . . . . 13
β’ (π§ β β β
(ββπ§) β
β) |
142 | 141 | mulid1d 11179 |
. . . . . . . . . . . 12
β’ (π§ β β β
((ββπ§) Β·
1) = (ββπ§)) |
143 | 135 | recnd 11190 |
. . . . . . . . . . . . 13
β’ (π§ β β β
(ββπ§) β
β) |
144 | 28 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π§ β β β i β
β) |
145 | 143, 144 | mulcomd 11183 |
. . . . . . . . . . . 12
β’ (π§ β β β
((ββπ§) Β·
i) = (i Β· (ββπ§))) |
146 | 142, 145 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (π§ β β β
(((ββπ§) Β·
1) + ((ββπ§)
Β· i)) = ((ββπ§) + (i Β· (ββπ§)))) |
147 | 140, 146 | eqtr4d 2780 |
. . . . . . . . . 10
β’ (π§ β β β π§ = (((ββπ§) Β· 1) +
((ββπ§) Β·
i))) |
148 | 135, 139,
147 | rspcedvd 3586 |
. . . . . . . . 9
β’ (π§ β β β
βπ¦ β β
π§ = (((ββπ§) Β· 1) + (π¦ Β· i))) |
149 | 129, 134,
148 | rspcedvd 3586 |
. . . . . . . 8
β’ (π§ β β β
βπ₯ β β
βπ¦ β β
π§ = ((π₯ Β· 1) + (π¦ Β· i))) |
150 | 128, 149 | impbii 208 |
. . . . . . 7
β’
(βπ₯ β
β βπ¦ β
β π§ = ((π₯ Β· 1) + (π¦ Β· i)) β π§ β
β) |
151 | 116, 150 | bitri 275 |
. . . . . 6
β’ (π§ β
((LSpanβ((subringAlg
ββfld)ββ))β{1, i}) β π§ β
β) |
152 | 151 | eqriv 2734 |
. . . . 5
β’
((LSpanβ((subringAlg
ββfld)ββ))β{1, i}) =
β |
153 | | eqid 2737 |
. . . . . 6
β’
(LBasisβ((subringAlg ββfld)ββ))
= (LBasisβ((subringAlg
ββfld)ββ)) |
154 | 24, 153, 9 | islbs4 21254 |
. . . . 5
β’ ({1, i}
β (LBasisβ((subringAlg ββfld)ββ))
β ({1, i} β (LIndSβ((subringAlg
ββfld)ββ)) β§ ((LSpanβ((subringAlg
ββfld)ββ))β{1, i}) =
β)) |
155 | 107, 152,
154 | mpbir2an 710 |
. . . 4
β’ {1, i}
β (LBasisβ((subringAlg
ββfld)ββ)) |
156 | 153 | dimval 32340 |
. . . 4
β’
((((subringAlg ββfld)ββ) β LVec
β§ {1, i} β (LBasisβ((subringAlg
ββfld)ββ))) β (dimβ((subringAlg
ββfld)ββ)) = (β―β{1,
i})) |
157 | 7, 155, 156 | mp2an 691 |
. . 3
β’
(dimβ((subringAlg ββfld)ββ)) =
(β―β{1, i}) |
158 | | 1nei 31695 |
. . . 4
β’ 1 β
i |
159 | | hashprg 14302 |
. . . . 5
β’ ((1
β β β§ i β β) β (1 β i β
(β―β{1, i}) = 2)) |
160 | 20, 28, 159 | mp2an 691 |
. . . 4
β’ (1 β i
β (β―β{1, i}) = 2) |
161 | 158, 160 | mpbi 229 |
. . 3
β’
(β―β{1, i}) = 2 |
162 | 157, 161 | eqtri 2765 |
. 2
β’
(dimβ((subringAlg ββfld)ββ)) =
2 |
163 | 3, 6, 162 | 3eqtr2i 2771 |
1
β’
(βfld[:]βfld) = 2 |