Step | Hyp | Ref
| Expression |
1 | | baerlem5a.j1 |
. . 3
β’ (π β π = ((π Β· (π β π)) + (π Β· π))) |
2 | | baerlem3.v |
. . . . . 6
β’ π = (Baseβπ) |
3 | | baerlem3.t |
. . . . . 6
β’ Β· = (
Β·π βπ) |
4 | | baerlem3.r |
. . . . . 6
β’ π
= (Scalarβπ) |
5 | | baerlem3.b |
. . . . . 6
β’ π΅ = (Baseβπ
) |
6 | | baerlem3.m |
. . . . . 6
β’ β =
(-gβπ) |
7 | | baerlem3.w |
. . . . . . 7
β’ (π β π β LVec) |
8 | | lveclmod 20582 |
. . . . . . 7
β’ (π β LVec β π β LMod) |
9 | 7, 8 | syl 17 |
. . . . . 6
β’ (π β π β LMod) |
10 | | baerlem5a.a1 |
. . . . . 6
β’ (π β π β π΅) |
11 | | baerlem3.x |
. . . . . 6
β’ (π β π β π) |
12 | | baerlem3.y |
. . . . . . 7
β’ (π β π β (π β { 0 })) |
13 | 12 | eldifad 3923 |
. . . . . 6
β’ (π β π β π) |
14 | 2, 3, 4, 5, 6, 9, 10, 11, 13 | lmodsubdi 20394 |
. . . . 5
β’ (π β (π Β· (π β π)) = ((π Β· π) β (π Β· π))) |
15 | | baerlem3.p |
. . . . . 6
β’ + =
(+gβπ) |
16 | | baerlem3.i |
. . . . . 6
β’ πΌ = (invgβπ
) |
17 | 2, 4, 3, 5 | lmodvscl 20354 |
. . . . . . 7
β’ ((π β LMod β§ π β π΅ β§ π β π) β (π Β· π) β π) |
18 | 9, 10, 11, 17 | syl3anc 1372 |
. . . . . 6
β’ (π β (π Β· π) β π) |
19 | 2, 15, 6, 3, 4, 5, 16, 9, 10, 18, 13 | lmodsubvs 20393 |
. . . . 5
β’ (π β ((π Β· π) β (π Β· π)) = ((π Β· π) + ((πΌβπ) Β· π))) |
20 | 14, 19 | eqtrd 2773 |
. . . 4
β’ (π β (π Β· (π β π)) = ((π Β· π) + ((πΌβπ) Β· π))) |
21 | 20 | oveq1d 7373 |
. . 3
β’ (π β ((π Β· (π β π)) + (π Β· π)) = (((π Β· π) + ((πΌβπ) Β· π)) + (π Β· π))) |
22 | 4 | lmodring 20344 |
. . . . . . 7
β’ (π β LMod β π
β Ring) |
23 | | ringgrp 19974 |
. . . . . . 7
β’ (π
β Ring β π
β Grp) |
24 | 9, 22, 23 | 3syl 18 |
. . . . . 6
β’ (π β π
β Grp) |
25 | 5, 16 | grpinvcl 18803 |
. . . . . 6
β’ ((π
β Grp β§ π β π΅) β (πΌβπ) β π΅) |
26 | 24, 10, 25 | syl2anc 585 |
. . . . 5
β’ (π β (πΌβπ) β π΅) |
27 | 2, 4, 3, 5 | lmodvscl 20354 |
. . . . 5
β’ ((π β LMod β§ (πΌβπ) β π΅ β§ π β π) β ((πΌβπ) Β· π) β π) |
28 | 9, 26, 13, 27 | syl3anc 1372 |
. . . 4
β’ (π β ((πΌβπ) Β· π) β π) |
29 | | baerlem5a.b1 |
. . . . 5
β’ (π β π β π΅) |
30 | | baerlem3.z |
. . . . . 6
β’ (π β π β (π β { 0 })) |
31 | 30 | eldifad 3923 |
. . . . 5
β’ (π β π β π) |
32 | 2, 4, 3, 5 | lmodvscl 20354 |
. . . . 5
β’ ((π β LMod β§ π β π΅ β§ π β π) β (π Β· π) β π) |
33 | 9, 29, 31, 32 | syl3anc 1372 |
. . . 4
β’ (π β (π Β· π) β π) |
34 | 2, 15 | lmodass 20352 |
. . . 4
β’ ((π β LMod β§ ((π Β· π) β π β§ ((πΌβπ) Β· π) β π β§ (π Β· π) β π)) β (((π Β· π) + ((πΌβπ) Β· π)) + (π Β· π)) = ((π Β· π) + (((πΌβπ) Β· π) + (π Β· π)))) |
35 | 9, 18, 28, 33, 34 | syl13anc 1373 |
. . 3
β’ (π β (((π Β· π) + ((πΌβπ) Β· π)) + (π Β· π)) = ((π Β· π) + (((πΌβπ) Β· π) + (π Β· π)))) |
36 | 1, 21, 35 | 3eqtrd 2777 |
. 2
β’ (π β π = ((π Β· π) + (((πΌβπ) Β· π) + (π Β· π)))) |
37 | 2, 15 | lmodvacl 20351 |
. . . . . 6
β’ ((π β LMod β§ π β π β§ π β π) β (π + π) β π) |
38 | 9, 13, 31, 37 | syl3anc 1372 |
. . . . 5
β’ (π β (π + π) β π) |
39 | 2, 4, 3, 5 | lmodvscl 20354 |
. . . . 5
β’ ((π β LMod β§ π β π΅ β§ (π + π) β π) β (π Β· (π + π)) β π) |
40 | 9, 10, 38, 39 | syl3anc 1372 |
. . . 4
β’ (π β (π Β· (π + π)) β π) |
41 | | eqid 2733 |
. . . . 5
β’
(invgβπ) = (invgβπ) |
42 | 2, 15, 41, 6 | grpsubval 18801 |
. . . 4
β’ (((π Β· π) β π β§ (π Β· (π + π)) β π) β ((π Β· π) β (π Β· (π + π))) = ((π Β· π) +
((invgβπ)β(π Β· (π + π))))) |
43 | 18, 40, 42 | syl2anc 585 |
. . 3
β’ (π β ((π Β· π) β (π Β· (π + π))) = ((π Β· π) +
((invgβπ)β(π Β· (π + π))))) |
44 | 2, 3, 4, 5, 6, 9, 10, 11, 38 | lmodsubdi 20394 |
. . 3
β’ (π β (π Β· (π β (π + π))) = ((π Β· π) β (π Β· (π + π)))) |
45 | 2, 15, 4, 3, 5 | lmodvsdi 20360 |
. . . . . 6
β’ ((π β LMod β§ ((πΌβπ) β π΅ β§ π β π β§ π β π)) β ((πΌβπ) Β· (π + π)) = (((πΌβπ) Β· π) + ((πΌβπ) Β· π))) |
46 | 9, 26, 13, 31, 45 | syl13anc 1373 |
. . . . 5
β’ (π β ((πΌβπ) Β· (π + π)) = (((πΌβπ) Β· π) + ((πΌβπ) Β· π))) |
47 | 2, 4, 3, 41, 5, 16, 9, 38, 10 | lmodvsneg 20381 |
. . . . 5
β’ (π β
((invgβπ)β(π Β· (π + π))) = ((πΌβπ) Β· (π + π))) |
48 | | baerlem3.o |
. . . . . . . . . 10
β’ 0 =
(0gβπ) |
49 | | baerlem3.n |
. . . . . . . . . 10
β’ π = (LSpanβπ) |
50 | | baerlem5a.e1 |
. . . . . . . . . 10
β’ (π β π β π΅) |
51 | | baerlem5a.d1 |
. . . . . . . . . . 11
β’ (π β π β π΅) |
52 | 5, 16 | grpinvcl 18803 |
. . . . . . . . . . 11
β’ ((π
β Grp β§ π β π΅) β (πΌβπ) β π΅) |
53 | 24, 51, 52 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β (πΌβπ) β π΅) |
54 | | baerlem3.d |
. . . . . . . . . 10
β’ (π β (πβ{π}) β (πβ{π})) |
55 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(LSubSpβπ) =
(LSubSpβπ) |
56 | 2, 55, 49, 9, 13, 31 | lspprcl 20454 |
. . . . . . . . . . . 12
β’ (π β (πβ{π, π}) β (LSubSpβπ)) |
57 | | baerlem3.c |
. . . . . . . . . . . 12
β’ (π β Β¬ π β (πβ{π, π})) |
58 | 2, 15, 3, 4, 5, 49,
9, 26, 29, 13, 31 | lsppreli 20566 |
. . . . . . . . . . . 12
β’ (π β (((πΌβπ) Β· π) + (π Β· π)) β (πβ{π, π})) |
59 | 2, 15, 3, 4, 5, 49,
9, 50, 53, 13, 31 | lsppreli 20566 |
. . . . . . . . . . . 12
β’ (π β ((π Β· π) + ((πΌβπ) Β· π)) β (πβ{π, π})) |
60 | | baerlem5a.j2 |
. . . . . . . . . . . . 13
β’ (π β π = ((π Β· (π β π)) + (π Β· π))) |
61 | 2, 3, 4, 5, 6, 9, 51, 11, 31 | lmodsubdi 20394 |
. . . . . . . . . . . . . . . 16
β’ (π β (π Β· (π β π)) = ((π Β· π) β (π Β· π))) |
62 | 2, 4, 3, 5 | lmodvscl 20354 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β LMod β§ π β π΅ β§ π β π) β (π Β· π) β π) |
63 | 9, 51, 11, 62 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π Β· π) β π) |
64 | 2, 15, 6, 3, 4, 5, 16, 9, 51, 63, 31 | lmodsubvs 20393 |
. . . . . . . . . . . . . . . 16
β’ (π β ((π Β· π) β (π Β· π)) = ((π Β· π) + ((πΌβπ) Β· π))) |
65 | 61, 64 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ (π β (π Β· (π β π)) = ((π Β· π) + ((πΌβπ) Β· π))) |
66 | 65 | oveq1d 7373 |
. . . . . . . . . . . . . 14
β’ (π β ((π Β· (π β π)) + (π Β· π)) = (((π Β· π) + ((πΌβπ) Β· π)) + (π Β· π))) |
67 | | lmodabl 20384 |
. . . . . . . . . . . . . . . 16
β’ (π β LMod β π β Abel) |
68 | 7, 8, 67 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ (π β π β Abel) |
69 | 2, 4, 3, 5 | lmodvscl 20354 |
. . . . . . . . . . . . . . . 16
β’ ((π β LMod β§ (πΌβπ) β π΅ β§ π β π) β ((πΌβπ) Β· π) β π) |
70 | 9, 53, 31, 69 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (π β ((πΌβπ) Β· π) β π) |
71 | 2, 4, 3, 5 | lmodvscl 20354 |
. . . . . . . . . . . . . . . 16
β’ ((π β LMod β§ π β π΅ β§ π β π) β (π Β· π) β π) |
72 | 9, 50, 13, 71 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (π β (π Β· π) β π) |
73 | 2, 15, 68, 63, 70, 72 | abl32 19590 |
. . . . . . . . . . . . . 14
β’ (π β (((π Β· π) + ((πΌβπ) Β· π)) + (π Β· π)) = (((π Β· π) + (π Β· π)) + ((πΌβπ) Β· π))) |
74 | 2, 15 | lmodass 20352 |
. . . . . . . . . . . . . . 15
β’ ((π β LMod β§ ((π Β· π) β π β§ (π Β· π) β π β§ ((πΌβπ) Β· π) β π)) β (((π Β· π) + (π Β· π)) + ((πΌβπ) Β· π)) = ((π Β· π) + ((π Β· π) + ((πΌβπ) Β· π)))) |
75 | 9, 63, 72, 70, 74 | syl13anc 1373 |
. . . . . . . . . . . . . 14
β’ (π β (((π Β· π) + (π Β· π)) + ((πΌβπ) Β· π)) = ((π Β· π) + ((π Β· π) + ((πΌβπ) Β· π)))) |
76 | 66, 73, 75 | 3eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (π β ((π Β· (π β π)) + (π Β· π)) = ((π Β· π) + ((π Β· π) + ((πΌβπ) Β· π)))) |
77 | 60, 36, 76 | 3eqtr3d 2781 |
. . . . . . . . . . . 12
β’ (π β ((π Β· π) + (((πΌβπ) Β· π) + (π Β· π))) = ((π Β· π) + ((π Β· π) + ((πΌβπ) Β· π)))) |
78 | 2, 15, 4, 5, 3, 55,
7, 56, 11, 57, 58, 59, 10, 51, 77 | lvecindp 20615 |
. . . . . . . . . . 11
β’ (π β (π = π β§ (((πΌβπ) Β· π) + (π Β· π)) = ((π Β· π) + ((πΌβπ) Β· π)))) |
79 | 78 | simprd 497 |
. . . . . . . . . 10
β’ (π β (((πΌβπ) Β· π) + (π Β· π)) = ((π Β· π) + ((πΌβπ) Β· π))) |
80 | 2, 15, 4, 5, 3, 48,
49, 7, 12, 30, 26, 29, 50, 53, 54, 79 | lvecindp2 20616 |
. . . . . . . . 9
β’ (π β ((πΌβπ) = π β§ π = (πΌβπ))) |
81 | 80 | simprd 497 |
. . . . . . . 8
β’ (π β π = (πΌβπ)) |
82 | 78 | simpld 496 |
. . . . . . . . 9
β’ (π β π = π) |
83 | 82 | fveq2d 6847 |
. . . . . . . 8
β’ (π β (πΌβπ) = (πΌβπ)) |
84 | 81, 83 | eqtr4d 2776 |
. . . . . . 7
β’ (π β π = (πΌβπ)) |
85 | 84 | oveq1d 7373 |
. . . . . 6
β’ (π β (π Β· π) = ((πΌβπ) Β· π)) |
86 | 85 | oveq2d 7374 |
. . . . 5
β’ (π β (((πΌβπ) Β· π) + (π Β· π)) = (((πΌβπ) Β· π) + ((πΌβπ) Β· π))) |
87 | 46, 47, 86 | 3eqtr4rd 2784 |
. . . 4
β’ (π β (((πΌβπ) Β· π) + (π Β· π)) = ((invgβπ)β(π Β· (π + π)))) |
88 | 87 | oveq2d 7374 |
. . 3
β’ (π β ((π Β· π) + (((πΌβπ) Β· π) + (π Β· π))) = ((π Β· π) +
((invgβπ)β(π Β· (π + π))))) |
89 | 43, 44, 88 | 3eqtr4rd 2784 |
. 2
β’ (π β ((π Β· π) + (((πΌβπ) Β· π) + (π Β· π))) = (π Β· (π β (π + π)))) |
90 | 36, 89 | eqtrd 2773 |
1
β’ (π β π = (π Β· (π β (π + π)))) |