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