Step | Hyp | Ref
| Expression |
1 | | baerlem3.w |
. . . 4
β’ (π β π β LVec) |
2 | | lveclmod 20582 |
. . . 4
β’ (π β LVec β π β LMod) |
3 | 1, 2 | syl 17 |
. . 3
β’ (π β π β LMod) |
4 | | baerlem3.a1 |
. . . 4
β’ (π β π β π΅) |
5 | | baerlem3.y |
. . . . 5
β’ (π β π β (π β { 0 })) |
6 | 5 | eldifad 3923 |
. . . 4
β’ (π β π β π) |
7 | | baerlem3.v |
. . . . 5
β’ π = (Baseβπ) |
8 | | baerlem3.r |
. . . . 5
β’ π
= (Scalarβπ) |
9 | | baerlem3.t |
. . . . 5
β’ Β· = (
Β·π βπ) |
10 | | baerlem3.b |
. . . . 5
β’ π΅ = (Baseβπ
) |
11 | 7, 8, 9, 10 | lmodvscl 20354 |
. . . 4
β’ ((π β LMod β§ π β π΅ β§ π β π) β (π Β· π) β π) |
12 | 3, 4, 6, 11 | syl3anc 1372 |
. . 3
β’ (π β (π Β· π) β π) |
13 | | baerlem3.z |
. . . . 5
β’ (π β π β (π β { 0 })) |
14 | 13 | eldifad 3923 |
. . . 4
β’ (π β π β π) |
15 | 7, 8, 9, 10 | lmodvscl 20354 |
. . . 4
β’ ((π β LMod β§ π β π΅ β§ π β π) β (π Β· π) β π) |
16 | 3, 4, 14, 15 | syl3anc 1372 |
. . 3
β’ (π β (π Β· π) β π) |
17 | | baerlem3.p |
. . . 4
β’ + =
(+gβπ) |
18 | | baerlem3.m |
. . . 4
β’ β =
(-gβπ) |
19 | | baerlem3.i |
. . . 4
β’ πΌ = (invgβπ
) |
20 | | eqid 2733 |
. . . 4
β’
(1rβπ
) = (1rβπ
) |
21 | 7, 17, 18, 8, 9, 19, 20 | lmodvsubval2 20392 |
. . 3
β’ ((π β LMod β§ (π Β· π) β π β§ (π Β· π) β π) β ((π Β· π) β (π Β· π)) = ((π Β· π) + ((πΌβ(1rβπ
)) Β· (π Β· π)))) |
22 | 3, 12, 16, 21 | syl3anc 1372 |
. 2
β’ (π β ((π Β· π) β (π Β· π)) = ((π Β· π) + ((πΌβ(1rβπ
)) Β· (π Β· π)))) |
23 | 7, 9, 8, 10, 18, 3, 4, 6, 14 | lmodsubdi 20394 |
. 2
β’ (π β (π Β· (π β π)) = ((π Β· π) β (π Β· π))) |
24 | | baerlem3.j1 |
. . 3
β’ (π β π = ((π Β· π) + (π Β· π))) |
25 | 8 | lmodring 20344 |
. . . . . . . . 9
β’ (π β LMod β π
β Ring) |
26 | 3, 25 | syl 17 |
. . . . . . . 8
β’ (π β π
β Ring) |
27 | | ringgrp 19974 |
. . . . . . . 8
β’ (π
β Ring β π
β Grp) |
28 | 26, 27 | syl 17 |
. . . . . . 7
β’ (π β π
β Grp) |
29 | 8, 10, 20 | lmod1cl 20364 |
. . . . . . . 8
β’ (π β LMod β
(1rβπ
)
β π΅) |
30 | 3, 29 | syl 17 |
. . . . . . 7
β’ (π β (1rβπ
) β π΅) |
31 | 10, 19 | grpinvcl 18803 |
. . . . . . 7
β’ ((π
β Grp β§
(1rβπ
)
β π΅) β (πΌβ(1rβπ
)) β π΅) |
32 | 28, 30, 31 | syl2anc 585 |
. . . . . 6
β’ (π β (πΌβ(1rβπ
)) β π΅) |
33 | | eqid 2733 |
. . . . . . 7
β’
(.rβπ
) = (.rβπ
) |
34 | 7, 8, 9, 10, 33 | lmodvsass 20362 |
. . . . . 6
β’ ((π β LMod β§ ((πΌβ(1rβπ
)) β π΅ β§ π β π΅ β§ π β π)) β (((πΌβ(1rβπ
))(.rβπ
)π) Β· π) = ((πΌβ(1rβπ
)) Β· (π Β· π))) |
35 | 3, 32, 4, 14, 34 | syl13anc 1373 |
. . . . 5
β’ (π β (((πΌβ(1rβπ
))(.rβπ
)π) Β· π) = ((πΌβ(1rβπ
)) Β· (π Β· π))) |
36 | 10, 33, 20, 19, 26, 4 | ringnegl 20023 |
. . . . . . 7
β’ (π β ((πΌβ(1rβπ
))(.rβπ
)π) = (πΌβπ)) |
37 | | ringabl 20007 |
. . . . . . . . . . . 12
β’ (π
β Ring β π
β Abel) |
38 | 26, 37 | syl 17 |
. . . . . . . . . . 11
β’ (π β π
β Abel) |
39 | | baerlem3.d1 |
. . . . . . . . . . 11
β’ (π β π β π΅) |
40 | | baerlem3.e1 |
. . . . . . . . . . 11
β’ (π β π β π΅) |
41 | | baerlem3.a |
. . . . . . . . . . . 12
⒠⨣ =
(+gβπ
) |
42 | 10, 41, 19 | ablinvadd 19593 |
. . . . . . . . . . 11
β’ ((π
β Abel β§ π β π΅ β§ π β π΅) β (πΌβ(π ⨣ π)) = ((πΌβπ) ⨣ (πΌβπ))) |
43 | 38, 39, 40, 42 | syl3anc 1372 |
. . . . . . . . . 10
β’ (π β (πΌβ(π ⨣ π)) = ((πΌβπ) ⨣ (πΌβπ))) |
44 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(LSubSpβπ) =
(LSubSpβπ) |
45 | | baerlem3.n |
. . . . . . . . . . . . . 14
β’ π = (LSpanβπ) |
46 | 7, 44, 45, 3, 6, 14 | lspprcl 20454 |
. . . . . . . . . . . . 13
β’ (π β (πβ{π, π}) β (LSubSpβπ)) |
47 | | baerlem3.x |
. . . . . . . . . . . . 13
β’ (π β π β π) |
48 | | baerlem3.c |
. . . . . . . . . . . . 13
β’ (π β Β¬ π β (πβ{π, π})) |
49 | | baerlem3.b1 |
. . . . . . . . . . . . . 14
β’ (π β π β π΅) |
50 | 7, 17, 9, 8, 10, 45, 3, 4, 49, 6, 14 | lsppreli 20566 |
. . . . . . . . . . . . 13
β’ (π β ((π Β· π) + (π Β· π)) β (πβ{π, π})) |
51 | 7, 17, 9, 8, 10, 45, 3, 39, 40, 6, 14 | lsppreli 20566 |
. . . . . . . . . . . . . 14
β’ (π β ((π Β· π) + (π Β· π)) β (πβ{π, π})) |
52 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(invgβπ) = (invgβπ) |
53 | 44, 52 | lssvnegcl 20432 |
. . . . . . . . . . . . . 14
β’ ((π β LMod β§ (πβ{π, π}) β (LSubSpβπ) β§ ((π Β· π) + (π Β· π)) β (πβ{π, π})) β ((invgβπ)β((π Β· π) + (π Β· π))) β (πβ{π, π})) |
54 | 3, 46, 51, 53 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (π β
((invgβπ)β((π Β· π) + (π Β· π))) β (πβ{π, π})) |
55 | | baerlem3.q |
. . . . . . . . . . . . . . 15
β’ π = (0gβπ
) |
56 | 10, 55 | ring0cl 19995 |
. . . . . . . . . . . . . 14
β’ (π
β Ring β π β π΅) |
57 | 26, 56 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π β π΅) |
58 | 10, 41 | ringacl 20004 |
. . . . . . . . . . . . . 14
β’ ((π
β Ring β§ π β π΅ β§ π β π΅) β (π ⨣ π) β π΅) |
59 | 26, 39, 40, 58 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (π β (π ⨣ π) β π΅) |
60 | | baerlem3.o |
. . . . . . . . . . . . . . . . 17
β’ 0 =
(0gβπ) |
61 | 7, 8, 9, 55, 60 | lmod0vs 20370 |
. . . . . . . . . . . . . . . 16
β’ ((π β LMod β§ π β π) β (π Β· π) = 0 ) |
62 | 3, 47, 61 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β (π Β· π) = 0 ) |
63 | 62 | oveq1d 7373 |
. . . . . . . . . . . . . 14
β’ (π β ((π Β· π) + ((π Β· π) + (π Β· π))) = ( 0 + ((π Β· π) + (π Β· π)))) |
64 | | lmodgrp 20343 |
. . . . . . . . . . . . . . . 16
β’ (π β LMod β π β Grp) |
65 | 3, 64 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β π β Grp) |
66 | 7, 8, 9, 10 | lmodvscl 20354 |
. . . . . . . . . . . . . . . . 17
β’ ((π β LMod β§ π β π΅ β§ π β π) β (π Β· π) β π) |
67 | 3, 49, 14, 66 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (π β (π Β· π) β π) |
68 | 7, 17 | lmodvacl 20351 |
. . . . . . . . . . . . . . . 16
β’ ((π β LMod β§ (π Β· π) β π β§ (π Β· π) β π) β ((π Β· π) + (π Β· π)) β π) |
69 | 3, 12, 67, 68 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (π β ((π Β· π) + (π Β· π)) β π) |
70 | 7, 17, 60 | grplid 18785 |
. . . . . . . . . . . . . . 15
β’ ((π β Grp β§ ((π Β· π) + (π Β· π)) β π) β ( 0 + ((π Β· π) + (π Β· π))) = ((π Β· π) + (π Β· π))) |
71 | 65, 69, 70 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β ( 0 + ((π Β· π) + (π Β· π))) = ((π Β· π) + (π Β· π))) |
72 | | lmodabl 20384 |
. . . . . . . . . . . . . . . . . 18
β’ (π β LMod β π β Abel) |
73 | 3, 72 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β Abel) |
74 | 7, 8, 9, 10 | lmodvscl 20354 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β LMod β§ π β π΅ β§ π β π) β (π Β· π) β π) |
75 | 3, 39, 47, 74 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π Β· π) β π) |
76 | 7, 8, 9, 10 | lmodvscl 20354 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β LMod β§ π β π΅ β§ π β π) β (π Β· π) β π) |
77 | 3, 40, 47, 76 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π Β· π) β π) |
78 | 7, 8, 9, 10 | lmodvscl 20354 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β LMod β§ π β π΅ β§ π β π) β (π Β· π) β π) |
79 | 3, 39, 6, 78 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π Β· π) β π) |
80 | 7, 8, 9, 10 | lmodvscl 20354 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β LMod β§ π β π΅ β§ π β π) β (π Β· π) β π) |
81 | 3, 40, 14, 80 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π Β· π) β π) |
82 | 7, 17, 18 | ablsub4 19596 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Abel β§ ((π Β· π) β π β§ (π Β· π) β π) β§ ((π Β· π) β π β§ (π Β· π) β π)) β (((π Β· π) + (π Β· π)) β ((π Β· π) + (π Β· π))) = (((π Β· π) β (π Β· π)) + ((π Β· π) β (π Β· π)))) |
83 | 73, 75, 77, 79, 81, 82 | syl122anc 1380 |
. . . . . . . . . . . . . . . 16
β’ (π β (((π Β· π) + (π Β· π)) β ((π Β· π) + (π Β· π))) = (((π Β· π) β (π Β· π)) + ((π Β· π) β (π Β· π)))) |
84 | 7, 17, 8, 9, 10, 41 | lmodvsdir 20361 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β ((π ⨣ π) Β· π) = ((π Β· π) + (π Β· π))) |
85 | 3, 39, 40, 47, 84 | syl13anc 1373 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((π ⨣ π) Β· π) = ((π Β· π) + (π Β· π))) |
86 | 85 | oveq1d 7373 |
. . . . . . . . . . . . . . . 16
β’ (π β (((π ⨣ π) Β· π) β ((π Β· π) + (π Β· π))) = (((π Β· π) + (π Β· π)) β ((π Β· π) + (π Β· π)))) |
87 | | baerlem3.j2 |
. . . . . . . . . . . . . . . . 17
β’ (π β π = ((π Β· (π β π)) + (π Β· (π β π)))) |
88 | 7, 9, 8, 10, 18, 3, 39, 47, 6 | lmodsubdi 20394 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π Β· (π β π)) = ((π Β· π) β (π Β· π))) |
89 | 7, 9, 8, 10, 18, 3, 40, 47, 14 | lmodsubdi 20394 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π Β· (π β π)) = ((π Β· π) β (π Β· π))) |
90 | 88, 89 | oveq12d 7376 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((π Β· (π β π)) + (π Β· (π β π))) = (((π Β· π) β (π Β· π)) + ((π Β· π) β (π Β· π)))) |
91 | 87, 90 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
β’ (π β π = (((π Β· π) β (π Β· π)) + ((π Β· π) β (π Β· π)))) |
92 | 83, 86, 91 | 3eqtr4rd 2784 |
. . . . . . . . . . . . . . 15
β’ (π β π = (((π ⨣ π) Β· π) β ((π Β· π) + (π Β· π)))) |
93 | 7, 8, 9, 10 | lmodvscl 20354 |
. . . . . . . . . . . . . . . . 17
β’ ((π β LMod β§ (π ⨣ π) β π΅ β§ π β π) β ((π ⨣ π) Β· π) β π) |
94 | 3, 59, 47, 93 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (π β ((π ⨣ π) Β· π) β π) |
95 | 7, 17 | lmodvacl 20351 |
. . . . . . . . . . . . . . . . 17
β’ ((π β LMod β§ (π Β· π) β π β§ (π Β· π) β π) β ((π Β· π) + (π Β· π)) β π) |
96 | 3, 79, 81, 95 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (π β ((π Β· π) + (π Β· π)) β π) |
97 | 7, 17, 52, 18 | grpsubval 18801 |
. . . . . . . . . . . . . . . 16
β’ ((((π ⨣ π) Β· π) β π β§ ((π Β· π) + (π Β· π)) β π) β (((π ⨣ π) Β· π) β ((π Β· π) + (π Β· π))) = (((π ⨣ π) Β· π) +
((invgβπ)β((π Β· π) + (π Β· π))))) |
98 | 94, 96, 97 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β (((π ⨣ π) Β· π) β ((π Β· π) + (π Β· π))) = (((π ⨣ π) Β· π) +
((invgβπ)β((π Β· π) + (π Β· π))))) |
99 | 92, 24, 98 | 3eqtr3d 2781 |
. . . . . . . . . . . . . 14
β’ (π β ((π Β· π) + (π Β· π)) = (((π ⨣ π) Β· π) +
((invgβπ)β((π Β· π) + (π Β· π))))) |
100 | 63, 71, 99 | 3eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (π β ((π Β· π) + ((π Β· π) + (π Β· π))) = (((π ⨣ π) Β· π) +
((invgβπ)β((π Β· π) + (π Β· π))))) |
101 | 7, 17, 8, 10, 9, 44, 1, 46, 47, 48, 50, 54, 57, 59, 100 | lvecindp 20615 |
. . . . . . . . . . . 12
β’ (π β (π = (π ⨣ π) β§ ((π Β· π) + (π Β· π)) = ((invgβπ)β((π Β· π) + (π Β· π))))) |
102 | 101 | simpld 496 |
. . . . . . . . . . 11
β’ (π β π = (π ⨣ π)) |
103 | 102 | fveq2d 6847 |
. . . . . . . . . 10
β’ (π β (πΌβπ) = (πΌβ(π ⨣ π))) |
104 | 10, 19 | grpinvcl 18803 |
. . . . . . . . . . . . 13
β’ ((π
β Grp β§ π β π΅) β (πΌβπ) β π΅) |
105 | 28, 39, 104 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (πΌβπ) β π΅) |
106 | 10, 19 | grpinvcl 18803 |
. . . . . . . . . . . . 13
β’ ((π
β Grp β§ π β π΅) β (πΌβπ) β π΅) |
107 | 28, 40, 106 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (πΌβπ) β π΅) |
108 | | baerlem3.d |
. . . . . . . . . . . 12
β’ (π β (πβ{π}) β (πβ{π})) |
109 | 101 | simprd 497 |
. . . . . . . . . . . . 13
β’ (π β ((π Β· π) + (π Β· π)) = ((invgβπ)β((π Β· π) + (π Β· π)))) |
110 | 7, 17, 9, 52, 8, 10, 19, 3, 39, 40, 6, 14 | lmodnegadd 20386 |
. . . . . . . . . . . . 13
β’ (π β
((invgβπ)β((π Β· π) + (π Β· π))) = (((πΌβπ) Β· π) + ((πΌβπ) Β· π))) |
111 | 109, 110 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (π β ((π Β· π) + (π Β· π)) = (((πΌβπ) Β· π) + ((πΌβπ) Β· π))) |
112 | 7, 17, 8, 10, 9, 60, 45, 1, 5, 13, 4, 49, 105, 107, 108, 111 | lvecindp2 20616 |
. . . . . . . . . . 11
β’ (π β (π = (πΌβπ) β§ π = (πΌβπ))) |
113 | | oveq12 7367 |
. . . . . . . . . . 11
β’ ((π = (πΌβπ) β§ π = (πΌβπ)) β (π ⨣ π) = ((πΌβπ) ⨣ (πΌβπ))) |
114 | 112, 113 | syl 17 |
. . . . . . . . . 10
β’ (π β (π ⨣ π) = ((πΌβπ) ⨣ (πΌβπ))) |
115 | 43, 103, 114 | 3eqtr4rd 2784 |
. . . . . . . . 9
β’ (π β (π ⨣ π) = (πΌβπ)) |
116 | 55, 19 | grpinvid 18813 |
. . . . . . . . . 10
β’ (π
β Grp β (πΌβπ) = π) |
117 | 28, 116 | syl 17 |
. . . . . . . . 9
β’ (π β (πΌβπ) = π) |
118 | 115, 117 | eqtrd 2773 |
. . . . . . . 8
β’ (π β (π ⨣ π) = π) |
119 | 10, 41, 55, 19 | grpinvid1 18807 |
. . . . . . . . 9
β’ ((π
β Grp β§ π β π΅ β§ π β π΅) β ((πΌβπ) = π β (π ⨣ π) = π)) |
120 | 28, 4, 49, 119 | syl3anc 1372 |
. . . . . . . 8
β’ (π β ((πΌβπ) = π β (π ⨣ π) = π)) |
121 | 118, 120 | mpbird 257 |
. . . . . . 7
β’ (π β (πΌβπ) = π) |
122 | 36, 121 | eqtrd 2773 |
. . . . . 6
β’ (π β ((πΌβ(1rβπ
))(.rβπ
)π) = π) |
123 | 122 | oveq1d 7373 |
. . . . 5
β’ (π β (((πΌβ(1rβπ
))(.rβπ
)π) Β· π) = (π Β· π)) |
124 | 35, 123 | eqtr3d 2775 |
. . . 4
β’ (π β ((πΌβ(1rβπ
)) Β· (π Β· π)) = (π Β· π)) |
125 | 124 | oveq2d 7374 |
. . 3
β’ (π β ((π Β· π) + ((πΌβ(1rβπ
)) Β· (π Β· π))) = ((π Β· π) + (π Β· π))) |
126 | 24, 125 | eqtr4d 2776 |
. 2
β’ (π β π = ((π Β· π) + ((πΌβ(1rβπ
)) Β· (π Β· π)))) |
127 | 22, 23, 126 | 3eqtr4rd 2784 |
1
β’ (π β π = (π Β· (π β π))) |