Step | Hyp | Ref
| Expression |
1 | | baerlem3.w |
. . . . 5
β’ (π β π β LVec) |
2 | | lveclmod 20709 |
. . . . 5
β’ (π β LVec β π β LMod) |
3 | 1, 2 | syl 17 |
. . . 4
β’ (π β π β LMod) |
4 | | baerlem3.y |
. . . . 5
β’ (π β π β (π β { 0 })) |
5 | 4 | eldifad 3959 |
. . . 4
β’ (π β π β π) |
6 | | baerlem3.z |
. . . . 5
β’ (π β π β (π β { 0 })) |
7 | 6 | eldifad 3959 |
. . . 4
β’ (π β π β π) |
8 | | baerlem3.v |
. . . . 5
β’ π = (Baseβπ) |
9 | | baerlem3.p |
. . . . 5
β’ + =
(+gβπ) |
10 | | baerlem3.n |
. . . . 5
β’ π = (LSpanβπ) |
11 | | baerlem3.s |
. . . . 5
β’ β =
(LSSumβπ) |
12 | 8, 9, 10, 11 | lspsntri 20700 |
. . . 4
β’ ((π β LMod β§ π β π β§ π β π) β (πβ{(π + π)}) β ((πβ{π}) β (πβ{π}))) |
13 | 3, 5, 7, 12 | syl3anc 1371 |
. . 3
β’ (π β (πβ{(π + π)}) β ((πβ{π}) β (πβ{π}))) |
14 | | baerlem3.m |
. . . . . 6
β’ β =
(-gβπ) |
15 | | baerlem3.x |
. . . . . . 7
β’ (π β π β π) |
16 | 8, 9 | lmodvacl 20478 |
. . . . . . . 8
β’ ((π β LMod β§ π β π β§ π β π) β (π + π) β π) |
17 | 3, 5, 7, 16 | syl3anc 1371 |
. . . . . . 7
β’ (π β (π + π) β π) |
18 | 8, 14 | lmodvsubcl 20509 |
. . . . . . 7
β’ ((π β LMod β§ π β π β§ (π + π) β π) β (π β (π + π)) β π) |
19 | 3, 15, 17, 18 | syl3anc 1371 |
. . . . . 6
β’ (π β (π β (π + π)) β π) |
20 | 8, 14, 10, 3, 19, 15 | lspsnsub 20610 |
. . . . 5
β’ (π β (πβ{((π β (π + π)) β π)}) = (πβ{(π β (π β (π + π)))})) |
21 | | lmodabl 20511 |
. . . . . . . . 9
β’ (π β LMod β π β Abel) |
22 | 3, 21 | syl 17 |
. . . . . . . 8
β’ (π β π β Abel) |
23 | 8, 14, 22, 15, 17 | ablnncan 19682 |
. . . . . . 7
β’ (π β (π β (π β (π + π))) = (π + π)) |
24 | 23 | sneqd 4639 |
. . . . . 6
β’ (π β {(π β (π β (π + π)))} = {(π + π)}) |
25 | 24 | fveq2d 6892 |
. . . . 5
β’ (π β (πβ{(π β (π β (π + π)))}) = (πβ{(π + π)})) |
26 | 20, 25 | eqtrd 2772 |
. . . 4
β’ (π β (πβ{((π β (π + π)) β π)}) = (πβ{(π + π)})) |
27 | 8, 14, 11, 10 | lspsntrim 20701 |
. . . . 5
β’ ((π β LMod β§ (π β (π + π)) β π β§ π β π) β (πβ{((π β (π + π)) β π)}) β ((πβ{(π β (π + π))}) β (πβ{π}))) |
28 | 3, 19, 15, 27 | syl3anc 1371 |
. . . 4
β’ (π β (πβ{((π β (π + π)) β π)}) β ((πβ{(π β (π + π))}) β (πβ{π}))) |
29 | 26, 28 | eqsstrrd 4020 |
. . 3
β’ (π β (πβ{(π + π)}) β ((πβ{(π β (π + π))}) β (πβ{π}))) |
30 | 13, 29 | ssind 4231 |
. 2
β’ (π β (πβ{(π + π)}) β (((πβ{π}) β (πβ{π})) β© ((πβ{(π β (π + π))}) β (πβ{π})))) |
31 | | elin 3963 |
. . . . 5
β’ (π β (((πβ{π}) β (πβ{π})) β© ((πβ{(π β (π + π))}) β (πβ{π}))) β (π β ((πβ{π}) β (πβ{π})) β§ π β ((πβ{(π β (π + π))}) β (πβ{π})))) |
32 | | baerlem3.r |
. . . . . . 7
β’ π
= (Scalarβπ) |
33 | | baerlem3.b |
. . . . . . 7
β’ π΅ = (Baseβπ
) |
34 | | baerlem3.t |
. . . . . . 7
β’ Β· = (
Β·π βπ) |
35 | 8, 9, 32, 33, 34, 11, 10, 3, 5, 7 | lsmspsn 20687 |
. . . . . 6
β’ (π β (π β ((πβ{π}) β (πβ{π})) β βπ β π΅ βπ β π΅ π = ((π Β· π) + (π Β· π)))) |
36 | 8, 9, 32, 33, 34, 11, 10, 3, 19, 15 | lsmspsn 20687 |
. . . . . 6
β’ (π β (π β ((πβ{(π β (π + π))}) β (πβ{π})) β βπ β π΅ βπ β π΅ π = ((π Β· (π β (π + π))) + (π Β· π)))) |
37 | 35, 36 | anbi12d 631 |
. . . . 5
β’ (π β ((π β ((πβ{π}) β (πβ{π})) β§ π β ((πβ{(π β (π + π))}) β (πβ{π}))) β (βπ β π΅ βπ β π΅ π = ((π Β· π) + (π Β· π)) β§ βπ β π΅ βπ β π΅ π = ((π Β· (π β (π + π))) + (π Β· π))))) |
38 | 31, 37 | bitrid 282 |
. . . 4
β’ (π β (π β (((πβ{π}) β (πβ{π})) β© ((πβ{(π β (π + π))}) β (πβ{π}))) β (βπ β π΅ βπ β π΅ π = ((π Β· π) + (π Β· π)) β§ βπ β π΅ βπ β π΅ π = ((π Β· (π β (π + π))) + (π Β· π))))) |
39 | | baerlem3.o |
. . . . . . . . . . 11
β’ 0 =
(0gβπ) |
40 | | simp11 1203 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· π) + (π Β· π))) β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· (π β (π + π))) + (π Β· π))) β π) |
41 | 40, 1 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· π) + (π Β· π))) β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· (π β (π + π))) + (π Β· π))) β π β LVec) |
42 | 40, 15 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· π) + (π Β· π))) β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· (π β (π + π))) + (π Β· π))) β π β π) |
43 | | baerlem3.c |
. . . . . . . . . . . 12
β’ (π β Β¬ π β (πβ{π, π})) |
44 | 40, 43 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· π) + (π Β· π))) β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· (π β (π + π))) + (π Β· π))) β Β¬ π β (πβ{π, π})) |
45 | | baerlem3.d |
. . . . . . . . . . . 12
β’ (π β (πβ{π}) β (πβ{π})) |
46 | 40, 45 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· π) + (π Β· π))) β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· (π β (π + π))) + (π Β· π))) β (πβ{π}) β (πβ{π})) |
47 | 40, 4 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· π) + (π Β· π))) β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· (π β (π + π))) + (π Β· π))) β π β (π β { 0 })) |
48 | 40, 6 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· π) + (π Β· π))) β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· (π β (π + π))) + (π Β· π))) β π β (π β { 0 })) |
49 | | baerlem3.a |
. . . . . . . . . . 11
⒠⨣ =
(+gβπ
) |
50 | | baerlem3.l |
. . . . . . . . . . 11
β’ πΏ = (-gβπ
) |
51 | | baerlem3.q |
. . . . . . . . . . 11
β’ π = (0gβπ
) |
52 | | baerlem3.i |
. . . . . . . . . . 11
β’ πΌ = (invgβπ
) |
53 | | simp12l 1286 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· π) + (π Β· π))) β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· (π β (π + π))) + (π Β· π))) β π β π΅) |
54 | | simp12r 1287 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· π) + (π Β· π))) β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· (π β (π + π))) + (π Β· π))) β π β π΅) |
55 | | simp2l 1199 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· π) + (π Β· π))) β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· (π β (π + π))) + (π Β· π))) β π β π΅) |
56 | | simp2r 1200 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· π) + (π Β· π))) β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· (π β (π + π))) + (π Β· π))) β π β π΅) |
57 | | simp13 1205 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· π) + (π Β· π))) β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· (π β (π + π))) + (π Β· π))) β π = ((π Β· π) + (π Β· π))) |
58 | | simp3 1138 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· π) + (π Β· π))) β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· (π β (π + π))) + (π Β· π))) β π = ((π Β· (π β (π + π))) + (π Β· π))) |
59 | 8, 14, 39, 11, 10, 41, 42, 44, 46, 47, 48, 9, 34, 32, 33, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58 | baerlem5blem1 40568 |
. . . . . . . . . 10
β’ (((π β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· π) + (π Β· π))) β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· (π β (π + π))) + (π Β· π))) β π = ((πΌβπ) Β· (π + π))) |
60 | 40, 3 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· π) + (π Β· π))) β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· (π β (π + π))) + (π Β· π))) β π β LMod) |
61 | 32 | lmodring 20471 |
. . . . . . . . . . . . 13
β’ (π β LMod β π
β Ring) |
62 | | ringgrp 20054 |
. . . . . . . . . . . . 13
β’ (π
β Ring β π
β Grp) |
63 | 40, 3, 61, 62 | 4syl 19 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· π) + (π Β· π))) β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· (π β (π + π))) + (π Β· π))) β π
β Grp) |
64 | 33, 52 | grpinvcl 18868 |
. . . . . . . . . . . 12
β’ ((π
β Grp β§ π β π΅) β (πΌβπ) β π΅) |
65 | 63, 55, 64 | syl2anc 584 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· π) + (π Β· π))) β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· (π β (π + π))) + (π Β· π))) β (πΌβπ) β π΅) |
66 | 40, 17 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· π) + (π Β· π))) β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· (π β (π + π))) + (π Β· π))) β (π + π) β π) |
67 | 8, 34, 32, 33, 10, 60, 65, 66 | lspsneli 20604 |
. . . . . . . . . 10
β’ (((π β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· π) + (π Β· π))) β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· (π β (π + π))) + (π Β· π))) β ((πΌβπ) Β· (π + π)) β (πβ{(π + π)})) |
68 | 59, 67 | eqeltrd 2833 |
. . . . . . . . 9
β’ (((π β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· π) + (π Β· π))) β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· (π β (π + π))) + (π Β· π))) β π β (πβ{(π + π)})) |
69 | 68 | 3exp 1119 |
. . . . . . . 8
β’ ((π β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· π) + (π Β· π))) β ((π β π΅ β§ π β π΅) β (π = ((π Β· (π β (π + π))) + (π Β· π)) β π β (πβ{(π + π)})))) |
70 | 69 | rexlimdvv 3210 |
. . . . . . 7
β’ ((π β§ (π β π΅ β§ π β π΅) β§ π = ((π Β· π) + (π Β· π))) β (βπ β π΅ βπ β π΅ π = ((π Β· (π β (π + π))) + (π Β· π)) β π β (πβ{(π + π)}))) |
71 | 70 | 3exp 1119 |
. . . . . 6
β’ (π β ((π β π΅ β§ π β π΅) β (π = ((π Β· π) + (π Β· π)) β (βπ β π΅ βπ β π΅ π = ((π Β· (π β (π + π))) + (π Β· π)) β π β (πβ{(π + π)}))))) |
72 | 71 | rexlimdvv 3210 |
. . . . 5
β’ (π β (βπ β π΅ βπ β π΅ π = ((π Β· π) + (π Β· π)) β (βπ β π΅ βπ β π΅ π = ((π Β· (π β (π + π))) + (π Β· π)) β π β (πβ{(π + π)})))) |
73 | 72 | impd 411 |
. . . 4
β’ (π β ((βπ β π΅ βπ β π΅ π = ((π Β· π) + (π Β· π)) β§ βπ β π΅ βπ β π΅ π = ((π Β· (π β (π + π))) + (π Β· π))) β π β (πβ{(π + π)}))) |
74 | 38, 73 | sylbid 239 |
. . 3
β’ (π β (π β (((πβ{π}) β (πβ{π})) β© ((πβ{(π β (π + π))}) β (πβ{π}))) β π β (πβ{(π + π)}))) |
75 | 74 | ssrdv 3987 |
. 2
β’ (π β (((πβ{π}) β (πβ{π})) β© ((πβ{(π β (π + π))}) β (πβ{π}))) β (πβ{(π + π)})) |
76 | 30, 75 | eqssd 3998 |
1
β’ (π β (πβ{(π + π)}) = (((πβ{π}) β (πβ{π})) β© ((πβ{(π β (π + π))}) β (πβ{π})))) |